%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS162+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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:00:21 PM UTC 2026
% Result : Theorem 0.12s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS162+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n013.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 22:54:37 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 0.12/0.38 % Refutation found
% 0.12/0.38 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.38 fof(f13,axiom,(
% 0.12/0.38 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f14,axiom,(
% 0.12/0.38 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f15,axiom,(
% 0.12/0.38 (! [X,Y] :( rp(X,Y)=> cA(Y) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f16,axiom,(
% 0.12/0.38 (! [X,Y] :( rq(X,Y)=> cB(Y) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f17,axiom,(
% 0.12/0.38 (! [X] :~ ( cB(X)& cA(X) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f18,axiom,(
% 0.12/0.38 (! [X,Y] :( rq(X,Y)=> rr(X,Y) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f19,axiom,(
% 0.12/0.38 (! [X,Y] :( rp(X,Y)=> rr(X,Y) ) )),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f20,conjecture,(
% 0.12/0.38 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& (! [X] :( ( (? [Y0,Y1] :( rp(X,Y0)& rp(X,Y1)& Y0 != Y1 ))& (? [Y0,Y1,Y2] :( rq(X,Y0)& rq(X,Y1)& rq(X,Y2)& Y0 != Y1& Y0 != Y2& Y1 != Y2 ) ))=> (? [Y0,Y1,Y2,Y3,Y4] :( rr(X,Y0)& rr(X,Y1)& rr(X,Y2)& rr(X,Y3)& rr(X,Y4)& Y0 != Y1& Y0 != Y2& Y0 != Y3& Y0 != Y4& Y1 != Y2& Y1 != Y3& Y1 != Y4& Y2 != Y3& Y2 != Y4& Y3 != Y4 ) )) )) ),
% 0.12/0.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.38 fof(f21,negated_conjecture,(
% 0.12/0.38 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& (! [X] :( ( (? [Y0,Y1] :( rp(X,Y0)& rp(X,Y1)& Y0 != Y1 ))& (? [Y0,Y1,Y2] :( rq(X,Y0)& rq(X,Y1)& rq(X,Y2)& Y0 != Y1& Y0 != Y2& Y1 != Y2 ) ))=> (? [Y0,Y1,Y2,Y3,Y4] :( rr(X,Y0)& rr(X,Y1)& rr(X,Y2)& rr(X,Y3)& rr(X,Y4)& Y0 != Y1& Y0 != Y2& Y0 != Y3& Y0 != Y4& Y1 != Y2& Y1 != Y3& Y1 != Y4& Y2 != Y3& Y2 != Y4& Y3 != Y4 ) )) )) )),
% 0.12/0.38 inference(negated_conjecture,[status(cth)],[f20])).
% 0.12/0.38 fof(f58,plain,(
% 0.12/0.38 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f13])).
% 0.12/0.38 fof(f59,plain,(
% 0.12/0.38 ![X0]: (cowlThing(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.38 fof(f60,plain,(
% 0.12/0.38 ![X0]: (~cowlNothing(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.38 fof(f61,plain,(
% 0.12/0.38 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.12/0.38 inference(NNF_transformation,[status(thm)],[f14])).
% 0.12/0.38 fof(f62,plain,(
% 0.12/0.38 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f61])).
% 0.12/0.38 fof(f63,plain,(
% 0.12/0.38 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f62])).
% 0.12/0.38 fof(f64,plain,(
% 0.12/0.38 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f62])).
% 0.12/0.38 fof(f65,plain,(
% 0.12/0.38 ![X,Y]: (~rp(X,Y)|cA(Y))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.12/0.38 fof(f66,plain,(
% 0.12/0.38 ![Y]: ((![X]: ~rp(X,Y))|cA(Y))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f65])).
% 0.12/0.38 fof(f67,plain,(
% 0.12/0.38 ![X0,X1]: (~rp(X0,X1)|cA(X1))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f66])).
% 0.12/0.38 fof(f68,plain,(
% 0.12/0.38 ![X,Y]: (~rq(X,Y)|cB(Y))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.12/0.38 fof(f69,plain,(
% 0.12/0.38 ![Y]: ((![X]: ~rq(X,Y))|cB(Y))),
% 0.12/0.38 inference(miniscoping,[status(thm)],[f68])).
% 0.12/0.38 fof(f70,plain,(
% 0.12/0.38 ![X0,X1]: (~rq(X0,X1)|cB(X1))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f69])).
% 0.12/0.38 fof(f71,plain,(
% 0.12/0.38 ![X]: (~cB(X)|~cA(X))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 0.12/0.38 fof(f72,plain,(
% 0.12/0.38 ![X0]: (~cB(X0)|~cA(X0))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f71])).
% 0.12/0.38 fof(f73,plain,(
% 0.12/0.38 ![X,Y]: (~rq(X,Y)|rr(X,Y))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 0.12/0.38 fof(f74,plain,(
% 0.12/0.38 ![X0,X1]: (~rq(X0,X1)|rr(X0,X1))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f73])).
% 0.12/0.38 fof(f75,plain,(
% 0.12/0.38 ![X,Y]: (~rp(X,Y)|rr(X,Y))),
% 0.12/0.38 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 0.12/0.38 fof(f76,plain,(
% 0.12/0.38 ![X0,X1]: (~rp(X0,X1)|rr(X0,X1))),
% 0.12/0.38 inference(cnf_transformation,[status(thm)],[f75])).
% 0.12/0.38 fof(f77,plain,(
% 0.12/0.38 (((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|(?[X]: (((?[Y0,Y1]: ((rp(X,Y0)&rp(X,Y1))&~Y0=Y1))&(?[Y0,Y1,Y2]: (((((rq(X,Y0)&rq(X,Y1))&rq(X,Y2))&~Y0=Y1)&~Y0=Y2)&~Y1=Y2)))&(![Y0,Y1,Y2,Y3,Y4]: ((((((((((((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|~rr(X,Y4))|Y0=Y1)|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4)))))),
% 0.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.12/0.39 fof(f78,definition,(
% 0.12/0.39 ![X]: (sP0_prd(X)<=>(xsd_string(X)<~>~xsd_integer(X)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.39 fof(f79,plain,(
% 0.12/0.39 ((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: sP0_prd(X)))|(?[X]: (((?[Y0,Y1]: ((rp(X,Y0)&rp(X,Y1))&~Y0=Y1))&(?[Y0,Y1,Y2]: (((((rq(X,Y0)&rq(X,Y1))&rq(X,Y2))&~Y0=Y1)&~Y0=Y2)&~Y1=Y2)))&(![Y0,Y1,Y2,Y3,Y4]: ((((((((((((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|~rr(X,Y4))|Y0=Y1)|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4))))),
% 0.12/0.39 inference(formula_renaming,[status(thm)],[f77,f78])).
% 0.12/0.39 fof(f80,plain,(
% 0.12/0.39 (((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: sP0_prd(X)))|(?[X]: (((?[Y0,Y1]: ((rp(X,Y0)&rp(X,Y1))&~Y0=Y1))&(?[Y1,Y2]: ((?[Y0]: ((((rq(X,Y0)&rq(X,Y1))&rq(X,Y2))&~Y0=Y1)&~Y0=Y2))&~Y1=Y2)))&(![Y3,Y4]: ((![Y2]: (((![Y1]: ((((![Y0]: ((((((((~rr(X,Y0)|~rr(X,Y1))|~rr(X,Y2))|~rr(X,Y3))|~rr(X,Y4))|Y0=Y1)|Y0=Y2)|Y0=Y3)|Y0=Y4))|Y1=Y2)|Y1=Y3)|Y1=Y4))|Y2=Y3)|Y2=Y4))|Y3=Y4))))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f79])).
% 0.12/0.39 fof(f81,plain,(
% 0.12/0.39 ((~cowlThing(sK0_skl)|cowlNothing(sK1_skl))|sP0_prd(sK2_skl))|((((rp(sK3_skl,sK4_skl)&rp(sK3_skl,sK5_skl))&~sK4_skl=sK5_skl)&(((((rq(sK3_skl,sK8_skl)&rq(sK3_skl,sK6_skl))&rq(sK3_skl,sK7_skl))&~sK8_skl=sK6_skl)&~sK8_skl=sK7_skl)&~sK6_skl=sK7_skl))&(![Y3,Y4]: ((![Y2]: (((![Y1]: ((((![Y0]: ((((((((~rr(sK3_skl,Y0)|~rr(sK3_skl,Y1))|~rr(sK3_skl,Y2))|~rr(sK3_skl,Y3))|~rr(sK3_skl,Y4))|Y0=Y1)|Y0=Y2)|Y0=Y3)|Y0=Y4))|Y1=Y2)|Y1=Y3)|Y1=Y4))|Y2=Y3)|Y2=Y4))|Y3=Y4)))),
% 0.12/0.39 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]),skolemize(X,sK0_skl),skolemize(X,sK1_skl),skolemize(X,sK2_skl),skolemize(X,sK3_skl),skolemize(Y0,sK4_skl),skolemize(Y1,sK5_skl),skolemize(Y1,sK6_skl),skolemize(Y2,sK7_skl),skolemize(Y0,sK8_skl)],[f80])).
% 0.12/0.39 fof(f82,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|rp(sK3_skl,sK4_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f83,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|rp(sK3_skl,sK5_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f84,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|~sK4_skl=sK5_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f85,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|rq(sK3_skl,sK8_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f86,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|rq(sK3_skl,sK6_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f87,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|rq(sK3_skl,sK7_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f88,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|~sK8_skl=sK6_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f89,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|~sK8_skl=sK7_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f90,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|~sK6_skl=sK7_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f91,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4]: (~cowlThing(sK0_skl)|cowlNothing(sK1_skl)|sP0_prd(sK2_skl)|~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|~rr(sK3_skl,X2)|~rr(sK3_skl,X3)|~rr(sK3_skl,X4)|X0=X1|X0=X2|X0=X3|X0=X4|X1=X2|X1=X3|X1=X4|X2=X3|X2=X4|X3=X4)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f81])).
% 0.12/0.39 fof(f92,plain,(
% 0.12/0.39 ![X]: ((~sP0_prd(X)|((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X))))&(sP0_prd(X)|((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))))),
% 0.12/0.39 inference(NNF_transformation,[status(thm)],[f78])).
% 0.12/0.39 fof(f93,plain,(
% 0.12/0.39 (![X]: (~sP0_prd(X)|((xsd_string(X)|~xsd_integer(X))&(~xsd_string(X)|xsd_integer(X)))))&(![X]: (sP0_prd(X)|((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f92])).
% 0.12/0.39 fof(f94,plain,(
% 0.12/0.39 ![X0]: (~sP0_prd(X0)|xsd_string(X0)|~xsd_integer(X0))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.39 fof(f95,plain,(
% 0.12/0.39 ![X0]: (~sP0_prd(X0)|~xsd_string(X0)|xsd_integer(X0))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f93])).
% 0.12/0.39 fof(f98,definition,(
% 0.12/0.39 sQ0_spl <=> (cowlThing(sK0_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f100,plain,(
% 0.12/0.39 ~cowlThing(sK0_skl)|sQ0_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f98])).
% 0.12/0.39 fof(f101,definition,(
% 0.12/0.39 sQ1_spl <=> (cowlNothing(sK1_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f102,plain,(
% 0.12/0.39 cowlNothing(sK1_skl)|~sQ1_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f101])).
% 0.12/0.39 fof(f104,definition,(
% 0.12/0.39 sQ2_spl <=> (sP0_prd(sK2_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f105,plain,(
% 0.12/0.39 sP0_prd(sK2_skl)|~sQ2_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f104])).
% 0.12/0.39 fof(f107,definition,(
% 0.12/0.39 sQ3_spl <=> (rp(sK3_skl,sK4_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f108,plain,(
% 0.12/0.39 rp(sK3_skl,sK4_skl)|~sQ3_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f107])).
% 0.12/0.39 fof(f110,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f82,f98,f101,f104,f107])).
% 0.12/0.39 fof(f111,definition,(
% 0.12/0.39 sQ4_spl <=> (rp(sK3_skl,sK5_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f112,plain,(
% 0.12/0.39 rp(sK3_skl,sK5_skl)|~sQ4_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f111])).
% 0.12/0.39 fof(f114,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ4_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f83,f98,f101,f104,f111])).
% 0.12/0.39 fof(f115,definition,(
% 0.12/0.39 sQ5_spl <=> (sK4_skl=sK5_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f118,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|~sQ5_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f84,f98,f101,f104,f115])).
% 0.12/0.39 fof(f119,definition,(
% 0.12/0.39 sQ6_spl <=> (rq(sK3_skl,sK8_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f120,plain,(
% 0.12/0.39 rq(sK3_skl,sK8_skl)|~sQ6_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f119])).
% 0.12/0.39 fof(f122,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ6_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f85,f98,f101,f104,f119])).
% 0.12/0.39 fof(f123,definition,(
% 0.12/0.39 sQ7_spl <=> (rq(sK3_skl,sK6_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f124,plain,(
% 0.12/0.39 rq(sK3_skl,sK6_skl)|~sQ7_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f123])).
% 0.12/0.39 fof(f126,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ7_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f86,f98,f101,f104,f123])).
% 0.12/0.39 fof(f127,definition,(
% 0.12/0.39 sQ8_spl <=> (rq(sK3_skl,sK7_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f128,plain,(
% 0.12/0.39 rq(sK3_skl,sK7_skl)|~sQ8_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f127])).
% 0.12/0.39 fof(f130,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ8_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f87,f98,f101,f104,f127])).
% 0.12/0.39 fof(f131,definition,(
% 0.12/0.39 sQ9_spl <=> (sK8_skl=sK6_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f134,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|~sQ9_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f88,f98,f101,f104,f131])).
% 0.12/0.39 fof(f135,definition,(
% 0.12/0.39 sQ10_spl <=> (sK8_skl=sK7_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f138,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|~sQ10_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f89,f98,f101,f104,f135])).
% 0.12/0.39 fof(f139,definition,(
% 0.12/0.39 sQ11_spl <=> (sK6_skl=sK7_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f142,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|~sQ11_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f90,f98,f101,f104,f139])).
% 0.12/0.39 fof(f143,definition,(
% 0.12/0.39 ![X0,X1,X2,X3,X4]: (sQ12_spl <=> (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|~rr(sK3_skl,X2)|~rr(sK3_skl,X3)|~rr(sK3_skl,X4)|X0=X1|X0=X2|X0=X3|X0=X4|X1=X2|X1=X3|X1=X4|X2=X3|X2=X4|X3=X4))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f144,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4]: (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|~rr(sK3_skl,X2)|~rr(sK3_skl,X3)|~rr(sK3_skl,X4)|X0=X1|X0=X2|X0=X3|X0=X4|X1=X2|X1=X3|X1=X4|X2=X3|X2=X4|X3=X4|~sQ12_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f143])).
% 0.12/0.39 fof(f146,plain,(
% 0.12/0.39 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ12_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f91,f98,f101,f104,f143])).
% 0.12/0.39 fof(f147,plain,(
% 0.12/0.39 ![X0]: (~sP0_prd(X0)|~xsd_integer(X0))),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f94,f63])).
% 0.12/0.39 fof(f148,plain,(
% 0.12/0.39 ![X0]: (~sP0_prd(X0))),
% 0.12/0.39 inference(backward_subsumption_resolution,[status(thm)],[f147,f149])).
% 0.12/0.39 fof(f149,plain,(
% 0.12/0.39 ![X0]: (~sP0_prd(X0)|xsd_integer(X0))),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f95,f64])).
% 0.12/0.39 fof(f150,plain,(
% 0.12/0.39 $false|~sQ2_spl),
% 0.12/0.39 inference(backward_subsumption_resolution,[status(thm)],[f105,f148])).
% 0.12/0.39 fof(f151,plain,(
% 0.12/0.39 ~sQ2_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f150])).
% 0.12/0.39 fof(f152,plain,(
% 0.12/0.39 $false|~sQ1_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f102,f60])).
% 0.12/0.39 fof(f153,plain,(
% 0.12/0.39 ~sQ1_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f152])).
% 0.12/0.39 fof(f154,plain,(
% 0.12/0.39 $false|sQ0_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f100,f59])).
% 0.12/0.39 fof(f155,plain,(
% 0.12/0.39 sQ0_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f154])).
% 0.12/0.39 fof(f156,plain,(
% 0.12/0.39 rr(sK3_skl,sK5_skl)|~sQ4_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f76,f112])).
% 0.12/0.39 fof(f157,plain,(
% 0.12/0.39 rr(sK3_skl,sK4_skl)|~sQ3_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f76,f108])).
% 0.12/0.39 fof(f158,plain,(
% 0.12/0.39 cA(sK5_skl)|~sQ4_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f67,f112])).
% 0.12/0.39 fof(f159,plain,(
% 0.12/0.39 cA(sK4_skl)|~sQ3_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f67,f108])).
% 0.12/0.39 fof(f160,plain,(
% 0.12/0.39 cB(sK8_skl)|~sQ6_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f120,f70])).
% 0.12/0.39 fof(f161,plain,(
% 0.12/0.39 rr(sK3_skl,sK8_skl)|~sQ6_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f120,f74])).
% 0.12/0.39 fof(f162,plain,(
% 0.12/0.39 cB(sK6_skl)|~sQ7_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f124,f70])).
% 0.12/0.39 fof(f163,plain,(
% 0.12/0.39 rr(sK3_skl,sK6_skl)|~sQ7_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f124,f74])).
% 0.12/0.39 fof(f164,plain,(
% 0.12/0.39 cB(sK7_skl)|~sQ8_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f128,f70])).
% 0.12/0.39 fof(f165,plain,(
% 0.12/0.39 rr(sK3_skl,sK7_skl)|~sQ8_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f128,f74])).
% 0.12/0.39 fof(f185,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|~rr(sK3_skl,X2)|~rr(sK3_skl,X3)|sK4_skl=X0|sK4_skl=X1|sK4_skl=X2|sK4_skl=X3|X0=X1|X0=X2|X0=X3|X1=X2|X1=X3|X2=X3|~sQ3_spl|~sQ12_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f157,f144])).
% 0.12/0.39 fof(f225,plain,(
% 0.12/0.39 ~cA(sK8_skl)|~sQ6_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f160,f72])).
% 0.12/0.39 fof(f226,plain,(
% 0.12/0.39 ~cA(sK6_skl)|~sQ7_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f162,f72])).
% 0.12/0.39 fof(f227,plain,(
% 0.12/0.39 ~cA(sK7_skl)|~sQ8_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f164,f72])).
% 0.12/0.39 fof(f229,plain,(
% 0.12/0.39 ![X0,X1,X2]: (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|~rr(sK3_skl,X2)|sK4_skl=sK8_skl|sK4_skl=X0|sK4_skl=X1|sK4_skl=X2|sK8_skl=X0|sK8_skl=X1|sK8_skl=X2|X0=X1|X0=X2|X1=X2|~sQ6_spl|~sQ3_spl|~sQ12_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f161,f185])).
% 0.12/0.39 fof(f235,definition,(
% 0.12/0.39 sQ24_spl <=> (sK4_skl=sK8_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f236,plain,(
% 0.12/0.39 sK4_skl=sK8_skl|~sQ24_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f235])).
% 0.12/0.39 fof(f238,definition,(
% 0.12/0.39 sQ25_spl <=> (sK5_skl=sK8_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f239,plain,(
% 0.12/0.39 sK5_skl=sK8_skl|~sQ25_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f238])).
% 0.12/0.39 fof(f242,definition,(
% 0.12/0.39 ![X0,X1,X2]: (sQ26_spl <=> (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|~rr(sK3_skl,X2)|sK4_skl=X0|sK4_skl=X1|sK4_skl=X2|sK8_skl=X0|sK8_skl=X1|sK8_skl=X2|X0=X1|X0=X2|X1=X2))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f243,plain,(
% 0.12/0.39 ![X0,X1,X2]: (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|~rr(sK3_skl,X2)|sK4_skl=X0|sK4_skl=X1|sK4_skl=X2|sK8_skl=X0|sK8_skl=X1|sK8_skl=X2|X0=X1|X0=X2|X1=X2|~sQ26_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f242])).
% 0.12/0.39 fof(f245,plain,(
% 0.12/0.39 sQ26_spl|sQ24_spl|~sQ6_spl|~sQ3_spl|~sQ12_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f229,f242,f235,f119,f107,f143])).
% 0.12/0.39 fof(f251,plain,(
% 0.12/0.39 ~cA(sK4_skl)|~sQ24_spl|~sQ6_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f236,f225])).
% 0.12/0.39 fof(f265,plain,(
% 0.12/0.39 ![X0,X1]: (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|sK4_skl=sK5_skl|sK4_skl=X0|sK4_skl=X1|sK8_skl=sK5_skl|sK8_skl=X0|sK8_skl=X1|sK5_skl=X0|sK5_skl=X1|X0=X1|~sQ26_spl|~sQ4_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f243,f156])).
% 0.12/0.39 fof(f270,definition,(
% 0.12/0.39 ![X0,X1]: (sQ29_spl <=> (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|sK4_skl=X0|sK4_skl=X1|sK8_skl=X0|sK8_skl=X1|sK5_skl=X0|sK5_skl=X1|X0=X1))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f271,plain,(
% 0.12/0.39 ![X0,X1]: (~rr(sK3_skl,X0)|~rr(sK3_skl,X1)|sK4_skl=X0|sK4_skl=X1|sK8_skl=X0|sK8_skl=X1|sK5_skl=X0|sK5_skl=X1|X0=X1|~sQ29_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f270])).
% 0.12/0.39 fof(f273,plain,(
% 0.12/0.39 sQ29_spl|sQ5_spl|sQ25_spl|~sQ26_spl|~sQ4_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f265,f270,f115,f238,f242,f111])).
% 0.12/0.39 fof(f274,plain,(
% 0.12/0.39 $false|~sQ3_spl|~sQ24_spl|~sQ6_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f251,f159])).
% 0.12/0.39 fof(f275,plain,(
% 0.12/0.39 ~sQ3_spl|~sQ24_spl|~sQ6_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f274])).
% 0.12/0.39 fof(f281,plain,(
% 0.12/0.39 ~cA(sK5_skl)|~sQ25_spl|~sQ6_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f239,f225])).
% 0.12/0.39 fof(f290,plain,(
% 0.12/0.39 $false|~sQ4_spl|~sQ25_spl|~sQ6_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f281,f158])).
% 0.12/0.39 fof(f291,plain,(
% 0.12/0.39 ~sQ4_spl|~sQ25_spl|~sQ6_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f290])).
% 0.12/0.39 fof(f329,plain,(
% 0.12/0.39 ![X0]: (~rr(sK3_skl,X0)|sK4_skl=sK6_skl|sK4_skl=X0|sK8_skl=sK6_skl|sK8_skl=X0|sK5_skl=sK6_skl|sK5_skl=X0|sK6_skl=X0|~sQ7_spl|~sQ29_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f163,f271])).
% 0.12/0.39 fof(f337,definition,(
% 0.12/0.39 ![X0]: (sQ35_spl <=> (~rr(sK3_skl,X0)|sK4_skl=X0|sK8_skl=X0|sK5_skl=X0|sK6_skl=X0))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f338,plain,(
% 0.12/0.39 ![X0]: (~rr(sK3_skl,X0)|sK4_skl=X0|sK8_skl=X0|sK5_skl=X0|sK6_skl=X0|~sQ35_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f337])).
% 0.12/0.39 fof(f340,definition,(
% 0.12/0.39 sQ36_spl <=> (sK4_skl=sK6_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f341,plain,(
% 0.12/0.39 sK4_skl=sK6_skl|~sQ36_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f340])).
% 0.12/0.39 fof(f343,definition,(
% 0.12/0.39 sQ37_spl <=> (sK5_skl=sK6_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f344,plain,(
% 0.12/0.39 sK5_skl=sK6_skl|~sQ37_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f343])).
% 0.12/0.39 fof(f346,plain,(
% 0.12/0.39 sQ35_spl|sQ36_spl|sQ9_spl|sQ37_spl|~sQ7_spl|~sQ29_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f329,f337,f340,f131,f343,f123,f270])).
% 0.12/0.39 fof(f373,plain,(
% 0.12/0.39 ~cA(sK5_skl)|~sQ37_spl|~sQ7_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f344,f226])).
% 0.12/0.39 fof(f382,plain,(
% 0.12/0.39 $false|~sQ4_spl|~sQ37_spl|~sQ7_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f373,f158])).
% 0.12/0.39 fof(f383,plain,(
% 0.12/0.39 ~sQ4_spl|~sQ37_spl|~sQ7_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f382])).
% 0.12/0.39 fof(f391,plain,(
% 0.12/0.39 ~cA(sK4_skl)|~sQ36_spl|~sQ7_spl),
% 0.12/0.39 inference(forward_demodulation,[status(thm)],[f341,f226])).
% 0.12/0.39 fof(f392,plain,(
% 0.12/0.39 $false|~sQ3_spl|~sQ36_spl|~sQ7_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f391,f159])).
% 0.12/0.39 fof(f393,plain,(
% 0.12/0.39 ~sQ3_spl|~sQ36_spl|~sQ7_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f392])).
% 0.12/0.39 fof(f450,plain,(
% 0.12/0.39 sK4_skl=sK7_skl|sK8_skl=sK7_skl|sK5_skl=sK7_skl|sK6_skl=sK7_skl|~sQ8_spl|~sQ35_spl),
% 0.12/0.39 inference(resolution,[status(thm)],[f165,f338])).
% 0.12/0.39 fof(f467,definition,(
% 0.12/0.39 sQ51_spl <=> (sK5_skl=sK7_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f468,plain,(
% 0.12/0.39 sK5_skl=sK7_skl|~sQ51_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f467])).
% 0.12/0.39 fof(f474,definition,(
% 0.12/0.39 sQ53_spl <=> (sK4_skl=sK7_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f475,plain,(
% 0.12/0.39 sK4_skl=sK7_skl|~sQ53_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f474])).
% 0.12/0.39 fof(f478,plain,(
% 0.12/0.39 sQ53_spl|sQ10_spl|sQ51_spl|sQ11_spl|~sQ8_spl|~sQ35_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f450,f474,f135,f467,f139,f127,f337])).
% 0.12/0.39 fof(f530,plain,(
% 0.12/0.39 ~cA(sK5_skl)|~sQ51_spl|~sQ8_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f468,f227])).
% 0.12/0.39 fof(f543,plain,(
% 0.12/0.39 $false|~sQ4_spl|~sQ51_spl|~sQ8_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f530,f158])).
% 0.12/0.39 fof(f544,plain,(
% 0.12/0.39 ~sQ4_spl|~sQ51_spl|~sQ8_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f543])).
% 0.12/0.39 fof(f556,plain,(
% 0.12/0.39 ~cA(sK4_skl)|~sQ53_spl|~sQ8_spl),
% 0.12/0.39 inference(forward_demodulation,[status(thm)],[f475,f227])).
% 0.12/0.39 fof(f557,plain,(
% 0.12/0.39 $false|~sQ3_spl|~sQ53_spl|~sQ8_spl),
% 0.12/0.39 inference(forward_subsumption_resolution,[status(thm)],[f556,f159])).
% 0.12/0.39 fof(f558,plain,(
% 0.12/0.39 ~sQ3_spl|~sQ53_spl|~sQ8_spl),
% 0.12/0.39 inference(contradiction_clause,[status(thm)],[f557])).
% 0.12/0.39 fof(f559,plain,(
% 0.12/0.39 $false),
% 0.12/0.39 inference(sat_refutation,[status(thm)],[f110,f114,f118,f122,f126,f130,f134,f138,f142,f146,f151,f153,f155,f245,f273,f275,f291,f346,f383,f393,f478,f544,f558])).
% 0.12/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.41 % Elapsed time: 0.051068 seconds
% 0.12/0.41 % CPU time: 0.187151 seconds
% 0.12/0.41 % Total memory used: 81.913 MB
% 0.12/0.41 % Net memory used: 81.573 MB
%------------------------------------------------------------------------------