%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL652+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 : n009.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:38 PM UTC 2026
% Result : Theorem 188.38s 24.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL652+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.39 % Computer : n009.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 21 00:46:27 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 188.38/24.32 % Refutation found
% 188.38/24.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 188.38/24.32 % SZS output start CNFRefutation for theBenchmark
% 188.38/24.32 fof(f1,conjecture,(
% 188.38/24.32 ~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ p4(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )) )))& (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )) )) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p3(X) ))| ~ p2(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))| ~ p2(Y) ) ))& p2(X)& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p2(Y) ) )) )) )) ))| ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ p2(X) ) )) )))& (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p2(Y) ) )) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p2(X) ) )))& (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p3(X) ))| ~ p2(Y) ) )) )) )) ))| ( (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ p2(X) ))& (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p2(Y) ) )) )) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )) )) )),
% 188.38/24.32 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 188.38/24.32 fof(f2,negated_conjecture,(
% 188.38/24.32 ~(~ (? [X] :~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ p4(Y) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )) )))& (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )) )) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p3(X) ))| ~ p2(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ ( ~ (! [Y] :( ~ r1(X,Y)| ~ ( (! [X] :( ~ r1(Y,X)| p3(X) ))| ~ p2(Y) ) ))& p2(X)& ~ (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p2(Y) ) )) )) )) ))| ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ p2(X) ) )) )))& (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p2(Y) ) )) ))| ~ (! [X] :( ~ r1(Y,X)| ~ ( (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ p2(X) ) )))& (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| p3(X) ))| ~ p2(Y) ) )) )) )) ))| ( (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p3(Y) ))| ~ p2(X) ))& (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| ~ p2(Y) ) )) )) ) ))| ~ (! [Y] :( ~ r1(X,Y)| ~ ( ~ (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))& (! [X] :( ~ r1(Y,X)| p1(X) ) )) ))| (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p1(Y) ) )))| (! [X] :( ~ r1(Y,X)| p1(X) ) )))| (! [Y] :( ~ r1(X,Y)| ~ (! [X] :( ~ r1(Y,X)| ~ (! [Y] :( ~ r1(X,Y)| p2(Y) ) )) )))| ~ (! [Y] :( ~ r1(X,Y)| (! [X] :( ~ r1(Y,X)| (! [Y] :( ~ r1(X,Y)| ~ p1(Y) ) )))| ~ (! [X] :( ~ r1(Y,X)| ~ p1(X) ) )) )) ))),
% 188.38/24.32 inference(negated_conjecture,[status(cth)],[f1])).
% 188.38/24.32 fof(f3,plain,(
% 188.38/24.32 ?[X]: (((((((![Y]: (~r1(X,Y)|~p4(Y)))&(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&p1(X)))))))|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p1(Y)))))))))&(![Y]: (~r1(X,Y)|(((((![X]: (~r1(Y,X)|(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&~p3(X))))&p2(Y)))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))&p2(Y))))|~p2(X))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p2(Y)))))))))))&((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(?[X]: ((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X)))))))|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p2(Y)))))))&(![X]: (~r1(Y,X)|((?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|~p2(X)))))|(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&~p3(X))))&p2(Y)))))))))))&((?[X]: ((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X)))|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p2(Y))))))))))&(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y)))))|(?[X]: (r1(Y,X)&~p1(X)))))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p2(Y))))))))&(![Y]: ((~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|~p1(Y))))))|(?[X]: (r1(Y,X)&p1(X))))))),
% 188.38/24.32 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 188.38/24.32 fof(f4,definition,(
% 188.38/24.32 ![Y,X]: (sP0_prd(X,Y)<=>(r1(Y,X)&p1(X)))),
% 188.38/24.32 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 188.38/24.32 fof(f5,definition,(
% 188.38/24.32 ![Y,X]: (sP1_prd(X,Y)<=>((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X)))),
% 188.38/24.32 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 188.38/24.32 fof(f6,definition,(
% 188.38/24.32 ![X,Y]: (sP2_prd(Y,X)<=>(r1(X,Y)&(![X]: (~r1(Y,X)|~p2(X)))))),
% 188.38/24.32 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 188.38/24.32 fof(f7,definition,(
% 188.38/24.32 ![Y,X]: (sP3_prd(X,Y)<=>((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X)))),
% 188.38/24.32 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 188.38/24.32 fof(f8,plain,(
% 188.38/24.32 ?[X]: (((((((![Y]: (~r1(X,Y)|~p4(Y)))&(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(?[X]: sP0_prd(X,Y))))))|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p1(Y)))))))))&(![Y]: (~r1(X,Y)|(((((![X]: (~r1(Y,X)|(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&~p3(X))))&p2(Y)))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|((?[X]: (r1(Y,X)&~p3(X)))&p2(Y))))|~p2(X))|(![Y]: (~r1(X,Y)|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p2(Y)))))))))))&((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|(?[X]: sP1_prd(X,Y))))))|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p2(Y)))))))&(![X]: (~r1(Y,X)|((?[Y]: sP2_prd(Y,X))|(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&~p3(X))))&p2(Y)))))))))))&((?[X]: sP3_prd(X,Y))|(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|~p2(Y))))))))))&(![Y]: (~r1(X,Y)|((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y)))))|(?[X]: (r1(Y,X)&~p1(X)))))))&(?[Y]: ((r1(X,Y)&(?[X]: (r1(Y,X)&(![Y]: (~r1(X,Y)|p1(Y))))))&(?[X]: (r1(Y,X)&~p1(X))))))&(?[Y]: (r1(X,Y)&(![X]: (~r1(Y,X)|(?[Y]: (r1(X,Y)&~p2(Y))))))))&(![Y]: ((~r1(X,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|~p1(Y))))))|(?[X]: (r1(Y,X)&p1(X))))))),
% 188.38/24.32 inference(formula_renaming,[status(thm)],[f3,f7,f6,f5,f4])).
% 188.38/24.32 fof(f9,plain,(
% 188.38/24.32 (((((((![Y]: (~r1(sK0_skl,Y)|~p4(Y)))&(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|sP0_prd(sK1_skl(Y,X,Y),Y)))))|(r1(Y,sK2_skl(Y))&(![Y]: (~r1(sK2_skl(Y),Y)|~p1(Y))))))))&(![Y]: (~r1(sK0_skl,Y)|(((((![X]: (~r1(Y,X)|((r1(X,sK3_skl(X,Y))&(r1(sK3_skl(X,Y),sK4_skl(X,Y))&~p3(sK4_skl(X,Y))))&p2(sK3_skl(X,Y)))))&(![X]: (~r1(Y,X)|(((![Y]: (~r1(X,Y)|((r1(Y,sK5_skl(Y,X,Y))&~p3(sK5_skl(Y,X,Y)))&p2(Y))))|~p2(X))|(![Y]: (~r1(X,Y)|(r1(Y,sK6_skl(Y,X,Y))&(![Y]: (~r1(sK6_skl(Y,X,Y),Y)|~p2(Y))))))))))&((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|sP1_prd(sK7_skl(Y,X,Y),Y)))))|(r1(Y,sK8_skl(Y))&(![Y]: (~r1(sK8_skl(Y),Y)|~p2(Y))))))&(![X]: (~r1(Y,X)|(sP2_prd(sK9_skl(X,Y),X)|(r1(X,sK10_skl(X,Y))&(![X]: (~r1(sK10_skl(X,Y),X)|((r1(X,sK11_skl(X,X,Y))&(r1(sK11_skl(X,X,Y),sK12_skl(X,X,Y))&~p3(sK12_skl(X,X,Y))))&p2(sK11_skl(X,X,Y))))))))))&(sP3_prd(sK13_skl(Y),Y)|(r1(Y,sK14_skl(Y))&(![Y]: (~r1(sK14_skl(Y),Y)|~p2(Y)))))))))&(![Y]: (~r1(sK0_skl,Y)|((![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|p1(Y)))))|(r1(Y,sK15_skl(Y))&~p1(sK15_skl(Y)))))))&((r1(sK0_skl,sK16_skl)&(r1(sK16_skl,sK17_skl)&(![Y]: (~r1(sK17_skl,Y)|p1(Y)))))&(r1(sK16_skl,sK18_skl)&~p1(sK18_skl))))&(r1(sK0_skl,sK19_skl)&(![X]: (~r1(sK19_skl,X)|(r1(X,sK20_skl(X))&~p2(sK20_skl(X)))))))&(![Y]: ((~r1(sK0_skl,Y)|(![X]: (~r1(Y,X)|(![Y]: (~r1(X,Y)|~p1(Y))))))|(r1(Y,sK21_skl(Y))&p1(sK21_skl(Y))))))),
% 188.38/24.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl]),skolemize(X,sK0_skl),skolemize(X,sK1_skl(Y,X,Y)),skolemize(X,sK2_skl(Y)),skolemize(Y,sK3_skl(X,Y)),skolemize(X,sK4_skl(X,Y)),skolemize(X,sK5_skl(Y,X,Y)),skolemize(X,sK6_skl(Y,X,Y)),skolemize(X,sK7_skl(Y,X,Y)),skolemize(X,sK8_skl(Y)),skolemize(Y,sK9_skl(X,Y)),skolemize(Y,sK10_skl(X,Y)),skolemize(Y,sK11_skl(X,X,Y)),skolemize(X,sK12_skl(X,X,Y)),skolemize(X,sK13_skl(Y)),skolemize(X,sK14_skl(Y)),skolemize(X,sK15_skl(Y)),skolemize(Y,sK16_skl),skolemize(X,sK17_skl),skolemize(X,sK18_skl),skolemize(Y,sK19_skl),skolemize(Y,sK20_skl(X)),skolemize(X,sK21_skl(Y))],[f8])).
% 188.38/24.32 fof(f13,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|r1(X1,sK3_skl(X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f14,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|r1(sK3_skl(X1,X0),sK4_skl(X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f15,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~p3(sK4_skl(X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f16,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|p2(sK3_skl(X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f21,plain,(
% 188.38/24.32 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p2(X2)|~p2(X1)|~r1(X1,X3)|r1(X3,sK6_skl(X3,X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f22,plain,(
% 188.38/24.32 ![X0,X1,X2,X3,X4]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|p2(X2)|~p2(X1)|~r1(X1,X3)|~r1(sK6_skl(X3,X1,X0),X4)|~p2(X4))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f23,plain,(
% 188.38/24.32 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|sP1_prd(sK7_skl(X2,X1,X0),X2)|r1(X0,sK8_skl(X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f24,plain,(
% 188.38/24.32 ![X0,X1,X2,X3]: (~r1(sK0_skl,X0)|~r1(X0,X1)|~r1(X1,X2)|sP1_prd(sK7_skl(X2,X1,X0),X2)|~r1(sK8_skl(X0),X3)|~p2(X3))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f25,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK0_skl,X0)|~r1(X0,X1)|sP2_prd(sK9_skl(X1,X0),X1)|r1(X1,sK10_skl(X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f26,plain,(
% 188.38/24.32 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|sP2_prd(sK9_skl(X1,X0),X1)|~r1(sK10_skl(X1,X0),X2)|r1(X2,sK11_skl(X2,X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f29,plain,(
% 188.38/24.32 ![X0,X1,X2]: (~r1(sK0_skl,X0)|~r1(X0,X1)|sP2_prd(sK9_skl(X1,X0),X1)|~r1(sK10_skl(X1,X0),X2)|p2(sK11_skl(X2,X1,X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f30,plain,(
% 188.38/24.32 ![X0]: (~r1(sK0_skl,X0)|sP3_prd(sK13_skl(X0),X0)|r1(X0,sK14_skl(X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f31,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK0_skl,X0)|sP3_prd(sK13_skl(X0),X0)|~r1(sK14_skl(X0),X1)|~p2(X1))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f39,plain,(
% 188.38/24.32 r1(sK0_skl,sK19_skl)),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f40,plain,(
% 188.38/24.32 ![X0]: (~r1(sK19_skl,X0)|r1(X0,sK20_skl(X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f41,plain,(
% 188.38/24.32 ![X0]: (~r1(sK19_skl,X0)|~p2(sK20_skl(X0)))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f9])).
% 188.38/24.32 fof(f49,plain,(
% 188.38/24.32 ![Y,X]: ((~sP1_prd(X,Y)|((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X)))&(sP1_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p3(Y))))|~p2(X))))),
% 188.38/24.32 inference(NNF_transformation,[status(thm)],[f5])).
% 188.38/24.32 fof(f50,plain,(
% 188.38/24.32 (![Y,X]: (~sP1_prd(X,Y)|((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X))))&(![Y,X]: (sP1_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p3(Y))))|~p2(X))))),
% 188.38/24.32 inference(miniscoping,[status(thm)],[f49])).
% 188.38/24.32 fof(f51,plain,(
% 188.38/24.32 (![Y,X]: (~sP1_prd(X,Y)|((r1(Y,X)&(r1(X,sK22_skl(X,Y))&~p3(sK22_skl(X,Y))))&p2(X))))&(![Y,X]: (sP1_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p3(Y))))|~p2(X))))),
% 188.38/24.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(Y,sK22_skl(X,Y))],[f50])).
% 188.38/24.32 fof(f52,plain,(
% 188.38/24.32 ![X0,X1]: (~sP1_prd(X0,X1)|r1(X1,X0))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f51])).
% 188.38/24.32 fof(f55,plain,(
% 188.38/24.32 ![X0,X1]: (~sP1_prd(X0,X1)|p2(X0))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f51])).
% 188.38/24.32 fof(f57,plain,(
% 188.38/24.32 ![X,Y]: ((~sP2_prd(Y,X)|(r1(X,Y)&(![X]: (~r1(Y,X)|~p2(X)))))&(sP2_prd(Y,X)|(~r1(X,Y)|(?[X]: (r1(Y,X)&p2(X))))))),
% 188.38/24.32 inference(NNF_transformation,[status(thm)],[f6])).
% 188.38/24.32 fof(f58,plain,(
% 188.38/24.32 (![X,Y]: (~sP2_prd(Y,X)|(r1(X,Y)&(![X]: (~r1(Y,X)|~p2(X))))))&(![X,Y]: (sP2_prd(Y,X)|(~r1(X,Y)|(?[X]: (r1(Y,X)&p2(X))))))),
% 188.38/24.32 inference(miniscoping,[status(thm)],[f57])).
% 188.38/24.32 fof(f59,plain,(
% 188.38/24.32 (![X,Y]: (~sP2_prd(Y,X)|(r1(X,Y)&(![X]: (~r1(Y,X)|~p2(X))))))&(![X,Y]: (sP2_prd(Y,X)|(~r1(X,Y)|(r1(Y,sK23_skl(Y,X))&p2(sK23_skl(Y,X))))))),
% 188.38/24.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(X,sK23_skl(Y,X))],[f58])).
% 188.38/24.32 fof(f60,plain,(
% 188.38/24.32 ![X0,X1]: (~sP2_prd(X0,X1)|r1(X1,X0))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f59])).
% 188.38/24.32 fof(f61,plain,(
% 188.38/24.32 ![X0,X1,X2]: (~sP2_prd(X0,X1)|~r1(X0,X2)|~p2(X2))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f59])).
% 188.38/24.32 fof(f64,plain,(
% 188.38/24.32 ![Y,X]: ((~sP3_prd(X,Y)|((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X)))&(sP3_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p3(Y))))|~p2(X))))),
% 188.38/24.32 inference(NNF_transformation,[status(thm)],[f7])).
% 188.38/24.32 fof(f65,plain,(
% 188.38/24.32 (![Y,X]: (~sP3_prd(X,Y)|((r1(Y,X)&(?[Y]: (r1(X,Y)&~p3(Y))))&p2(X))))&(![Y,X]: (sP3_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p3(Y))))|~p2(X))))),
% 188.38/24.32 inference(miniscoping,[status(thm)],[f64])).
% 188.38/24.32 fof(f66,plain,(
% 188.38/24.32 (![Y,X]: (~sP3_prd(X,Y)|((r1(Y,X)&(r1(X,sK24_skl(X,Y))&~p3(sK24_skl(X,Y))))&p2(X))))&(![Y,X]: (sP3_prd(X,Y)|((~r1(Y,X)|(![Y]: (~r1(X,Y)|p3(Y))))|~p2(X))))),
% 188.38/24.32 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(Y,sK24_skl(X,Y))],[f65])).
% 188.38/24.32 fof(f67,plain,(
% 188.38/24.32 ![X0,X1]: (~sP3_prd(X0,X1)|r1(X1,X0))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f66])).
% 188.38/24.32 fof(f70,plain,(
% 188.38/24.32 ![X0,X1]: (~sP3_prd(X0,X1)|p2(X0))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f66])).
% 188.38/24.32 fof(f71,plain,(
% 188.38/24.32 ![X0,X1,X2]: (sP3_prd(X0,X1)|~r1(X1,X0)|~r1(X0,X2)|p3(X2)|~p2(X0))),
% 188.38/24.32 inference(cnf_transformation,[status(thm)],[f66])).
% 188.38/24.32 fof(f76,plain,(
% 188.38/24.32 ![X0]: (~r1(sK19_skl,X0)|r1(X0,sK3_skl(X0,sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f13,f39])).
% 188.38/24.32 fof(f102,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)|r1(sK19_skl,sK14_skl(sK19_skl))),
% 188.38/24.32 inference(resolution,[status(thm)],[f30,f39])).
% 188.38/24.32 fof(f104,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)|r1(sK14_skl(sK19_skl),sK3_skl(sK14_skl(sK19_skl),sK19_skl))),
% 188.38/24.32 inference(resolution,[status(thm)],[f102,f76])).
% 188.38/24.32 fof(f111,plain,(
% 188.38/24.32 ![X0,X1,X2,X3]: (sP3_prd(sK3_skl(X0,X1),X2)|~r1(X2,sK3_skl(X0,X1))|~r1(sK3_skl(X0,X1),X3)|p3(X3)|~r1(sK0_skl,X1)|~r1(X1,X0))),
% 188.38/24.32 inference(resolution,[status(thm)],[f71,f16])).
% 188.38/24.32 fof(f120,plain,(
% 188.38/24.32 ![X0,X1,X2]: (~r1(sK19_skl,X0)|~r1(X0,X1)|p2(X1)|~p2(X0)|~r1(X0,X2)|r1(X2,sK6_skl(X2,X0,sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f21,f39])).
% 188.38/24.32 fof(f122,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK19_skl,X0)|~r1(X0,X1)|sP1_prd(sK7_skl(X1,X0,sK19_skl),X1)|r1(sK19_skl,sK8_skl(sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f23,f39])).
% 188.38/24.32 fof(f147,plain,(
% 188.38/24.32 ![X0]: (~r1(sK19_skl,X0)|sP2_prd(sK9_skl(X0,sK19_skl),X0)|r1(X0,sK10_skl(X0,sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f25,f39])).
% 188.38/24.32 fof(f170,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)|~r1(sK0_skl,sK19_skl)|sP3_prd(sK13_skl(sK19_skl),sK19_skl)|~p2(sK3_skl(sK14_skl(sK19_skl),sK19_skl))),
% 188.38/24.32 inference(resolution,[status(thm)],[f104,f31])).
% 188.38/24.32 fof(f172,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)|~r1(sK0_skl,sK19_skl)|~p2(sK3_skl(sK14_skl(sK19_skl),sK19_skl))),
% 188.38/24.32 inference(duplicate_literals_removal,[status(thm)],[f170])).
% 188.38/24.32 fof(f173,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)|~p2(sK3_skl(sK14_skl(sK19_skl),sK19_skl))),
% 188.38/24.32 inference(forward_subsumption_resolution,[status(thm)],[f172,f39])).
% 188.38/24.32 fof(f174,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)|~r1(sK0_skl,sK19_skl)|~r1(sK19_skl,sK14_skl(sK19_skl))),
% 188.38/24.32 inference(resolution,[status(thm)],[f173,f16])).
% 188.38/24.32 fof(f175,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)|~r1(sK19_skl,sK14_skl(sK19_skl))),
% 188.38/24.32 inference(forward_subsumption_resolution,[status(thm)],[f174,f39])).
% 188.38/24.32 fof(f176,plain,(
% 188.38/24.32 sP3_prd(sK13_skl(sK19_skl),sK19_skl)),
% 188.38/24.32 inference(forward_subsumption_resolution,[status(thm)],[f175,f102])).
% 188.38/24.32 fof(f178,plain,(
% 188.38/24.32 r1(sK19_skl,sK13_skl(sK19_skl))),
% 188.38/24.32 inference(resolution,[status(thm)],[f176,f67])).
% 188.38/24.32 fof(f179,plain,(
% 188.38/24.32 p2(sK13_skl(sK19_skl))),
% 188.38/24.32 inference(resolution,[status(thm)],[f176,f70])).
% 188.38/24.32 fof(f183,plain,(
% 188.38/24.32 sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|r1(sK13_skl(sK19_skl),sK10_skl(sK13_skl(sK19_skl),sK19_skl))),
% 188.38/24.32 inference(resolution,[status(thm)],[f178,f147])).
% 188.38/24.32 fof(f188,plain,(
% 188.38/24.32 r1(sK13_skl(sK19_skl),sK20_skl(sK13_skl(sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f178,f40])).
% 188.38/24.32 fof(f281,plain,(
% 188.38/24.32 ![X0,X1,X2]: (sP3_prd(sK3_skl(X0,X1),X2)|~r1(X2,sK3_skl(X0,X1))|p3(sK4_skl(X0,X1))|~r1(sK0_skl,X1)|~r1(X1,X0)|~r1(sK0_skl,X1)|~r1(X1,X0))),
% 188.38/24.32 inference(resolution,[status(thm)],[f111,f14])).
% 188.38/24.32 fof(f282,plain,(
% 188.38/24.32 ![X0,X1,X2]: (sP3_prd(sK3_skl(X0,X1),X2)|~r1(X2,sK3_skl(X0,X1))|p3(sK4_skl(X0,X1))|~r1(sK0_skl,X1)|~r1(X1,X0))),
% 188.38/24.32 inference(duplicate_literals_removal,[status(thm)],[f281])).
% 188.38/24.32 fof(f283,plain,(
% 188.38/24.32 ![X0,X1,X2]: (sP3_prd(sK3_skl(X0,X1),X2)|~r1(X2,sK3_skl(X0,X1))|~r1(sK0_skl,X1)|~r1(X1,X0))),
% 188.38/24.32 inference(forward_subsumption_resolution,[status(thm)],[f282,f15])).
% 188.38/24.32 fof(f325,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|r1(X1,sK6_skl(X1,sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f120,f179])).
% 188.38/24.32 fof(f328,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|r1(X1,sK6_skl(X1,sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.32 inference(forward_subsumption_resolution,[status(thm)],[f325,f178])).
% 188.38/24.32 fof(f333,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK19_skl,X0)|~r1(X0,X1)|r1(sK19_skl,sK8_skl(sK19_skl))|r1(X1,sK7_skl(X1,X0,sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f122,f52])).
% 188.38/24.32 fof(f334,plain,(
% 188.38/24.32 ![X0,X1]: (~r1(sK19_skl,X0)|~r1(X0,X1)|r1(sK19_skl,sK8_skl(sK19_skl))|p2(sK7_skl(X1,X0,sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f122,f55])).
% 188.38/24.32 fof(f512,plain,(
% 188.38/24.32 ![X0,X1]: (sP3_prd(sK3_skl(X0,sK19_skl),X1)|~r1(X1,sK3_skl(X0,sK19_skl))|~r1(sK19_skl,X0))),
% 188.38/24.32 inference(resolution,[status(thm)],[f283,f39])).
% 188.38/24.32 fof(f608,plain,(
% 188.38/24.32 ![X0,X1,X2,X3]: (~r1(sK19_skl,X0)|~r1(X0,X1)|r1(sK19_skl,sK8_skl(sK19_skl))|~sP2_prd(X2,X3)|~r1(X2,sK7_skl(X1,X0,sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f334,f61])).
% 188.38/24.32 fof(f642,plain,(
% 188.38/24.32 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|r1(sK19_skl,sK8_skl(sK19_skl))|r1(X0,sK7_skl(X0,sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f333,f178])).
% 188.38/24.32 fof(f831,plain,(
% 188.38/24.32 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|r1(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl))|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f328,f183])).
% 188.38/24.32 fof(f3711,plain,(
% 188.38/24.32 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK0_skl,sK19_skl)|~r1(sK19_skl,sK13_skl(sK19_skl))|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f831,f29])).
% 188.38/24.32 fof(f3713,plain,(
% 188.38/24.32 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK0_skl,sK19_skl)|~r1(sK19_skl,sK13_skl(sK19_skl))|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|r1(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.32 inference(resolution,[status(thm)],[f831,f26])).
% 188.38/24.32 fof(f3715,plain,(
% 188.38/24.32 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK0_skl,sK19_skl)|~r1(sK19_skl,sK13_skl(sK19_skl))|p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.32 inference(duplicate_literals_removal,[status(thm)],[f3711])).
% 188.38/24.32 fof(f3716,plain,(
% 188.38/24.32 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK19_skl,sK13_skl(sK19_skl))|p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.32 inference(forward_subsumption_resolution,[status(thm)],[f3715,f39])).
% 188.38/24.32 fof(f3719,plain,(
% 188.38/24.32 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK0_skl,sK19_skl)|~r1(sK19_skl,sK13_skl(sK19_skl))|r1(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(duplicate_literals_removal,[status(thm)],[f3713])).
% 188.38/24.33 fof(f3720,plain,(
% 188.38/24.33 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK19_skl,sK13_skl(sK19_skl))|r1(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(forward_subsumption_resolution,[status(thm)],[f3719,f39])).
% 188.38/24.33 fof(f4927,plain,(
% 188.38/24.33 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(forward_subsumption_resolution,[status(thm)],[f3716,f178])).
% 188.38/24.33 fof(f6262,plain,(
% 188.38/24.33 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|r1(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(forward_subsumption_resolution,[status(thm)],[f3720,f178])).
% 188.38/24.33 fof(f6263,plain,(
% 188.38/24.33 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK0_skl,sK19_skl)|~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X1)|p2(X1)|~p2(sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK10_skl(sK13_skl(sK19_skl),sK19_skl))|~p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(resolution,[status(thm)],[f6262,f22])).
% 188.38/24.33 fof(f6268,plain,(
% 188.38/24.33 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X1)|p2(X1)|~p2(sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK10_skl(sK13_skl(sK19_skl),sK19_skl))|~p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(forward_subsumption_resolution,[status(thm)],[f6263,f39])).
% 188.38/24.33 fof(f7981,plain,(
% 188.38/24.33 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X1)|p2(X1)|~p2(sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK10_skl(sK13_skl(sK19_skl),sK19_skl))|~p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(forward_subsumption_resolution,[status(thm)],[f6268,f178])).
% 188.38/24.33 fof(f7982,plain,(
% 188.38/24.33 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X1)|p2(X1)|~r1(sK13_skl(sK19_skl),sK10_skl(sK13_skl(sK19_skl),sK19_skl))|~p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(resolution,[status(thm)],[f7981,f179])).
% 188.38/24.33 fof(f7983,plain,(
% 188.38/24.33 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X1)|p2(X1)|~p2(sK11_skl(sK6_skl(sK10_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(forward_subsumption_resolution,[status(thm)],[f7982,f183])).
% 188.38/24.33 fof(f7984,plain,(
% 188.38/24.33 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X1)|p2(X1))),
% 188.38/24.33 inference(forward_subsumption_resolution,[status(thm)],[f7983,f4927])).
% 188.38/24.33 fof(f7991,plain,(
% 188.38/24.33 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1)|r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(resolution,[status(thm)],[f7984,f60])).
% 188.38/24.33 fof(f8000,plain,(
% 188.38/24.33 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl)))),
% 188.38/24.33 inference(resolution,[status(thm)],[f7991,f188])).
% 188.38/24.34 fof(f8018,plain,(
% 188.38/24.34 p2(sK20_skl(sK13_skl(sK19_skl)))|p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8000,f188])).
% 188.38/24.34 fof(f8021,plain,(
% 188.38/24.34 p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))),
% 188.38/24.34 inference(duplicate_literals_removal,[status(thm)],[f8018])).
% 188.38/24.34 fof(f8035,plain,(
% 188.38/24.34 p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK19_skl,sK8_skl(sK19_skl))|r1(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK7_skl(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8021,f642])).
% 188.38/24.34 fof(f8279,plain,(
% 188.38/24.34 ![X0]: (p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK19_skl,sK8_skl(sK19_skl))|~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|r1(sK19_skl,sK8_skl(sK19_skl))|~sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),X0))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8035,f608])).
% 188.38/24.34 fof(f8285,plain,(
% 188.38/24.34 ![X0]: (p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK19_skl,sK8_skl(sK19_skl))|~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),X0))),
% 188.38/24.34 inference(duplicate_literals_removal,[status(thm)],[f8279])).
% 188.38/24.34 fof(f8286,plain,(
% 188.38/24.34 ![X0]: (r1(sK19_skl,sK8_skl(sK19_skl))|~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),X0))),
% 188.38/24.34 inference(forward_subsumption_resolution,[status(thm)],[f8285,f41])).
% 188.38/24.34 fof(f8287,plain,(
% 188.38/24.34 ![X0]: (r1(sK19_skl,sK8_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~sP2_prd(sK9_skl(sK13_skl(sK19_skl),sK19_skl),X0))),
% 188.38/24.34 inference(forward_subsumption_resolution,[status(thm)],[f8286,f178])).
% 188.38/24.34 fof(f8288,plain,(
% 188.38/24.34 ![X0,X1]: (r1(sK19_skl,sK8_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8287,f7984])).
% 188.38/24.34 fof(f8290,plain,(
% 188.38/24.34 ![X0,X1]: (r1(sK19_skl,sK8_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1))),
% 188.38/24.34 inference(forward_subsumption_resolution,[status(thm)],[f8288,f7991])).
% 188.38/24.34 fof(f8304,plain,(
% 188.38/24.34 ![X0]: (r1(sK19_skl,sK8_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|p2(sK20_skl(sK13_skl(sK19_skl))))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8290,f188])).
% 188.38/24.34 fof(f8319,plain,(
% 188.38/24.34 r1(sK19_skl,sK8_skl(sK19_skl))|p2(sK20_skl(sK13_skl(sK19_skl)))|p2(sK20_skl(sK13_skl(sK19_skl)))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8304,f188])).
% 188.38/24.34 fof(f8322,plain,(
% 188.38/24.34 r1(sK19_skl,sK8_skl(sK19_skl))|p2(sK20_skl(sK13_skl(sK19_skl)))),
% 188.38/24.34 inference(duplicate_literals_removal,[status(thm)],[f8319])).
% 188.38/24.34 fof(f8334,plain,(
% 188.38/24.34 ![X0]: (p2(sK20_skl(sK13_skl(sK19_skl)))|sP3_prd(sK3_skl(sK8_skl(sK19_skl),sK19_skl),X0)|~r1(X0,sK3_skl(sK8_skl(sK19_skl),sK19_skl)))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8322,f512])).
% 188.38/24.34 fof(f8342,plain,(
% 188.38/24.34 p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK8_skl(sK19_skl),sK3_skl(sK8_skl(sK19_skl),sK19_skl))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8322,f76])).
% 188.38/24.34 fof(f8348,plain,(
% 188.38/24.34 ![X0,X1]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK0_skl,sK19_skl)|~r1(sK19_skl,X0)|~r1(X0,X1)|sP1_prd(sK7_skl(X1,X0,sK19_skl),X1)|~p2(sK3_skl(sK8_skl(sK19_skl),sK19_skl)))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8342,f24])).
% 188.38/24.34 fof(f8350,plain,(
% 188.38/24.34 ![X0,X1]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,X0)|~r1(X0,X1)|sP1_prd(sK7_skl(X1,X0,sK19_skl),X1)|~p2(sK3_skl(sK8_skl(sK19_skl),sK19_skl)))),
% 188.38/24.34 inference(forward_subsumption_resolution,[status(thm)],[f8348,f39])).
% 188.38/24.34 fof(f8425,plain,(
% 188.38/24.34 p2(sK20_skl(sK13_skl(sK19_skl)))|sP3_prd(sK3_skl(sK8_skl(sK19_skl),sK19_skl),sK8_skl(sK19_skl))|p2(sK20_skl(sK13_skl(sK19_skl)))),
% 188.38/24.34 inference(resolution,[status(thm)],[f8334,f8342])).
% 188.38/24.34 fof(f8426,plain,(
% 188.38/24.34 p2(sK20_skl(sK13_skl(sK19_skl)))|sP3_prd(sK3_skl(sK8_skl(sK19_skl),sK19_skl),sK8_skl(sK19_skl))),
% 188.38/24.34 inference(duplicate_literals_removal,[status(thm)],[f8425])).
% 188.38/24.34 fof(f8429,plain,(
% 188.38/24.34 p2(sK20_skl(sK13_skl(sK19_skl)))|p2(sK3_skl(sK8_skl(sK19_skl),sK19_skl))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8426,f70])).
% 104.37/24.44 fof(f8527,plain,(
% 104.37/24.44 ![X0,X1]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,X0)|~r1(X0,X1)|sP1_prd(sK7_skl(X1,X0,sK19_skl),X1))),
% 104.37/24.44 inference(forward_subsumption_resolution,[status(thm)],[f8350,f8429])).
% 104.37/24.44 fof(f8529,plain,(
% 104.37/24.44 ![X0,X1]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,X0)|~r1(X0,X1)|r1(X1,sK7_skl(X1,X0,sK19_skl)))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8527,f52])).
% 104.37/24.44 fof(f8530,plain,(
% 104.37/24.44 ![X0,X1]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,X0)|~r1(X0,X1)|p2(sK7_skl(X1,X0,sK19_skl)))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8527,f55])).
% 104.37/24.44 fof(f8536,plain,(
% 104.37/24.44 ![X0,X1,X2,X3]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,X0)|~r1(X0,X1)|~sP2_prd(X2,X3)|~r1(X2,sK7_skl(X1,X0,sK19_skl)))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8530,f61])).
% 104.37/24.44 fof(f8546,plain,(
% 104.37/24.44 ![X0]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK13_skl(sK19_skl),X0)|r1(X0,sK7_skl(X0,sK13_skl(sK19_skl),sK19_skl)))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8529,f178])).
% 104.37/24.44 fof(f8561,plain,(
% 104.37/24.44 p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK7_skl(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl))|p2(sK20_skl(sK13_skl(sK19_skl)))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8546,f8021])).
% 104.37/24.44 fof(f8571,plain,(
% 104.37/24.44 p2(sK20_skl(sK13_skl(sK19_skl)))|r1(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK7_skl(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK13_skl(sK19_skl),sK19_skl))),
% 104.37/24.44 inference(duplicate_literals_removal,[status(thm)],[f8561])).
% 104.37/24.44 fof(f8579,plain,(
% 104.37/24.44 ![X0,X1,X2,X3]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,X0)|~r1(X0,X1)|~r1(sK9_skl(sK13_skl(sK19_skl),sK19_skl),sK7_skl(X1,X0,sK19_skl))|~r1(sK13_skl(sK19_skl),X2)|p2(X2)|~r1(sK13_skl(sK19_skl),X3)|p2(X3))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8536,f7984])).
% 104.37/24.44 fof(f9913,plain,(
% 104.37/24.44 ![X0,X1]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1)|p2(sK20_skl(sK13_skl(sK19_skl))))),
% 104.37/24.44 inference(resolution,[status(thm)],[f8579,f8571])).
% 104.37/24.44 fof(f9914,plain,(
% 104.37/24.44 ![X0,X1]: (p2(sK20_skl(sK13_skl(sK19_skl)))|~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1))),
% 104.37/24.44 inference(duplicate_literals_removal,[status(thm)],[f9913])).
% 104.37/24.44 fof(f9915,plain,(
% 104.37/24.44 ![X0,X1]: (~r1(sK19_skl,sK13_skl(sK19_skl))|~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1))),
% 104.37/24.44 inference(forward_subsumption_resolution,[status(thm)],[f9914,f41])).
% 104.37/24.44 fof(f9916,plain,(
% 104.37/24.44 ![X0,X1]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1))),
% 104.37/24.44 inference(backward_subsumption_resolution,[status(thm)],[f7991,f9917])).
% 104.37/24.44 fof(f9917,plain,(
% 104.37/24.44 ![X0,X1]: (~r1(sK13_skl(sK19_skl),sK9_skl(sK13_skl(sK19_skl),sK19_skl))|~r1(sK13_skl(sK19_skl),X0)|p2(X0)|~r1(sK13_skl(sK19_skl),X1)|p2(X1))),
% 104.37/24.44 inference(forward_subsumption_resolution,[status(thm)],[f9915,f178])).
% 104.37/24.44 fof(f9937,plain,(
% 104.37/24.44 ![X0]: (~r1(sK13_skl(sK19_skl),X0)|p2(X0)|p2(sK20_skl(sK13_skl(sK19_skl))))),
% 104.37/24.44 inference(resolution,[status(thm)],[f9916,f188])).
% 104.37/24.44 fof(f9951,plain,(
% 104.37/24.44 p2(sK20_skl(sK13_skl(sK19_skl)))|p2(sK20_skl(sK13_skl(sK19_skl)))),
% 104.37/24.44 inference(resolution,[status(thm)],[f9937,f188])).
% 104.37/24.44 fof(f9953,plain,(
% 104.37/24.44 p2(sK20_skl(sK13_skl(sK19_skl)))),
% 104.37/24.44 inference(duplicate_literals_removal,[status(thm)],[f9951])).
% 104.37/24.44 fof(f9954,plain,(
% 104.37/24.44 ~r1(sK19_skl,sK13_skl(sK19_skl))),
% 104.37/24.44 inference(resolution,[status(thm)],[f9953,f41])).
% 104.37/24.44 fof(f9961,plain,(
% 104.37/24.44 $false),
% 104.37/24.44 inference(forward_subsumption_resolution,[status(thm)],[f9954,f178])).
% 104.37/24.44 % SZS output end CNFRefutation for theBenchmark.p
% 13.52/24.54 % Elapsed time: 24.131779 seconds
% 13.52/24.54 % CPU time: 190.347065 seconds
% 13.52/24.54 % Total memory used: 472.091 MB
% 13.52/24.54 % Net memory used: 451.503 MB
%------------------------------------------------------------------------------