%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL672+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 : n004.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:49 PM UTC 2026
% Result : Theorem 10.88s 2.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL672+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.10/0.59 % Computer : n004.cluster.edu
% 0.10/0.59 % Model : x86_64 x86_64
% 0.10/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.59 % Memory : 8046.5625MB
% 0.10/0.59 % OS : Linux 6.8.0-71-generic
% 0.10/0.59 % CPULimit : 300
% 0.10/0.59 % WCLimit : 300
% 0.10/0.59 % DateTime : Mon Sep 21 00:53:09 UTC 2026
% 0.10/0.60 % CPUTime :
% 0.10/0.61 % Drodi V4.1.1
% 10.88/2.06 % Refutation found
% 10.88/2.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.88/2.06 % SZS output start CNFRefutation for theBenchmark
% 10.88/2.06 fof(f2,axiom,(
% 10.88/2.06 (! [X,Y,Z] :( ( r1(X,Y)& r1(Y,Z) )=> r1(X,Z) ) )),
% 10.88/2.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.88/2.06 fof(f3,conjecture,(
% 10.88/2.06 ~ (? [X] :~ ( ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))& p1(X) ) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| $false ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))& p1(X) ) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| $false ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )),
% 10.88/2.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 10.88/2.06 fof(f4,negated_conjecture,(
% 10.88/2.06 ~(~ (? [X] :~ ( ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))& p1(X) ) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| $false ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [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)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))& p1(X) ) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )) ))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| p2(X) ))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| $false ) )))& ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))& p1(Y) ) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| p1(X) ) )) )))& ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) )) ))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| ( ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ))& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| $false ) )))& ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p2(X) ))| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )) ))),
% 10.88/2.06 inference(negated_conjecture,[status(cth)],[f3])).
% 10.88/2.06 fof(f6,plain,(
% 10.88/2.06 ![X,Y,Z]: ((~r1(X,Y)|~r1(Y,Z))|r1(X,Z))),
% 10.88/2.06 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 10.88/2.06 fof(f7,plain,(
% 10.88/2.06 ![X,Z]: ((![Y]: (~r1(X,Y)|~r1(Y,Z)))|r1(X,Z))),
% 10.88/2.06 inference(miniscoping,[status(thm)],[f6])).
% 10.88/2.06 fof(f8,plain,(
% 10.88/2.06 ![X0,X1,X2]: (~r1(X0,X1)|~r1(X1,X2)|r1(X0,X2))),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f7])).
% 10.88/2.06 fof(f9,plain,(
% 10.88/2.06 ?[X]: (((((((((((((((((((((((((((((((((((((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&$true)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&p1(X)))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y)))))))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&$true)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&$true)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&p1(X)))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y)))))))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&$true)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&$true)))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))),
% 10.88/2.06 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 10.88/2.06 fof(f10,plain,(
% 10.88/2.06 ?[X]: (((((((((((((((((((((((((((((((((((((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((?[X]: r1(Y,X))&$true))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&p1(X)))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y)))))))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((?[Y]: r1(X,Y))&$true))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((?[X]: r1(Y,X))&$true))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&p1(X)))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y)))))))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((?[Y]: r1(X,Y))&$true))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&p1(Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&~p1(X)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((?[X]: r1(Y,X))&$true))))|(![Y]: (~r1(X,Y)|p1(Y)))))&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p2(X))))&(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p2(Y))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&~p1(Y))))),
% 10.88/2.06 inference(miniscoping,[status(thm)],[f9])).
% 10.88/2.06 fof(f11,plain,(
% 10.88/2.06 (((((((((((((((((((((((((((((((((((((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(r1(X,sK1_skl(X,Y,X,Y,X,Y))&p1(sK1_skl(X,Y,X,Y,X,Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK2_skl(Y,X,Y,X,Y,X,Y))&~p1(sK2_skl(Y,X,Y,X,Y,X,Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(r1(X,sK3_skl(X,Y,X,Y,X,Y))&(![X]: (~r1(sK3_skl(X,Y,X,Y,X,Y),X)|p1(X))))))|(![X]: (~r1(Y,X)|(r1(X,sK4_skl(X,Y,X,Y,X,Y))&~p1(sK4_skl(X,Y,X,Y,X,Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(r1(Y,sK5_skl(Y,X,Y,X,Y))&$true))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(r1(sK0_skl,sK6_skl)&~p2(sK6_skl)))&(((r1(sK0_skl,sK7_skl)&(r1(sK7_skl,sK8_skl)&~p2(sK8_skl)))&(((r1(sK7_skl,sK9_skl)&(r1(sK9_skl,sK10_skl)&~p2(sK10_skl)))&(((r1(sK9_skl,sK11_skl)&(r1(sK11_skl,sK12_skl)&~p2(sK12_skl)))&(((r1(sK11_skl,sK13_skl)&(r1(sK13_skl,sK14_skl)&~p2(sK14_skl)))&((r1(sK13_skl,sK15_skl)&(r1(sK15_skl,sK16_skl)&(![Y]: (~r1(sK16_skl,Y)|p1(Y)))))&(r1(sK15_skl,sK17_skl)&~p1(sK17_skl))))&(r1(sK13_skl,sK18_skl)&~p1(sK18_skl))))&(r1(sK11_skl,sK19_skl)&~p1(sK19_skl))))&(r1(sK9_skl,sK20_skl)&~p1(sK20_skl))))&(r1(sK7_skl,sK21_skl)&~p1(sK21_skl))))&(r1(sK0_skl,sK22_skl)&~p1(sK22_skl)))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK23_skl(Y,X,Y,X,Y))&p1(sK23_skl(Y,X,Y,X,Y)))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(r1(X,sK24_skl(X,Y,X,Y,X,Y))&~p1(sK24_skl(X,Y,X,Y,X,Y)))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK25_skl(Y,X,Y,X,Y))&(![Y]: (~r1(sK25_skl(Y,X,Y,X,Y),Y)|p1(Y))))))|(![Y]: (~r1(X,Y)|(r1(Y,sK26_skl(Y,X,Y,X,Y))&~p1(sK26_skl(Y,X,Y,X,Y)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(r1(X,sK27_skl(X,Y,X,Y))&$true))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(r1(sK0_skl,sK28_skl)&~p2(sK28_skl)))&(((r1(sK0_skl,sK29_skl)&(r1(sK29_skl,sK30_skl)&~p2(sK30_skl)))&(((r1(sK29_skl,sK31_skl)&(r1(sK31_skl,sK32_skl)&~p2(sK32_skl)))&(((r1(sK31_skl,sK33_skl)&(r1(sK33_skl,sK34_skl)&~p2(sK34_skl)))&(((r1(sK33_skl,sK35_skl)&(r1(sK35_skl,sK36_skl)&~p2(sK36_skl)))&((r1(sK35_skl,sK37_skl)&(r1(sK37_skl,sK38_skl)&(![Y]: (~r1(sK38_skl,Y)|p1(Y)))))&(r1(sK37_skl,sK39_skl)&~p1(sK39_skl))))&(r1(sK35_skl,sK40_skl)&~p1(sK40_skl))))&(r1(sK33_skl,sK41_skl)&~p1(sK41_skl))))&(r1(sK31_skl,sK42_skl)&~p1(sK42_skl))))&(r1(sK29_skl,sK43_skl)&~p1(sK43_skl))))&(r1(sK0_skl,sK44_skl)&~p1(sK44_skl)))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(r1(X,sK45_skl(X,Y,X,Y))&p1(sK45_skl(X,Y,X,Y)))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK46_skl(Y,X,Y,X,Y))&~p1(sK46_skl(Y,X,Y,X,Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(r1(X,sK47_skl(X,Y,X,Y))&(![X]: (~r1(sK47_skl(X,Y,X,Y),X)|p1(X))))))|(![X]: (~r1(Y,X)|(r1(X,sK48_skl(X,Y,X,Y))&~p1(sK48_skl(X,Y,X,Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(r1(Y,sK49_skl(Y,X,Y))&$true))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(r1(sK0_skl,sK50_skl)&~p2(sK50_skl)))&(((r1(sK0_skl,sK51_skl)&(r1(sK51_skl,sK52_skl)&~p2(sK52_skl)))&(((r1(sK51_skl,sK53_skl)&(r1(sK53_skl,sK54_skl)&~p2(sK54_skl)))&(((r1(sK53_skl,sK55_skl)&(r1(sK55_skl,sK56_skl)&~p2(sK56_skl)))&(((r1(sK55_skl,sK57_skl)&(r1(sK57_skl,sK58_skl)&~p2(sK58_skl)))&((r1(sK57_skl,sK59_skl)&(r1(sK59_skl,sK60_skl)&(![Y]: (~r1(sK60_skl,Y)|p1(Y)))))&(r1(sK59_skl,sK61_skl)&~p1(sK61_skl))))&(r1(sK57_skl,sK62_skl)&~p1(sK62_skl))))&(r1(sK55_skl,sK63_skl)&~p1(sK63_skl))))&(r1(sK53_skl,sK64_skl)&~p1(sK64_skl))))&(r1(sK51_skl,sK65_skl)&~p1(sK65_skl))))&(r1(sK0_skl,sK66_skl)&~p1(sK66_skl)))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK67_skl(Y,X,Y))&p1(sK67_skl(Y,X,Y)))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(r1(X,sK68_skl(X,Y,X,Y))&~p1(sK68_skl(X,Y,X,Y)))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK69_skl(Y,X,Y))&(![Y]: (~r1(sK69_skl(Y,X,Y),Y)|p1(Y))))))|(![Y]: (~r1(X,Y)|(r1(Y,sK70_skl(Y,X,Y))&~p1(sK70_skl(Y,X,Y)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(r1(X,sK71_skl(X,Y))&$true))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(r1(sK0_skl,sK72_skl)&~p2(sK72_skl)))&(((r1(sK0_skl,sK73_skl)&(r1(sK73_skl,sK74_skl)&~p2(sK74_skl)))&(((r1(sK73_skl,sK75_skl)&(r1(sK75_skl,sK76_skl)&~p2(sK76_skl)))&(((r1(sK75_skl,sK77_skl)&(r1(sK77_skl,sK78_skl)&~p2(sK78_skl)))&(((r1(sK77_skl,sK79_skl)&(r1(sK79_skl,sK80_skl)&~p2(sK80_skl)))&((r1(sK79_skl,sK81_skl)&(r1(sK81_skl,sK82_skl)&(![Y]: (~r1(sK82_skl,Y)|p1(Y)))))&(r1(sK81_skl,sK83_skl)&~p1(sK83_skl))))&(r1(sK79_skl,sK84_skl)&~p1(sK84_skl))))&(r1(sK77_skl,sK85_skl)&~p1(sK85_skl))))&(r1(sK75_skl,sK86_skl)&~p1(sK86_skl))))&(r1(sK73_skl,sK87_skl)&~p1(sK87_skl))))&(r1(sK0_skl,sK88_skl)&~p1(sK88_skl)))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(r1(X,sK89_skl(X,Y))&p1(sK89_skl(X,Y)))))|~p1(Y)))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(r1(Y,sK90_skl(Y,X,Y))&~p1(sK90_skl(Y,X,Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(r1(X,sK91_skl(X,Y))&(![X]: (~r1(sK91_skl(X,Y),X)|p1(X))))))|(![X]: (~r1(Y,X)|(r1(X,sK92_skl(X,Y))&~p1(sK92_skl(X,Y)))))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(r1(Y,sK93_skl(Y))&$true))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(r1(sK0_skl,sK94_skl)&~p2(sK94_skl)))&(((r1(sK0_skl,sK95_skl)&(r1(sK95_skl,sK96_skl)&~p2(sK96_skl)))&(((r1(sK95_skl,sK97_skl)&(r1(sK97_skl,sK98_skl)&~p2(sK98_skl)))&(((r1(sK97_skl,sK99_skl)&(r1(sK99_skl,sK100_skl)&~p2(sK100_skl)))&(((r1(sK99_skl,sK101_skl)&(r1(sK101_skl,sK102_skl)&~p2(sK102_skl)))&((r1(sK101_skl,sK103_skl)&(r1(sK103_skl,sK104_skl)&(![Y]: (~r1(sK104_skl,Y)|p1(Y)))))&(r1(sK103_skl,sK105_skl)&~p1(sK105_skl))))&(r1(sK101_skl,sK106_skl)&~p1(sK106_skl))))&(r1(sK99_skl,sK107_skl)&~p1(sK107_skl))))&(r1(sK97_skl,sK108_skl)&~p1(sK108_skl))))&(r1(sK95_skl,sK109_skl)&~p1(sK109_skl))))&(r1(sK0_skl,sK110_skl)&~p1(sK110_skl)))),
% 10.88/2.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,sK69_skl,sK70_skl,sK71_skl,sK72_skl,sK73_skl,sK74_skl,sK75_skl,sK76_skl,sK77_skl,sK78_skl,sK79_skl,sK80_skl,sK81_skl,sK82_skl,sK83_skl,sK84_skl,sK85_skl,sK86_skl,sK87_skl,sK88_skl,sK89_skl,sK90_skl,sK91_skl,sK92_skl,sK93_skl,sK94_skl,sK95_skl,sK96_skl,sK97_skl,sK98_skl,sK99_skl,sK100_skl,sK101_skl,sK102_skl,sK103_skl,sK104_skl,sK105_skl,sK106_skl,sK107_skl,sK108_skl,sK109_skl,sK110_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y,X,Y,X,Y)),skolemize(X,sK2_skl(Y,X,Y,X,Y,X,Y)),skolemize(Y,sK3_skl(X,Y,X,Y,X,Y)),skolemize(Y,sK4_skl(X,Y,X,Y,X,Y)),skolemize(X,sK5_skl(Y,X,Y,X,Y)),skolemize(Y,sK6_skl),skolemize(Y,sK7_skl),skolemize(X,sK8_skl),skolemize(X,sK9_skl),skolemize(Y,sK10_skl),skolemize(Y,sK11_skl),skolemize(X,sK12_skl),skolemize(X,sK13_skl),skolemize(Y,sK14_skl),skolemize(Y,sK15_skl),skolemize(X,sK16_skl),skolemize(X,sK17_skl),skolemize(Y,sK18_skl),skolemize(X,sK19_skl),skolemize(Y,sK20_skl),skolemize(X,sK21_skl),skolemize(Y,sK22_skl),skolemize(X,sK23_skl(Y,X,Y,X,Y)),skolemize(Y,sK24_skl(X,Y,X,Y,X,Y)),skolemize(X,sK25_skl(Y,X,Y,X,Y)),skolemize(X,sK26_skl(Y,X,Y,X,Y)),skolemize(Y,sK27_skl(X,Y,X,Y)),skolemize(Y,sK28_skl),skolemize(Y,sK29_skl),skolemize(X,sK30_skl),skolemize(X,sK31_skl),skolemize(Y,sK32_skl),skolemize(Y,sK33_skl),skolemize(X,sK34_skl),skolemize(X,sK35_skl),skolemize(Y,sK36_skl),skolemize(Y,sK37_skl),skolemize(X,sK38_skl),skolemize(X,sK39_skl),skolemize(Y,sK40_skl),skolemize(X,sK41_skl),skolemize(Y,sK42_skl),skolemize(X,sK43_skl),skolemize(Y,sK44_skl),skolemize(Y,sK45_skl(X,Y,X,Y)),skolemize(X,sK46_skl(Y,X,Y,X,Y)),skolemize(Y,sK47_skl(X,Y,X,Y)),skolemize(Y,sK48_skl(X,Y,X,Y)),skolemize(X,sK49_skl(Y,X,Y)),skolemize(Y,sK50_skl),skolemize(Y,sK51_skl),skolemize(X,sK52_skl),skolemize(X,sK53_skl),skolemize(Y,sK54_skl),skolemize(Y,sK55_skl),skolemize(X,sK56_skl),skolemize(X,sK57_skl),skolemize(Y,sK58_skl),skolemize(Y,sK59_skl),skolemize(X,sK60_skl),skolemize(X,sK61_skl),skolemize(Y,sK62_skl),skolemize(X,sK63_skl),skolemize(Y,sK64_skl),skolemize(X,sK65_skl),skolemize(Y,sK66_skl),skolemize(X,sK67_skl(Y,X,Y)),skolemize(Y,sK68_skl(X,Y,X,Y)),skolemize(X,sK69_skl(Y,X,Y)),skolemize(X,sK70_skl(Y,X,Y)),skolemize(Y,sK71_skl(X,Y)),skolemize(Y,sK72_skl),skolemize(Y,sK73_skl),skolemize(X,sK74_skl),skolemize(X,sK75_skl),skolemize(Y,sK76_skl),skolemize(Y,sK77_skl),skolemize(X,sK78_skl),skolemize(X,sK79_skl),skolemize(Y,sK80_skl),skolemize(Y,sK81_skl),skolemize(X,sK82_skl),skolemize(X,sK83_skl),skolemize(Y,sK84_skl),skolemize(X,sK85_skl),skolemize(Y,sK86_skl),skolemize(X,sK87_skl),skolemize(Y,sK88_skl),skolemize(Y,sK89_skl(X,Y)),skolemize(X,sK90_skl(Y,X,Y)),skolemize(Y,sK91_skl(X,Y)),skolemize(Y,sK92_skl(X,Y)),skolemize(X,sK93_skl(Y)),skolemize(Y,sK94_skl),skolemize(Y,sK95_skl),skolemize(X,sK96_skl),skolemize(X,sK97_skl),skolemize(Y,sK98_skl),skolemize(Y,sK99_skl),skolemize(X,sK100_skl),skolemize(X,sK101_skl),skolemize(Y,sK102_skl),skolemize(Y,sK103_skl),skolemize(X,sK104_skl),skolemize(X,sK105_skl),skolemize(Y,sK106_skl),skolemize(X,sK107_skl),skolemize(Y,sK108_skl),skolemize(X,sK109_skl),skolemize(Y,sK110_skl)],[f10])).
% 10.88/2.06 fof(f12,plain,(
% 10.88/2.06 ?[X]: (((((((((((((((((((((((((((((((((((((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK1_skl(X,Y,X,Y,X,Y))&p1(sK1_skl(X,Y,X,Y,X,Y))))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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,sK2_skl(Y,X,Y,X,Y,X,Y))&~p1(sK2_skl(Y,X,Y,X,Y,X,Y))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK3_skl(X,Y,X,Y,X,Y))&(![X]: (~r1(sK3_skl(X,Y,X,Y,X,Y),X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK4_skl(X,Y,X,Y,X,Y))&~p1(sK4_skl(X,Y,X,Y,X,Y))))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(?[X]: r1(Y,sK5_skl(Y,X,Y,X,Y))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(?[Y]: (r1(sK0_skl,sK6_skl)&~p2(sK6_skl))))&(?[Y]: (((r1(sK0_skl,sK7_skl)&(?[X]: (r1(sK7_skl,sK8_skl)&~p2(sK8_skl))))&(?[X]: (((r1(sK7_skl,sK9_skl)&(?[Y]: (r1(sK9_skl,sK10_skl)&~p2(sK10_skl))))&(?[Y]: (((r1(sK9_skl,sK11_skl)&(?[X]: (r1(sK11_skl,sK12_skl)&~p2(sK12_skl))))&(?[X]: (((r1(sK11_skl,sK13_skl)&(?[Y]: (r1(sK13_skl,sK14_skl)&~p2(sK14_skl))))&(?[Y]: ((r1(sK13_skl,sK15_skl)&(?[X]: (r1(sK15_skl,sK16_skl)&(![Y]: (~r1(sK16_skl,Y)|p1(Y))))))&(?[X]: (r1(sK15_skl,sK17_skl)&~p1(sK17_skl))))))&(?[Y]: (r1(sK13_skl,sK18_skl)&~p1(sK18_skl))))))&(?[X]: (r1(sK11_skl,sK19_skl)&~p1(sK19_skl))))))&(?[Y]: (r1(sK9_skl,sK20_skl)&~p1(sK20_skl))))))&(?[X]: (r1(sK7_skl,sK21_skl)&~p1(sK21_skl))))))&(?[Y]: (r1(sK0_skl,sK22_skl)&~p1(sK22_skl))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK23_skl(Y,X,Y,X,Y))&p1(sK23_skl(Y,X,Y,X,Y))))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK24_skl(X,Y,X,Y,X,Y))&~p1(sK24_skl(X,Y,X,Y,X,Y))))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK25_skl(Y,X,Y,X,Y))&(![Y]: (~r1(sK25_skl(Y,X,Y,X,Y),Y)|p1(Y)))))))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK26_skl(Y,X,Y,X,Y))&~p1(sK26_skl(Y,X,Y,X,Y))))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(?[Y]: r1(X,sK27_skl(X,Y,X,Y))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(?[Y]: (r1(sK0_skl,sK28_skl)&~p2(sK28_skl))))&(?[Y]: (((r1(sK0_skl,sK29_skl)&(?[X]: (r1(sK29_skl,sK30_skl)&~p2(sK30_skl))))&(?[X]: (((r1(sK29_skl,sK31_skl)&(?[Y]: (r1(sK31_skl,sK32_skl)&~p2(sK32_skl))))&(?[Y]: (((r1(sK31_skl,sK33_skl)&(?[X]: (r1(sK33_skl,sK34_skl)&~p2(sK34_skl))))&(?[X]: (((r1(sK33_skl,sK35_skl)&(?[Y]: (r1(sK35_skl,sK36_skl)&~p2(sK36_skl))))&(?[Y]: ((r1(sK35_skl,sK37_skl)&(?[X]: (r1(sK37_skl,sK38_skl)&(![Y]: (~r1(sK38_skl,Y)|p1(Y))))))&(?[X]: (r1(sK37_skl,sK39_skl)&~p1(sK39_skl))))))&(?[Y]: (r1(sK35_skl,sK40_skl)&~p1(sK40_skl))))))&(?[X]: (r1(sK33_skl,sK41_skl)&~p1(sK41_skl))))))&(?[Y]: (r1(sK31_skl,sK42_skl)&~p1(sK42_skl))))))&(?[X]: (r1(sK29_skl,sK43_skl)&~p1(sK43_skl))))))&(?[Y]: (r1(sK0_skl,sK44_skl)&~p1(sK44_skl))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK45_skl(X,Y,X,Y))&p1(sK45_skl(X,Y,X,Y))))))|~p1(Y)))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![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,sK46_skl(Y,X,Y,X,Y))&~p1(sK46_skl(Y,X,Y,X,Y))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK47_skl(X,Y,X,Y))&(![X]: (~r1(sK47_skl(X,Y,X,Y),X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK48_skl(X,Y,X,Y))&~p1(sK48_skl(X,Y,X,Y))))))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|p2(Y)))|(![Y]: (~r1(X,Y)|(?[X]: r1(Y,sK49_skl(Y,X,Y))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(?[Y]: (r1(sK0_skl,sK50_skl)&~p2(sK50_skl))))&(?[Y]: (((r1(sK0_skl,sK51_skl)&(?[X]: (r1(sK51_skl,sK52_skl)&~p2(sK52_skl))))&(?[X]: (((r1(sK51_skl,sK53_skl)&(?[Y]: (r1(sK53_skl,sK54_skl)&~p2(sK54_skl))))&(?[Y]: (((r1(sK53_skl,sK55_skl)&(?[X]: (r1(sK55_skl,sK56_skl)&~p2(sK56_skl))))&(?[X]: (((r1(sK55_skl,sK57_skl)&(?[Y]: (r1(sK57_skl,sK58_skl)&~p2(sK58_skl))))&(?[Y]: ((r1(sK57_skl,sK59_skl)&(?[X]: (r1(sK59_skl,sK60_skl)&(![Y]: (~r1(sK60_skl,Y)|p1(Y))))))&(?[X]: (r1(sK59_skl,sK61_skl)&~p1(sK61_skl))))))&(?[Y]: (r1(sK57_skl,sK62_skl)&~p1(sK62_skl))))))&(?[X]: (r1(sK55_skl,sK63_skl)&~p1(sK63_skl))))))&(?[Y]: (r1(sK53_skl,sK64_skl)&~p1(sK64_skl))))))&(?[X]: (r1(sK51_skl,sK65_skl)&~p1(sK65_skl))))))&(?[Y]: (r1(sK0_skl,sK66_skl)&~p1(sK66_skl))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK67_skl(Y,X,Y))&p1(sK67_skl(Y,X,Y))))))|~p1(X)))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK68_skl(X,Y,X,Y))&~p1(sK68_skl(X,Y,X,Y))))))|(![X]: (~r1(Y,X)|p1(X)))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK69_skl(Y,X,Y))&(![Y]: (~r1(sK69_skl(Y,X,Y),Y)|p1(Y)))))))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK70_skl(Y,X,Y))&~p1(sK70_skl(Y,X,Y))))))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(((![X]: (~r1(Y,X)|p2(X)))|(![X]: (~r1(Y,X)|(?[Y]: r1(X,sK71_skl(X,Y))))))|(![X]: (~r1(Y,X)|p1(X)))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(?[Y]: (r1(sK0_skl,sK72_skl)&~p2(sK72_skl))))&(?[Y]: (((r1(sK0_skl,sK73_skl)&(?[X]: (r1(sK73_skl,sK74_skl)&~p2(sK74_skl))))&(?[X]: (((r1(sK73_skl,sK75_skl)&(?[Y]: (r1(sK75_skl,sK76_skl)&~p2(sK76_skl))))&(?[Y]: (((r1(sK75_skl,sK77_skl)&(?[X]: (r1(sK77_skl,sK78_skl)&~p2(sK78_skl))))&(?[X]: (((r1(sK77_skl,sK79_skl)&(?[Y]: (r1(sK79_skl,sK80_skl)&~p2(sK80_skl))))&(?[Y]: ((r1(sK79_skl,sK81_skl)&(?[X]: (r1(sK81_skl,sK82_skl)&(![Y]: (~r1(sK82_skl,Y)|p1(Y))))))&(?[X]: (r1(sK81_skl,sK83_skl)&~p1(sK83_skl))))))&(?[Y]: (r1(sK79_skl,sK84_skl)&~p1(sK84_skl))))))&(?[X]: (r1(sK77_skl,sK85_skl)&~p1(sK85_skl))))))&(?[Y]: (r1(sK75_skl,sK86_skl)&~p1(sK86_skl))))))&(?[X]: (r1(sK73_skl,sK87_skl)&~p1(sK87_skl))))))&(?[Y]: (r1(sK0_skl,sK88_skl)&~p1(sK88_skl))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK89_skl(X,Y))&p1(sK89_skl(X,Y))))))|~p1(Y)))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|((![Y]: (~r1(X,Y)|(?[X]: (r1(Y,sK90_skl(Y,X,Y))&~p1(sK90_skl(Y,X,Y))))))|(![Y]: (~r1(X,Y)|p1(Y)))))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK91_skl(X,Y))&(![X]: (~r1(sK91_skl(X,Y),X)|p1(X)))))))|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,sK92_skl(X,Y))&~p1(sK92_skl(X,Y))))))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(((![Y]: (~r1(sK0_skl,Y)|p2(Y)))|(![Y]: (~r1(sK0_skl,Y)|(?[X]: r1(Y,sK93_skl(Y))))))|(![Y]: (~r1(sK0_skl,Y)|p1(Y)))))&(?[Y]: (r1(sK0_skl,sK94_skl)&~p2(sK94_skl))))&(?[Y]: (((r1(sK0_skl,sK95_skl)&(?[X]: (r1(sK95_skl,sK96_skl)&~p2(sK96_skl))))&(?[X]: (((r1(sK95_skl,sK97_skl)&(?[Y]: (r1(sK97_skl,sK98_skl)&~p2(sK98_skl))))&(?[Y]: (((r1(sK97_skl,sK99_skl)&(?[X]: (r1(sK99_skl,sK100_skl)&~p2(sK100_skl))))&(?[X]: (((r1(sK99_skl,sK101_skl)&(?[Y]: (r1(sK101_skl,sK102_skl)&~p2(sK102_skl))))&(?[Y]: ((r1(sK101_skl,sK103_skl)&(?[X]: (r1(sK103_skl,sK104_skl)&(![Y]: (~r1(sK104_skl,Y)|p1(Y))))))&(?[X]: (r1(sK103_skl,sK105_skl)&~p1(sK105_skl))))))&(?[Y]: (r1(sK101_skl,sK106_skl)&~p1(sK106_skl))))))&(?[X]: (r1(sK99_skl,sK107_skl)&~p1(sK107_skl))))))&(?[Y]: (r1(sK97_skl,sK108_skl)&~p1(sK108_skl))))))&(?[X]: (r1(sK95_skl,sK109_skl)&~p1(sK109_skl))))))&(?[Y]: (r1(sK0_skl,sK110_skl)&~p1(sK110_skl))))),
% 10.88/2.06 inference(true_and_false_simplification,[status(thm)],[f11])).
% 10.88/2.06 fof(f167,plain,(
% 10.88/2.06 ![X0,X1,X2,X3,X4,X5]: (~r1(sK0_skl,X0)|p2(X0)|~r1(sK0_skl,X1)|~r1(X1,X2)|~r1(X2,X3)|r1(X3,sK90_skl(X3,X2,X1))|~r1(X2,X4)|p1(X4)|~r1(sK0_skl,X5)|p1(X5))),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f168,plain,(
% 10.88/2.06 ![X0,X1,X2,X3,X4,X5]: (~r1(sK0_skl,X0)|p2(X0)|~r1(sK0_skl,X1)|~r1(X1,X2)|~r1(X2,X3)|~p1(sK90_skl(X3,X2,X1))|~r1(X2,X4)|p1(X4)|~r1(sK0_skl,X5)|p1(X5))),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f174,plain,(
% 10.88/2.06 r1(sK0_skl,sK94_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f175,plain,(
% 10.88/2.06 ~p2(sK94_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f176,plain,(
% 10.88/2.06 r1(sK0_skl,sK95_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f179,plain,(
% 10.88/2.06 r1(sK95_skl,sK97_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f182,plain,(
% 10.88/2.06 r1(sK97_skl,sK99_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f185,plain,(
% 10.88/2.06 r1(sK99_skl,sK101_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f188,plain,(
% 10.88/2.06 r1(sK101_skl,sK103_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f189,plain,(
% 10.88/2.06 r1(sK103_skl,sK104_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f190,plain,(
% 10.88/2.06 ![X0]: (~r1(sK104_skl,X0)|p1(X0))),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f197,plain,(
% 10.88/2.06 r1(sK97_skl,sK108_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f198,plain,(
% 10.88/2.06 ~p1(sK108_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f201,plain,(
% 10.88/2.06 r1(sK0_skl,sK110_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f202,plain,(
% 10.88/2.06 ~p1(sK110_skl)),
% 10.88/2.06 inference(cnf_transformation,[status(thm)],[f12])).
% 10.88/2.06 fof(f203,definition,(
% 10.88/2.06 ![X0]: (sQ0_spl <=> (~r1(sK0_skl,X0)|p2(X0)))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f204,plain,(
% 10.88/2.06 ![X0]: (~r1(sK0_skl,X0)|p2(X0)|~sQ0_spl)),
% 10.88/2.06 inference(component_clause,[status(thm)],[f203])).
% 10.88/2.06 fof(f209,definition,(
% 10.88/2.06 ![X15]: (sQ2_spl <=> (~r1(sK0_skl,X15)|p1(X15)))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f210,plain,(
% 10.88/2.06 ![X0]: (~r1(sK0_skl,X0)|p1(X0)|~sQ2_spl)),
% 10.88/2.06 inference(component_clause,[status(thm)],[f209])).
% 10.88/2.06 fof(f361,definition,(
% 10.88/2.06 ![X1,X2,X3,X4]: (sQ40_spl <=> (~r1(sK0_skl,X1)|~r1(X1,X2)|~r1(X2,X3)|r1(X3,sK90_skl(X3,X2,X1))|~r1(X2,X4)|p1(X4)))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f362,plain,(
% 10.88/2.06 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|r1(X2,sK90_skl(X2,X1,X0))|~r1(X1,X3)|p1(X3)|~sQ40_spl)),
% 10.88/2.06 inference(component_clause,[status(thm)],[f361])).
% 10.88/2.06 fof(f364,plain,(
% 10.88/2.06 sQ0_spl|sQ40_spl|sQ2_spl),
% 10.88/2.06 inference(split_clause,[status(thm)],[f167,f203,f361,f209])).
% 10.88/2.06 fof(f365,definition,(
% 10.88/2.06 ![X1,X2,X3,X4]: (sQ41_spl <=> (~r1(sK0_skl,X1)|~r1(X1,X2)|~r1(X2,X3)|~p1(sK90_skl(X3,X2,X1))|~r1(X2,X4)|p1(X4)))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f366,plain,(
% 10.88/2.06 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~p1(sK90_skl(X2,X1,X0))|~r1(X1,X3)|p1(X3)|~sQ41_spl)),
% 10.88/2.06 inference(component_clause,[status(thm)],[f365])).
% 10.88/2.06 fof(f368,plain,(
% 10.88/2.06 sQ0_spl|sQ41_spl|sQ2_spl),
% 10.88/2.06 inference(split_clause,[status(thm)],[f168,f203,f365,f209])).
% 10.88/2.06 fof(f399,plain,(
% 10.88/2.06 p1(sK110_skl)|~sQ2_spl),
% 10.88/2.06 inference(resolution,[status(thm)],[f210,f201])).
% 10.88/2.06 fof(f416,plain,(
% 10.88/2.06 $false|~sQ2_spl),
% 10.88/2.06 inference(forward_subsumption_resolution,[status(thm)],[f399,f202])).
% 10.88/2.06 fof(f417,plain,(
% 10.88/2.06 ~sQ2_spl),
% 10.88/2.06 inference(contradiction_clause,[status(thm)],[f416])).
% 10.88/2.06 fof(f420,plain,(
% 10.88/2.06 p2(sK94_skl)|~sQ0_spl),
% 10.88/2.06 inference(resolution,[status(thm)],[f204,f174])).
% 10.88/2.06 fof(f435,plain,(
% 10.88/2.06 $false|~sQ0_spl),
% 10.88/2.06 inference(forward_subsumption_resolution,[status(thm)],[f420,f175])).
% 10.88/2.06 fof(f436,plain,(
% 10.88/2.06 ~sQ0_spl),
% 10.88/2.06 inference(contradiction_clause,[status(thm)],[f435])).
% 10.88/2.06 fof(f843,plain,(
% 10.88/2.06 ![X0,X1,X2]: (~r1(sK95_skl,X0)|~r1(X0,X1)|r1(X1,sK90_skl(X1,X0,sK95_skl))|~r1(X0,X2)|p1(X2)|~sQ40_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f362,f176])).
% 10.88/2.06 fof(f1000,plain,(
% 10.88/2.06 ![X0,X1]: (~r1(sK97_skl,X0)|r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~r1(sK97_skl,X1)|p1(X1)|~sQ40_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f843,f179])).
% 10.88/2.06 fof(f1012,definition,(
% 10.88/2.06 ![X0]: (sQ120_spl <=> (~r1(sK97_skl,X0)|r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f1013,plain,(
% 10.88/2.06 ![X0]: (~r1(sK97_skl,X0)|r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~sQ120_spl)),
% 10.88/2.06 inference(component_clause,[status(thm)],[f1012])).
% 10.88/2.06 fof(f1015,definition,(
% 10.88/2.06 ![X1]: (sQ121_spl <=> (~r1(sK97_skl,X1)|p1(X1)))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f1016,plain,(
% 10.88/2.06 ![X0]: (~r1(sK97_skl,X0)|p1(X0)|~sQ121_spl)),
% 10.88/2.06 inference(component_clause,[status(thm)],[f1015])).
% 10.88/2.06 fof(f1018,plain,(
% 10.88/2.06 sQ120_spl|sQ121_spl|~sQ40_spl),
% 10.88/2.06 inference(split_clause,[status(thm)],[f1000,f1012,f1015,f361])).
% 10.88/2.06 fof(f1032,definition,(
% 10.88/2.06 sQ126_spl <=> (r1(sK0_skl,sK95_skl))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f1034,plain,(
% 10.88/2.06 ~r1(sK0_skl,sK95_skl)|sQ126_spl),
% 10.88/2.06 inference(component_clause,[status(thm)],[f1032])).
% 10.88/2.06 fof(f1043,plain,(
% 10.88/2.06 $false|sQ126_spl),
% 10.88/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1034,f176])).
% 10.88/2.06 fof(f1044,plain,(
% 10.88/2.06 sQ126_spl),
% 10.88/2.06 inference(contradiction_clause,[status(thm)],[f1043])).
% 10.88/2.06 fof(f1074,plain,(
% 10.88/2.06 ![X0,X1]: (r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~r1(sK97_skl,X1)|~r1(X1,X0)|~sQ120_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f1013,f8])).
% 10.88/2.06 fof(f1084,plain,(
% 10.88/2.06 p1(sK108_skl)|~sQ121_spl),
% 10.88/2.06 inference(resolution,[status(thm)],[f1016,f197])).
% 10.88/2.06 fof(f1090,plain,(
% 10.88/2.06 $false|~sQ121_spl),
% 10.88/2.06 inference(forward_subsumption_resolution,[status(thm)],[f1084,f198])).
% 10.88/2.06 fof(f1091,plain,(
% 10.88/2.06 ~sQ121_spl),
% 10.88/2.06 inference(contradiction_clause,[status(thm)],[f1090])).
% 10.88/2.06 fof(f1220,plain,(
% 10.88/2.06 ![X0]: (r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~r1(sK99_skl,X0)|~sQ120_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f1074,f182])).
% 10.88/2.06 fof(f1251,plain,(
% 10.88/2.06 ![X0,X1]: (r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~r1(sK99_skl,X1)|~r1(X1,X0)|~sQ120_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f1220,f8])).
% 10.88/2.06 fof(f1422,plain,(
% 10.88/2.06 ![X0]: (r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~r1(sK101_skl,X0)|~sQ120_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f1251,f185])).
% 10.88/2.06 fof(f1453,plain,(
% 10.88/2.06 ![X0,X1]: (r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~r1(sK101_skl,X1)|~r1(X1,X0)|~sQ120_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f1422,f8])).
% 10.88/2.06 fof(f1638,plain,(
% 10.88/2.06 ![X0]: (r1(X0,sK90_skl(X0,sK97_skl,sK95_skl))|~r1(sK103_skl,X0)|~sQ120_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f1453,f188])).
% 10.88/2.06 fof(f1666,plain,(
% 10.88/2.06 r1(sK104_skl,sK90_skl(sK104_skl,sK97_skl,sK95_skl))|~sQ120_spl),
% 10.88/2.06 inference(resolution,[status(thm)],[f1638,f189])).
% 10.88/2.06 fof(f1680,plain,(
% 10.88/2.06 p1(sK90_skl(sK104_skl,sK97_skl,sK95_skl))|~sQ120_spl),
% 10.88/2.06 inference(resolution,[status(thm)],[f1666,f190])).
% 10.88/2.06 fof(f1681,plain,(
% 10.88/2.06 ![X0]: (~r1(sK0_skl,sK95_skl)|~r1(sK95_skl,sK97_skl)|~r1(sK97_skl,sK104_skl)|~r1(sK97_skl,X0)|p1(X0)|~sQ120_spl|~sQ41_spl)),
% 10.88/2.06 inference(resolution,[status(thm)],[f1680,f366])).
% 10.88/2.06 fof(f1683,definition,(
% 10.88/2.06 sQ200_spl <=> (r1(sK95_skl,sK97_skl))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f1685,plain,(
% 10.88/2.06 ~r1(sK95_skl,sK97_skl)|sQ200_spl),
% 10.88/2.06 inference(component_clause,[status(thm)],[f1683])).
% 10.88/2.06 fof(f1686,definition,(
% 10.88/2.06 sQ201_spl <=> (r1(sK97_skl,sK104_skl))),
% 10.88/2.06 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 10.88/2.06 fof(f1688,plain,(
% 10.88/2.06 ~r1(sK97_skl,sK104_skl)|sQ201_spl),
% 10.88/2.06 inference(component_clause,[status(thm)],[f1686])).
% 10.88/2.06 fof(f1689,plain,(
% 10.88/2.06 ~sQ126_spl|~sQ200_spl|~sQ201_spl|sQ121_spl|~sQ120_spl|~sQ41_spl),
% 10.88/2.06 inference(split_clause,[status(thm)],[f1681,f1032,f1683,f1686,f1015,f1012,f365])).
% 10.88/2.06 fof(f1697,plain,(
% 10.88/2.06 $false|sQ200_spl),
% 10.88/2.07 inference(forward_subsumption_resolution,[status(thm)],[f1685,f179])).
% 10.88/2.07 fof(f1698,plain,(
% 10.88/2.07 sQ200_spl),
% 10.88/2.07 inference(contradiction_clause,[status(thm)],[f1697])).
% 10.88/2.07 fof(f1699,plain,(
% 10.88/2.07 ![X0]: (~r1(sK97_skl,X0)|~r1(X0,sK104_skl)|sQ201_spl)),
% 10.88/2.07 inference(resolution,[status(thm)],[f1688,f8])).
% 10.88/2.07 fof(f1700,plain,(
% 10.88/2.07 ~r1(sK97_skl,sK103_skl)|sQ201_spl),
% 10.88/2.07 inference(resolution,[status(thm)],[f1699,f189])).
% 10.88/2.07 fof(f1704,plain,(
% 10.88/2.07 ![X0]: (~r1(sK97_skl,X0)|~r1(X0,sK103_skl)|sQ201_spl)),
% 10.88/2.07 inference(resolution,[status(thm)],[f1700,f8])).
% 10.88/2.07 fof(f1706,plain,(
% 10.88/2.07 ~r1(sK97_skl,sK101_skl)|sQ201_spl),
% 10.88/2.07 inference(resolution,[status(thm)],[f1704,f188])).
% 10.88/2.07 fof(f1709,plain,(
% 10.88/2.07 ![X0]: (~r1(sK97_skl,X0)|~r1(X0,sK101_skl)|sQ201_spl)),
% 10.88/2.07 inference(resolution,[status(thm)],[f1706,f8])).
% 10.88/2.07 fof(f1712,plain,(
% 10.88/2.07 ~r1(sK97_skl,sK99_skl)|sQ201_spl),
% 10.88/2.07 inference(resolution,[status(thm)],[f1709,f185])).
% 10.88/2.07 fof(f1716,plain,(
% 10.88/2.07 $false|sQ201_spl),
% 10.88/2.07 inference(forward_subsumption_resolution,[status(thm)],[f1712,f182])).
% 10.88/2.07 fof(f1717,plain,(
% 10.88/2.07 sQ201_spl),
% 10.88/2.07 inference(contradiction_clause,[status(thm)],[f1716])).
% 10.88/2.07 fof(f1718,plain,(
% 10.88/2.07 $false),
% 10.88/2.07 inference(sat_refutation,[status(thm)],[f364,f368,f417,f436,f1018,f1044,f1091,f1689,f1698,f1717])).
% 10.88/2.07 % SZS output end CNFRefutation for theBenchmark.p
% 10.88/2.07 % Elapsed time: 1.470553 seconds
% 10.88/2.07 % CPU time: 11.464252 seconds
% 10.88/2.07 % Total memory used: 56.786 MB
% 10.88/2.07 % Net memory used: 53.170 MB
%------------------------------------------------------------------------------