%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL640+1.001 : 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:25 PM UTC 2026
% Result : Theorem 34.36s 4.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL640+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n002.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 00:45:01 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 % Drodi V4.1.1
% 34.36/4.84 % Refutation found
% 34.36/4.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 34.36/4.84 % SZS output start CNFRefutation for theBenchmark
% 34.36/4.84 fof(f1,conjecture,(
% 34.36/4.84 ~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| ( ( (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ~ p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ~ p1(X) ))| ~ ( (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) ) )) ))& ( p1(Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )) ))& (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& ( (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y)| ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ~ p1(X) ) )) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )) )) ) ))| ~ ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )) )) )) )),
% 34.36/4.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 34.36/4.84 fof(f2,negated_conjecture,(
% 34.36/4.84 ~(~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| ( ( (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ~ p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ~ p1(X) ))| ~ ( (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) ) )) ))& ( p1(Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )) ))& (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& ( (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y)| ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ))| ~ p1(X) ) )) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )) )) ) ))| ~ ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| p1(X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p1(X) ))| ~ p1(Y) ) )) )) )) ))),
% 34.36/4.84 inference(negated_conjecture,[status(cth)],[f1])).
% 34.36/4.84 fof(f3,plain,(
% 34.36/4.84 ?[X]: ((![Y]: (~r1(X,Y)|(((((((![X]: (~r1(Y,X)|p1(X)))|~p1(Y))|(![X]: (~r1(Y,X)|(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&p1(Y))))))|(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))&p1(X))&(![Y]: ((~r1(X,Y)|(![X]: ((~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y))))|~p1(X))))|((?[X]: (r1(Y,X)&~p1(X)))&p1(Y)))))))&((p1(Y)|(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p1(Y))))))|(?[X]: ((r1(Y,X)&~p1(X))&(![Y]: ((~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y)))))))&(![X]: ((~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))))|(?[Y]: (r1(X,Y)&~p1(Y))))))&((![X]: (~r1(Y,X)|(![Y]: ((~r1(X,Y)|p1(Y))|(?[X]: ((r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))&p1(X)))))))|(?[X]: ((r1(Y,X)&~p1(X))&(![Y]: ((~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y)))))))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(![X]: ((~r1(Y,X)|p1(X))|(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&p1(Y))))))))),
% 34.36/4.84 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 34.36/4.84 fof(f4,definition,(
% 34.36/4.84 ![X,Y]: (sP0_prd(Y,X)<=>((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&p1(Y)))),
% 34.36/4.84 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 34.36/4.84 fof(f5,definition,(
% 34.36/4.84 ![X,Y]: (sP1_prd(Y,X)<=>(r1(X,Y)&~p1(Y)))),
% 34.36/4.84 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 34.36/4.84 fof(f6,definition,(
% 34.36/4.84 ![Y,X]: (sP2_prd(X,Y)<=>((r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))&p1(X)))),
% 34.36/4.84 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 34.36/4.84 fof(f7,plain,(
% 34.36/4.84 ?[X]: ((![Y]: (~r1(X,Y)|(((((((![X]: (~r1(Y,X)|p1(X)))|~p1(Y))|(![X]: (~r1(Y,X)|(?[Y]: sP0_prd(Y,X)))))|(?[X]: (((r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))&p1(X))&(![Y]: ((~r1(X,Y)|(![X]: ((~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y))))|~p1(X))))|((?[X]: (r1(Y,X)&~p1(X)))&p1(Y)))))))&((p1(Y)|(![X]: (~r1(Y,X)|(?[Y]: sP1_prd(Y,X)))))|(?[X]: ((r1(Y,X)&~p1(X))&(![Y]: ((~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y)))))))&(![X]: ((~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))))|(?[Y]: (r1(X,Y)&~p1(Y))))))&((![X]: (~r1(Y,X)|(![Y]: ((~r1(X,Y)|p1(Y))|(?[X]: sP2_prd(X,Y))))))|(?[X]: ((r1(Y,X)&~p1(X))&(![Y]: ((~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y)))))))))&(?[Y]: (((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(![X]: ((~r1(Y,X)|p1(X))|(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&p1(Y))))))))),
% 34.36/4.84 inference(formula_renaming,[status(thm)],[f3,f6,f5,f4])).
% 34.36/4.84 fof(f8,plain,(
% 34.36/4.84 ((![Y]: (~r1(sK0_skl,Y)|(((((((![X]: (~r1(Y,X)|p1(X)))|~p1(Y))|(![X]: (~r1(Y,X)|sP0_prd(sK1_skl(X,Y),X))))|(((r1(Y,sK2_skl(Y))&(r1(sK2_skl(Y),sK3_skl(Y))&~p1(sK3_skl(Y))))&p1(sK2_skl(Y)))&(![Y]: ((~r1(sK2_skl(Y),Y)|(![X]: ((~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y))))|~p1(X))))|((r1(Y,sK4_skl(Y,Y))&~p1(sK4_skl(Y,Y)))&p1(Y))))))&((p1(Y)|(![X]: (~r1(Y,X)|sP1_prd(sK5_skl(X,Y),X))))|((r1(Y,sK6_skl(Y))&~p1(sK6_skl(Y)))&(![Y]: ((~r1(sK6_skl(Y),Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y))))))&(![X]: ((~r1(Y,X)|(![Y]: (~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))))|(r1(X,sK7_skl(X,Y))&~p1(sK7_skl(X,Y))))))&((![X]: (~r1(Y,X)|(![Y]: ((~r1(X,Y)|p1(Y))|sP2_prd(sK8_skl(Y,X,Y),Y)))))|((r1(Y,sK9_skl(Y))&~p1(sK9_skl(Y)))&(![Y]: ((~r1(sK9_skl(Y),Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y))))))))&(((r1(sK0_skl,sK10_skl)&(r1(sK10_skl,sK11_skl)&~p1(sK11_skl)))&(r1(sK10_skl,sK12_skl)&(![Y]: (~r1(sK12_skl,Y)|p1(Y)))))&(![X]: ((~r1(sK10_skl,X)|p1(X))|((r1(X,sK13_skl(X))&(r1(sK13_skl(X),sK14_skl(X))&~p1(sK14_skl(X))))&p1(sK13_skl(X)))))))),
% 34.36/4.84 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]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y)),skolemize(X,sK2_skl(Y)),skolemize(Y,sK3_skl(Y)),skolemize(X,sK4_skl(Y,Y)),skolemize(Y,sK5_skl(X,Y)),skolemize(X,sK6_skl(Y)),skolemize(Y,sK7_skl(X,Y)),skolemize(X,sK8_skl(Y,X,Y)),skolemize(X,sK9_skl(Y)),skolemize(Y,sK10_skl),skolemize(X,sK11_skl),skolemize(X,sK12_skl),skolemize(Y,sK13_skl(X)),skolemize(X,sK14_skl(X))],[f7])).
% 34.36/4.84 fof(f9,plain,(
% 34.36/4.84 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|p1(X1)|~p1(X0)|~r1(X0,X2)|sP0_prd(sK1_skl(X2,X0),X2)|r1(X0,sK2_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f10,plain,(
% 34.36/4.84 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|p1(X1)|~p1(X0)|~r1(X0,X2)|sP0_prd(sK1_skl(X2,X0),X2)|r1(sK2_skl(X0),sK3_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f11,plain,(
% 34.36/4.84 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|p1(X1)|~p1(X0)|~r1(X0,X2)|sP0_prd(sK1_skl(X2,X0),X2)|~p1(sK3_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f15,plain,(
% 34.36/4.84 ![X0,X1,X2,X3,X4,X5]: (~r1(sK0_skl,X0)|~r1(X0,X1)|p1(X1)|~p1(X0)|~r1(X0,X2)|sP0_prd(sK1_skl(X2,X0),X2)|~r1(sK2_skl(X0),X3)|~r1(X3,X4)|~r1(X4,X5)|p1(X5)|~p1(X4)|p1(X3))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f16,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK0_skl,X0)|p1(X0)|~r1(X0,X1)|sP1_prd(sK5_skl(X1,X0),X1)|r1(X0,sK6_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f17,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK0_skl,X0)|p1(X0)|~r1(X0,X1)|sP1_prd(sK5_skl(X1,X0),X1)|~p1(sK6_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f18,plain,(
% 34.36/4.84 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|p1(X0)|~r1(X0,X1)|sP1_prd(sK5_skl(X1,X0),X1)|~r1(sK6_skl(X0),X2)|~r1(X2,X3)|p1(X3)|~p1(X2))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f19,plain,(
% 34.36/4.84 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p1(X3)|r1(X1,sK7_skl(X1,X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f20,plain,(
% 34.36/4.84 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|~r1(X2,X3)|p1(X3)|~p1(sK7_skl(X1,X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f21,plain,(
% 34.36/4.84 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p1(X2)|sP2_prd(sK8_skl(X2,X1,X0),X2)|r1(X0,sK9_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f22,plain,(
% 34.36/4.84 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p1(X2)|sP2_prd(sK8_skl(X2,X1,X0),X2)|~p1(sK9_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f23,plain,(
% 34.36/4.84 ![X0,X1,X2,X3,X4]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p1(X2)|sP2_prd(sK8_skl(X2,X1,X0),X2)|~r1(sK9_skl(X0),X3)|~r1(X3,X4)|p1(X4)|~p1(X3))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f24,plain,(
% 34.36/4.84 r1(sK0_skl,sK10_skl)),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f25,plain,(
% 34.36/4.84 r1(sK10_skl,sK11_skl)),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f26,plain,(
% 34.36/4.84 ~p1(sK11_skl)),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f27,plain,(
% 34.36/4.84 r1(sK10_skl,sK12_skl)),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f28,plain,(
% 34.36/4.84 ![X0]: (~r1(sK12_skl,X0)|p1(X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f29,plain,(
% 34.36/4.84 ![X0]: (~r1(sK10_skl,X0)|p1(X0)|r1(X0,sK13_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f30,plain,(
% 34.36/4.84 ![X0]: (~r1(sK10_skl,X0)|p1(X0)|r1(sK13_skl(X0),sK14_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f31,plain,(
% 34.36/4.84 ![X0]: (~r1(sK10_skl,X0)|p1(X0)|~p1(sK14_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f32,plain,(
% 34.36/4.84 ![X0]: (~r1(sK10_skl,X0)|p1(X0)|p1(sK13_skl(X0)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f8])).
% 34.36/4.84 fof(f33,plain,(
% 34.36/4.84 ![X,Y]: ((~sP0_prd(Y,X)|((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&p1(Y)))&(sP0_prd(Y,X)|((~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y))))),
% 34.36/4.84 inference(NNF_transformation,[status(thm)],[f4])).
% 34.36/4.84 fof(f34,plain,(
% 34.36/4.84 (![X,Y]: (~sP0_prd(Y,X)|((r1(X,Y)&(?[X]: (r1(Y,X)&~p1(X))))&p1(Y))))&(![X,Y]: (sP0_prd(Y,X)|((~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y))))),
% 34.36/4.84 inference(miniscoping,[status(thm)],[f33])).
% 34.36/4.84 fof(f35,plain,(
% 34.36/4.84 (![X,Y]: (~sP0_prd(Y,X)|((r1(X,Y)&(r1(Y,sK15_skl(Y,X))&~p1(sK15_skl(Y,X))))&p1(Y))))&(![X,Y]: (sP0_prd(Y,X)|((~r1(X,Y)|(![X]: (~r1(Y,X)|p1(X))))|~p1(Y))))),
% 34.36/4.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl]),skolemize(X,sK15_skl(Y,X))],[f34])).
% 34.36/4.84 fof(f36,plain,(
% 34.36/4.84 ![X0,X1]: (~sP0_prd(X0,X1)|r1(X1,X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f35])).
% 34.36/4.84 fof(f37,plain,(
% 34.36/4.84 ![X0,X1]: (~sP0_prd(X0,X1)|r1(X0,sK15_skl(X0,X1)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f35])).
% 34.36/4.84 fof(f38,plain,(
% 34.36/4.84 ![X0,X1]: (~sP0_prd(X0,X1)|~p1(sK15_skl(X0,X1)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f35])).
% 34.36/4.84 fof(f39,plain,(
% 34.36/4.84 ![X0,X1]: (~sP0_prd(X0,X1)|p1(X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f35])).
% 34.36/4.84 fof(f41,plain,(
% 34.36/4.84 ![X,Y]: ((~sP1_prd(Y,X)|(r1(X,Y)&~p1(Y)))&(sP1_prd(Y,X)|(~r1(X,Y)|p1(Y))))),
% 34.36/4.84 inference(NNF_transformation,[status(thm)],[f5])).
% 34.36/4.84 fof(f42,plain,(
% 34.36/4.84 (![X,Y]: (~sP1_prd(Y,X)|(r1(X,Y)&~p1(Y))))&(![X,Y]: (sP1_prd(Y,X)|(~r1(X,Y)|p1(Y))))),
% 34.36/4.84 inference(miniscoping,[status(thm)],[f41])).
% 34.36/4.84 fof(f43,plain,(
% 34.36/4.84 ![X0,X1]: (~sP1_prd(X0,X1)|r1(X1,X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f42])).
% 34.36/4.84 fof(f44,plain,(
% 34.36/4.84 ![X0,X1]: (~sP1_prd(X0,X1)|~p1(X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f42])).
% 34.36/4.84 fof(f46,plain,(
% 34.36/4.84 ![Y,X]: ((~sP2_prd(X,Y)|((r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))&p1(X)))&(sP2_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y))))|~p1(X))))),
% 34.36/4.84 inference(NNF_transformation,[status(thm)],[f6])).
% 34.36/4.84 fof(f47,plain,(
% 34.36/4.84 (![Y,X]: (~sP2_prd(X,Y)|((r1(Y,X)&(?[Y]: (r1(X,Y)&~p1(Y))))&p1(X))))&(![Y,X]: (sP2_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y))))|~p1(X))))),
% 34.36/4.84 inference(miniscoping,[status(thm)],[f46])).
% 34.36/4.84 fof(f48,plain,(
% 34.36/4.84 (![Y,X]: (~sP2_prd(X,Y)|((r1(Y,X)&(r1(X,sK16_skl(X,Y))&~p1(sK16_skl(X,Y))))&p1(X))))&(![Y,X]: (sP2_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y))))|~p1(X))))),
% 34.36/4.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(Y,sK16_skl(X,Y))],[f47])).
% 34.36/4.84 fof(f49,plain,(
% 34.36/4.84 ![X0,X1]: (~sP2_prd(X0,X1)|r1(X1,X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f48])).
% 34.36/4.84 fof(f50,plain,(
% 34.36/4.84 ![X0,X1]: (~sP2_prd(X0,X1)|r1(X0,sK16_skl(X0,X1)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f48])).
% 34.36/4.84 fof(f51,plain,(
% 34.36/4.84 ![X0,X1]: (~sP2_prd(X0,X1)|~p1(sK16_skl(X0,X1)))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f48])).
% 34.36/4.84 fof(f52,plain,(
% 34.36/4.84 ![X0,X1]: (~sP2_prd(X0,X1)|p1(X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f48])).
% 34.36/4.84 fof(f53,plain,(
% 34.36/4.84 ![X0,X1,X2]: (sP2_prd(X0,X1)|~r1(X1,X0)|~r1(X0,X2)|p1(X2)|~p1(X0))),
% 34.36/4.84 inference(cnf_transformation,[status(thm)],[f48])).
% 34.36/4.84 fof(f54,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK10_skl,X0)|p1(X0)|~p1(sK10_skl)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f24,f10])).
% 34.36/4.84 fof(f55,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK10_skl,X0)|p1(X0)|~p1(sK10_skl)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|r1(sK10_skl,sK2_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f24,f9])).
% 34.36/4.84 fof(f58,plain,(
% 34.36/4.84 ![X0,X1,X2,X3,X4]: (~r1(sK10_skl,X0)|p1(X0)|~p1(sK10_skl)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK2_skl(sK10_skl),X2)|~r1(X2,X3)|~r1(X3,X4)|p1(X4)|~p1(X3)|p1(X2))),
% 34.36/4.84 inference(resolution,[status(thm)],[f15,f24])).
% 34.36/4.84 fof(f59,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0)|r1(sK10_skl,sK6_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f16,f24])).
% 34.36/4.84 fof(f60,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK10_skl)|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0)|~r1(sK6_skl(sK10_skl),X1)|~r1(X1,X2)|p1(X2)|~p1(X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f18,f24])).
% 34.36/4.84 fof(f61,plain,(
% 34.36/4.84 ![X0,X1,X2]: (~r1(sK10_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p1(X2)|r1(X0,sK7_skl(X0,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f19,f24])).
% 34.36/4.84 fof(f62,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1)|r1(sK10_skl,sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f21,f24])).
% 34.36/4.84 fof(f63,plain,(
% 34.36/4.84 ![X0,X1,X2,X3]: (~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1)|~r1(sK9_skl(sK10_skl),X2)|~r1(X2,X3)|p1(X3)|~p1(X2))),
% 34.36/4.84 inference(resolution,[status(thm)],[f23,f24])).
% 34.36/4.84 fof(f93,plain,(
% 34.36/4.84 ![X0]: (p1(sK11_skl)|~p1(sK10_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f54,f25])).
% 34.36/4.84 fof(f94,plain,(
% 34.36/4.84 ![X0]: (~p1(sK10_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f93,f26])).
% 34.36/4.84 fof(f96,plain,(
% 34.36/4.84 ![X0]: (p1(sK11_skl)|~p1(sK10_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|r1(sK10_skl,sK2_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f55,f25])).
% 34.36/4.84 fof(f97,plain,(
% 34.36/4.84 ![X0]: (~p1(sK10_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|r1(sK10_skl,sK2_skl(sK10_skl)))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f96,f26])).
% 34.36/4.84 fof(f104,plain,(
% 34.36/4.84 p1(sK10_skl)|sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK10_skl,sK6_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f59,f27])).
% 34.36/4.84 fof(f106,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1)|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f61,f27])).
% 34.36/4.84 fof(f131,plain,(
% 34.36/4.84 ~p1(sK10_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f94,f27])).
% 34.36/4.84 fof(f138,plain,(
% 34.36/4.84 ~p1(sK10_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK10_skl,sK2_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f97,f27])).
% 34.36/4.84 fof(f148,plain,(
% 34.36/4.84 p1(sK10_skl)|r1(sK10_skl,sK6_skl(sK10_skl))|r1(sK12_skl,sK5_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f104,f43])).
% 34.36/4.84 fof(f182,plain,(
% 34.36/4.84 p1(sK10_skl)|r1(sK10_skl,sK6_skl(sK10_skl))|p1(sK5_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f148,f28])).
% 34.36/4.84 fof(f191,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|r1(sK10_skl,sK6_skl(sK10_skl))|~sP1_prd(sK5_skl(sK12_skl,sK10_skl),X0))),
% 34.36/4.84 inference(resolution,[status(thm)],[f182,f44])).
% 34.36/4.84 fof(f251,plain,(
% 34.36/4.84 p1(sK10_skl)|r1(sK10_skl,sK6_skl(sK10_skl))),
% 34.36/4.84 inference(backward_subsumption_resolution,[status(thm)],[f104,f191])).
% 34.36/4.84 fof(f257,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK13_skl(sK6_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f251,f32])).
% 34.36/4.84 fof(f258,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|r1(sK13_skl(sK6_skl(sK10_skl)),sK14_skl(sK6_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f251,f30])).
% 34.36/4.84 fof(f259,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|r1(sK6_skl(sK10_skl),sK13_skl(sK6_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f251,f29])).
% 34.36/4.84 fof(f269,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK10_skl)|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0)|~r1(sK13_skl(sK6_skl(sK10_skl)),X1)|p1(X1)|~p1(sK13_skl(sK6_skl(sK10_skl))))),
% 34.36/4.84 inference(resolution,[status(thm)],[f259,f60])).
% 34.36/4.84 fof(f275,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK10_skl)|p1(sK6_skl(sK10_skl))|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0)|~r1(sK13_skl(sK6_skl(sK10_skl)),X1)|p1(X1)|~p1(sK13_skl(sK6_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f269])).
% 34.36/4.84 fof(f276,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK10_skl)|p1(sK6_skl(sK10_skl))|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0)|~r1(sK13_skl(sK6_skl(sK10_skl)),X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f275,f257])).
% 34.36/4.84 fof(f285,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|p1(sK6_skl(sK10_skl))|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0)|p1(sK14_skl(sK6_skl(sK10_skl)))|p1(sK10_skl)|p1(sK6_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f276,f258])).
% 34.36/4.84 fof(f286,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|p1(sK6_skl(sK10_skl))|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0)|p1(sK14_skl(sK6_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f285])).
% 34.36/4.84 fof(f309,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK14_skl(sK6_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f286,f27])).
% 34.36/4.84 fof(f312,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK14_skl(sK6_skl(sK10_skl)))|r1(sK12_skl,sK5_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f309,f43])).
% 34.36/4.84 fof(f336,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK14_skl(sK6_skl(sK10_skl)))|p1(sK5_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f312,f28])).
% 34.36/4.84 fof(f340,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK5_skl(sK12_skl,sK10_skl))|~r1(sK10_skl,sK6_skl(sK10_skl))|p1(sK6_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f336,f31])).
% 34.36/4.84 fof(f342,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK5_skl(sK12_skl,sK10_skl))|~r1(sK10_skl,sK6_skl(sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f340])).
% 34.36/4.84 fof(f343,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK5_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f342,f251])).
% 34.36/4.84 fof(f359,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|p1(sK6_skl(sK10_skl))|~sP1_prd(sK5_skl(sK12_skl,sK10_skl),X0))),
% 34.36/4.84 inference(resolution,[status(thm)],[f343,f44])).
% 34.36/4.84 fof(f365,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|p1(sK14_skl(sK6_skl(sK10_skl)))),
% 34.36/4.84 inference(backward_subsumption_resolution,[status(thm)],[f309,f359])).
% 34.36/4.84 fof(f368,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|~r1(sK10_skl,sK6_skl(sK10_skl))|p1(sK6_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f365,f31])).
% 34.36/4.84 fof(f370,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))|~r1(sK10_skl,sK6_skl(sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f368])).
% 34.36/4.84 fof(f371,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK6_skl(sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f370,f251])).
% 34.36/4.84 fof(f375,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|~r1(sK0_skl,sK10_skl)|p1(sK10_skl)|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0))),
% 34.36/4.84 inference(resolution,[status(thm)],[f371,f17])).
% 34.36/4.84 fof(f377,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f375])).
% 34.36/4.84 fof(f378,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|~r1(sK10_skl,X0)|sP1_prd(sK5_skl(X0,sK10_skl),X0))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f377,f24])).
% 34.36/4.84 fof(f383,plain,(
% 34.36/4.84 p1(sK10_skl)|sP1_prd(sK5_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f378,f27])).
% 34.36/4.84 fof(f386,plain,(
% 34.36/4.84 p1(sK10_skl)|r1(sK12_skl,sK5_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f383,f43])).
% 34.36/4.84 fof(f389,plain,(
% 34.36/4.84 p1(sK10_skl)|p1(sK5_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f386,f28])).
% 34.36/4.84 fof(f393,plain,(
% 34.36/4.84 ![X0]: (p1(sK10_skl)|~sP1_prd(sK5_skl(sK12_skl,sK10_skl),X0))),
% 34.36/4.84 inference(resolution,[status(thm)],[f389,f44])).
% 34.36/4.84 fof(f419,plain,(
% 34.36/4.84 p1(sK10_skl)),
% 34.36/4.84 inference(backward_subsumption_resolution,[status(thm)],[f383,f393])).
% 34.36/4.84 fof(f424,plain,(
% 34.36/4.84 sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK10_skl,sK2_skl(sK10_skl))),
% 34.36/4.84 inference(backward_subsumption_resolution,[status(thm)],[f138,f419])).
% 34.36/4.84 fof(f426,plain,(
% 34.36/4.84 sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK2_skl(sK10_skl),sK3_skl(sK10_skl))),
% 34.36/4.84 inference(backward_subsumption_resolution,[status(thm)],[f131,f419])).
% 34.36/4.84 fof(f431,plain,(
% 34.36/4.84 ![X0,X1,X2,X3,X4]: (~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK2_skl(sK10_skl),X2)|~r1(X2,X3)|~r1(X3,X4)|p1(X4)|~p1(X3)|p1(X2))),
% 34.36/4.84 inference(backward_subsumption_resolution,[status(thm)],[f58,f419])).
% 34.36/4.84 fof(f471,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f424,f37])).
% 34.36/4.84 fof(f472,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f424,f36])).
% 34.36/4.84 fof(f473,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|p1(sK1_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f424,f39])).
% 34.36/4.84 fof(f480,plain,(
% 34.36/4.84 ![X0,X1,X2,X3]: (sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK3_skl(sK10_skl),X2)|~r1(X2,X3)|p1(X3)|~p1(X2)|p1(sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f426,f431])).
% 34.36/4.84 fof(f557,plain,(
% 34.36/4.84 ![X0]: (r1(sK10_skl,sK2_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f472,f106])).
% 34.36/4.84 fof(f559,plain,(
% 34.36/4.84 ![X0]: (r1(sK10_skl,sK2_skl(sK10_skl))|sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|~p1(sK1_skl(sK12_skl,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f472,f53])).
% 34.36/4.84 fof(f562,plain,(
% 34.36/4.84 ![X0]: (r1(sK10_skl,sK2_skl(sK10_skl))|sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f559,f473])).
% 34.36/4.84 fof(f703,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|r1(sK10_skl,sK2_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f557,f471])).
% 34.36/4.84 fof(f704,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f703])).
% 34.36/4.84 fof(f714,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK10_skl,sK2_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f562,f471])).
% 34.36/4.84 fof(f715,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f714])).
% 34.36/4.84 fof(f756,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f715,f38])).
% 34.36/4.84 fof(f758,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f756,f424])).
% 34.36/4.84 fof(f766,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|r1(sK1_skl(sK12_skl,sK10_skl),sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f758,f50])).
% 34.36/4.84 fof(f823,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f704,f38])).
% 34.36/4.84 fof(f825,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f823,f424])).
% 34.36/4.84 fof(f827,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|p1(sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f825,f28])).
% 34.36/4.84 fof(f831,plain,(
% 34.36/4.84 ![X0,X1]: (r1(sK10_skl,sK2_skl(sK10_skl))|~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f827,f20])).
% 34.36/4.84 fof(f833,plain,(
% 34.36/4.84 ![X0,X1]: (r1(sK10_skl,sK2_skl(sK10_skl))|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f831,f24])).
% 34.36/4.84 fof(f846,plain,(
% 34.36/4.84 ![X0,X1]: (r1(sK10_skl,sK2_skl(sK10_skl))|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f833,f27])).
% 34.36/4.84 fof(f848,plain,(
% 34.36/4.84 ![X0]: (r1(sK10_skl,sK2_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|r1(sK10_skl,sK2_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f846,f472])).
% 34.36/4.84 fof(f850,plain,(
% 34.36/4.84 ![X0]: (r1(sK10_skl,sK2_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f848])).
% 34.36/4.84 fof(f854,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK10_skl,sK2_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f850,f766])).
% 34.36/4.84 fof(f856,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|p1(sK16_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f854])).
% 34.36/4.84 fof(f864,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))|~sP2_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f856,f51])).
% 34.36/4.84 fof(f866,plain,(
% 34.36/4.84 r1(sK10_skl,sK2_skl(sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f864,f758])).
% 34.36/4.84 fof(f868,plain,(
% 34.36/4.84 ![X0]: (~r1(sK2_skl(sK10_skl),X0)|p1(X0)|sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0)|r1(sK10_skl,sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f866,f62])).
% 34.36/4.84 fof(f1018,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f868,f426])).
% 34.36/4.84 fof(f1177,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1018,f50])).
% 34.36/4.84 fof(f1178,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK3_skl(sK10_skl),sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1018,f49])).
% 34.36/4.84 fof(f1179,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1018,f52])).
% 34.36/4.84 fof(f1271,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2)|~p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))|p1(sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1178,f480])).
% 34.36/4.84 fof(f1281,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2)|~p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl)))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1271])).
% 34.36/4.84 fof(f1282,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1281,f1179])).
% 34.36/4.84 fof(f1365,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))|p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1282,f1177])).
% 34.36/4.84 fof(f1367,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1365])).
% 34.36/4.84 fof(f1442,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK11_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1367,f25])).
% 34.36/4.84 fof(f1443,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1442,f26])).
% 34.36/4.84 fof(f1500,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1443,f27])).
% 34.36/4.84 fof(f1502,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1500])).
% 34.36/4.84 fof(f1538,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1502,f51])).
% 34.36/4.84 fof(f1540,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1538,f1018])).
% 34.36/4.84 fof(f1541,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1540,f37])).
% 34.36/4.84 fof(f1542,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1540,f36])).
% 34.36/4.84 fof(f1545,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1542,f106])).
% 34.36/4.84 fof(f1581,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1545,f1541])).
% 34.36/4.84 fof(f1582,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1581])).
% 34.36/4.84 fof(f1589,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f1582,f38])).
% 34.36/4.84 fof(f1591,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1589,f1540])).
% 34.36/4.84 fof(f1593,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|p1(sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1591,f28])).
% 34.36/4.84 fof(f1597,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1593,f20])).
% 34.36/4.84 fof(f1599,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1597,f24])).
% 34.36/4.84 fof(f1600,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1599,f27])).
% 34.36/4.84 fof(f1602,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1600,f1542])).
% 34.36/4.84 fof(f1604,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1602])).
% 34.36/4.84 fof(f1605,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1604,f1541])).
% 34.36/4.84 fof(f1606,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1605])).
% 34.36/4.84 fof(f1607,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f1606,f38])).
% 34.36/4.84 fof(f1609,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK10_skl,sK9_skl(sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1607,f1540])).
% 34.36/4.84 fof(f1613,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK13_skl(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1609,f32])).
% 34.36/4.84 fof(f1614,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|r1(sK13_skl(sK9_skl(sK10_skl)),sK14_skl(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1609,f30])).
% 34.36/4.84 fof(f1615,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|r1(sK9_skl(sK10_skl),sK13_skl(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1609,f29])).
% 34.36/4.84 fof(f1624,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1)|~r1(sK13_skl(sK9_skl(sK10_skl)),X2)|p1(X2)|~p1(sK13_skl(sK9_skl(sK10_skl))))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1615,f63])).
% 34.36/4.84 fof(f1628,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1)|~r1(sK13_skl(sK9_skl(sK10_skl)),X2)|p1(X2))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f1624,f1613])).
% 34.36/4.84 fof(f1755,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1)|p1(sK14_skl(sK9_skl(sK10_skl)))|p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1628,f1614])).
% 34.36/4.84 fof(f1756,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1)|p1(sK14_skl(sK9_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1755])).
% 34.36/4.84 fof(f1760,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK2_skl(sK10_skl),X0)|p1(X0)|sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0)|p1(sK14_skl(sK9_skl(sK10_skl))))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1756,f866])).
% 34.36/4.84 fof(f1785,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK3_skl(sK10_skl))|sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f1760,f426])).
% 34.36/4.84 fof(f1791,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1785])).
% 34.36/4.84 fof(f1853,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1791,f50])).
% 34.36/4.84 fof(f1854,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK3_skl(sK10_skl),sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1791,f49])).
% 34.36/4.84 fof(f1855,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1791,f52])).
% 34.36/4.84 fof(f1994,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2)|~p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))|p1(sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f1854,f480])).
% 34.36/4.84 fof(f2004,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2)|~p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl)))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f1994])).
% 34.36/4.84 fof(f2005,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2004,f1855])).
% 34.36/4.84 fof(f2206,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))|p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2005,f1853])).
% 34.36/4.84 fof(f2208,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2206])).
% 34.36/4.84 fof(f2480,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))|p1(sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2208,f1609])).
% 34.36/4.84 fof(f2486,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2480])).
% 34.36/4.84 fof(f2503,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2486,f27])).
% 34.36/4.84 fof(f2506,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2503])).
% 34.36/4.84 fof(f2509,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2506,f51])).
% 34.36/4.84 fof(f2511,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2509,f1791])).
% 34.36/4.84 fof(f2531,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2511,f37])).
% 34.36/4.84 fof(f2532,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2511,f36])).
% 34.36/4.84 fof(f2551,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2532,f106])).
% 34.36/4.84 fof(f2566,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2551,f2531])).
% 34.36/4.84 fof(f2567,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2566])).
% 34.36/4.84 fof(f2574,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f2567,f38])).
% 34.36/4.84 fof(f2576,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2574,f2511])).
% 34.36/4.84 fof(f2578,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|p1(sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2576,f28])).
% 34.36/4.84 fof(f2582,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK7_skl(sK12_skl,sK10_skl))|~r1(sK10_skl,sK9_skl(sK10_skl))|p1(sK9_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2578,f31])).
% 34.36/4.84 fof(f2584,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK7_skl(sK12_skl,sK10_skl))|~r1(sK10_skl,sK9_skl(sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2582])).
% 34.36/4.84 fof(f2585,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2584,f1609])).
% 34.36/4.84 fof(f2592,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2585,f20])).
% 34.36/4.84 fof(f2594,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2592,f24])).
% 34.36/4.84 fof(f2603,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2594,f27])).
% 34.36/4.84 fof(f2605,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl))))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2603,f2532])).
% 34.36/4.84 fof(f2607,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|p1(sK14_skl(sK9_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2605])).
% 34.36/4.84 fof(f2617,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2607,f2531])).
% 34.36/4.84 fof(f2618,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2617])).
% 34.36/4.84 fof(f2628,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f2618,f38])).
% 34.36/4.84 fof(f2630,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|p1(sK14_skl(sK9_skl(sK10_skl)))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2628,f2511])).
% 34.36/4.84 fof(f2634,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,sK9_skl(sK10_skl))|p1(sK9_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2630,f31])).
% 34.36/4.84 fof(f2636,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))|~r1(sK10_skl,sK9_skl(sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2634])).
% 34.36/4.84 fof(f2637,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK9_skl(sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2636,f1609])).
% 34.36/4.84 fof(f2642,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2637,f22])).
% 34.36/4.84 fof(f2644,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|~r1(sK10_skl,X0)|~r1(X0,X1)|p1(X1)|sP2_prd(sK8_skl(X1,X0,sK10_skl),X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2642,f24])).
% 34.36/4.84 fof(f2654,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|~r1(sK2_skl(sK10_skl),X0)|p1(X0)|sP2_prd(sK8_skl(X0,sK2_skl(sK10_skl),sK10_skl),X0))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2644,f866])).
% 34.36/4.84 fof(f2685,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK3_skl(sK10_skl))|sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f2654,f426])).
% 34.36/4.84 fof(f2691,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2685])).
% 34.36/4.84 fof(f2718,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2691,f50])).
% 34.36/4.84 fof(f2719,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|r1(sK3_skl(sK10_skl),sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2691,f49])).
% 34.36/4.84 fof(f2720,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2691,f52])).
% 34.36/4.84 fof(f2761,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2)|~p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl))|p1(sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2719,f480])).
% 34.36/4.84 fof(f2771,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2)|~p1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl)))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f2761])).
% 34.36/4.84 fof(f2772,plain,(
% 34.36/4.84 ![X0,X1,X2]: (p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|~r1(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),X2)|p1(X2))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f2771,f2720])).
% 34.36/4.84 fof(f3291,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))|p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f2772,f2718])).
% 34.36/4.84 fof(f3299,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f3291])).
% 34.36/4.84 fof(f3433,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK11_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(resolution,[status(thm)],[f3299,f25])).
% 34.36/4.84 fof(f3435,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~r1(sK10_skl,X0)|sP0_prd(sK1_skl(X0,sK10_skl),X0)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f3433,f26])).
% 34.36/4.84 fof(f4069,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f3435,f27])).
% 34.36/4.84 fof(f4072,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|p1(sK16_skl(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f4069])).
% 34.36/4.84 fof(f4179,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)|~sP2_prd(sK8_skl(sK3_skl(sK10_skl),sK2_skl(sK10_skl),sK10_skl),sK3_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4072,f51])).
% 34.36/4.84 fof(f4181,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4179,f2691])).
% 34.36/4.84 fof(f4184,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4181,f37])).
% 34.36/4.84 fof(f4185,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4181,f36])).
% 34.36/4.84 fof(f4193,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4185,f106])).
% 34.36/4.84 fof(f4205,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|p1(sK3_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4193,f4184])).
% 34.36/4.84 fof(f4206,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f4205])).
% 34.36/4.84 fof(f4215,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f4206,f38])).
% 34.36/4.84 fof(f4217,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4215,f4181])).
% 34.36/4.84 fof(f4219,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4217,f28])).
% 34.36/4.84 fof(f4242,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4219,f20])).
% 34.36/4.84 fof(f4244,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4242,f24])).
% 34.36/4.84 fof(f4245,plain,(
% 34.36/4.84 ![X0,X1]: (p1(sK3_skl(sK10_skl))|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4244,f27])).
% 34.36/4.84 fof(f4247,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|p1(sK3_skl(sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4245,f4185])).
% 34.36/4.84 fof(f4249,plain,(
% 34.36/4.84 ![X0]: (p1(sK3_skl(sK10_skl))|~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f4247])).
% 34.36/4.84 fof(f4250,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|p1(sK3_skl(sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4249,f4184])).
% 34.36/4.84 fof(f4251,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(duplicate_literals_removal,[status(thm)],[f4250])).
% 34.36/4.84 fof(f4252,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f4251,f38])).
% 34.36/4.84 fof(f4254,plain,(
% 34.36/4.84 p1(sK3_skl(sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4252,f4181])).
% 34.36/4.84 fof(f4257,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,X0)|p1(X0)|~p1(sK10_skl)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4254,f11])).
% 34.36/4.84 fof(f4259,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK10_skl,X0)|p1(X0)|~p1(sK10_skl)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4257,f24])).
% 34.36/4.84 fof(f4260,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK10_skl,X0)|p1(X0)|~r1(sK10_skl,X1)|sP0_prd(sK1_skl(X1,sK10_skl),X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4259,f419])).
% 34.36/4.84 fof(f4264,plain,(
% 34.36/4.84 ![X0]: (~r1(sK10_skl,X0)|p1(X0)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4260,f27])).
% 34.36/4.84 fof(f4270,plain,(
% 34.36/4.84 p1(sK11_skl)|sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f4264,f25])).
% 34.36/4.84 fof(f4271,plain,(
% 34.36/4.84 sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4270,f26])).
% 34.36/4.84 fof(f4272,plain,(
% 34.36/4.84 r1(sK1_skl(sK12_skl,sK10_skl),sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4271,f37])).
% 34.36/4.84 fof(f4273,plain,(
% 34.36/4.84 r1(sK12_skl,sK1_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4271,f36])).
% 34.36/4.84 fof(f4276,plain,(
% 34.36/4.84 ![X0]: (~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0)|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl)))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4273,f106])).
% 34.36/4.84 fof(f4322,plain,(
% 34.36/4.84 p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))|r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4276,f4272])).
% 34.36/4.84 fof(f4326,plain,(
% 34.36/4.84 r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))|~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.84 inference(resolution,[status(thm)],[f4322,f38])).
% 34.36/4.84 fof(f4328,plain,(
% 34.36/4.84 r1(sK12_skl,sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4326,f4271])).
% 34.36/4.84 fof(f4329,plain,(
% 34.36/4.84 p1(sK7_skl(sK12_skl,sK10_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4328,f28])).
% 34.36/4.84 fof(f4333,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK0_skl,sK10_skl)|~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4329,f20])).
% 34.36/4.84 fof(f4335,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK10_skl,sK12_skl)|~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4333,f24])).
% 34.36/4.84 fof(f4336,plain,(
% 34.36/4.84 ![X0,X1]: (~r1(sK12_skl,X0)|~r1(X0,X1)|p1(X1))),
% 34.36/4.84 inference(forward_subsumption_resolution,[status(thm)],[f4335,f27])).
% 34.36/4.84 fof(f4338,plain,(
% 34.36/4.84 ![X0]: (~r1(sK1_skl(sK12_skl,sK10_skl),X0)|p1(X0))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4336,f4273])).
% 34.36/4.84 fof(f4339,plain,(
% 34.36/4.84 p1(sK15_skl(sK1_skl(sK12_skl,sK10_skl),sK12_skl))),
% 34.36/4.84 inference(resolution,[status(thm)],[f4338,f4272])).
% 34.36/4.84 fof(f4340,plain,(
% 34.36/4.84 ~sP0_prd(sK1_skl(sK12_skl,sK10_skl),sK12_skl)),
% 34.36/4.90 inference(resolution,[status(thm)],[f4339,f38])).
% 34.36/4.90 fof(f4342,plain,(
% 34.36/4.90 $false),
% 34.36/4.90 inference(forward_subsumption_resolution,[status(thm)],[f4340,f4271])).
% 34.36/4.90 % SZS output end CNFRefutation for theBenchmark.p
% 34.36/4.90 % Elapsed time: 4.454824 seconds
% 34.36/4.90 % CPU time: 34.885645 seconds
% 34.36/4.90 % Total memory used: 148.436 MB
% 34.36/4.90 % Net memory used: 140.349 MB
%------------------------------------------------------------------------------