%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN551+3 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 03:20:08 PM UTC 2026
% Result : Theorem 0.13s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN551+3 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n003.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 11:10:01 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.37 % Refutation found
% 0.13/0.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.37 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.37 fof(f1,conjecture,(
% 0.13/0.37 ( (? [X] :( X = f(g(X))& (! [Y] :( Y = f(g(Y))=> Y = X ) )))<=> (? [X] :( X = g(f(X))& (! [Y] :( Y = g(f(Y))=> Y = X ) )) )) ),
% 0.13/0.37 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.37 fof(f2,negated_conjecture,(
% 0.13/0.37 ~(( (? [X] :( X = f(g(X))& (! [Y] :( Y = f(g(Y))=> Y = X ) )))<=> (? [X] :( X = g(f(X))& (! [Y] :( Y = g(f(Y))=> Y = X ) )) )) )),
% 0.13/0.37 inference(negated_conjecture,[status(cth)],[f1])).
% 0.13/0.37 fof(f3,plain,(
% 0.13/0.37 ((?[X]: (X=f(g(X))&(![Y]: (~Y=f(g(Y))|Y=X))))<~>(?[X]: (X=g(f(X))&(![Y]: (~Y=g(f(Y))|Y=X)))))),
% 0.13/0.37 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/0.37 fof(f4,plain,(
% 0.13/0.37 ((?[X]: (X=f(g(X))&(![Y]: (~Y=f(g(Y))|Y=X))))|(?[X]: (X=g(f(X))&(![Y]: (~Y=g(f(Y))|Y=X)))))&((![X]: (~X=f(g(X))|(?[Y]: (Y=f(g(Y))&~Y=X))))|(![X]: (~X=g(f(X))|(?[Y]: (Y=g(f(Y))&~Y=X)))))),
% 0.13/0.37 inference(NNF_transformation,[status(thm)],[f3])).
% 0.13/0.37 fof(f5,plain,(
% 0.13/0.37 ((sK0_skl=f(g(sK0_skl))&(![Y]: (~Y=f(g(Y))|Y=sK0_skl)))|(sK1_skl=g(f(sK1_skl))&(![Y]: (~Y=g(f(Y))|Y=sK1_skl))))&((![X]: (~X=f(g(X))|(sK2_skl(X)=f(g(sK2_skl(X)))&~sK2_skl(X)=X)))|(![X]: (~X=g(f(X))|(sK3_skl(X)=g(f(sK3_skl(X)))&~sK3_skl(X)=X))))),
% 0.13/0.37 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(X,sK0_skl),skolemize(X,sK1_skl),skolemize(Y,sK2_skl(X)),skolemize(Y,sK3_skl(X))],[f4])).
% 0.13/0.37 fof(f6,plain,(
% 0.13/0.37 sK0_skl=f(g(sK0_skl))|sK1_skl=g(f(sK1_skl))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f7,plain,(
% 0.13/0.37 ![X0]: (sK0_skl=f(g(sK0_skl))|~X0=g(f(X0))|X0=sK1_skl)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f8,plain,(
% 0.13/0.37 ![X0]: (~X0=f(g(X0))|X0=sK0_skl|sK1_skl=g(f(sK1_skl)))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f9,plain,(
% 0.13/0.37 ![X0,X1]: (~X0=f(g(X0))|X0=sK0_skl|~X1=g(f(X1))|X1=sK1_skl)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f10,plain,(
% 0.13/0.37 ![X0,X1]: (~X0=f(g(X0))|sK2_skl(X0)=f(g(sK2_skl(X0)))|~X1=g(f(X1))|sK3_skl(X1)=g(f(sK3_skl(X1))))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f11,plain,(
% 0.13/0.37 ![X0,X1]: (~X0=f(g(X0))|sK2_skl(X0)=f(g(sK2_skl(X0)))|~X1=g(f(X1))|~sK3_skl(X1)=X1)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f12,plain,(
% 0.13/0.37 ![X0,X1]: (~X0=f(g(X0))|~sK2_skl(X0)=X0|~X1=g(f(X1))|sK3_skl(X1)=g(f(sK3_skl(X1))))),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f13,plain,(
% 0.13/0.37 ![X0,X1]: (~X0=f(g(X0))|~sK2_skl(X0)=X0|~X1=g(f(X1))|~sK3_skl(X1)=X1)),
% 0.13/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.37 fof(f14,definition,(
% 0.13/0.37 sQ0_spl <=> (sK0_skl=f(g(sK0_skl)))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f15,plain,(
% 0.13/0.37 sK0_skl=f(g(sK0_skl))|~sQ0_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f14])).
% 0.13/0.37 fof(f17,definition,(
% 0.13/0.37 sQ1_spl <=> (sK1_skl=g(f(sK1_skl)))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f18,plain,(
% 0.13/0.37 sK1_skl=g(f(sK1_skl))|~sQ1_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f17])).
% 0.13/0.37 fof(f19,plain,(
% 0.13/0.37 ~sK1_skl=g(f(sK1_skl))|sQ1_spl),
% 0.13/0.37 inference(component_clause,[status(thm)],[f17])).
% 0.13/0.37 fof(f20,plain,(
% 0.13/0.37 sQ0_spl|sQ1_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f6,f14,f17])).
% 0.13/0.37 fof(f21,definition,(
% 0.13/0.37 ![X0]: (sQ2_spl <=> (~X0=g(f(X0))|X0=sK1_skl))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f22,plain,(
% 0.13/0.37 ![X0]: (~X0=g(f(X0))|X0=sK1_skl|~sQ2_spl)),
% 0.13/0.37 inference(component_clause,[status(thm)],[f21])).
% 0.13/0.37 fof(f24,plain,(
% 0.13/0.37 sQ0_spl|sQ2_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f7,f14,f21])).
% 0.13/0.37 fof(f25,definition,(
% 0.13/0.37 ![X0]: (sQ3_spl <=> (~X0=f(g(X0))|X0=sK0_skl))),
% 0.13/0.37 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.37 fof(f26,plain,(
% 0.13/0.37 ![X0]: (~X0=f(g(X0))|X0=sK0_skl|~sQ3_spl)),
% 0.13/0.37 inference(component_clause,[status(thm)],[f25])).
% 0.13/0.37 fof(f28,plain,(
% 0.13/0.37 sQ3_spl|sQ1_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f8,f25,f17])).
% 0.13/0.37 fof(f29,plain,(
% 0.13/0.37 sQ3_spl|sQ2_spl),
% 0.13/0.37 inference(split_clause,[status(thm)],[f9,f25,f21])).
% 0.13/0.37 fof(f30,definition,(
% 0.13/0.38 ![X0]: (sQ4_spl <=> (~X0=f(g(X0))|sK2_skl(X0)=f(g(sK2_skl(X0)))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f31,plain,(
% 0.13/0.38 ![X0]: (~X0=f(g(X0))|sK2_skl(X0)=f(g(sK2_skl(X0)))|~sQ4_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f30])).
% 0.13/0.38 fof(f33,definition,(
% 0.13/0.38 ![X1]: (sQ5_spl <=> (~X1=g(f(X1))|sK3_skl(X1)=g(f(sK3_skl(X1)))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f34,plain,(
% 0.13/0.38 ![X0]: (~X0=g(f(X0))|sK3_skl(X0)=g(f(sK3_skl(X0)))|~sQ5_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f33])).
% 0.13/0.38 fof(f36,plain,(
% 0.13/0.38 sQ4_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f10,f30,f33])).
% 0.13/0.38 fof(f37,definition,(
% 0.13/0.38 ![X1]: (sQ6_spl <=> (~X1=g(f(X1))|~sK3_skl(X1)=X1))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f38,plain,(
% 0.13/0.38 ![X0]: (~X0=g(f(X0))|~sK3_skl(X0)=X0|~sQ6_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f37])).
% 0.13/0.38 fof(f40,plain,(
% 0.13/0.38 sQ4_spl|sQ6_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f11,f30,f37])).
% 0.13/0.38 fof(f41,definition,(
% 0.13/0.38 ![X0]: (sQ7_spl <=> (~X0=f(g(X0))|~sK2_skl(X0)=X0))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f42,plain,(
% 0.13/0.38 ![X0]: (~X0=f(g(X0))|~sK2_skl(X0)=X0|~sQ7_spl)),
% 0.13/0.38 inference(component_clause,[status(thm)],[f41])).
% 0.13/0.38 fof(f44,plain,(
% 0.13/0.38 sQ7_spl|sQ5_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f12,f41,f33])).
% 0.13/0.38 fof(f45,plain,(
% 0.13/0.38 sQ7_spl|sQ6_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f13,f41,f37])).
% 0.13/0.38 fof(f48,definition,(
% 0.13/0.38 sQ8_spl <=> (sK0_skl=sK0_skl)),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f50,plain,(
% 0.13/0.38 ~sK0_skl=sK0_skl|sQ8_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f48])).
% 0.13/0.38 fof(f55,plain,(
% 0.13/0.38 ~f(sK1_skl)=f(sK1_skl)|sK2_skl(f(sK1_skl))=f(g(sK2_skl(f(sK1_skl))))|~sQ4_spl|~sQ1_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f18,f31])).
% 0.13/0.38 fof(f56,definition,(
% 0.13/0.38 sQ10_spl <=> (f(sK1_skl)=f(sK1_skl))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f58,plain,(
% 0.13/0.38 ~f(sK1_skl)=f(sK1_skl)|sQ10_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f56])).
% 0.13/0.38 fof(f59,definition,(
% 0.13/0.38 sQ11_spl <=> (sK2_skl(f(sK1_skl))=f(g(sK2_skl(f(sK1_skl)))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f60,plain,(
% 0.13/0.38 sK2_skl(f(sK1_skl))=f(g(sK2_skl(f(sK1_skl))))|~sQ11_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f59])).
% 0.13/0.38 fof(f62,plain,(
% 0.13/0.38 ~sQ10_spl|sQ11_spl|~sQ4_spl|~sQ1_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f55,f56,f59,f30,f17])).
% 0.13/0.38 fof(f63,plain,(
% 0.13/0.38 $false|sQ10_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f58])).
% 0.13/0.38 fof(f64,plain,(
% 0.13/0.38 sQ10_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f63])).
% 0.13/0.38 fof(f68,plain,(
% 0.13/0.38 ~g(sK0_skl)=g(sK0_skl)|g(sK0_skl)=sK1_skl|~sQ2_spl|~sQ0_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f15,f22])).
% 0.13/0.38 fof(f69,definition,(
% 0.13/0.38 sQ12_spl <=> (g(sK0_skl)=g(sK0_skl))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f71,plain,(
% 0.13/0.38 ~g(sK0_skl)=g(sK0_skl)|sQ12_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f69])).
% 0.13/0.38 fof(f72,definition,(
% 0.13/0.38 sQ13_spl <=> (g(sK0_skl)=sK1_skl)),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f73,plain,(
% 0.13/0.38 g(sK0_skl)=sK1_skl|~sQ13_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f72])).
% 0.13/0.38 fof(f75,plain,(
% 0.13/0.38 ~sQ12_spl|sQ13_spl|~sQ2_spl|~sQ0_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f68,f69,f72,f21,f14])).
% 0.13/0.38 fof(f80,plain,(
% 0.13/0.38 $false|sQ12_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f71])).
% 0.13/0.38 fof(f81,plain,(
% 0.13/0.38 sQ12_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f80])).
% 0.13/0.38 fof(f90,plain,(
% 0.13/0.38 ~sK1_skl=sK1_skl|~sK3_skl(sK1_skl)=sK1_skl|~sQ6_spl|~sQ1_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f18,f38])).
% 0.13/0.38 fof(f91,plain,(
% 0.13/0.38 ~sK1_skl=sK1_skl|sK3_skl(sK1_skl)=g(f(sK3_skl(sK1_skl)))|~sQ5_spl|~sQ1_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f18,f34])).
% 0.13/0.38 fof(f94,definition,(
% 0.13/0.38 sQ15_spl <=> (sK1_skl=sK1_skl)),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f96,plain,(
% 0.13/0.38 ~sK1_skl=sK1_skl|sQ15_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f94])).
% 0.13/0.38 fof(f97,definition,(
% 0.13/0.38 sQ16_spl <=> (sK3_skl(sK1_skl)=sK1_skl)),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f99,plain,(
% 0.13/0.38 ~sK3_skl(sK1_skl)=sK1_skl|sQ16_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f97])).
% 0.13/0.38 fof(f100,plain,(
% 0.13/0.38 ~sQ15_spl|~sQ16_spl|~sQ6_spl|~sQ1_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f90,f94,f97,f37,f17])).
% 0.13/0.38 fof(f101,definition,(
% 0.13/0.38 sQ17_spl <=> (sK3_skl(sK1_skl)=g(f(sK3_skl(sK1_skl))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f102,plain,(
% 0.13/0.38 sK3_skl(sK1_skl)=g(f(sK3_skl(sK1_skl)))|~sQ17_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f101])).
% 0.13/0.38 fof(f104,plain,(
% 0.13/0.38 ~sQ15_spl|sQ17_spl|~sQ5_spl|~sQ1_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f91,f94,f101,f33,f17])).
% 0.13/0.38 fof(f107,plain,(
% 0.13/0.38 sK0_skl=f(sK1_skl)|~sQ13_spl|~sQ0_spl),
% 0.13/0.38 inference(forward_demodulation,[status(thm)],[f73,f15])).
% 0.13/0.38 fof(f110,plain,(
% 0.13/0.38 ~sK1_skl=g(sK0_skl)|~sQ13_spl|~sQ0_spl|sQ1_spl),
% 0.13/0.38 inference(backward_demodulation,[status(thm)],[f107,f19])).
% 0.13/0.38 fof(f111,plain,(
% 0.13/0.38 ~sQ13_spl|~sQ0_spl|sQ1_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f110,f72,f14,f17])).
% 0.13/0.38 fof(f112,plain,(
% 0.13/0.38 $false|sQ15_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f96])).
% 0.13/0.38 fof(f113,plain,(
% 0.13/0.38 sQ15_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f112])).
% 0.13/0.38 fof(f140,plain,(
% 0.13/0.38 sK2_skl(sK0_skl)=f(g(sK2_skl(sK0_skl)))|~sQ0_spl|~sQ4_spl),
% 0.13/0.38 inference(resolution,[status(thm)],[f15,f31])).
% 0.13/0.38 fof(f141,plain,(
% 0.13/0.38 ~sK2_skl(sK0_skl)=sK0_skl|~sQ0_spl|~sQ7_spl),
% 0.13/0.38 inference(resolution,[status(thm)],[f15,f42])).
% 0.13/0.38 fof(f149,plain,(
% 0.13/0.38 $false|sQ8_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f50])).
% 0.13/0.38 fof(f150,plain,(
% 0.13/0.38 sQ8_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f149])).
% 0.13/0.38 fof(f153,plain,(
% 0.13/0.38 sK2_skl(sK0_skl)=sK0_skl|~sQ0_spl|~sQ4_spl|~sQ3_spl),
% 0.13/0.38 inference(resolution,[status(thm)],[f140,f26])).
% 0.13/0.38 fof(f157,plain,(
% 0.13/0.38 $false|~sQ7_spl|~sQ0_spl|~sQ4_spl|~sQ3_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f153,f141])).
% 0.13/0.38 fof(f158,plain,(
% 0.13/0.38 ~sQ7_spl|~sQ0_spl|~sQ4_spl|~sQ3_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f157])).
% 0.13/0.38 fof(f181,plain,(
% 0.13/0.38 ~g(sK0_skl)=g(sK0_skl)|~sK3_skl(g(sK0_skl))=g(sK0_skl)|~sQ6_spl|~sQ0_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f15,f38])).
% 0.13/0.38 fof(f182,definition,(
% 0.13/0.38 sQ21_spl <=> (sK3_skl(g(sK0_skl))=g(sK0_skl))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f184,plain,(
% 0.13/0.38 ~sK3_skl(g(sK0_skl))=g(sK0_skl)|sQ21_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f182])).
% 0.13/0.38 fof(f185,plain,(
% 0.13/0.38 ~sQ12_spl|~sQ21_spl|~sQ6_spl|~sQ0_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f181,f69,f182,f37,f14])).
% 0.13/0.38 fof(f186,plain,(
% 0.13/0.38 ~g(sK0_skl)=g(sK0_skl)|sK3_skl(g(sK0_skl))=g(f(sK3_skl(g(sK0_skl))))|~sQ5_spl|~sQ0_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f15,f34])).
% 0.13/0.38 fof(f187,definition,(
% 0.13/0.38 sQ22_spl <=> (sK3_skl(g(sK0_skl))=g(f(sK3_skl(g(sK0_skl)))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f188,plain,(
% 0.13/0.38 sK3_skl(g(sK0_skl))=g(f(sK3_skl(g(sK0_skl))))|~sQ22_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f187])).
% 0.13/0.38 fof(f190,plain,(
% 0.13/0.38 ~sQ12_spl|sQ22_spl|~sQ5_spl|~sQ0_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f186,f69,f187,f33,f14])).
% 0.13/0.38 fof(f196,plain,(
% 0.13/0.38 ~f(sK3_skl(g(sK0_skl)))=f(sK3_skl(g(sK0_skl)))|f(sK3_skl(g(sK0_skl)))=sK0_skl|~sQ3_spl|~sQ22_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f188,f26])).
% 0.13/0.38 fof(f197,definition,(
% 0.13/0.38 sQ23_spl <=> (sK3_skl(g(sK0_skl))=sK3_skl(g(sK0_skl)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f199,plain,(
% 0.13/0.38 ~sK3_skl(g(sK0_skl))=sK3_skl(g(sK0_skl))|sQ23_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f197])).
% 0.13/0.38 fof(f208,definition,(
% 0.13/0.38 sQ26_spl <=> (f(sK3_skl(g(sK0_skl)))=f(sK3_skl(g(sK0_skl))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f210,plain,(
% 0.13/0.38 ~f(sK3_skl(g(sK0_skl)))=f(sK3_skl(g(sK0_skl)))|sQ26_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f208])).
% 0.13/0.38 fof(f215,definition,(
% 0.13/0.38 sQ28_spl <=> (f(sK3_skl(g(sK0_skl)))=sK0_skl)),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f216,plain,(
% 0.13/0.38 f(sK3_skl(g(sK0_skl)))=sK0_skl|~sQ28_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f215])).
% 0.13/0.38 fof(f218,plain,(
% 0.13/0.38 ~sQ26_spl|sQ28_spl|~sQ3_spl|~sQ22_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f196,f208,f215,f25,f187])).
% 0.13/0.38 fof(f219,plain,(
% 0.13/0.38 $false|sQ23_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f199])).
% 0.13/0.38 fof(f220,plain,(
% 0.13/0.38 sQ23_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f219])).
% 0.13/0.38 fof(f221,plain,(
% 0.13/0.38 $false|sQ26_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f210])).
% 0.13/0.38 fof(f222,plain,(
% 0.13/0.38 sQ26_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f221])).
% 0.13/0.38 fof(f223,plain,(
% 0.13/0.38 sK3_skl(g(sK0_skl))=g(sK0_skl)|~sQ28_spl|~sQ22_spl),
% 0.13/0.38 inference(backward_demodulation,[status(thm)],[f216,f188])).
% 0.13/0.38 fof(f225,plain,(
% 0.13/0.38 $false|sQ21_spl|~sQ28_spl|~sQ22_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f223,f184])).
% 0.13/0.38 fof(f226,plain,(
% 0.13/0.38 sQ21_spl|~sQ28_spl|~sQ22_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f225])).
% 0.13/0.38 fof(f232,plain,(
% 0.13/0.38 ~f(sK1_skl)=f(sK1_skl)|~sK2_skl(f(sK1_skl))=f(sK1_skl)|~sQ7_spl|~sQ1_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f18,f42])).
% 0.13/0.38 fof(f233,definition,(
% 0.13/0.38 sQ29_spl <=> (sK2_skl(f(sK1_skl))=f(sK1_skl))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f235,plain,(
% 0.13/0.38 ~sK2_skl(f(sK1_skl))=f(sK1_skl)|sQ29_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f233])).
% 0.13/0.38 fof(f236,plain,(
% 0.13/0.38 ~sQ10_spl|~sQ29_spl|~sQ7_spl|~sQ1_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f232,f56,f233,f41,f17])).
% 0.13/0.38 fof(f244,plain,(
% 0.13/0.38 sK3_skl(sK1_skl)=sK1_skl|~sQ17_spl|~sQ2_spl),
% 0.13/0.38 inference(resolution,[status(thm)],[f102,f22])).
% 0.13/0.38 fof(f250,plain,(
% 0.13/0.38 $false|sQ16_spl|~sQ17_spl|~sQ2_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f244,f99])).
% 0.13/0.38 fof(f251,plain,(
% 0.13/0.38 sQ16_spl|~sQ17_spl|~sQ2_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f250])).
% 0.13/0.38 fof(f264,definition,(
% 0.13/0.38 sQ31_spl <=> (g(sK2_skl(sK0_skl))=g(sK2_skl(sK0_skl)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f266,plain,(
% 0.13/0.38 ~g(sK2_skl(sK0_skl))=g(sK2_skl(sK0_skl))|sQ31_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f264])).
% 0.13/0.38 fof(f267,definition,(
% 0.13/0.38 sQ32_spl <=> (g(sK2_skl(sK0_skl))=sK1_skl)),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f268,plain,(
% 0.13/0.38 g(sK2_skl(sK0_skl))=sK1_skl|~sQ32_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f267])).
% 0.13/0.38 fof(f271,plain,(
% 0.13/0.38 ~sK1_skl=g(sK2_skl(sK0_skl))|~sQ32_spl|sQ31_spl),
% 0.13/0.38 inference(forward_demodulation,[status(thm)],[f268,f266])).
% 0.13/0.38 fof(f272,plain,(
% 0.13/0.38 ~sK1_skl=sK1_skl|~sQ32_spl|sQ31_spl),
% 0.13/0.38 inference(forward_demodulation,[status(thm)],[f268,f271])).
% 0.13/0.38 fof(f273,plain,(
% 0.13/0.38 $false|~sQ32_spl|sQ31_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f272])).
% 0.13/0.38 fof(f274,plain,(
% 0.13/0.38 ~sQ32_spl|sQ31_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f273])).
% 0.13/0.38 fof(f277,plain,(
% 0.13/0.38 ~sK2_skl(f(sK1_skl))=sK2_skl(f(sK1_skl))|~sK2_skl(sK2_skl(f(sK1_skl)))=sK2_skl(f(sK1_skl))|~sQ7_spl|~sQ11_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f60,f42])).
% 0.13/0.38 fof(f278,plain,(
% 0.13/0.38 ~sK2_skl(f(sK1_skl))=sK2_skl(f(sK1_skl))|sK2_skl(sK2_skl(f(sK1_skl)))=f(g(sK2_skl(sK2_skl(f(sK1_skl)))))|~sQ4_spl|~sQ11_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f60,f31])).
% 0.13/0.38 fof(f279,plain,(
% 0.13/0.38 ~g(sK2_skl(f(sK1_skl)))=g(sK2_skl(f(sK1_skl)))|g(sK2_skl(f(sK1_skl)))=sK1_skl|~sQ2_spl|~sQ11_spl),
% 0.13/0.38 inference(paramodulation,[status(thm)],[f60,f22])).
% 0.13/0.38 fof(f280,definition,(
% 0.13/0.38 sQ33_spl <=> (sK2_skl(f(sK1_skl))=sK2_skl(f(sK1_skl)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f282,plain,(
% 0.13/0.38 ~sK2_skl(f(sK1_skl))=sK2_skl(f(sK1_skl))|sQ33_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f280])).
% 0.13/0.38 fof(f283,definition,(
% 0.13/0.38 sQ34_spl <=> (sK2_skl(sK2_skl(f(sK1_skl)))=sK2_skl(f(sK1_skl)))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f286,plain,(
% 0.13/0.38 ~sQ33_spl|~sQ34_spl|~sQ7_spl|~sQ11_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f277,f280,f283,f41,f59])).
% 0.13/0.38 fof(f287,definition,(
% 0.13/0.38 sQ35_spl <=> (sK2_skl(sK2_skl(f(sK1_skl)))=f(g(sK2_skl(sK2_skl(f(sK1_skl))))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f290,plain,(
% 0.13/0.38 ~sQ33_spl|sQ35_spl|~sQ4_spl|~sQ11_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f278,f280,f287,f30,f59])).
% 0.13/0.38 fof(f291,definition,(
% 0.13/0.38 sQ36_spl <=> (g(sK2_skl(f(sK1_skl)))=g(sK2_skl(f(sK1_skl))))),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f293,plain,(
% 0.13/0.38 ~g(sK2_skl(f(sK1_skl)))=g(sK2_skl(f(sK1_skl)))|sQ36_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f291])).
% 0.13/0.38 fof(f294,definition,(
% 0.13/0.38 sQ37_spl <=> (g(sK2_skl(f(sK1_skl)))=sK1_skl)),
% 0.13/0.38 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.38 fof(f295,plain,(
% 0.13/0.38 g(sK2_skl(f(sK1_skl)))=sK1_skl|~sQ37_spl),
% 0.13/0.38 inference(component_clause,[status(thm)],[f294])).
% 0.13/0.38 fof(f297,plain,(
% 0.13/0.38 ~sQ36_spl|sQ37_spl|~sQ2_spl|~sQ11_spl),
% 0.13/0.38 inference(split_clause,[status(thm)],[f279,f291,f294,f21,f59])).
% 0.13/0.38 fof(f298,plain,(
% 0.13/0.38 $false|sQ33_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f282])).
% 0.13/0.38 fof(f299,plain,(
% 0.13/0.38 sQ33_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f298])).
% 0.13/0.38 fof(f300,plain,(
% 0.13/0.38 $false|sQ36_spl),
% 0.13/0.38 inference(trivial_equality_resolution,[status(thm)],[f293])).
% 0.13/0.38 fof(f301,plain,(
% 0.13/0.38 sQ36_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f300])).
% 0.13/0.38 fof(f302,plain,(
% 0.13/0.38 sK2_skl(f(sK1_skl))=f(sK1_skl)|~sQ37_spl|~sQ11_spl),
% 0.13/0.38 inference(backward_demodulation,[status(thm)],[f295,f60])).
% 0.13/0.38 fof(f303,plain,(
% 0.13/0.38 $false|sQ29_spl|~sQ37_spl|~sQ11_spl),
% 0.13/0.38 inference(forward_subsumption_resolution,[status(thm)],[f302,f235])).
% 0.13/0.38 fof(f304,plain,(
% 0.13/0.38 sQ29_spl|~sQ37_spl|~sQ11_spl),
% 0.13/0.38 inference(contradiction_clause,[status(thm)],[f303])).
% 0.13/0.38 fof(f305,plain,(
% 0.13/0.38 $false),
% 0.13/0.38 inference(sat_refutation,[status(thm)],[f20,f24,f28,f29,f36,f40,f44,f45,f62,f64,f75,f81,f100,f104,f111,f113,f150,f158,f185,f190,f218,f220,f222,f226,f236,f251,f274,f286,f290,f297,f299,f301,f304])).
% 0.13/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.40 % Elapsed time: 0.045404 seconds
% 0.13/0.40 % CPU time: 0.143521 seconds
% 0.13/0.40 % Total memory used: 65.283 MB
% 0.13/0.40 % Net memory used: 64.907 MB
%------------------------------------------------------------------------------