%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL686+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 : n002.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:56 PM UTC 2026
% Result : Theorem 0.14s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL686+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.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 01:00:16 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.14/0.40 % Refutation found
% 0.14/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.14/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.40 fof(f1,axiom,(
% 0.14/0.40 (! [X] : r1(X,X) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f3,conjecture,(
% 0.14/0.40 ~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| ~ p15(Y)| (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| $false ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p14(Y)& ~ p13(Y) )| ( ~ p14(Y)& p13(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p13(X)& ~ p12(X) )| ( ~ p13(X)& p12(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p12(Y)& ~ p11(Y) )| ( ~ p12(Y)& p11(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p11(X)& ~ p10(X) )| ( ~ p11(X)& p10(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p10(Y)& ~ p9(Y) )| ( ~ p10(Y)& p9(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p9(X)& ~ p8(X) )| ( ~ p9(X)& p8(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p8(Y)& ~ p7(Y) )| ( ~ p8(Y)& p7(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p7(X)& ~ p6(X) )| ( ~ p7(X)& p6(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p6(Y)& ~ p5(Y) )| ( ~ p6(Y)& p5(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p5(X)& ~ p4(X) )| ( ~ p5(X)& p4(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p4(Y)& ~ p3(Y) )| ( ~ p4(Y)& p3(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p3(X)& ~ p2(X) )| ( ~ p3(X)& p2(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p2(Y)& ~ p1(Y) )| ( ~ p2(Y)& p1(Y) ) ) ))| (! [Y] :( ~ r1(X,Y)| p15(Y) ))| (! [Y] :( ~ r1(X,Y)| ( ~ p13(Y)& ~ p14(Y) )| ( p14(Y)& p13(Y) )| ( ~ p12(Y)& ~ p13(Y) )| ( p13(Y)& p12(Y) )| ( ~ p11(Y)& ~ p12(Y) )| ( p12(Y)& p11(Y) )| ( ~ p10(Y)& ~ p11(Y) )| ( p11(Y)& p10(Y) )| ( ~ p9(Y)& ~ p10(Y) )| ( p10(Y)& p9(Y) )| ( ~ p8(Y)& ~ p9(Y) )| ( p9(Y)& p8(Y) )| ( ~ p7(Y)& ~ p8(Y) )| ( p8(Y)& p7(Y) )| ( ~ p6(Y)& ~ p7(Y) )| ( p7(Y)& p6(Y) )| ( ~ p5(Y)& ~ p6(Y) )| ( p6(Y)& p5(Y) )| ( ~ p4(Y)& ~ p5(Y) )| ( p5(Y)& p4(Y) )| ( ~ p3(Y)& ~ p4(Y) )| ( p4(Y)& p3(Y) )| ( ~ p2(Y)& ~ p3(Y) )| ( p3(Y)& p2(Y) )| ( ~ p1(Y)& ~ p2(Y) )| ( p2(Y)& p1(Y) ) ) )) ) )) )) )),
% 0.14/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.40 fof(f4,negated_conjecture,(
% 0.14/0.40 ~(~ (? [X] :~ ( (! [Y] :( ~ r1(X,Y)| ~ p15(Y)| (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| $false ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p14(Y)& ~ p13(Y) )| ( ~ p14(Y)& p13(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p13(X)& ~ p12(X) )| ( ~ p13(X)& p12(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p12(Y)& ~ p11(Y) )| ( ~ p12(Y)& p11(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p11(X)& ~ p10(X) )| ( ~ p11(X)& p10(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p10(Y)& ~ p9(Y) )| ( ~ p10(Y)& p9(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p9(X)& ~ p8(X) )| ( ~ p9(X)& p8(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p8(Y)& ~ p7(Y) )| ( ~ p8(Y)& p7(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p7(X)& ~ p6(X) )| ( ~ p7(X)& p6(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p6(Y)& ~ p5(Y) )| ( ~ p6(Y)& p5(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p5(X)& ~ p4(X) )| ( ~ p5(X)& p4(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p4(Y)& ~ p3(Y) )| ( ~ p4(Y)& p3(Y) ) ) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ( p3(X)& ~ p2(X) )| ( ~ p3(X)& p2(X) ) ) ) )))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ( p2(Y)& ~ p1(Y) )| ( ~ p2(Y)& p1(Y) ) ) ))| (! [Y] :( ~ r1(X,Y)| p15(Y) ))| (! [Y] :( ~ r1(X,Y)| ( ~ p13(Y)& ~ p14(Y) )| ( p14(Y)& p13(Y) )| ( ~ p12(Y)& ~ p13(Y) )| ( p13(Y)& p12(Y) )| ( ~ p11(Y)& ~ p12(Y) )| ( p12(Y)& p11(Y) )| ( ~ p10(Y)& ~ p11(Y) )| ( p11(Y)& p10(Y) )| ( ~ p9(Y)& ~ p10(Y) )| ( p10(Y)& p9(Y) )| ( ~ p8(Y)& ~ p9(Y) )| ( p9(Y)& p8(Y) )| ( ~ p7(Y)& ~ p8(Y) )| ( p8(Y)& p7(Y) )| ( ~ p6(Y)& ~ p7(Y) )| ( p7(Y)& p6(Y) )| ( ~ p5(Y)& ~ p6(Y) )| ( p6(Y)& p5(Y) )| ( ~ p4(Y)& ~ p5(Y) )| ( p5(Y)& p4(Y) )| ( ~ p3(Y)& ~ p4(Y) )| ( p4(Y)& p3(Y) )| ( ~ p2(Y)& ~ p3(Y) )| ( p3(Y)& p2(Y) )| ( ~ p1(Y)& ~ p2(Y) )| ( p2(Y)& p1(Y) ) ) )) ) )) )) ))),
% 0.14/0.40 inference(negated_conjecture,[status(cth)],[f3])).
% 0.14/0.40 fof(f5,plain,(
% 0.14/0.40 ![X0]: (r1(X0,X0))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f1])).
% 0.14/0.40 fof(f9,plain,(
% 0.14/0.40 ?[X]: ((?[Y]: ((r1(X,Y)&p15(Y))&(?[X]: (r1(Y,X)&p1(X)))))&(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|((((?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: (r1(X,Y)&$true)))&(![Y]: (~r1(X,Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]: (~r1(Y,X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]: (~r1(X,Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]: (~r1(Y,X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]: (~r1(X,Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]: (~r1(Y,X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]: (~r1(X,Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]: (~r1(Y,X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]: (~r1(X,Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]: (~r1(Y,X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]: (~r1(X,Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]: (~r1(Y,X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]: (r1(X,Y)&~p15(Y))))&(?[Y]: ((((((((((((((((((((((((((r1(X,Y)&(p13(Y)|p14(Y)))&(~p14(Y)|~p13(Y)))&(p12(Y)|p13(Y)))&(~p13(Y)|~p12(Y)))&(p11(Y)|p12(Y)))&(~p12(Y)|~p11(Y)))&(p10(Y)|p11(Y)))&(~p11(Y)|~p10(Y)))&(p9(Y)|p10(Y)))&(~p10(Y)|~p9(Y)))&(p8(Y)|p9(Y)))&(~p9(Y)|~p8(Y)))&(p7(Y)|p8(Y)))&(~p8(Y)|~p7(Y)))&(p6(Y)|p7(Y)))&(~p7(Y)|~p6(Y)))&(p5(Y)|p6(Y)))&(~p6(Y)|~p5(Y)))&(p4(Y)|p5(Y)))&(~p5(Y)|~p4(Y)))&(p3(Y)|p4(Y)))&(~p4(Y)|~p3(Y)))&(p2(Y)|p3(Y)))&(~p3(Y)|~p2(Y)))&(p1(Y)|p2(Y)))&(~p2(Y)|~p1(Y))))))))))),
% 0.14/0.40 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.14/0.40 fof(f10,plain,(
% 0.14/0.40 ?[X]: ((?[Y]: ((r1(X,Y)&p15(Y))&(?[X]: (r1(Y,X)&p1(X)))))&(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|((((?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&(?[Y]: ((r1(X,Y)&(?[X]: ((r1(Y,X)&((?[Y]: r1(X,Y))&$true))&(![Y]: (~r1(X,Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]: (~r1(Y,X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]: (~r1(X,Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]: (~r1(Y,X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]: (~r1(X,Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]: (~r1(Y,X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]: (~r1(X,Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]: (~r1(Y,X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]: (~r1(X,Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]: (~r1(Y,X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]: (~r1(X,Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]: (~r1(Y,X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]: (r1(X,Y)&~p15(Y))))&(?[Y]: ((((((((((((((((((((((((((r1(X,Y)&(p13(Y)|p14(Y)))&(~p14(Y)|~p13(Y)))&(p12(Y)|p13(Y)))&(~p13(Y)|~p12(Y)))&(p11(Y)|p12(Y)))&(~p12(Y)|~p11(Y)))&(p10(Y)|p11(Y)))&(~p11(Y)|~p10(Y)))&(p9(Y)|p10(Y)))&(~p10(Y)|~p9(Y)))&(p8(Y)|p9(Y)))&(~p9(Y)|~p8(Y)))&(p7(Y)|p8(Y)))&(~p8(Y)|~p7(Y)))&(p6(Y)|p7(Y)))&(~p7(Y)|~p6(Y)))&(p5(Y)|p6(Y)))&(~p6(Y)|~p5(Y)))&(p4(Y)|p5(Y)))&(~p5(Y)|~p4(Y)))&(p3(Y)|p4(Y)))&(~p4(Y)|~p3(Y)))&(p2(Y)|p3(Y)))&(~p3(Y)|~p2(Y)))&(p1(Y)|p2(Y)))&(~p2(Y)|~p1(Y))))))))))),
% 0.14/0.40 inference(miniscoping,[status(thm)],[f9])).
% 0.14/0.40 fof(f11,plain,(
% 0.14/0.40 (((r1(sK0_skl,sK1_skl)&p15(sK1_skl))&(r1(sK1_skl,sK2_skl)&p1(sK2_skl)))&(r1(sK0_skl,sK3_skl)&(![X]: (~r1(sK3_skl,X)|(((((r1(X,sK4_skl(X))&((r1(sK4_skl(X),sK5_skl(X))&((r1(sK5_skl(X),sK6_skl(X))&((r1(sK6_skl(X),sK7_skl(X))&((r1(sK7_skl(X),sK8_skl(X))&((r1(sK8_skl(X),sK9_skl(X))&((r1(sK9_skl(X),sK10_skl(X))&((r1(sK10_skl(X),sK11_skl(X))&((r1(sK11_skl(X),sK12_skl(X))&((r1(sK12_skl(X),sK13_skl(X))&((r1(sK13_skl(X),sK14_skl(X))&((r1(sK14_skl(X),sK15_skl(X))&(r1(sK15_skl(X),sK16_skl(X))&$true))&(![Y]: (~r1(sK15_skl(X),Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y)))))))&(![X]: (~r1(sK14_skl(X),X)|((~p13(X)|p12(X))&(p13(X)|~p12(X)))))))&(![Y]: (~r1(sK13_skl(X),Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y)))))))&(![X]: (~r1(sK12_skl(X),X)|((~p11(X)|p10(X))&(p11(X)|~p10(X)))))))&(![Y]: (~r1(sK11_skl(X),Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y)))))))&(![X]: (~r1(sK10_skl(X),X)|((~p9(X)|p8(X))&(p9(X)|~p8(X)))))))&(![Y]: (~r1(sK9_skl(X),Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y)))))))&(![X]: (~r1(sK8_skl(X),X)|((~p7(X)|p6(X))&(p7(X)|~p6(X)))))))&(![Y]: (~r1(sK7_skl(X),Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y)))))))&(![X]: (~r1(sK6_skl(X),X)|((~p5(X)|p4(X))&(p5(X)|~p4(X)))))))&(![Y]: (~r1(sK5_skl(X),Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y)))))))&(![X]: (~r1(sK4_skl(X),X)|((~p3(X)|p2(X))&(p3(X)|~p2(X))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(r1(X,sK17_skl(X))&~p15(sK17_skl(X))))&((((((((((((((((((((((((((r1(X,sK18_skl(X))&(p13(sK18_skl(X))|p14(sK18_skl(X))))&(~p14(sK18_skl(X))|~p13(sK18_skl(X))))&(p12(sK18_skl(X))|p13(sK18_skl(X))))&(~p13(sK18_skl(X))|~p12(sK18_skl(X))))&(p11(sK18_skl(X))|p12(sK18_skl(X))))&(~p12(sK18_skl(X))|~p11(sK18_skl(X))))&(p10(sK18_skl(X))|p11(sK18_skl(X))))&(~p11(sK18_skl(X))|~p10(sK18_skl(X))))&(p9(sK18_skl(X))|p10(sK18_skl(X))))&(~p10(sK18_skl(X))|~p9(sK18_skl(X))))&(p8(sK18_skl(X))|p9(sK18_skl(X))))&(~p9(sK18_skl(X))|~p8(sK18_skl(X))))&(p7(sK18_skl(X))|p8(sK18_skl(X))))&(~p8(sK18_skl(X))|~p7(sK18_skl(X))))&(p6(sK18_skl(X))|p7(sK18_skl(X))))&(~p7(sK18_skl(X))|~p6(sK18_skl(X))))&(p5(sK18_skl(X))|p6(sK18_skl(X))))&(~p6(sK18_skl(X))|~p5(sK18_skl(X))))&(p4(sK18_skl(X))|p5(sK18_skl(X))))&(~p5(sK18_skl(X))|~p4(sK18_skl(X))))&(p3(sK18_skl(X))|p4(sK18_skl(X))))&(~p4(sK18_skl(X))|~p3(sK18_skl(X))))&(p2(sK18_skl(X))|p3(sK18_skl(X))))&(~p3(sK18_skl(X))|~p2(sK18_skl(X))))&(p1(sK18_skl(X))|p2(sK18_skl(X))))&(~p2(sK18_skl(X))|~p1(sK18_skl(X)))))))))),
% 0.14/0.40 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]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl),skolemize(X,sK2_skl),skolemize(Y,sK3_skl),skolemize(Y,sK4_skl(X)),skolemize(X,sK5_skl(X)),skolemize(Y,sK6_skl(X)),skolemize(X,sK7_skl(X)),skolemize(Y,sK8_skl(X)),skolemize(X,sK9_skl(X)),skolemize(Y,sK10_skl(X)),skolemize(X,sK11_skl(X)),skolemize(Y,sK12_skl(X)),skolemize(X,sK13_skl(X)),skolemize(Y,sK14_skl(X)),skolemize(X,sK15_skl(X)),skolemize(Y,sK16_skl(X)),skolemize(Y,sK17_skl(X)),skolemize(Y,sK18_skl(X))],[f10])).
% 0.14/0.40 fof(f12,plain,(
% 0.14/0.40 ?[X]: ((?[Y]: ((r1(sK0_skl,sK1_skl)&p15(sK1_skl))&(?[X]: (r1(sK1_skl,sK2_skl)&p1(sK2_skl)))))&(?[Y]: (r1(sK0_skl,sK3_skl)&(![X]: (~r1(sK3_skl,X)|((((?[Y]: ((r1(X,sK4_skl(X))&(?[X]: ((r1(sK4_skl(X),sK5_skl(X))&(?[Y]: ((r1(sK5_skl(X),sK6_skl(X))&(?[X]: ((r1(sK6_skl(X),sK7_skl(X))&(?[Y]: ((r1(sK7_skl(X),sK8_skl(X))&(?[X]: ((r1(sK8_skl(X),sK9_skl(X))&(?[Y]: ((r1(sK9_skl(X),sK10_skl(X))&(?[X]: ((r1(sK10_skl(X),sK11_skl(X))&(?[Y]: ((r1(sK11_skl(X),sK12_skl(X))&(?[X]: ((r1(sK12_skl(X),sK13_skl(X))&(?[Y]: ((r1(sK13_skl(X),sK14_skl(X))&(?[X]: ((r1(sK14_skl(X),sK15_skl(X))&(?[Y]: r1(sK15_skl(X),sK16_skl(X))))&(![Y]: (~r1(sK15_skl(X),Y)|((~p14(Y)|p13(Y))&(p14(Y)|~p13(Y))))))))&(![X]: (~r1(sK14_skl(X),X)|((~p13(X)|p12(X))&(p13(X)|~p12(X))))))))&(![Y]: (~r1(sK13_skl(X),Y)|((~p12(Y)|p11(Y))&(p12(Y)|~p11(Y))))))))&(![X]: (~r1(sK12_skl(X),X)|((~p11(X)|p10(X))&(p11(X)|~p10(X))))))))&(![Y]: (~r1(sK11_skl(X),Y)|((~p10(Y)|p9(Y))&(p10(Y)|~p9(Y))))))))&(![X]: (~r1(sK10_skl(X),X)|((~p9(X)|p8(X))&(p9(X)|~p8(X))))))))&(![Y]: (~r1(sK9_skl(X),Y)|((~p8(Y)|p7(Y))&(p8(Y)|~p7(Y))))))))&(![X]: (~r1(sK8_skl(X),X)|((~p7(X)|p6(X))&(p7(X)|~p6(X))))))))&(![Y]: (~r1(sK7_skl(X),Y)|((~p6(Y)|p5(Y))&(p6(Y)|~p5(Y))))))))&(![X]: (~r1(sK6_skl(X),X)|((~p5(X)|p4(X))&(p5(X)|~p4(X))))))))&(![Y]: (~r1(sK5_skl(X),Y)|((~p4(Y)|p3(Y))&(p4(Y)|~p3(Y))))))))&(![X]: (~r1(sK4_skl(X),X)|((~p3(X)|p2(X))&(p3(X)|~p2(X)))))))&(![Y]: (~r1(X,Y)|((~p2(Y)|p1(Y))&(p2(Y)|~p1(Y))))))&(?[Y]: (r1(X,sK17_skl(X))&~p15(sK17_skl(X)))))&(?[Y]: ((((((((((((((((((((((((((r1(X,sK18_skl(X))&(p13(sK18_skl(X))|p14(sK18_skl(X))))&(~p14(sK18_skl(X))|~p13(sK18_skl(X))))&(p12(sK18_skl(X))|p13(sK18_skl(X))))&(~p13(sK18_skl(X))|~p12(sK18_skl(X))))&(p11(sK18_skl(X))|p12(sK18_skl(X))))&(~p12(sK18_skl(X))|~p11(sK18_skl(X))))&(p10(sK18_skl(X))|p11(sK18_skl(X))))&(~p11(sK18_skl(X))|~p10(sK18_skl(X))))&(p9(sK18_skl(X))|p10(sK18_skl(X))))&(~p10(sK18_skl(X))|~p9(sK18_skl(X))))&(p8(sK18_skl(X))|p9(sK18_skl(X))))&(~p9(sK18_skl(X))|~p8(sK18_skl(X))))&(p7(sK18_skl(X))|p8(sK18_skl(X))))&(~p8(sK18_skl(X))|~p7(sK18_skl(X))))&(p6(sK18_skl(X))|p7(sK18_skl(X))))&(~p7(sK18_skl(X))|~p6(sK18_skl(X))))&(p5(sK18_skl(X))|p6(sK18_skl(X))))&(~p6(sK18_skl(X))|~p5(sK18_skl(X))))&(p4(sK18_skl(X))|p5(sK18_skl(X))))&(~p5(sK18_skl(X))|~p4(sK18_skl(X))))&(p3(sK18_skl(X))|p4(sK18_skl(X))))&(~p4(sK18_skl(X))|~p3(sK18_skl(X))))&(p2(sK18_skl(X))|p3(sK18_skl(X))))&(~p3(sK18_skl(X))|~p2(sK18_skl(X))))&(p1(sK18_skl(X))|p2(sK18_skl(X))))&(~p2(sK18_skl(X))|~p1(sK18_skl(X)))))))))))),
% 0.14/0.40 inference(true_and_false_simplification,[status(thm)],[f11])).
% 0.14/0.40 fof(f18,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK4_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f55,plain,(
% 0.14/0.40 ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|~p2(X1)|p1(X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f56,plain,(
% 0.14/0.40 ![X0,X1]: (~r1(sK3_skl,X0)|~r1(X0,X1)|p2(X1)|~p1(X1))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f59,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|r1(X0,sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f60,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p13(sK18_skl(X0))|p14(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f61,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p14(sK18_skl(X0))|~p13(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f62,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p12(sK18_skl(X0))|p13(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f63,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p13(sK18_skl(X0))|~p12(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f64,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p11(sK18_skl(X0))|p12(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f65,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p12(sK18_skl(X0))|~p11(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f66,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p10(sK18_skl(X0))|p11(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f68,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p9(sK18_skl(X0))|p10(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f69,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p10(sK18_skl(X0))|~p9(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f70,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p8(sK18_skl(X0))|p9(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f72,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p7(sK18_skl(X0))|p8(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f73,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p8(sK18_skl(X0))|~p7(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f74,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p6(sK18_skl(X0))|p7(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f76,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p5(sK18_skl(X0))|p6(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f77,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p6(sK18_skl(X0))|~p5(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f78,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p4(sK18_skl(X0))|p5(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f79,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p5(sK18_skl(X0))|~p4(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f80,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p3(sK18_skl(X0))|p4(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f81,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p4(sK18_skl(X0))|~p3(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f82,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p2(sK18_skl(X0))|p3(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f83,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p3(sK18_skl(X0))|~p2(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f84,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p1(sK18_skl(X0))|p2(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f85,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p2(sK18_skl(X0))|~p1(sK18_skl(X0)))),
% 0.14/0.40 inference(cnf_transformation,[status(thm)],[f12])).
% 0.14/0.40 fof(f90,plain,(
% 0.14/0.40 r1(sK3_skl,sK4_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f18,f5])).
% 0.14/0.40 fof(f109,plain,(
% 0.14/0.40 p13(sK18_skl(sK3_skl))|p14(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f60,f5])).
% 0.14/0.40 fof(f117,definition,(
% 0.14/0.40 sQ2_spl <=> (p13(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f118,plain,(
% 0.14/0.40 p13(sK18_skl(sK3_skl))|~sQ2_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f117])).
% 0.14/0.40 fof(f120,definition,(
% 0.14/0.40 sQ3_spl <=> (p14(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f123,plain,(
% 0.14/0.40 sQ2_spl|sQ3_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f109,f117,f120])).
% 0.14/0.40 fof(f125,plain,(
% 0.14/0.40 p12(sK18_skl(sK3_skl))|p13(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f62,f5])).
% 0.14/0.40 fof(f130,definition,(
% 0.14/0.40 sQ5_spl <=> (p12(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f131,plain,(
% 0.14/0.40 p12(sK18_skl(sK3_skl))|~sQ5_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f130])).
% 0.14/0.40 fof(f133,plain,(
% 0.14/0.40 sQ5_spl|sQ2_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f125,f130,f117])).
% 0.14/0.40 fof(f135,plain,(
% 0.14/0.40 p11(sK18_skl(sK3_skl))|p12(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f64,f5])).
% 0.14/0.40 fof(f140,definition,(
% 0.14/0.40 sQ7_spl <=> (p11(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f141,plain,(
% 0.14/0.40 p11(sK18_skl(sK3_skl))|~sQ7_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f140])).
% 0.14/0.40 fof(f143,plain,(
% 0.14/0.40 sQ7_spl|sQ5_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f135,f140,f130])).
% 0.14/0.40 fof(f145,plain,(
% 0.14/0.40 p10(sK18_skl(sK3_skl))|p11(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f66,f5])).
% 0.14/0.40 fof(f150,definition,(
% 0.14/0.40 sQ9_spl <=> (p10(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f153,plain,(
% 0.14/0.40 sQ9_spl|sQ7_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f145,f150,f140])).
% 0.14/0.40 fof(f155,plain,(
% 0.14/0.40 p9(sK18_skl(sK3_skl))|p10(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f68,f5])).
% 0.14/0.40 fof(f160,definition,(
% 0.14/0.40 sQ11_spl <=> (p9(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f161,plain,(
% 0.14/0.40 p9(sK18_skl(sK3_skl))|~sQ11_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f160])).
% 0.14/0.40 fof(f163,plain,(
% 0.14/0.40 sQ11_spl|sQ9_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f155,f160,f150])).
% 0.14/0.40 fof(f165,plain,(
% 0.14/0.40 p8(sK18_skl(sK3_skl))|p9(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f70,f5])).
% 0.14/0.40 fof(f170,definition,(
% 0.14/0.40 sQ13_spl <=> (p8(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f173,plain,(
% 0.14/0.40 sQ13_spl|sQ11_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f165,f170,f160])).
% 0.14/0.40 fof(f175,plain,(
% 0.14/0.40 p7(sK18_skl(sK3_skl))|p8(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f72,f5])).
% 0.14/0.40 fof(f180,definition,(
% 0.14/0.40 sQ15_spl <=> (p7(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f181,plain,(
% 0.14/0.40 p7(sK18_skl(sK3_skl))|~sQ15_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f180])).
% 0.14/0.40 fof(f183,plain,(
% 0.14/0.40 sQ15_spl|sQ13_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f175,f180,f170])).
% 0.14/0.40 fof(f185,plain,(
% 0.14/0.40 p6(sK18_skl(sK3_skl))|p7(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f74,f5])).
% 0.14/0.40 fof(f190,definition,(
% 0.14/0.40 sQ17_spl <=> (p6(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f193,plain,(
% 0.14/0.40 sQ17_spl|sQ15_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f185,f190,f180])).
% 0.14/0.40 fof(f195,plain,(
% 0.14/0.40 p5(sK18_skl(sK3_skl))|p6(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f76,f5])).
% 0.14/0.40 fof(f200,definition,(
% 0.14/0.40 sQ19_spl <=> (p5(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f201,plain,(
% 0.14/0.40 p5(sK18_skl(sK3_skl))|~sQ19_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f200])).
% 0.14/0.40 fof(f203,plain,(
% 0.14/0.40 sQ19_spl|sQ17_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f195,f200,f190])).
% 0.14/0.40 fof(f205,plain,(
% 0.14/0.40 p4(sK18_skl(sK3_skl))|p5(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f78,f5])).
% 0.14/0.40 fof(f210,definition,(
% 0.14/0.40 sQ21_spl <=> (p4(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f211,plain,(
% 0.14/0.40 p4(sK18_skl(sK3_skl))|~sQ21_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f210])).
% 0.14/0.40 fof(f213,plain,(
% 0.14/0.40 sQ21_spl|sQ19_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f205,f210,f200])).
% 0.14/0.40 fof(f215,plain,(
% 0.14/0.40 p3(sK18_skl(sK3_skl))|p4(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f80,f5])).
% 0.14/0.40 fof(f220,definition,(
% 0.14/0.40 sQ23_spl <=> (p3(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f221,plain,(
% 0.14/0.40 p3(sK18_skl(sK3_skl))|~sQ23_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f220])).
% 0.14/0.40 fof(f223,plain,(
% 0.14/0.40 sQ23_spl|sQ21_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f215,f220,f210])).
% 0.14/0.40 fof(f225,plain,(
% 0.14/0.40 p2(sK18_skl(sK3_skl))|p3(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f82,f5])).
% 0.14/0.40 fof(f230,definition,(
% 0.14/0.40 sQ25_spl <=> (p2(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f231,plain,(
% 0.14/0.40 p2(sK18_skl(sK3_skl))|~sQ25_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f230])).
% 0.14/0.40 fof(f233,plain,(
% 0.14/0.40 sQ25_spl|sQ23_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f225,f230,f220])).
% 0.14/0.40 fof(f235,plain,(
% 0.14/0.40 p1(sK18_skl(sK3_skl))|p2(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f84,f5])).
% 0.14/0.40 fof(f240,definition,(
% 0.14/0.40 sQ27_spl <=> (p1(sK18_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f243,plain,(
% 0.14/0.40 sQ27_spl|sQ25_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f235,f240,f230])).
% 0.14/0.40 fof(f279,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|~p2(X0)|p1(X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f55,f5])).
% 0.14/0.40 fof(f281,plain,(
% 0.14/0.40 ![X0]: (~r1(sK3_skl,X0)|p2(X0)|~p1(X0))),
% 0.14/0.40 inference(resolution,[status(thm)],[f56,f5])).
% 0.14/0.40 fof(f285,plain,(
% 0.14/0.40 r1(sK3_skl,sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f59,f5])).
% 0.14/0.40 fof(f287,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p14(sK18_skl(sK3_skl))|~sQ2_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f61,f118])).
% 0.14/0.40 fof(f288,definition,(
% 0.14/0.40 sQ28_spl <=> (r1(sK3_skl,sK4_skl(sK3_skl)))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f290,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK4_skl(sK3_skl))|sQ28_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f288])).
% 0.14/0.40 fof(f292,definition,(
% 0.14/0.40 sQ29_spl <=> (r1(sK3_skl,sK3_skl))),
% 0.14/0.40 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/0.40 fof(f294,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|sQ29_spl),
% 0.14/0.40 inference(component_clause,[status(thm)],[f292])).
% 0.14/0.40 fof(f295,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ3_spl|~sQ2_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f287,f292,f120,f117])).
% 0.14/0.40 fof(f296,plain,(
% 0.14/0.40 $false|sQ29_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f294,f5])).
% 0.14/0.40 fof(f297,plain,(
% 0.14/0.40 sQ29_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f296])).
% 0.14/0.40 fof(f298,plain,(
% 0.14/0.40 $false|sQ28_spl),
% 0.14/0.40 inference(forward_subsumption_resolution,[status(thm)],[f290,f90])).
% 0.14/0.40 fof(f299,plain,(
% 0.14/0.40 sQ28_spl),
% 0.14/0.40 inference(contradiction_clause,[status(thm)],[f298])).
% 0.14/0.40 fof(f301,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p13(sK18_skl(sK3_skl))|~sQ5_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f63,f131])).
% 0.14/0.40 fof(f303,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ2_spl|~sQ5_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f301,f292,f117,f130])).
% 0.14/0.40 fof(f305,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p10(sK18_skl(sK3_skl))|~sQ11_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f69,f161])).
% 0.14/0.40 fof(f307,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ9_spl|~sQ11_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f305,f292,f150,f160])).
% 0.14/0.40 fof(f309,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p8(sK18_skl(sK3_skl))|~sQ15_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f73,f181])).
% 0.14/0.40 fof(f311,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ13_spl|~sQ15_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f309,f292,f170,f180])).
% 0.14/0.40 fof(f312,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p12(sK18_skl(sK3_skl))|~sQ7_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f141,f65])).
% 0.14/0.40 fof(f313,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ5_spl|~sQ7_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f312,f292,f130,f140])).
% 0.14/0.40 fof(f314,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p6(sK18_skl(sK3_skl))|~sQ19_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f77,f201])).
% 0.14/0.40 fof(f315,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ17_spl|~sQ19_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f314,f292,f190,f200])).
% 0.14/0.40 fof(f316,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p4(sK18_skl(sK3_skl))|~sQ23_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f81,f221])).
% 0.14/0.40 fof(f317,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ21_spl|~sQ23_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f316,f292,f210,f220])).
% 0.14/0.40 fof(f318,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p3(sK18_skl(sK3_skl))|~sQ25_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f83,f231])).
% 0.14/0.40 fof(f319,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ23_spl|~sQ25_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f318,f292,f220,f230])).
% 0.14/0.40 fof(f626,plain,(
% 0.14/0.40 p2(sK18_skl(sK3_skl))|~p1(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f285,f281])).
% 0.14/0.40 fof(f627,plain,(
% 0.14/0.40 ~p2(sK18_skl(sK3_skl))|p1(sK18_skl(sK3_skl))),
% 0.14/0.40 inference(resolution,[status(thm)],[f285,f279])).
% 0.14/0.40 fof(f660,plain,(
% 0.14/0.40 sQ25_spl|~sQ27_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f626,f230,f240])).
% 0.14/0.40 fof(f661,plain,(
% 0.14/0.40 ~sQ25_spl|sQ27_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f627,f230,f240])).
% 0.14/0.40 fof(f717,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p5(sK18_skl(sK3_skl))|~sQ21_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f211,f79])).
% 0.14/0.40 fof(f718,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ19_spl|~sQ21_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f717,f292,f200,f210])).
% 0.14/0.40 fof(f719,plain,(
% 0.14/0.40 ~r1(sK3_skl,sK3_skl)|~p1(sK18_skl(sK3_skl))|~sQ25_spl),
% 0.14/0.40 inference(resolution,[status(thm)],[f231,f85])).
% 0.14/0.40 fof(f721,plain,(
% 0.14/0.40 ~sQ29_spl|~sQ27_spl|~sQ25_spl),
% 0.14/0.40 inference(split_clause,[status(thm)],[f719,f292,f240,f230])).
% 0.14/0.40 fof(f723,plain,(
% 0.14/0.40 $false),
% 0.14/0.40 inference(sat_refutation,[status(thm)],[f123,f133,f143,f153,f163,f173,f183,f193,f203,f213,f223,f233,f243,f295,f297,f299,f303,f307,f311,f313,f315,f317,f319,f660,f661,f718,f721])).
% 0.14/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.42 % Elapsed time: 0.051559 seconds
% 0.14/0.42 % CPU time: 0.165324 seconds
% 0.14/0.42 % Total memory used: 21.375 MB
% 0.14/0.42 % Net memory used: 21.261 MB
%------------------------------------------------------------------------------