%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS144+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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:19 PM UTC 2026
% Result : Theorem 0.09s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS144+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 22:56:43 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.09/0.40 % Refutation found
% 0.09/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.40 fof(f8,axiom,(
% 0.09/0.40 (! [X] :( cowlThing(X)& ~ cowlNothing(X) ) )),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f9,axiom,(
% 0.09/0.40 (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ) )),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f10,axiom,(
% 0.09/0.40 (! [X] :( cc(X)=> ( (? [Y0,Y1] :( rp(X,Y0)& rp(X,Y1)& Y0 != Y1 ))& (! [Y0,Y1,Y2] :( ( rp(X,Y0)& rp(X,Y1)& rp(X,Y2) )=> ( Y0 = Y1| Y0 = Y2| Y1 = Y2 ) ) )) ) )),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f11,conjecture,(
% 0.09/0.40 ( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& (! [X] :( cc(X)=> (! [Y0,Y1,Y2] :( ( rp(X,Y0)& rp(X,Y1)& rp(X,Y2) )=> ( Y0 = Y1| Y0 = Y2| Y1 = Y2 ) ) )))& (! [X] :( cc(X)=> (? [Y0,Y1] :( rp(X,Y0)& rp(X,Y1)& Y0 != Y1 ) )) )) ),
% 0.09/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.40 fof(f12,negated_conjecture,(
% 0.09/0.40 ~(( (! [X] :( cowlThing(X)& ~ cowlNothing(X) ))& (! [X] :( xsd_string(X)<=> ~ xsd_integer(X) ))& (! [X] :( cc(X)=> (! [Y0,Y1,Y2] :( ( rp(X,Y0)& rp(X,Y1)& rp(X,Y2) )=> ( Y0 = Y1| Y0 = Y2| Y1 = Y2 ) ) )))& (! [X] :( cc(X)=> (? [Y0,Y1] :( rp(X,Y0)& rp(X,Y1)& Y0 != Y1 ) )) )) )),
% 0.09/0.40 inference(negated_conjecture,[status(cth)],[f11])).
% 0.09/0.40 fof(f34,plain,(
% 0.09/0.40 (![X]: cowlThing(X))&(![X]: ~cowlNothing(X))),
% 0.09/0.40 inference(miniscoping,[status(thm)],[f8])).
% 0.09/0.40 fof(f35,plain,(
% 0.09/0.40 ![X0]: (cowlThing(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f34])).
% 0.09/0.40 fof(f36,plain,(
% 0.09/0.40 ![X0]: (~cowlNothing(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f34])).
% 0.09/0.40 fof(f37,plain,(
% 0.09/0.40 ![X]: ((~xsd_string(X)|~xsd_integer(X))&(xsd_string(X)|xsd_integer(X)))),
% 0.09/0.40 inference(NNF_transformation,[status(thm)],[f9])).
% 0.09/0.40 fof(f38,plain,(
% 0.09/0.40 (![X]: (~xsd_string(X)|~xsd_integer(X)))&(![X]: (xsd_string(X)|xsd_integer(X)))),
% 0.09/0.40 inference(miniscoping,[status(thm)],[f37])).
% 0.09/0.40 fof(f39,plain,(
% 0.09/0.40 ![X0]: (~xsd_string(X0)|~xsd_integer(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f38])).
% 0.09/0.40 fof(f40,plain,(
% 0.09/0.40 ![X0]: (xsd_string(X0)|xsd_integer(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f38])).
% 0.09/0.40 fof(f41,plain,(
% 0.09/0.40 ![X]: (~cc(X)|((?[Y0,Y1]: ((rp(X,Y0)&rp(X,Y1))&~Y0=Y1))&(![Y0,Y1,Y2]: (((~rp(X,Y0)|~rp(X,Y1))|~rp(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2)))))),
% 0.09/0.40 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.09/0.40 fof(f42,plain,(
% 0.09/0.40 ![X]: (~cc(X)|(((rp(X,sK0_skl(X))&rp(X,sK1_skl(X)))&~sK0_skl(X)=sK1_skl(X))&(![Y0,Y1,Y2]: (((~rp(X,Y0)|~rp(X,Y1))|~rp(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2)))))),
% 0.09/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y0,sK0_skl(X)),skolemize(Y1,sK1_skl(X))],[f41])).
% 0.09/0.40 fof(f43,plain,(
% 0.09/0.40 ![X0]: (~cc(X0)|rp(X0,sK0_skl(X0)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.40 fof(f44,plain,(
% 0.09/0.40 ![X0]: (~cc(X0)|rp(X0,sK1_skl(X0)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.40 fof(f45,plain,(
% 0.09/0.40 ![X0]: (~cc(X0)|~sK0_skl(X0)=sK1_skl(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.40 fof(f46,plain,(
% 0.09/0.40 ![X0,X1,X2,X3]: (~cc(X0)|~rp(X0,X1)|~rp(X0,X2)|~rp(X0,X3)|X1=X2|X1=X3|X2=X3)),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.40 fof(f47,plain,(
% 0.09/0.40 ((((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: (xsd_string(X)<~>~xsd_integer(X))))|(?[X]: (cc(X)&(?[Y0,Y1,Y2]: (((rp(X,Y0)&rp(X,Y1))&rp(X,Y2))&((~Y0=Y1&~Y0=Y2)&~Y1=Y2))))))|(?[X]: (cc(X)&(![Y0,Y1]: ((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1)))))),
% 0.09/0.40 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.09/0.40 fof(f48,definition,(
% 0.09/0.40 ![X]: (sP0_prd(X)<=>(xsd_string(X)<~>~xsd_integer(X)))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.09/0.40 fof(f49,definition,(
% 0.09/0.40 ![X]: (sP1_prd(X)<=>(cc(X)&(?[Y0,Y1,Y2]: (((rp(X,Y0)&rp(X,Y1))&rp(X,Y2))&((~Y0=Y1&~Y0=Y2)&~Y1=Y2)))))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.09/0.40 fof(f50,plain,(
% 0.09/0.40 (((?[X]: (~cowlThing(X)|cowlNothing(X)))|(?[X]: sP0_prd(X)))|(?[X]: sP1_prd(X)))|(?[X]: (cc(X)&(![Y0,Y1]: ((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1))))),
% 0.09/0.40 inference(formula_renaming,[status(thm)],[f47,f49,f48])).
% 0.09/0.40 fof(f51,plain,(
% 0.09/0.40 ((((?[X]: ~cowlThing(X))|(?[X]: cowlNothing(X)))|(?[X]: sP0_prd(X)))|(?[X]: sP1_prd(X)))|(?[X]: (cc(X)&(![Y0,Y1]: ((~rp(X,Y0)|~rp(X,Y1))|Y0=Y1))))),
% 0.09/0.40 inference(miniscoping,[status(thm)],[f50])).
% 0.09/0.40 fof(f52,plain,(
% 0.09/0.40 (((~cowlThing(sK2_skl)|cowlNothing(sK3_skl))|sP0_prd(sK4_skl))|sP1_prd(sK5_skl))|(cc(sK6_skl)&(![Y0,Y1]: ((~rp(sK6_skl,Y0)|~rp(sK6_skl,Y1))|Y0=Y1)))),
% 0.09/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl]),skolemize(X,sK2_skl),skolemize(X,sK3_skl),skolemize(X,sK4_skl),skolemize(X,sK5_skl),skolemize(X,sK6_skl)],[f51])).
% 0.09/0.40 fof(f53,plain,(
% 0.09/0.40 ~cowlThing(sK2_skl)|cowlNothing(sK3_skl)|sP0_prd(sK4_skl)|sP1_prd(sK5_skl)|cc(sK6_skl)),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f52])).
% 0.09/0.40 fof(f54,plain,(
% 0.09/0.40 ![X0,X1]: (~cowlThing(sK2_skl)|cowlNothing(sK3_skl)|sP0_prd(sK4_skl)|sP1_prd(sK5_skl)|~rp(sK6_skl,X0)|~rp(sK6_skl,X1)|X0=X1)),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f52])).
% 0.09/0.40 fof(f55,plain,(
% 0.09/0.40 ![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.09/0.40 inference(NNF_transformation,[status(thm)],[f48])).
% 0.09/0.40 fof(f56,plain,(
% 0.09/0.40 (![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.09/0.40 inference(miniscoping,[status(thm)],[f55])).
% 0.09/0.40 fof(f57,plain,(
% 0.09/0.40 ![X0]: (~sP0_prd(X0)|xsd_string(X0)|~xsd_integer(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f56])).
% 0.09/0.40 fof(f58,plain,(
% 0.09/0.40 ![X0]: (~sP0_prd(X0)|~xsd_string(X0)|xsd_integer(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f56])).
% 0.09/0.40 fof(f61,plain,(
% 0.09/0.40 ![X]: ((~sP1_prd(X)|(cc(X)&(?[Y0,Y1,Y2]: (((rp(X,Y0)&rp(X,Y1))&rp(X,Y2))&((~Y0=Y1&~Y0=Y2)&~Y1=Y2)))))&(sP1_prd(X)|(~cc(X)|(![Y0,Y1,Y2]: (((~rp(X,Y0)|~rp(X,Y1))|~rp(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2))))))),
% 0.09/0.40 inference(NNF_transformation,[status(thm)],[f49])).
% 0.09/0.40 fof(f62,plain,(
% 0.09/0.40 (![X]: (~sP1_prd(X)|(cc(X)&(?[Y0,Y1,Y2]: (((rp(X,Y0)&rp(X,Y1))&rp(X,Y2))&((~Y0=Y1&~Y0=Y2)&~Y1=Y2))))))&(![X]: (sP1_prd(X)|(~cc(X)|(![Y0,Y1,Y2]: (((~rp(X,Y0)|~rp(X,Y1))|~rp(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2))))))),
% 0.09/0.40 inference(miniscoping,[status(thm)],[f61])).
% 0.09/0.40 fof(f63,plain,(
% 0.09/0.40 (![X]: (~sP1_prd(X)|(cc(X)&(((rp(X,sK7_skl(X))&rp(X,sK8_skl(X)))&rp(X,sK9_skl(X)))&((~sK7_skl(X)=sK8_skl(X)&~sK7_skl(X)=sK9_skl(X))&~sK8_skl(X)=sK9_skl(X))))))&(![X]: (sP1_prd(X)|(~cc(X)|(![Y0,Y1,Y2]: (((~rp(X,Y0)|~rp(X,Y1))|~rp(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2))))))),
% 0.09/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl,sK9_skl]),skolemize(Y0,sK7_skl(X)),skolemize(Y1,sK8_skl(X)),skolemize(Y2,sK9_skl(X))],[f62])).
% 0.09/0.40 fof(f64,plain,(
% 0.09/0.40 ![X0]: (~sP1_prd(X0)|cc(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.40 fof(f65,plain,(
% 0.09/0.40 ![X0]: (~sP1_prd(X0)|rp(X0,sK7_skl(X0)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.40 fof(f66,plain,(
% 0.09/0.40 ![X0]: (~sP1_prd(X0)|rp(X0,sK8_skl(X0)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.40 fof(f67,plain,(
% 0.09/0.40 ![X0]: (~sP1_prd(X0)|rp(X0,sK9_skl(X0)))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.40 fof(f68,plain,(
% 0.09/0.40 ![X0]: (~sP1_prd(X0)|~sK7_skl(X0)=sK8_skl(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.40 fof(f69,plain,(
% 0.09/0.40 ![X0]: (~sP1_prd(X0)|~sK7_skl(X0)=sK9_skl(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.40 fof(f70,plain,(
% 0.09/0.40 ![X0]: (~sP1_prd(X0)|~sK8_skl(X0)=sK9_skl(X0))),
% 0.09/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.09/0.40 fof(f72,definition,(
% 0.09/0.40 sQ0_spl <=> (cowlThing(sK2_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f74,plain,(
% 0.09/0.40 ~cowlThing(sK2_skl)|sQ0_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f72])).
% 0.09/0.40 fof(f75,definition,(
% 0.09/0.40 sQ1_spl <=> (cowlNothing(sK3_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f76,plain,(
% 0.09/0.40 cowlNothing(sK3_skl)|~sQ1_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f75])).
% 0.09/0.40 fof(f78,definition,(
% 0.09/0.40 sQ2_spl <=> (sP0_prd(sK4_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f79,plain,(
% 0.09/0.40 sP0_prd(sK4_skl)|~sQ2_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f78])).
% 0.09/0.40 fof(f81,definition,(
% 0.09/0.40 sQ3_spl <=> (sP1_prd(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f82,plain,(
% 0.09/0.40 sP1_prd(sK5_skl)|~sQ3_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f81])).
% 0.09/0.40 fof(f84,definition,(
% 0.09/0.40 sQ4_spl <=> (cc(sK6_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f85,plain,(
% 0.09/0.40 cc(sK6_skl)|~sQ4_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f84])).
% 0.09/0.40 fof(f87,plain,(
% 0.09/0.40 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ4_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f53,f72,f75,f78,f81,f84])).
% 0.09/0.40 fof(f88,definition,(
% 0.09/0.40 ![X0,X1]: (sQ5_spl <=> (~rp(sK6_skl,X0)|~rp(sK6_skl,X1)|X0=X1))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f89,plain,(
% 0.09/0.40 ![X0,X1]: (~rp(sK6_skl,X0)|~rp(sK6_skl,X1)|X0=X1|~sQ5_spl)),
% 0.09/0.40 inference(component_clause,[status(thm)],[f88])).
% 0.09/0.40 fof(f91,plain,(
% 0.09/0.40 ~sQ0_spl|sQ1_spl|sQ2_spl|sQ3_spl|sQ5_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f54,f72,f75,f78,f81,f88])).
% 0.09/0.40 fof(f92,plain,(
% 0.09/0.40 ![X0]: (~sP0_prd(X0)|~xsd_integer(X0))),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f57,f39])).
% 0.09/0.40 fof(f93,plain,(
% 0.09/0.40 ![X0]: (~sP0_prd(X0))),
% 0.09/0.40 inference(backward_subsumption_resolution,[status(thm)],[f92,f94])).
% 0.09/0.40 fof(f94,plain,(
% 0.09/0.40 ![X0]: (~sP0_prd(X0)|xsd_integer(X0))),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f58,f40])).
% 0.09/0.40 fof(f95,plain,(
% 0.09/0.40 ~sK7_skl(sK5_skl)=sK8_skl(sK5_skl)|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f82,f68])).
% 0.09/0.40 fof(f96,plain,(
% 0.09/0.40 rp(sK5_skl,sK9_skl(sK5_skl))|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f82,f67])).
% 0.09/0.40 fof(f97,plain,(
% 0.09/0.40 rp(sK5_skl,sK8_skl(sK5_skl))|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f82,f66])).
% 0.09/0.40 fof(f98,plain,(
% 0.09/0.40 rp(sK5_skl,sK7_skl(sK5_skl))|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f82,f65])).
% 0.09/0.40 fof(f99,plain,(
% 0.09/0.40 cc(sK5_skl)|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f82,f64])).
% 0.09/0.40 fof(f100,plain,(
% 0.09/0.40 rp(sK5_skl,sK0_skl(sK5_skl))|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f43,f99])).
% 0.09/0.40 fof(f101,plain,(
% 0.09/0.40 rp(sK5_skl,sK1_skl(sK5_skl))|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f44,f99])).
% 0.09/0.40 fof(f102,plain,(
% 0.09/0.40 ~sK0_skl(sK5_skl)=sK1_skl(sK5_skl)|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f45,f99])).
% 0.09/0.40 fof(f103,plain,(
% 0.09/0.40 ~sK7_skl(sK5_skl)=sK9_skl(sK5_skl)|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f69,f82])).
% 0.09/0.40 fof(f104,plain,(
% 0.09/0.40 ~sK8_skl(sK5_skl)=sK9_skl(sK5_skl)|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f70,f82])).
% 0.09/0.40 fof(f106,plain,(
% 0.09/0.40 ![X0,X1]: (~cc(sK5_skl)|~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK9_skl(sK5_skl)=X0|sK9_skl(sK5_skl)=X1|X0=X1|~sQ3_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f46,f96])).
% 0.09/0.40 fof(f107,definition,(
% 0.09/0.40 sQ6_spl <=> (cc(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f109,plain,(
% 0.09/0.40 ~cc(sK5_skl)|sQ6_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f107])).
% 0.09/0.40 fof(f110,definition,(
% 0.09/0.40 ![X0,X1]: (sQ7_spl <=> (~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK9_skl(sK5_skl)=X0|sK9_skl(sK5_skl)=X1|X0=X1))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f111,plain,(
% 0.09/0.40 ![X0,X1]: (~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK9_skl(sK5_skl)=X0|sK9_skl(sK5_skl)=X1|X0=X1|~sQ7_spl)),
% 0.09/0.40 inference(component_clause,[status(thm)],[f110])).
% 0.09/0.40 fof(f113,plain,(
% 0.09/0.40 ~sQ6_spl|sQ7_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f106,f107,f110,f81])).
% 0.09/0.40 fof(f114,plain,(
% 0.09/0.40 $false|~sQ2_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f79,f93])).
% 0.09/0.40 fof(f115,plain,(
% 0.09/0.40 ~sQ2_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f114])).
% 0.09/0.40 fof(f116,plain,(
% 0.09/0.40 $false|~sQ1_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f76,f36])).
% 0.09/0.40 fof(f117,plain,(
% 0.09/0.40 ~sQ1_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f116])).
% 0.09/0.40 fof(f118,plain,(
% 0.09/0.40 $false|sQ0_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f74,f35])).
% 0.09/0.40 fof(f119,plain,(
% 0.09/0.40 sQ0_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f118])).
% 0.09/0.40 fof(f120,plain,(
% 0.09/0.40 $false|sQ6_spl|~sQ3_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f99,f109])).
% 0.09/0.40 fof(f121,plain,(
% 0.09/0.40 sQ6_spl|~sQ3_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f120])).
% 0.09/0.40 fof(f122,plain,(
% 0.09/0.40 ~sK0_skl(sK6_skl)=sK1_skl(sK6_skl)|~sQ4_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f85,f45])).
% 0.09/0.40 fof(f123,plain,(
% 0.09/0.40 rp(sK6_skl,sK1_skl(sK6_skl))|~sQ4_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f85,f44])).
% 0.09/0.40 fof(f124,plain,(
% 0.09/0.40 rp(sK6_skl,sK0_skl(sK6_skl))|~sQ4_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f85,f43])).
% 0.09/0.40 fof(f125,plain,(
% 0.09/0.40 ![X0]: (~rp(sK6_skl,X0)|sK1_skl(sK6_skl)=X0|~sQ4_spl|~sQ5_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f123,f89])).
% 0.09/0.40 fof(f141,plain,(
% 0.09/0.40 ![X0]: (~rp(sK5_skl,X0)|sK9_skl(sK5_skl)=sK0_skl(sK5_skl)|sK9_skl(sK5_skl)=X0|sK0_skl(sK5_skl)=X0|~sQ3_spl|~sQ7_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f100,f111])).
% 0.09/0.40 fof(f142,plain,(
% 0.09/0.40 ![X0,X1]: (~cc(sK5_skl)|~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK0_skl(sK5_skl)=X0|sK0_skl(sK5_skl)=X1|X0=X1|~sQ3_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f100,f46])).
% 0.09/0.40 fof(f143,definition,(
% 0.09/0.40 ![X0]: (sQ9_spl <=> (~rp(sK5_skl,X0)|sK9_skl(sK5_skl)=X0|sK0_skl(sK5_skl)=X0))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f144,plain,(
% 0.09/0.40 ![X0]: (~rp(sK5_skl,X0)|sK9_skl(sK5_skl)=X0|sK0_skl(sK5_skl)=X0|~sQ9_spl)),
% 0.09/0.40 inference(component_clause,[status(thm)],[f143])).
% 0.09/0.40 fof(f146,definition,(
% 0.09/0.40 sQ10_spl <=> (sK9_skl(sK5_skl)=sK0_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f147,plain,(
% 0.09/0.40 sK9_skl(sK5_skl)=sK0_skl(sK5_skl)|~sQ10_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f146])).
% 0.09/0.40 fof(f149,plain,(
% 0.09/0.40 sQ9_spl|sQ10_spl|~sQ3_spl|~sQ7_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f141,f143,f146,f81,f110])).
% 0.09/0.40 fof(f150,definition,(
% 0.09/0.40 ![X0,X1]: (sQ11_spl <=> (~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK0_skl(sK5_skl)=X0|sK0_skl(sK5_skl)=X1|X0=X1))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f151,plain,(
% 0.09/0.40 ![X0,X1]: (~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK0_skl(sK5_skl)=X0|sK0_skl(sK5_skl)=X1|X0=X1|~sQ11_spl)),
% 0.09/0.40 inference(component_clause,[status(thm)],[f150])).
% 0.09/0.40 fof(f153,plain,(
% 0.09/0.40 ~sQ6_spl|sQ11_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f142,f107,f150,f81])).
% 0.09/0.40 fof(f155,definition,(
% 0.09/0.40 sQ12_spl <=> (sK0_skl(sK5_skl)=sK0_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f159,plain,(
% 0.09/0.40 ~sK8_skl(sK5_skl)=sK0_skl(sK5_skl)|~sQ10_spl|~sQ3_spl),
% 0.09/0.40 inference(backward_demodulation,[status(thm)],[f147,f104])).
% 0.09/0.40 fof(f160,plain,(
% 0.09/0.40 ~sK7_skl(sK5_skl)=sK0_skl(sK5_skl)|~sQ10_spl|~sQ3_spl),
% 0.09/0.40 inference(backward_demodulation,[status(thm)],[f147,f103])).
% 0.09/0.40 fof(f169,plain,(
% 0.09/0.40 ![X0]: (~rp(sK5_skl,X0)|sK0_skl(sK5_skl)=sK1_skl(sK5_skl)|sK0_skl(sK5_skl)=X0|sK1_skl(sK5_skl)=X0|~sQ3_spl|~sQ11_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f101,f151])).
% 0.09/0.40 fof(f170,plain,(
% 0.09/0.40 ![X0,X1]: (~cc(sK5_skl)|~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK1_skl(sK5_skl)=X0|sK1_skl(sK5_skl)=X1|X0=X1|~sQ3_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f101,f46])).
% 0.09/0.40 fof(f171,definition,(
% 0.09/0.40 ![X0]: (sQ14_spl <=> (~rp(sK5_skl,X0)|sK0_skl(sK5_skl)=X0|sK1_skl(sK5_skl)=X0))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f172,plain,(
% 0.09/0.40 ![X0]: (~rp(sK5_skl,X0)|sK0_skl(sK5_skl)=X0|sK1_skl(sK5_skl)=X0|~sQ14_spl)),
% 0.09/0.40 inference(component_clause,[status(thm)],[f171])).
% 0.09/0.40 fof(f174,definition,(
% 0.09/0.40 sQ15_spl <=> (sK0_skl(sK5_skl)=sK1_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f175,plain,(
% 0.09/0.40 sK0_skl(sK5_skl)=sK1_skl(sK5_skl)|~sQ15_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f174])).
% 0.09/0.40 fof(f177,plain,(
% 0.09/0.40 sQ14_spl|sQ15_spl|~sQ3_spl|~sQ11_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f169,f171,f174,f81,f150])).
% 0.09/0.40 fof(f178,definition,(
% 0.09/0.40 ![X0,X1]: (sQ16_spl <=> (~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK1_skl(sK5_skl)=X0|sK1_skl(sK5_skl)=X1|X0=X1))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f181,plain,(
% 0.09/0.40 ~sQ6_spl|sQ16_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f170,f107,f178,f81])).
% 0.09/0.40 fof(f182,plain,(
% 0.09/0.40 sK0_skl(sK5_skl)=sK1_skl(sK5_skl)|sK1_skl(sK5_skl)=sK1_skl(sK5_skl)|~sQ14_spl|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f172,f101])).
% 0.09/0.40 fof(f183,plain,(
% 0.09/0.40 sK0_skl(sK5_skl)=sK0_skl(sK5_skl)|sK1_skl(sK5_skl)=sK0_skl(sK5_skl)|~sQ14_spl|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f172,f100])).
% 0.09/0.40 fof(f184,definition,(
% 0.09/0.40 sQ17_spl <=> (sK1_skl(sK5_skl)=sK1_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f187,plain,(
% 0.09/0.40 sQ15_spl|sQ17_spl|~sQ14_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f182,f174,f184,f171,f81])).
% 0.09/0.40 fof(f188,plain,(
% 0.09/0.40 sQ12_spl|sQ15_spl|~sQ14_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f183,f155,f174,f171,f81])).
% 0.09/0.40 fof(f189,plain,(
% 0.09/0.40 $false|~sQ3_spl|~sQ15_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f175,f102])).
% 0.09/0.40 fof(f190,plain,(
% 0.09/0.40 ~sQ3_spl|~sQ15_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f189])).
% 0.09/0.40 fof(f203,plain,(
% 0.09/0.40 sK0_skl(sK5_skl)=sK8_skl(sK5_skl)|sK1_skl(sK5_skl)=sK8_skl(sK5_skl)|~sQ3_spl|~sQ14_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f97,f172])).
% 0.09/0.40 fof(f205,plain,(
% 0.09/0.40 ![X0,X1]: (~cc(sK5_skl)|~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK8_skl(sK5_skl)=X0|sK8_skl(sK5_skl)=X1|X0=X1|~sQ3_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f97,f46])).
% 0.09/0.40 fof(f209,definition,(
% 0.09/0.40 sQ20_spl <=> (sK1_skl(sK5_skl)=sK8_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f210,plain,(
% 0.09/0.40 sK1_skl(sK5_skl)=sK8_skl(sK5_skl)|~sQ20_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f209])).
% 0.09/0.40 fof(f213,definition,(
% 0.09/0.40 sQ21_spl <=> (sK0_skl(sK5_skl)=sK8_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f214,plain,(
% 0.09/0.40 sK0_skl(sK5_skl)=sK8_skl(sK5_skl)|~sQ21_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f213])).
% 0.09/0.40 fof(f216,plain,(
% 0.09/0.40 sQ21_spl|sQ20_spl|~sQ3_spl|~sQ14_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f203,f213,f209,f81,f171])).
% 0.09/0.40 fof(f221,definition,(
% 0.09/0.40 ![X0,X1]: (sQ23_spl <=> (~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK8_skl(sK5_skl)=X0|sK8_skl(sK5_skl)=X1|X0=X1))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f224,plain,(
% 0.09/0.40 ~sQ6_spl|sQ23_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f205,f107,f221,f81])).
% 0.09/0.40 fof(f225,plain,(
% 0.09/0.40 $false|~sQ10_spl|~sQ3_spl|~sQ21_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f214,f159])).
% 0.09/0.40 fof(f226,plain,(
% 0.09/0.40 ~sQ10_spl|~sQ3_spl|~sQ21_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f225])).
% 0.09/0.40 fof(f228,plain,(
% 0.09/0.40 ~sK7_skl(sK5_skl)=sK1_skl(sK5_skl)|~sQ20_spl|~sQ3_spl),
% 0.09/0.40 inference(backward_demodulation,[status(thm)],[f210,f95])).
% 0.09/0.40 fof(f235,plain,(
% 0.09/0.40 sK0_skl(sK5_skl)=sK7_skl(sK5_skl)|sK1_skl(sK5_skl)=sK7_skl(sK5_skl)|~sQ3_spl|~sQ14_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f98,f172])).
% 0.09/0.40 fof(f237,plain,(
% 0.09/0.40 ![X0,X1]: (~cc(sK5_skl)|~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK7_skl(sK5_skl)=X0|sK7_skl(sK5_skl)=X1|X0=X1|~sQ3_spl)),
% 0.09/0.40 inference(resolution,[status(thm)],[f98,f46])).
% 0.09/0.40 fof(f241,definition,(
% 0.09/0.40 sQ25_spl <=> (sK1_skl(sK5_skl)=sK7_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f242,plain,(
% 0.09/0.40 sK1_skl(sK5_skl)=sK7_skl(sK5_skl)|~sQ25_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f241])).
% 0.09/0.40 fof(f245,definition,(
% 0.09/0.40 sQ26_spl <=> (sK0_skl(sK5_skl)=sK7_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f246,plain,(
% 0.09/0.40 sK0_skl(sK5_skl)=sK7_skl(sK5_skl)|~sQ26_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f245])).
% 0.09/0.40 fof(f248,plain,(
% 0.09/0.40 sQ26_spl|sQ25_spl|~sQ3_spl|~sQ14_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f235,f245,f241,f81,f171])).
% 0.09/0.40 fof(f253,definition,(
% 0.09/0.40 ![X0,X1]: (sQ28_spl <=> (~rp(sK5_skl,X0)|~rp(sK5_skl,X1)|sK7_skl(sK5_skl)=X0|sK7_skl(sK5_skl)=X1|X0=X1))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f256,plain,(
% 0.09/0.40 ~sQ6_spl|sQ28_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f237,f107,f253,f81])).
% 0.09/0.40 fof(f257,plain,(
% 0.09/0.40 $false|~sQ10_spl|~sQ3_spl|~sQ26_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f246,f160])).
% 0.09/0.40 fof(f258,plain,(
% 0.09/0.40 ~sQ10_spl|~sQ3_spl|~sQ26_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f257])).
% 0.09/0.40 fof(f259,plain,(
% 0.09/0.40 $false|~sQ20_spl|~sQ3_spl|~sQ25_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f242,f228])).
% 0.09/0.40 fof(f260,plain,(
% 0.09/0.40 ~sQ20_spl|~sQ3_spl|~sQ25_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f259])).
% 0.09/0.40 fof(f268,plain,(
% 0.09/0.40 ~sK0_skl(sK5_skl)=sK8_skl(sK5_skl)|~sQ26_spl|~sQ3_spl),
% 0.09/0.40 inference(forward_demodulation,[status(thm)],[f246,f95])).
% 0.09/0.40 fof(f269,plain,(
% 0.09/0.40 ~sK0_skl(sK5_skl)=sK0_skl(sK5_skl)|~sQ21_spl|~sQ26_spl|~sQ3_spl),
% 0.09/0.40 inference(forward_demodulation,[status(thm)],[f214,f268])).
% 0.09/0.40 fof(f270,plain,(
% 0.09/0.40 $false|~sQ21_spl|~sQ26_spl|~sQ3_spl),
% 0.09/0.40 inference(trivial_equality_resolution,[status(thm)],[f269])).
% 0.09/0.40 fof(f271,plain,(
% 0.09/0.40 ~sQ21_spl|~sQ26_spl|~sQ3_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f270])).
% 0.09/0.40 fof(f277,plain,(
% 0.09/0.40 ~sK1_skl(sK5_skl)=sK9_skl(sK5_skl)|~sQ20_spl|~sQ3_spl),
% 0.09/0.40 inference(forward_demodulation,[status(thm)],[f210,f104])).
% 0.09/0.40 fof(f287,definition,(
% 0.09/0.40 sQ30_spl <=> (sK9_skl(sK5_skl)=sK1_skl(sK5_skl))),
% 0.09/0.40 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.09/0.40 fof(f288,plain,(
% 0.09/0.40 sK9_skl(sK5_skl)=sK1_skl(sK5_skl)|~sQ30_spl),
% 0.09/0.40 inference(component_clause,[status(thm)],[f287])).
% 0.09/0.40 fof(f292,plain,(
% 0.09/0.40 sK9_skl(sK5_skl)=sK1_skl(sK5_skl)|sK0_skl(sK5_skl)=sK1_skl(sK5_skl)|~sQ9_spl|~sQ3_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f144,f101])).
% 0.09/0.40 fof(f294,plain,(
% 0.09/0.40 sQ30_spl|sQ15_spl|~sQ9_spl|~sQ3_spl),
% 0.09/0.40 inference(split_clause,[status(thm)],[f292,f287,f174,f143,f81])).
% 0.09/0.40 fof(f296,plain,(
% 0.09/0.40 $false|~sQ20_spl|~sQ3_spl|~sQ30_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f288,f277])).
% 0.09/0.40 fof(f297,plain,(
% 0.09/0.40 ~sQ20_spl|~sQ3_spl|~sQ30_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f296])).
% 0.09/0.40 fof(f311,plain,(
% 0.09/0.40 ~sK1_skl(sK5_skl)=sK9_skl(sK5_skl)|~sQ25_spl|~sQ3_spl),
% 0.09/0.40 inference(forward_demodulation,[status(thm)],[f242,f103])).
% 0.09/0.40 fof(f312,plain,(
% 0.09/0.40 ~sK1_skl(sK5_skl)=sK1_skl(sK5_skl)|~sQ30_spl|~sQ25_spl|~sQ3_spl),
% 0.09/0.40 inference(forward_demodulation,[status(thm)],[f288,f311])).
% 0.09/0.40 fof(f313,plain,(
% 0.09/0.40 $false|~sQ30_spl|~sQ25_spl|~sQ3_spl),
% 0.09/0.40 inference(trivial_equality_resolution,[status(thm)],[f312])).
% 0.09/0.40 fof(f314,plain,(
% 0.09/0.40 ~sQ30_spl|~sQ25_spl|~sQ3_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f313])).
% 0.09/0.40 fof(f328,plain,(
% 0.09/0.40 sK1_skl(sK6_skl)=sK0_skl(sK6_skl)|~sQ5_spl|~sQ4_spl),
% 0.09/0.40 inference(resolution,[status(thm)],[f125,f124])).
% 0.09/0.40 fof(f329,plain,(
% 0.09/0.40 $false|~sQ5_spl|~sQ4_spl),
% 0.09/0.40 inference(forward_subsumption_resolution,[status(thm)],[f328,f122])).
% 0.09/0.40 fof(f330,plain,(
% 0.09/0.40 ~sQ5_spl|~sQ4_spl),
% 0.09/0.40 inference(contradiction_clause,[status(thm)],[f329])).
% 0.09/0.40 fof(f331,plain,(
% 0.09/0.40 $false),
% 0.09/0.40 inference(sat_refutation,[status(thm)],[f87,f91,f113,f115,f117,f119,f121,f149,f153,f177,f181,f187,f188,f190,f216,f224,f226,f248,f256,f258,f260,f271,f294,f297,f314,f330])).
% 0.09/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.42 % Elapsed time: 0.052038 seconds
% 0.09/0.42 % CPU time: 0.171971 seconds
% 0.09/0.42 % Total memory used: 74.259 MB
% 0.09/0.42 % Net memory used: 74.028 MB
%------------------------------------------------------------------------------