%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL644+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 : n014.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:27 PM UTC 2026
% Result : Theorem 0.16s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n014.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 00:44:19 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.45 % Refutation found
% 0.16/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.45 fof(f1,conjecture,(
% 0.16/0.45 ~ (? [X] :~ ( ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y) ))| (! [Y] :( ~ r1(X,Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p6(X)& (! [Y] :( ~ r1(X,Y)| p6(Y) ) ))| p5(X) ))| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| (! [X] :( ~ r1(Y,X)| p6(X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ))& p5(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y) ))| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ) ))| p4(X) ))| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| (! [X] :( ~ r1(Y,X)| p5(X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ))& p4(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y) ))| (! [Y] :( ~ r1(X,Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ) ))| p3(X) ))| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| (! [X] :( ~ r1(Y,X)| p4(X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ))& p3(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ) ))| p2(X) ))| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| (! [X] :( ~ r1(Y,X)| p3(X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ))& p2(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ) )) )| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y) ))| (! [Y] :( ~ r1(X,Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ) ))| p1(X) ))| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| (! [X] :( ~ r1(Y,X)| p2(X)| ~ ( p1(X)& (! [Y] :( ~ r1(X,Y)| p1(Y) ))& p1(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ) )) ) ) )),
% 0.16/0.45 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.45 fof(f2,negated_conjecture,(
% 0.16/0.45 ~(~ (? [X] :~ ( ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y) ))| (! [Y] :( ~ r1(X,Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p6(X)& (! [Y] :( ~ r1(X,Y)| p6(Y) ) ))| p5(X) ))| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| (! [X] :( ~ r1(Y,X)| p6(X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ))& p5(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p6(Y)& (! [X] :( ~ r1(Y,X)| p6(X) ) ))| p5(Y)| p6(Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y) ))| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p5(X)& (! [Y] :( ~ r1(X,Y)| p5(Y) ) ))| p4(X) ))| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| (! [X] :( ~ r1(Y,X)| p5(X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ))& p4(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p5(Y)& (! [X] :( ~ r1(Y,X)| p5(X) ) ))| p4(Y)| p5(Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ))& p4(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y) ))| (! [Y] :( ~ r1(X,Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p4(X)& (! [Y] :( ~ r1(X,Y)| p4(Y) ) ))| p3(X) ))| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| (! [X] :( ~ r1(Y,X)| p4(X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ))& p3(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p4(Y)& (! [X] :( ~ r1(Y,X)| p4(X) ) ))| p3(Y)| p4(Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ))& p3(Y) ) ) )) )| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y) ))| (! [Y] :( ~ r1(X,Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p3(X)& (! [Y] :( ~ r1(X,Y)| p3(Y) ) ))| p2(X) ))| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| (! [X] :( ~ r1(Y,X)| p3(X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ))& p2(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p3(Y)& (! [X] :( ~ r1(Y,X)| p3(X) ) ))| p2(Y)| p3(Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ))& p2(Y) ) ) )) )| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| (! [Y] :( ~ r1(X,Y)| p5(Y)| ~ ( (! [X] :( ~ r1(Y,X)| p5(X) ))& p5(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y) ))| (! [Y] :( ~ r1(X,Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ ( p2(X)& (! [Y] :( ~ r1(X,Y)| p2(Y) ) ))| p1(X) ))| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| (! [X] :( ~ r1(Y,X)| p2(X)| ~ ( p1(X)& (! [Y] :( ~ r1(X,Y)| p1(Y) ))& p1(X) ) ) )))& (! [Y] :( ~ r1(X,Y)| ~ ( p2(Y)& (! [X] :( ~ r1(Y,X)| p2(X) ) ))| p1(Y)| p2(Y)| ~ ( p1(Y)& (! [X] :( ~ r1(Y,X)| p1(X) ))& p1(Y) ) ) )) ) ) ))),
% 0.16/0.45 inference(negated_conjecture,[status(cth)],[f1])).
% 0.16/0.45 fof(f3,plain,(
% 0.16/0.45 ?[X]: (((((((((![Y]: ((~r1(X,Y)|(~p6(Y)|(?[X]: (r1(Y,X)&~p6(X)))))|p5(Y)))|(![Y]: ((~r1(X,Y)|p6(Y))|((~p5(Y)|(?[X]: (r1(Y,X)&~p5(X))))|~p5(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p6(X)&(![Y]: (~r1(X,Y)|p6(Y)))))&~p5(X))))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y))))|(?[Y]: (((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&(?[X]: ((r1(Y,X)&~p6(X))&((p5(X)&(![Y]: (~r1(X,Y)|p5(Y))))&p5(X)))))))|(?[Y]: ((((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y))))))&(((![Y]: ((~r1(X,Y)|(~p5(Y)|(?[X]: (r1(Y,X)&~p5(X)))))|p4(Y)))|(![Y]: ((~r1(X,Y)|p5(Y))|((~p4(Y)|(?[X]: (r1(Y,X)&~p4(X))))|~p4(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p5(X)&(![Y]: (~r1(X,Y)|p5(Y)))))&~p4(X))))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y))))|(?[Y]: (((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&(?[X]: ((r1(Y,X)&~p5(X))&((p4(X)&(![Y]: (~r1(X,Y)|p4(Y))))&p4(X)))))))|(?[Y]: ((((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p4(Y)|(?[X]: (r1(Y,X)&~p4(X)))))|p3(Y)))|(![Y]: ((~r1(X,Y)|p4(Y))|((~p3(Y)|(?[X]: (r1(Y,X)&~p3(X))))|~p3(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p4(X)&(![Y]: (~r1(X,Y)|p4(Y)))))&~p3(X))))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y))))|(?[Y]: (((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&(?[X]: ((r1(Y,X)&~p4(X))&((p3(X)&(![Y]: (~r1(X,Y)|p3(Y))))&p3(X)))))))|(?[Y]: ((((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p3(Y)|(?[X]: (r1(Y,X)&~p3(X)))))|p2(Y)))|(![Y]: ((~r1(X,Y)|p3(Y))|((~p2(Y)|(?[X]: (r1(Y,X)&~p2(X))))|~p2(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p3(X)&(![Y]: (~r1(X,Y)|p3(Y)))))&~p2(X))))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y))))|(?[Y]: (((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&(?[X]: ((r1(Y,X)&~p3(X))&((p2(X)&(![Y]: (~r1(X,Y)|p2(Y))))&p2(X)))))))|(?[Y]: ((((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y)))))))&(?[Y]: ((r1(X,Y)&~p5(Y))&((![X]: (~r1(Y,X)|p5(X)))&p5(Y)))))&(?[Y]: ((r1(X,Y)&~p5(Y))&((![X]: (~r1(Y,X)|p5(X)))&p5(Y)))))&(((![Y]: ((~r1(X,Y)|(~p2(Y)|(?[X]: (r1(Y,X)&~p2(X)))))|p1(Y)))|(![Y]: ((~r1(X,Y)|p2(Y))|((~p1(Y)|(?[X]: (r1(Y,X)&~p1(X))))|~p1(Y)))))|(((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p2(X)&(![Y]: (~r1(X,Y)|p2(Y)))))&~p1(X))))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y))))|(?[Y]: (((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&(?[X]: ((r1(Y,X)&~p2(X))&((p1(X)&(![Y]: (~r1(X,Y)|p1(Y))))&p1(X)))))))|(?[Y]: ((((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y)))))))),
% 0.16/0.45 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.16/0.45 fof(f4,definition,(
% 0.16/0.45 ![Y,X]: (sP0_prd(X,Y)<=>(r1(Y,X)&~p6(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.16/0.45 fof(f5,definition,(
% 0.16/0.45 ![Y,X]: (sP1_prd(X,Y)<=>(r1(Y,X)&~p5(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.16/0.45 fof(f6,definition,(
% 0.16/0.45 ![X]: (sP2_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p6(X)&(![Y]: (~r1(X,Y)|p6(Y)))))&~p5(X))))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y))))|(?[Y]: (((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&(?[X]: ((r1(Y,X)&~p6(X))&((p5(X)&(![Y]: (~r1(X,Y)|p5(Y))))&p5(X))))))))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.16/0.45 fof(f7,definition,(
% 0.16/0.45 ![Y,X]: (sP3_prd(X,Y)<=>(r1(Y,X)&~p5(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.16/0.45 fof(f8,definition,(
% 0.16/0.45 ![Y,X]: (sP4_prd(X,Y)<=>(r1(Y,X)&~p4(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.16/0.45 fof(f9,definition,(
% 0.16/0.45 ![X]: (sP5_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p5(X)&(![Y]: (~r1(X,Y)|p5(Y)))))&~p4(X))))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y))))|(?[Y]: (((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&(?[X]: ((r1(Y,X)&~p5(X))&((p4(X)&(![Y]: (~r1(X,Y)|p4(Y))))&p4(X))))))))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.16/0.45 fof(f10,definition,(
% 0.16/0.45 ![Y,X]: (sP6_prd(X,Y)<=>(r1(Y,X)&~p4(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.16/0.45 fof(f11,definition,(
% 0.16/0.45 ![Y,X]: (sP7_prd(X,Y)<=>(r1(Y,X)&~p3(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP7_prd])],[])).
% 0.16/0.45 fof(f12,definition,(
% 0.16/0.45 ![X]: (sP8_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p4(X)&(![Y]: (~r1(X,Y)|p4(Y)))))&~p3(X))))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y))))|(?[Y]: (((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&(?[X]: ((r1(Y,X)&~p4(X))&((p3(X)&(![Y]: (~r1(X,Y)|p3(Y))))&p3(X))))))))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP8_prd])],[])).
% 0.16/0.45 fof(f13,definition,(
% 0.16/0.45 ![Y,X]: (sP9_prd(X,Y)<=>(r1(Y,X)&~p3(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 0.16/0.45 fof(f14,definition,(
% 0.16/0.45 ![Y,X]: (sP10_prd(X,Y)<=>(r1(Y,X)&~p2(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 0.16/0.45 fof(f15,definition,(
% 0.16/0.45 ![X]: (sP11_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p3(X)&(![Y]: (~r1(X,Y)|p3(Y)))))&~p2(X))))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y))))|(?[Y]: (((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&(?[X]: ((r1(Y,X)&~p3(X))&((p2(X)&(![Y]: (~r1(X,Y)|p2(Y))))&p2(X))))))))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 0.16/0.45 fof(f16,definition,(
% 0.16/0.45 ![Y,X]: (sP12_prd(X,Y)<=>(r1(Y,X)&~p2(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP12_prd])],[])).
% 0.16/0.45 fof(f17,definition,(
% 0.16/0.45 ![Y,X]: (sP13_prd(X,Y)<=>(r1(Y,X)&~p1(X)))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP13_prd])],[])).
% 0.16/0.45 fof(f18,definition,(
% 0.16/0.45 ![X]: (sP14_prd(X)<=>((?[Y]: (((r1(X,Y)&(?[X]: ((r1(Y,X)&(p2(X)&(![Y]: (~r1(X,Y)|p2(Y)))))&~p1(X))))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y))))|(?[Y]: (((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&(?[X]: ((r1(Y,X)&~p2(X))&((p1(X)&(![Y]: (~r1(X,Y)|p1(Y))))&p1(X))))))))),
% 0.16/0.45 introduced(definition,[new_symbols(definition,[sP14_prd])],[])).
% 0.16/0.45 fof(f19,plain,(
% 0.16/0.45 ?[X]: (((((((((![Y]: ((~r1(X,Y)|(~p6(Y)|(?[X]: sP0_prd(X,Y))))|p5(Y)))|(![Y]: ((~r1(X,Y)|p6(Y))|((~p5(Y)|(?[X]: sP1_prd(X,Y)))|~p5(Y)))))|(sP2_prd(X)|(?[Y]: ((((r1(X,Y)&(p6(Y)&(![X]: (~r1(Y,X)|p6(X)))))&~p5(Y))&~p6(Y))&((p5(Y)&(![X]: (~r1(Y,X)|p5(X))))&p5(Y))))))&(((![Y]: ((~r1(X,Y)|(~p5(Y)|(?[X]: sP3_prd(X,Y))))|p4(Y)))|(![Y]: ((~r1(X,Y)|p5(Y))|((~p4(Y)|(?[X]: sP4_prd(X,Y)))|~p4(Y)))))|(sP5_prd(X)|(?[Y]: ((((r1(X,Y)&(p5(Y)&(![X]: (~r1(Y,X)|p5(X)))))&~p4(Y))&~p5(Y))&((p4(Y)&(![X]: (~r1(Y,X)|p4(X))))&p4(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p4(Y)|(?[X]: sP6_prd(X,Y))))|p3(Y)))|(![Y]: ((~r1(X,Y)|p4(Y))|((~p3(Y)|(?[X]: sP7_prd(X,Y)))|~p3(Y)))))|(sP8_prd(X)|(?[Y]: ((((r1(X,Y)&(p4(Y)&(![X]: (~r1(Y,X)|p4(X)))))&~p3(Y))&~p4(Y))&((p3(Y)&(![X]: (~r1(Y,X)|p3(X))))&p3(Y)))))))&(((![Y]: ((~r1(X,Y)|(~p3(Y)|(?[X]: sP9_prd(X,Y))))|p2(Y)))|(![Y]: ((~r1(X,Y)|p3(Y))|((~p2(Y)|(?[X]: sP10_prd(X,Y)))|~p2(Y)))))|(sP11_prd(X)|(?[Y]: ((((r1(X,Y)&(p3(Y)&(![X]: (~r1(Y,X)|p3(X)))))&~p2(Y))&~p3(Y))&((p2(Y)&(![X]: (~r1(Y,X)|p2(X))))&p2(Y)))))))&(?[Y]: ((r1(X,Y)&~p5(Y))&((![X]: (~r1(Y,X)|p5(X)))&p5(Y)))))&(?[Y]: ((r1(X,Y)&~p5(Y))&((![X]: (~r1(Y,X)|p5(X)))&p5(Y)))))&(((![Y]: ((~r1(X,Y)|(~p2(Y)|(?[X]: sP12_prd(X,Y))))|p1(Y)))|(![Y]: ((~r1(X,Y)|p2(Y))|((~p1(Y)|(?[X]: sP13_prd(X,Y)))|~p1(Y)))))|(sP14_prd(X)|(?[Y]: ((((r1(X,Y)&(p2(Y)&(![X]: (~r1(Y,X)|p2(X)))))&~p1(Y))&~p2(Y))&((p1(Y)&(![X]: (~r1(Y,X)|p1(X))))&p1(Y)))))))),
% 0.16/0.45 inference(formula_renaming,[status(thm)],[f3,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8,f7,f6,f5,f4])).
% 0.16/0.45 fof(f20,plain,(
% 0.16/0.45 (((((((((![Y]: ((~r1(sK0_skl,Y)|(~p6(Y)|sP0_prd(sK1_skl(Y),Y)))|p5(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p6(Y))|((~p5(Y)|sP1_prd(sK2_skl(Y),Y))|~p5(Y)))))|(sP2_prd(sK0_skl)|((((r1(sK0_skl,sK3_skl)&(p6(sK3_skl)&(![X]: (~r1(sK3_skl,X)|p6(X)))))&~p5(sK3_skl))&~p6(sK3_skl))&((p5(sK3_skl)&(![X]: (~r1(sK3_skl,X)|p5(X))))&p5(sK3_skl)))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p5(Y)|sP3_prd(sK4_skl(Y),Y)))|p4(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p5(Y))|((~p4(Y)|sP4_prd(sK5_skl(Y),Y))|~p4(Y)))))|(sP5_prd(sK0_skl)|((((r1(sK0_skl,sK6_skl)&(p5(sK6_skl)&(![X]: (~r1(sK6_skl,X)|p5(X)))))&~p4(sK6_skl))&~p5(sK6_skl))&((p4(sK6_skl)&(![X]: (~r1(sK6_skl,X)|p4(X))))&p4(sK6_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p4(Y)|sP6_prd(sK7_skl(Y),Y)))|p3(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p4(Y))|((~p3(Y)|sP7_prd(sK8_skl(Y),Y))|~p3(Y)))))|(sP8_prd(sK0_skl)|((((r1(sK0_skl,sK9_skl)&(p4(sK9_skl)&(![X]: (~r1(sK9_skl,X)|p4(X)))))&~p3(sK9_skl))&~p4(sK9_skl))&((p3(sK9_skl)&(![X]: (~r1(sK9_skl,X)|p3(X))))&p3(sK9_skl))))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p3(Y)|sP9_prd(sK10_skl(Y),Y)))|p2(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p3(Y))|((~p2(Y)|sP10_prd(sK11_skl(Y),Y))|~p2(Y)))))|(sP11_prd(sK0_skl)|((((r1(sK0_skl,sK12_skl)&(p3(sK12_skl)&(![X]: (~r1(sK12_skl,X)|p3(X)))))&~p2(sK12_skl))&~p3(sK12_skl))&((p2(sK12_skl)&(![X]: (~r1(sK12_skl,X)|p2(X))))&p2(sK12_skl))))))&((r1(sK0_skl,sK13_skl)&~p5(sK13_skl))&((![X]: (~r1(sK13_skl,X)|p5(X)))&p5(sK13_skl))))&((r1(sK0_skl,sK14_skl)&~p5(sK14_skl))&((![X]: (~r1(sK14_skl,X)|p5(X)))&p5(sK14_skl))))&(((![Y]: ((~r1(sK0_skl,Y)|(~p2(Y)|sP12_prd(sK15_skl(Y),Y)))|p1(Y)))|(![Y]: ((~r1(sK0_skl,Y)|p2(Y))|((~p1(Y)|sP13_prd(sK16_skl(Y),Y))|~p1(Y)))))|(sP14_prd(sK0_skl)|((((r1(sK0_skl,sK17_skl)&(p2(sK17_skl)&(![X]: (~r1(sK17_skl,X)|p2(X)))))&~p1(sK17_skl))&~p2(sK17_skl))&((p1(sK17_skl)&(![X]: (~r1(sK17_skl,X)|p1(X))))&p1(sK17_skl))))))),
% 0.16/0.45 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]),skolemize(X,sK0_skl),skolemize(X,sK1_skl(Y)),skolemize(X,sK2_skl(Y)),skolemize(Y,sK3_skl),skolemize(X,sK4_skl(Y)),skolemize(X,sK5_skl(Y)),skolemize(Y,sK6_skl),skolemize(X,sK7_skl(Y)),skolemize(X,sK8_skl(Y)),skolemize(Y,sK9_skl),skolemize(X,sK10_skl(Y)),skolemize(X,sK11_skl(Y)),skolemize(Y,sK12_skl),skolemize(Y,sK13_skl),skolemize(Y,sK14_skl),skolemize(X,sK15_skl(Y)),skolemize(X,sK16_skl(Y)),skolemize(Y,sK17_skl)],[f19])).
% 0.16/0.46 fof(f54,plain,(
% 0.16/0.46 ~p5(sK13_skl)),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f20])).
% 0.16/0.46 fof(f56,plain,(
% 0.16/0.46 p5(sK13_skl)),
% 0.16/0.46 inference(cnf_transformation,[status(thm)],[f20])).
% 0.16/0.46 fof(f454,plain,(
% 0.16/0.46 $false),
% 0.16/0.46 inference(forward_subsumption_resolution,[status(thm)],[f56,f54])).
% 0.16/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.50 % Elapsed time: 0.071618 seconds
% 0.16/0.50 % CPU time: 0.081248 seconds
% 0.16/0.50 % Total memory used: 4.254 MB
% 0.16/0.50 % Net memory used: 4.211 MB
%------------------------------------------------------------------------------