%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL646+1.005 : 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 : n007.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:30 PM UTC 2026
% Result : Theorem 20.65s 3.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL646+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n007.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 00:42:35 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 20.65/3.06 % Refutation found
% 20.65/3.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.65/3.06 % SZS output start CNFRefutation for theBenchmark
% 20.65/3.06 fof(f1,conjecture,(
% 20.65/3.06 ~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p6(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p4(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p4(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p6(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p4(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p2(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p6(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p4(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p2(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p6(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p4(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p2(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p6(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p2(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p5(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p5(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p5(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p6(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p2(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p3(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p3(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p3(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p6(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p2(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p6(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p4(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p2(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p5(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p5(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p6(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p4(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p2(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p1(X) ))& ~ p4(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p3(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p3(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p6(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p4(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p2(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p1(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p1(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p6(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p4(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p5(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p5(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p5(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p6(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p4(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p3(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p3(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p3(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p6(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p4(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p5(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p5(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p3(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p3(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p1(X) ))& ~ p2(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p1(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p5(Y) ))| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )),
% 20.65/3.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 20.65/3.06 fof(f2,negated_conjecture,(
% 20.65/3.06 ~(~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p6(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p4(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p4(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ) )) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p6(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p4(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p2(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p6(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p4(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p2(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p6(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p4(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p2(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p6(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p2(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p5(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p5(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p5(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p6(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p2(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p3(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p3(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p3(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p6(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p2(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p1(X) ) ) )) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p6(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p4(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p6(Y) ))& ~ p2(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p5(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p5(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p6(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p4(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p2(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p1(X) ))& ~ p4(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p3(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p3(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p6(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p4(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ p2(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p1(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p1(Y) ) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p6(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p6(X) ))& ~ p4(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p5(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p5(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p5(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p6(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p4(X) ))& ~ p4(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p3(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p3(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p3(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p6(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ p4(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p5(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p4(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p3(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| p1(Y) ))& ~ p1(X) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p5(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p5(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p3(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p3(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p1(X) ))& ~ p2(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& ~ p1(Y) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))& ~ p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p5(Y) ))| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))),
% 20.65/3.06 inference(negated_conjecture,[status(cth)],[f1])).
% 20.65/3.06 fof(f3,plain,(
% 20.65/3.06 ?[X]: ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p6(Y)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p4(Y))))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p4(Y))))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p2(Y))))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p6(Y)))|p6(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p6(Y)))|p4(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p6(Y)))|p2(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p6(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p4(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p2(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p2(Y)))|p6(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p2(Y)))|p4(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p2(Y)))|p2(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p6(X)))|p6(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p6(X)))|p2(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p5(Y)))|p5(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p3(Y)))|p5(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p1(Y)))|p5(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p4(X)))|p6(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p4(X)))|p2(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p5(Y)))|p3(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p3(Y)))|p3(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p1(Y)))|p3(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p2(X)))|p6(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p2(X)))|p2(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p5(Y)))|p1(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p1(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p3(Y)))|p1(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p1(Y)))|p1(X)))))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p6(Y)))|p6(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p6(Y)))|p4(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p6(Y)))|p2(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p5(X)))|p5(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))|p5(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p6(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p4(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p2(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p1(X)))|p4(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p5(X)))|p3(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))|p3(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p2(Y)))|p6(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p2(Y)))|p4(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p2(Y)))|p2(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p5(X)))|p1(Y)))))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))|p1(Y)))))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p6(X)))|p6(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p6(X)))|p4(Y)))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p5(Y)))|p5(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p3(Y)))|p5(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p1(Y)))|p5(X)))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p4(X)))|p6(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p4(X)))|p4(Y)))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p5(Y)))|p3(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p3(Y)))|p3(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p1(Y)))|p3(X)))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p2(X)))|p6(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p2(X)))|p4(Y)))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p5(Y)))|p1(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p4(Y)))|p1(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p3(Y)))|p1(X)))))))&(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&~p1(Y)))|p1(X)))))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p5(X)))|p5(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))|p5(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p5(X)))|p3(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))|p3(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p1(X)))|p2(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p5(X)))|p1(Y)))))&(![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))|p1(Y)))))&(?[Y]: (r1(X,Y)&~p5(Y))))&(?[Y]: (r1(X,Y)&~p3(Y))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (r1(X,Y)&~p1(Y))))),
% 20.65/3.06 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 20.65/3.06 fof(f4,plain,(
% 20.65/3.06 ((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p6(Y)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p4(Y))))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p4(Y))))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p2(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))&~p6(sK1_skl(X,Y,X,Y)))|p6(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))&~p6(sK2_skl(X,Y,X,Y)))|p4(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))&~p6(sK3_skl(X,Y,X,Y)))|p2(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))&~p4(sK4_skl(X,Y,X,Y)))|p6(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))&~p4(sK5_skl(X,Y,X,Y)))|p4(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))&~p4(sK6_skl(X,Y,X,Y)))|p2(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))&~p2(sK7_skl(X,Y,X,Y)))|p6(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))&~p2(sK8_skl(X,Y,X,Y)))|p4(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))&~p2(sK9_skl(X,Y,X,Y)))|p2(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK10_skl(Y,X,Y))&~p6(sK10_skl(Y,X,Y)))|p6(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK11_skl(Y,X,Y))&~p6(sK11_skl(Y,X,Y)))|p2(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))&~p5(sK12_skl(X,Y,X,Y)))|p5(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))&~p3(sK13_skl(X,Y,X,Y)))|p5(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))&~p1(sK14_skl(X,Y,X,Y)))|p5(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK15_skl(Y,X,Y))&~p4(sK15_skl(Y,X,Y)))|p6(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK16_skl(Y,X,Y))&~p4(sK16_skl(Y,X,Y)))|p2(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))&~p5(sK17_skl(X,Y,X,Y)))|p3(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))&~p3(sK18_skl(X,Y,X,Y)))|p3(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))&~p1(sK19_skl(X,Y,X,Y)))|p3(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK20_skl(Y,X,Y))&~p2(sK20_skl(Y,X,Y)))|p6(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK21_skl(Y,X,Y))&~p2(sK21_skl(Y,X,Y)))|p2(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))&~p5(sK22_skl(X,Y,X,Y)))|p1(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))&~p4(sK23_skl(X,Y,X,Y)))|p1(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))&~p3(sK24_skl(X,Y,X,Y)))|p1(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))&~p1(sK25_skl(X,Y,X,Y)))|p1(X)))))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK26_skl(X,Y))&~p6(sK26_skl(X,Y)))|p6(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK27_skl(X,Y))&~p6(sK27_skl(X,Y)))|p4(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK28_skl(X,Y))&~p6(sK28_skl(X,Y)))|p2(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK29_skl(Y,X,Y))&~p5(sK29_skl(Y,X,Y)))|p5(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK30_skl(Y,X,Y))&~p3(sK30_skl(Y,X,Y)))|p5(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK31_skl(X,Y))&~p4(sK31_skl(X,Y)))|p6(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK32_skl(X,Y))&~p4(sK32_skl(X,Y)))|p4(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK33_skl(X,Y))&~p4(sK33_skl(X,Y)))|p2(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK34_skl(Y,X,Y))&~p1(sK34_skl(Y,X,Y)))|p4(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK35_skl(Y,X,Y))&~p5(sK35_skl(Y,X,Y)))|p3(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK36_skl(Y,X,Y))&~p3(sK36_skl(Y,X,Y)))|p3(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK37_skl(X,Y))&~p2(sK37_skl(X,Y)))|p6(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK38_skl(X,Y))&~p2(sK38_skl(X,Y)))|p4(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK39_skl(X,Y))&~p2(sK39_skl(X,Y)))|p2(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK40_skl(Y,X,Y))&~p5(sK40_skl(Y,X,Y)))|p1(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((r1(Y,sK41_skl(Y,X,Y))&~p3(sK41_skl(Y,X,Y)))|p1(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK42_skl(Y))&~p6(sK42_skl(Y)))|p6(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK43_skl(Y))&~p6(sK43_skl(Y)))|p4(Y)))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK44_skl(X,Y))&~p5(sK44_skl(X,Y)))|p5(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK45_skl(X,Y))&~p3(sK45_skl(X,Y)))|p5(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK46_skl(X,Y))&~p1(sK46_skl(X,Y)))|p5(X)))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK47_skl(Y))&~p4(sK47_skl(Y)))|p6(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK48_skl(Y))&~p4(sK48_skl(Y)))|p4(Y)))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK49_skl(X,Y))&~p5(sK49_skl(X,Y)))|p3(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK50_skl(X,Y))&~p3(sK50_skl(X,Y)))|p3(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK51_skl(X,Y))&~p1(sK51_skl(X,Y)))|p3(X)))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK52_skl(Y))&~p2(sK52_skl(Y)))|p6(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK53_skl(Y))&~p2(sK53_skl(Y)))|p4(Y)))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK54_skl(X,Y))&~p5(sK54_skl(X,Y)))|p1(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK55_skl(X,Y))&~p4(sK55_skl(X,Y)))|p1(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK56_skl(X,Y))&~p3(sK56_skl(X,Y)))|p1(X)))))))&(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((r1(X,sK57_skl(X,Y))&~p1(sK57_skl(X,Y)))|p1(X)))))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK58_skl(Y))&~p5(sK58_skl(Y)))|p5(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK59_skl(Y))&~p3(sK59_skl(Y)))|p5(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK60_skl(Y))&~p5(sK60_skl(Y)))|p3(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK61_skl(Y))&~p3(sK61_skl(Y)))|p3(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK62_skl(Y))&~p1(sK62_skl(Y)))|p2(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK63_skl(Y))&~p5(sK63_skl(Y)))|p1(Y)))))&(![Y]: (~r1(sK0_skl,Y)|((r1(Y,sK64_skl(Y))&~p3(sK64_skl(Y)))|p1(Y)))))&(r1(sK0_skl,sK65_skl)&~p5(sK65_skl)))&(r1(sK0_skl,sK66_skl)&~p3(sK66_skl)))&(r1(sK0_skl,sK67_skl)&~p2(sK67_skl)))&(r1(sK0_skl,sK68_skl)&~p1(sK68_skl)))),
% 20.65/3.06 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)],[f3])).
% 20.65/3.06 fof(f6,plain,(
% 20.65/3.06 ![X0,X1,X2,X3,X4]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~r1(X3,X4)|p4(X4))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f53,plain,(
% 20.65/3.06 ![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))|p1(X3))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f54,plain,(
% 20.65/3.06 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|~p4(sK23_skl(X3,X2,X1,X0))|p1(X3))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f75,plain,(
% 20.65/3.06 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|r1(X2,sK34_skl(X2,X1,X0))|p4(X2))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f76,plain,(
% 20.65/3.06 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~p1(sK34_skl(X2,X1,X0))|p4(X2))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f117,plain,(
% 20.65/3.06 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|r1(X1,sK55_skl(X1,X0))|p1(X1))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f118,plain,(
% 20.65/3.06 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~p4(sK55_skl(X1,X0))|p1(X1))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f131,plain,(
% 20.65/3.06 ![X0]: (~r1(sK0_skl,X0)|r1(X0,sK62_skl(X0))|p2(X0))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f132,plain,(
% 20.65/3.06 ![X0]: (~r1(sK0_skl,X0)|~p1(sK62_skl(X0))|p2(X0))),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f141,plain,(
% 20.65/3.06 r1(sK0_skl,sK67_skl)),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f142,plain,(
% 20.65/3.06 ~p2(sK67_skl)),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f143,plain,(
% 20.65/3.06 r1(sK0_skl,sK68_skl)),
% 20.65/3.06 inference(cnf_transformation,[status(thm)],[f4])).
% 20.65/3.06 fof(f149,plain,(
% 20.65/3.06 ![X0,X1,X2,X3]: (~r1(sK67_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p4(X3))),
% 20.65/3.06 inference(resolution,[status(thm)],[f141,f6])).
% 20.65/3.06 fof(f426,plain,(
% 20.65/3.06 r1(sK67_skl,sK62_skl(sK67_skl))|p2(sK67_skl)),
% 20.65/3.06 inference(resolution,[status(thm)],[f131,f141])).
% 20.65/3.06 fof(f436,definition,(
% 20.65/3.06 sQ58_spl <=> (r1(sK67_skl,sK62_skl(sK67_skl)))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f437,plain,(
% 20.65/3.06 r1(sK67_skl,sK62_skl(sK67_skl))|~sQ58_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f436])).
% 20.65/3.06 fof(f439,definition,(
% 20.65/3.06 sQ59_spl <=> (p2(sK67_skl))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f440,plain,(
% 20.65/3.06 p2(sK67_skl)|~sQ59_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f439])).
% 20.65/3.06 fof(f442,plain,(
% 20.65/3.06 sQ58_spl|sQ59_spl),
% 20.65/3.06 inference(split_clause,[status(thm)],[f426,f436,f439])).
% 20.65/3.06 fof(f612,plain,(
% 20.65/3.06 ![X0,X1,X2]: (~r1(sK67_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|r1(X2,sK23_skl(X2,X1,X0,sK67_skl))|p1(X2))),
% 20.65/3.06 inference(resolution,[status(thm)],[f53,f141])).
% 20.65/3.06 fof(f640,plain,(
% 20.65/3.06 ![X0,X1]: (~r1(sK67_skl,X0)|~r1(X0,X1)|r1(X1,sK34_skl(X1,X0,sK67_skl))|p4(X1))),
% 20.65/3.06 inference(resolution,[status(thm)],[f75,f141])).
% 20.65/3.06 fof(f688,plain,(
% 20.65/3.06 ![X0]: (~r1(sK67_skl,X0)|r1(X0,sK55_skl(X0,sK67_skl))|p1(X0))),
% 20.65/3.06 inference(resolution,[status(thm)],[f117,f141])).
% 20.65/3.06 fof(f1571,plain,(
% 20.65/3.06 ![X0,X1]: (~r1(sK62_skl(sK67_skl),X0)|~r1(X0,X1)|r1(X1,sK23_skl(X1,X0,sK62_skl(sK67_skl),sK67_skl))|p1(X1)|~sQ58_spl)),
% 20.65/3.06 inference(resolution,[status(thm)],[f437,f612])).
% 20.65/3.06 fof(f1586,plain,(
% 20.65/3.06 ![X0]: (~r1(sK62_skl(sK67_skl),X0)|r1(X0,sK34_skl(X0,sK62_skl(sK67_skl),sK67_skl))|p4(X0)|~sQ58_spl)),
% 20.65/3.06 inference(resolution,[status(thm)],[f437,f640])).
% 20.65/3.06 fof(f1603,plain,(
% 20.65/3.06 r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))|p1(sK62_skl(sK67_skl))|~sQ58_spl),
% 20.65/3.06 inference(resolution,[status(thm)],[f437,f688])).
% 20.65/3.06 fof(f1623,definition,(
% 20.65/3.06 sQ227_spl <=> (p1(sK62_skl(sK67_skl)))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f1624,plain,(
% 20.65/3.06 p1(sK62_skl(sK67_skl))|~sQ227_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f1623])).
% 20.65/3.06 fof(f1631,definition,(
% 20.65/3.06 sQ229_spl <=> (r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl)))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f1632,plain,(
% 20.65/3.06 r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ229_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f1631])).
% 20.65/3.06 fof(f1634,plain,(
% 20.65/3.06 sQ229_spl|sQ227_spl|~sQ58_spl),
% 20.65/3.06 inference(split_clause,[status(thm)],[f1603,f1631,f1623,f436])).
% 20.65/3.06 fof(f2168,plain,(
% 20.65/3.06 ~r1(sK0_skl,sK67_skl)|p2(sK67_skl)|~sQ227_spl),
% 20.65/3.06 inference(resolution,[status(thm)],[f132,f1624])).
% 20.65/3.06 fof(f2171,definition,(
% 20.65/3.06 sQ328_spl <=> (r1(sK0_skl,sK68_skl))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ328_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f2173,plain,(
% 20.65/3.06 ~r1(sK0_skl,sK68_skl)|sQ328_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f2171])).
% 20.65/3.06 fof(f2175,definition,(
% 20.65/3.06 sQ329_spl <=> (r1(sK0_skl,sK67_skl))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ329_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f2177,plain,(
% 20.65/3.06 ~r1(sK0_skl,sK67_skl)|sQ329_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f2175])).
% 20.65/3.06 fof(f2178,plain,(
% 20.65/3.06 ~sQ329_spl|sQ59_spl|~sQ227_spl),
% 20.65/3.06 inference(split_clause,[status(thm)],[f2168,f2175,f439,f1623])).
% 20.65/3.06 fof(f2181,plain,(
% 20.65/3.06 $false|~sQ59_spl),
% 20.65/3.06 inference(forward_subsumption_resolution,[status(thm)],[f440,f142])).
% 20.65/3.06 fof(f2182,plain,(
% 20.65/3.06 ~sQ59_spl),
% 20.65/3.06 inference(contradiction_clause,[status(thm)],[f2181])).
% 20.65/3.06 fof(f2183,plain,(
% 20.65/3.06 $false|sQ329_spl),
% 20.65/3.06 inference(forward_subsumption_resolution,[status(thm)],[f2177,f141])).
% 20.65/3.06 fof(f2184,plain,(
% 20.65/3.06 sQ329_spl),
% 20.65/3.06 inference(contradiction_clause,[status(thm)],[f2183])).
% 20.65/3.06 fof(f2187,plain,(
% 20.65/3.06 $false|sQ328_spl),
% 20.65/3.06 inference(forward_subsumption_resolution,[status(thm)],[f2173,f143])).
% 20.65/3.06 fof(f2188,plain,(
% 20.65/3.06 sQ328_spl),
% 20.65/3.06 inference(contradiction_clause,[status(thm)],[f2187])).
% 20.65/3.06 fof(f2199,plain,(
% 20.65/3.06 ![X0,X1,X2]: (~r1(sK62_skl(sK67_skl),X0)|~r1(X0,X1)|~r1(X1,X2)|p4(X2)|~sQ58_spl)),
% 20.65/3.06 inference(resolution,[status(thm)],[f149,f437])).
% 20.65/3.06 fof(f3666,plain,(
% 20.65/3.06 ![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))|p1(X0)|~sQ229_spl|~sQ58_spl)),
% 20.65/3.06 inference(resolution,[status(thm)],[f1632,f1571])).
% 20.65/3.06 fof(f3677,plain,(
% 20.65/3.06 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))|p4(sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ229_spl|~sQ58_spl),
% 20.65/3.06 inference(resolution,[status(thm)],[f1632,f1586])).
% 20.65/3.06 fof(f3723,definition,(
% 20.65/3.06 sQ607_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)))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f3724,plain,(
% 20.65/3.06 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))|~sQ607_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f3723])).
% 20.65/3.06 fof(f3726,definition,(
% 20.65/3.06 sQ608_spl <=> (p4(sK55_skl(sK62_skl(sK67_skl),sK67_skl)))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ608_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f3727,plain,(
% 20.65/3.06 p4(sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ608_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f3726])).
% 20.65/3.06 fof(f3729,plain,(
% 20.65/3.06 sQ607_spl|sQ608_spl|~sQ229_spl|~sQ58_spl),
% 20.65/3.06 inference(split_clause,[status(thm)],[f3677,f3723,f3726,f1631,f436])).
% 20.65/3.06 fof(f4505,plain,(
% 20.65/3.06 ![X0,X1]: (~r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),X0)|~r1(X0,X1)|p4(X1)|~sQ58_spl|~sQ229_spl)),
% 20.65/3.06 inference(resolution,[status(thm)],[f2199,f1632])).
% 20.65/3.06 fof(f7288,plain,(
% 20.65/3.06 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))|p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ607_spl|~sQ229_spl|~sQ58_spl),
% 20.65/3.06 inference(resolution,[status(thm)],[f3724,f3666])).
% 20.65/3.06 fof(f7308,definition,(
% 20.65/3.06 sQ1349_spl <=> (p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ1349_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f7309,plain,(
% 20.65/3.06 p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ1349_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f7308])).
% 20.65/3.06 fof(f7316,definition,(
% 20.65/3.06 sQ1351_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)))),
% 20.65/3.06 introduced(definition,[new_symbols(definition,[sQ1351_spl])],[split_symbol_definition])).
% 20.65/3.06 fof(f7317,plain,(
% 20.65/3.06 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))|~sQ1351_spl),
% 20.65/3.06 inference(component_clause,[status(thm)],[f7316])).
% 20.65/3.06 fof(f7319,plain,(
% 20.65/3.06 sQ1351_spl|sQ1349_spl|~sQ607_spl|~sQ229_spl|~sQ58_spl),
% 20.65/3.06 inference(split_clause,[status(thm)],[f7288,f7316,f7308,f3723,f1631,f436])).
% 20.65/3.06 fof(f7777,plain,(
% 20.65/3.06 ![X0]: (~r1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),X0)|p4(X0)|~sQ58_spl|~sQ229_spl|~sQ607_spl)),
% 20.65/3.09 inference(resolution,[status(thm)],[f4505,f3724])).
% 20.65/3.09 fof(f12036,plain,(
% 20.65/3.09 ~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))|p4(sK55_skl(sK62_skl(sK67_skl),sK67_skl))|~sQ1349_spl),
% 20.65/3.09 inference(resolution,[status(thm)],[f7309,f76])).
% 20.65/3.09 fof(f12037,plain,(
% 20.65/3.09 ~sQ329_spl|~sQ58_spl|~sQ229_spl|sQ608_spl|~sQ1349_spl),
% 20.65/3.09 inference(split_clause,[status(thm)],[f12036,f2175,f436,f1631,f3726,f7308])).
% 20.65/3.09 fof(f12038,plain,(
% 20.65/3.09 ~r1(sK0_skl,sK67_skl)|~r1(sK67_skl,sK62_skl(sK67_skl))|p1(sK62_skl(sK67_skl))|~sQ608_spl),
% 20.65/3.09 inference(resolution,[status(thm)],[f3727,f118])).
% 20.65/3.09 fof(f12039,plain,(
% 20.65/3.09 ~sQ329_spl|~sQ58_spl|sQ227_spl|~sQ608_spl),
% 20.65/3.09 inference(split_clause,[status(thm)],[f12038,f2175,f436,f1623,f3726])).
% 20.65/3.09 fof(f12216,plain,(
% 20.65/3.09 p4(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))|~sQ1351_spl|~sQ58_spl|~sQ229_spl|~sQ607_spl),
% 20.65/3.09 inference(resolution,[status(thm)],[f7317,f7777])).
% 20.65/3.09 fof(f12310,plain,(
% 20.65/3.09 ~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))|p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))|~sQ1351_spl|~sQ58_spl|~sQ229_spl|~sQ607_spl),
% 20.65/3.09 inference(resolution,[status(thm)],[f12216,f54])).
% 20.65/3.09 fof(f12311,plain,(
% 20.65/3.09 ~sQ329_spl|~sQ58_spl|~sQ229_spl|~sQ607_spl|sQ1349_spl|~sQ1351_spl),
% 20.65/3.09 inference(split_clause,[status(thm)],[f12310,f2175,f436,f1631,f3723,f7308,f7316])).
% 20.65/3.09 fof(f12312,plain,(
% 20.65/3.09 $false),
% 20.65/3.09 inference(sat_refutation,[status(thm)],[f442,f1634,f2178,f2182,f2184,f2188,f3729,f7319,f12037,f12039,f12311])).
% 20.65/3.09 % SZS output end CNFRefutation for theBenchmark.p
% 20.65/3.10 % Elapsed time: 2.741329 seconds
% 20.65/3.10 % CPU time: 21.305864 seconds
% 20.65/3.10 % Total memory used: 188.921 MB
% 20.65/3.10 % Net memory used: 186.053 MB
%------------------------------------------------------------------------------