%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU297+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 02:22:15 PM UTC 2026
% Result : Theorem 0.09s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU297+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n010.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 06:09:11 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.43 % Refutation found
% 0.09/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.43 fof(f1,conjecture,(
% 0.09/0.43 (! [A,B,C] :( ( element(B,powerset(powerset(A)))& relation(C)& function(C) )=> (? [D] :(! [E] :( in(E,D)<=> ( in(E,powerset(relation_dom(C)))& in(relation_image(C,E),B) ) ) ))) )),
% 0.09/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.43 fof(f2,negated_conjecture,(
% 0.09/0.43 ~((! [A,B,C] :( ( element(B,powerset(powerset(A)))& relation(C)& function(C) )=> (? [D] :(! [E] :( in(E,D)<=> ( in(E,powerset(relation_dom(C)))& in(relation_image(C,E),B) ) ) ))) ))),
% 0.09/0.43 inference(negated_conjecture,[status(cth)],[f1])).
% 0.09/0.43 fof(f5,axiom,(
% 0.09/0.43 (? [A] :( ~ empty(A)& finite(A) ) )),
% 0.09/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.43 fof(f38,axiom,(
% 0.09/0.43 (! [A,B,C] :( ( element(B,powerset(powerset(A)))& relation(C)& function(C) )=> ( (! [D,E,F] :( ( D = E& in(relation_image(C,E),B)& D = F& in(relation_image(C,F),B) )=> E = F ))=> (? [D] :(! [E] :( in(E,D)<=> (? [F] :( in(F,powerset(relation_dom(C)))& F = E& in(relation_image(C,E),B) ) )) ))) ) )),
% 0.09/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.43 fof(f39,plain,(
% 0.09/0.43 (?[A,B,C]: (((element(B,powerset(powerset(A)))&relation(C))&function(C))&(![D]: ?[E]: (in(E,D)<~>(in(E,powerset(relation_dom(C)))&in(relation_image(C,E),B))))))),
% 0.09/0.43 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.09/0.43 fof(f40,plain,(
% 0.09/0.43 ?[A,B,C]: (((element(B,powerset(powerset(A)))&relation(C))&function(C))&(![D]: ?[E]: ((in(E,D)|(in(E,powerset(relation_dom(C)))&in(relation_image(C,E),B)))&(~in(E,D)|(~in(E,powerset(relation_dom(C)))|~in(relation_image(C,E),B))))))),
% 0.09/0.43 inference(NNF_transformation,[status(thm)],[f39])).
% 0.09/0.43 fof(f41,plain,(
% 0.09/0.43 ?[B,C]: ((((?[A]: element(B,powerset(powerset(A))))&relation(C))&function(C))&(![D]: ?[E]: ((in(E,D)|(in(E,powerset(relation_dom(C)))&in(relation_image(C,E),B)))&(~in(E,D)|(~in(E,powerset(relation_dom(C)))|~in(relation_image(C,E),B))))))),
% 0.09/0.43 inference(miniscoping,[status(thm)],[f40])).
% 0.09/0.43 fof(f42,plain,(
% 0.09/0.43 (((element(sK0_skl,powerset(powerset(sK2_skl)))&relation(sK1_skl))&function(sK1_skl))&(![D]: ((in(sK3_skl(D),D)|(in(sK3_skl(D),powerset(relation_dom(sK1_skl)))&in(relation_image(sK1_skl,sK3_skl(D)),sK0_skl)))&(~in(sK3_skl(D),D)|(~in(sK3_skl(D),powerset(relation_dom(sK1_skl)))|~in(relation_image(sK1_skl,sK3_skl(D)),sK0_skl))))))),
% 0.09/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(B,sK0_skl),skolemize(C,sK1_skl),skolemize(A,sK2_skl),skolemize(E,sK3_skl(D))],[f41])).
% 0.09/0.43 fof(f43,plain,(
% 0.09/0.43 element(sK0_skl,powerset(powerset(sK2_skl)))),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.43 fof(f44,plain,(
% 0.09/0.43 relation(sK1_skl)),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.43 fof(f45,plain,(
% 0.09/0.43 function(sK1_skl)),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.43 fof(f46,plain,(
% 0.09/0.43 ![X0]: (in(sK3_skl(X0),X0)|in(sK3_skl(X0),powerset(relation_dom(sK1_skl))))),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.43 fof(f47,plain,(
% 0.09/0.43 ![X0]: (in(sK3_skl(X0),X0)|in(relation_image(sK1_skl,sK3_skl(X0)),sK0_skl))),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.43 fof(f48,plain,(
% 0.09/0.43 ![X0]: (~in(sK3_skl(X0),X0)|~in(sK3_skl(X0),powerset(relation_dom(sK1_skl)))|~in(relation_image(sK1_skl,sK3_skl(X0)),sK0_skl))),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f42])).
% 0.09/0.43 fof(f66,plain,(
% 0.09/0.43 (~empty(sK6_skl)&finite(sK6_skl))),
% 0.09/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(A,sK6_skl)],[f5])).
% 0.09/0.43 fof(f67,plain,(
% 0.09/0.43 ~empty(sK6_skl)),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f66])).
% 0.09/0.43 fof(f159,plain,(
% 0.09/0.43 ![A,B,C]: (((~element(B,powerset(powerset(A)))|~relation(C))|~function(C))|((?[D,E,F]: ((((D=E&in(relation_image(C,E),B))&D=F)&in(relation_image(C,F),B))&~E=F))|(?[D]: ![E]: (in(E,D)<=>(?[F]: ((in(F,powerset(relation_dom(C)))&F=E)&in(relation_image(C,E),B)))))))),
% 0.09/0.43 inference(pre_NNF_transformation,[status(thm)],[f38])).
% 0.09/0.43 fof(f160,definition,(
% 0.09/0.43 ![B,C,D,E,F]: (sP0_prd(F,E,D,C,B)<=>((((D=E&in(relation_image(C,E),B))&D=F)&in(relation_image(C,F),B))&~E=F))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.09/0.43 fof(f161,plain,(
% 0.09/0.43 ![A,B,C]: (((~element(B,powerset(powerset(A)))|~relation(C))|~function(C))|((?[D,E,F]: sP0_prd(F,E,D,C,B))|(?[D]: ![E]: (in(E,D)<=>(?[F]: ((in(F,powerset(relation_dom(C)))&F=E)&in(relation_image(C,E),B)))))))),
% 0.09/0.43 inference(formula_renaming,[status(thm)],[f159,f160])).
% 0.09/0.43 fof(f162,plain,(
% 0.09/0.43 ![A,B,C]: (((~element(B,powerset(powerset(A)))|~relation(C))|~function(C))|((?[D,E,F]: sP0_prd(F,E,D,C,B))|(?[D]: ![E]: ((~in(E,D)|(?[F]: ((in(F,powerset(relation_dom(C)))&F=E)&in(relation_image(C,E),B))))&(in(E,D)|(![F]: ((~in(F,powerset(relation_dom(C)))|~F=E)|~in(relation_image(C,E),B))))))))),
% 0.09/0.43 inference(NNF_transformation,[status(thm)],[f161])).
% 0.09/0.43 fof(f163,plain,(
% 0.09/0.43 ![B,C]: ((((![A]: ~element(B,powerset(powerset(A))))|~relation(C))|~function(C))|((?[D,E,F]: sP0_prd(F,E,D,C,B))|(?[D]: ((![E]: (~in(E,D)|((?[F]: (in(F,powerset(relation_dom(C)))&F=E))&in(relation_image(C,E),B))))&(![E]: (in(E,D)|((![F]: (~in(F,powerset(relation_dom(C)))|~F=E))|~in(relation_image(C,E),B))))))))),
% 0.09/0.43 inference(miniscoping,[status(thm)],[f162])).
% 0.09/0.43 fof(f164,plain,(
% 0.09/0.43 ![B,C]: ((((![A]: ~element(B,powerset(powerset(A))))|~relation(C))|~function(C))|(sP0_prd(sK22_skl(C,B),sK21_skl(C,B),sK20_skl(C,B),C,B)|((![E]: (~in(E,sK23_skl(C,B))|((in(sK24_skl(E,C,B),powerset(relation_dom(C)))&sK24_skl(E,C,B)=E)&in(relation_image(C,E),B))))&(![E]: (in(E,sK23_skl(C,B))|((![F]: (~in(F,powerset(relation_dom(C)))|~F=E))|~in(relation_image(C,E),B)))))))),
% 0.09/0.43 inference(skolemize,[status(esa),new_symbols(skolem,[sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl]),skolemize(D,sK20_skl(C,B)),skolemize(E,sK21_skl(C,B)),skolemize(F,sK22_skl(C,B)),skolemize(D,sK23_skl(C,B)),skolemize(F,sK24_skl(E,C,B))],[f163])).
% 0.09/0.43 fof(f165,plain,(
% 0.09/0.43 ![X0,X1,X2,X3]: (~element(X0,powerset(powerset(X1)))|~relation(X2)|~function(X2)|sP0_prd(sK22_skl(X2,X0),sK21_skl(X2,X0),sK20_skl(X2,X0),X2,X0)|~in(X3,sK23_skl(X2,X0))|in(sK24_skl(X3,X2,X0),powerset(relation_dom(X2))))),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f164])).
% 0.09/0.43 fof(f166,plain,(
% 0.09/0.43 ![X0,X1,X2,X3]: (~element(X0,powerset(powerset(X1)))|~relation(X2)|~function(X2)|sP0_prd(sK22_skl(X2,X0),sK21_skl(X2,X0),sK20_skl(X2,X0),X2,X0)|~in(X3,sK23_skl(X2,X0))|sK24_skl(X3,X2,X0)=X3)),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f164])).
% 0.09/0.43 fof(f167,plain,(
% 0.09/0.43 ![X0,X1,X2,X3]: (~element(X0,powerset(powerset(X1)))|~relation(X2)|~function(X2)|sP0_prd(sK22_skl(X2,X0),sK21_skl(X2,X0),sK20_skl(X2,X0),X2,X0)|~in(X3,sK23_skl(X2,X0))|in(relation_image(X2,X3),X0))),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f164])).
% 0.09/0.43 fof(f168,plain,(
% 0.09/0.43 ![X0,X1,X2,X3,X4]: (~element(X0,powerset(powerset(X1)))|~relation(X2)|~function(X2)|sP0_prd(sK22_skl(X2,X0),sK21_skl(X2,X0),sK20_skl(X2,X0),X2,X0)|in(X3,sK23_skl(X2,X0))|~in(X4,powerset(relation_dom(X2)))|~X4=X3|~in(relation_image(X2,X3),X0))),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f164])).
% 0.09/0.43 fof(f169,plain,(
% 0.09/0.43 ![B,C,D,E,F]: ((~sP0_prd(F,E,D,C,B)|((((D=E&in(relation_image(C,E),B))&D=F)&in(relation_image(C,F),B))&~E=F))&(sP0_prd(F,E,D,C,B)|((((~D=E|~in(relation_image(C,E),B))|~D=F)|~in(relation_image(C,F),B))|E=F)))),
% 0.09/0.43 inference(NNF_transformation,[status(thm)],[f160])).
% 0.09/0.43 fof(f170,plain,(
% 0.09/0.43 (![B,C,D,E,F]: (~sP0_prd(F,E,D,C,B)|((((D=E&in(relation_image(C,E),B))&D=F)&in(relation_image(C,F),B))&~E=F)))&(![B,C,D,E,F]: (sP0_prd(F,E,D,C,B)|((((~D=E|~in(relation_image(C,E),B))|~D=F)|~in(relation_image(C,F),B))|E=F)))),
% 0.09/0.43 inference(miniscoping,[status(thm)],[f169])).
% 0.09/0.43 fof(f171,plain,(
% 0.09/0.43 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|X2=X1)),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f170])).
% 0.09/0.43 fof(f173,plain,(
% 0.09/0.43 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|X2=X0)),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f170])).
% 0.09/0.43 fof(f175,plain,(
% 0.09/0.43 ![X0,X1,X2,X3,X4]: (~sP0_prd(X0,X1,X2,X3,X4)|~X1=X0)),
% 0.09/0.43 inference(cnf_transformation,[status(thm)],[f170])).
% 0.09/0.43 fof(f180,plain,(
% 0.09/0.43 ![X0,X1,X2,X3]: (~element(X0,powerset(powerset(X1)))|~relation(X2)|~function(X2)|sP0_prd(sK22_skl(X2,X0),sK21_skl(X2,X0),sK20_skl(X2,X0),X2,X0)|in(X3,sK23_skl(X2,X0))|~in(X3,powerset(relation_dom(X2)))|~in(relation_image(X2,X3),X0))),
% 0.09/0.43 inference(destructive_equality_resolution,[status(thm)],[f168])).
% 0.09/0.43 fof(f181,plain,(
% 0.09/0.43 ![X0,X1,X2,X3]: (~sP0_prd(X0,X0,X1,X2,X3))),
% 0.09/0.43 inference(destructive_equality_resolution,[status(thm)],[f175])).
% 0.09/0.43 fof(f275,plain,(
% 0.09/0.43 ![X0,X1]: (~element(sK0_skl,powerset(powerset(X0)))|~relation(sK1_skl)|~function(sK1_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK3_skl(X1),sK23_skl(sK1_skl,sK0_skl))|~in(sK3_skl(X1),powerset(relation_dom(sK1_skl)))|in(sK3_skl(X1),X1))),
% 0.09/0.43 inference(resolution,[status(thm)],[f180,f47])).
% 0.09/0.43 fof(f276,definition,(
% 0.09/0.43 ![X0]: (sQ8_spl <=> (~element(sK0_skl,powerset(powerset(X0)))))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f277,plain,(
% 0.09/0.43 ![X0]: (~element(sK0_skl,powerset(powerset(X0)))|~sQ8_spl)),
% 0.09/0.43 inference(component_clause,[status(thm)],[f276])).
% 0.09/0.43 fof(f279,definition,(
% 0.09/0.43 sQ9_spl <=> (relation(sK1_skl))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f281,plain,(
% 0.09/0.43 ~relation(sK1_skl)|sQ9_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f279])).
% 0.09/0.43 fof(f282,definition,(
% 0.09/0.43 sQ10_spl <=> (function(sK1_skl))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f284,plain,(
% 0.09/0.43 ~function(sK1_skl)|sQ10_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f282])).
% 0.09/0.43 fof(f285,definition,(
% 0.09/0.43 sQ11_spl <=> (sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f286,plain,(
% 0.09/0.43 sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ11_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f285])).
% 0.09/0.43 fof(f288,definition,(
% 0.09/0.43 ![X1]: (sQ12_spl <=> (in(sK3_skl(X1),sK23_skl(sK1_skl,sK0_skl))|~in(sK3_skl(X1),powerset(relation_dom(sK1_skl)))|in(sK3_skl(X1),X1)))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f289,plain,(
% 0.09/0.43 ![X0]: (in(sK3_skl(X0),sK23_skl(sK1_skl,sK0_skl))|~in(sK3_skl(X0),powerset(relation_dom(sK1_skl)))|in(sK3_skl(X0),X0)|~sQ12_spl)),
% 0.09/0.43 inference(component_clause,[status(thm)],[f288])).
% 0.09/0.43 fof(f291,plain,(
% 0.09/0.43 sQ8_spl|~sQ9_spl|~sQ10_spl|sQ11_spl|sQ12_spl),
% 0.09/0.43 inference(split_clause,[status(thm)],[f275,f276,f279,f282,f285,f288])).
% 0.09/0.43 fof(f292,plain,(
% 0.09/0.43 ![X0]: (in(sK3_skl(X0),sK23_skl(sK1_skl,sK0_skl))|in(sK3_skl(X0),X0)|~sQ12_spl)),
% 0.09/0.43 inference(forward_subsumption_resolution,[status(thm)],[f289,f46])).
% 0.09/0.43 fof(f293,plain,(
% 0.09/0.43 ![X0]: (~element(sK0_skl,powerset(powerset(X0)))|~relation(sK1_skl)|~function(sK1_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(relation_image(sK1_skl,sK3_skl(sK23_skl(sK1_skl,sK0_skl))),sK0_skl)|~sQ12_spl)),
% 0.09/0.43 inference(resolution,[status(thm)],[f292,f167])).
% 0.09/0.43 fof(f295,plain,(
% 0.09/0.43 ![X0]: (~element(sK0_skl,powerset(powerset(X0)))|~relation(sK1_skl)|~function(sK1_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|sK24_skl(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK3_skl(sK23_skl(sK1_skl,sK0_skl))|~sQ12_spl)),
% 0.09/0.43 inference(resolution,[status(thm)],[f292,f166])).
% 0.09/0.43 fof(f297,plain,(
% 0.09/0.43 ![X0]: (~element(sK0_skl,powerset(powerset(X0)))|~relation(sK1_skl)|~function(sK1_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK24_skl(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(relation_dom(sK1_skl)))|~sQ12_spl)),
% 0.09/0.43 inference(resolution,[status(thm)],[f292,f165])).
% 0.09/0.43 fof(f306,definition,(
% 0.09/0.43 sQ13_spl <=> (in(relation_image(sK1_skl,sK3_skl(sK23_skl(sK1_skl,sK0_skl))),sK0_skl))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f307,plain,(
% 0.09/0.43 in(relation_image(sK1_skl,sK3_skl(sK23_skl(sK1_skl,sK0_skl))),sK0_skl)|~sQ13_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f306])).
% 0.09/0.43 fof(f309,plain,(
% 0.09/0.43 sQ8_spl|~sQ9_spl|~sQ10_spl|sQ11_spl|sQ13_spl|~sQ12_spl),
% 0.09/0.43 inference(split_clause,[status(thm)],[f293,f276,f279,f282,f285,f306,f288])).
% 0.09/0.43 fof(f314,definition,(
% 0.09/0.43 sQ15_spl <=> (sK24_skl(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK3_skl(sK23_skl(sK1_skl,sK0_skl)))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f315,plain,(
% 0.09/0.43 sK24_skl(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl)=sK3_skl(sK23_skl(sK1_skl,sK0_skl))|~sQ15_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f314])).
% 0.09/0.43 fof(f317,plain,(
% 0.09/0.43 sQ8_spl|~sQ9_spl|~sQ10_spl|sQ11_spl|sQ15_spl|~sQ12_spl),
% 0.09/0.43 inference(split_clause,[status(thm)],[f295,f276,f279,f282,f285,f314,f288])).
% 0.09/0.43 fof(f322,definition,(
% 0.09/0.43 sQ17_spl <=> (in(sK24_skl(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(relation_dom(sK1_skl))))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f323,plain,(
% 0.09/0.43 in(sK24_skl(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK1_skl,sK0_skl),powerset(relation_dom(sK1_skl)))|~sQ17_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f322])).
% 0.09/0.43 fof(f325,plain,(
% 0.09/0.43 sQ8_spl|~sQ9_spl|~sQ10_spl|sQ11_spl|sQ17_spl|~sQ12_spl),
% 0.09/0.43 inference(split_clause,[status(thm)],[f297,f276,f279,f282,f285,f322,f288])).
% 0.09/0.43 fof(f338,plain,(
% 0.09/0.43 sK20_skl(sK1_skl,sK0_skl)=sK22_skl(sK1_skl,sK0_skl)|~sQ11_spl),
% 0.09/0.43 inference(resolution,[status(thm)],[f286,f173])).
% 0.09/0.43 fof(f339,plain,(
% 0.09/0.43 sK20_skl(sK1_skl,sK0_skl)=sK21_skl(sK1_skl,sK0_skl)|~sQ11_spl),
% 0.09/0.43 inference(resolution,[status(thm)],[f286,f171])).
% 0.09/0.43 fof(f342,plain,(
% 0.09/0.43 sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ11_spl),
% 0.09/0.43 inference(backward_demodulation,[status(thm)],[f338,f286])).
% 0.09/0.43 fof(f345,plain,(
% 0.09/0.43 sP0_prd(sK20_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|~sQ11_spl),
% 0.09/0.43 inference(forward_demodulation,[status(thm)],[f339,f342])).
% 0.09/0.43 fof(f346,plain,(
% 0.09/0.43 $false|~sQ11_spl),
% 0.09/0.43 inference(forward_subsumption_resolution,[status(thm)],[f345,f181])).
% 0.09/0.43 fof(f347,plain,(
% 0.09/0.43 ~sQ11_spl),
% 0.09/0.43 inference(contradiction_clause,[status(thm)],[f346])).
% 0.09/0.43 fof(f348,plain,(
% 0.09/0.43 $false|sQ10_spl),
% 0.09/0.43 inference(forward_subsumption_resolution,[status(thm)],[f284,f45])).
% 0.09/0.43 fof(f349,plain,(
% 0.09/0.43 sQ10_spl),
% 0.09/0.43 inference(contradiction_clause,[status(thm)],[f348])).
% 0.09/0.43 fof(f350,plain,(
% 0.09/0.43 $false|sQ9_spl),
% 0.09/0.43 inference(forward_subsumption_resolution,[status(thm)],[f281,f44])).
% 0.09/0.43 fof(f351,plain,(
% 0.09/0.43 sQ9_spl),
% 0.09/0.43 inference(contradiction_clause,[status(thm)],[f350])).
% 0.09/0.43 fof(f352,plain,(
% 0.09/0.43 $false|~sQ8_spl),
% 0.09/0.43 inference(backward_subsumption_resolution,[status(thm)],[f43,f277])).
% 0.09/0.43 fof(f353,plain,(
% 0.09/0.43 ~sQ8_spl),
% 0.09/0.43 inference(contradiction_clause,[status(thm)],[f352])).
% 0.09/0.43 fof(f354,plain,(
% 0.09/0.43 in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(relation_dom(sK1_skl)))|~sQ15_spl|~sQ17_spl),
% 0.09/0.43 inference(forward_demodulation,[status(thm)],[f315,f323])).
% 0.09/0.43 fof(f383,definition,(
% 0.09/0.43 sQ20_spl <=> (empty(sK6_skl))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f384,plain,(
% 0.09/0.43 empty(sK6_skl)|~sQ20_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f383])).
% 0.09/0.43 fof(f391,plain,(
% 0.09/0.43 $false|~sQ20_spl),
% 0.09/0.43 inference(forward_subsumption_resolution,[status(thm)],[f384,f67])).
% 0.09/0.43 fof(f392,plain,(
% 0.09/0.43 ~sQ20_spl),
% 0.09/0.43 inference(contradiction_clause,[status(thm)],[f391])).
% 0.09/0.43 fof(f409,plain,(
% 0.09/0.43 ~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl))|~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(relation_dom(sK1_skl)))|~sQ13_spl),
% 0.09/0.43 inference(resolution,[status(thm)],[f307,f48])).
% 0.09/0.43 fof(f410,plain,(
% 0.09/0.43 ![X0]: (~element(sK0_skl,powerset(powerset(X0)))|~relation(sK1_skl)|~function(sK1_skl)|sP0_prd(sK22_skl(sK1_skl,sK0_skl),sK21_skl(sK1_skl,sK0_skl),sK20_skl(sK1_skl,sK0_skl),sK1_skl,sK0_skl)|in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl))|~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(relation_dom(sK1_skl)))|~sQ13_spl)),
% 0.09/0.43 inference(resolution,[status(thm)],[f307,f180])).
% 0.09/0.43 fof(f412,definition,(
% 0.09/0.43 sQ24_spl <=> (in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),sK23_skl(sK1_skl,sK0_skl)))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f415,definition,(
% 0.09/0.43 sQ25_spl <=> (in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(relation_dom(sK1_skl))))),
% 0.09/0.43 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.09/0.43 fof(f417,plain,(
% 0.09/0.43 ~in(sK3_skl(sK23_skl(sK1_skl,sK0_skl)),powerset(relation_dom(sK1_skl)))|sQ25_spl),
% 0.09/0.43 inference(component_clause,[status(thm)],[f415])).
% 0.09/0.43 fof(f418,plain,(
% 0.09/0.43 ~sQ24_spl|~sQ25_spl|~sQ13_spl),
% 0.09/0.43 inference(split_clause,[status(thm)],[f409,f412,f415,f306])).
% 0.09/0.43 fof(f419,plain,(
% 0.09/0.43 sQ8_spl|~sQ9_spl|~sQ10_spl|sQ11_spl|sQ24_spl|~sQ25_spl|~sQ13_spl),
% 0.09/0.43 inference(split_clause,[status(thm)],[f410,f276,f279,f282,f285,f412,f415,f306])).
% 0.09/0.43 fof(f420,plain,(
% 0.09/0.43 $false|~sQ15_spl|~sQ17_spl|sQ25_spl),
% 0.09/0.43 inference(forward_subsumption_resolution,[status(thm)],[f417,f354])).
% 0.09/0.43 fof(f421,plain,(
% 0.09/0.43 ~sQ15_spl|~sQ17_spl|sQ25_spl),
% 0.09/0.43 inference(contradiction_clause,[status(thm)],[f420])).
% 0.09/0.43 fof(f422,plain,(
% 0.09/0.43 $false),
% 0.09/0.43 inference(sat_refutation,[status(thm)],[f291,f309,f317,f325,f347,f349,f351,f353,f392,f418,f419,f421])).
% 0.09/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.47 % Elapsed time: 0.081054 seconds
% 0.09/0.47 % CPU time: 0.441538 seconds
% 0.09/0.47 % Total memory used: 94.300 MB
% 0.09/0.47 % Net memory used: 93.836 MB
%------------------------------------------------------------------------------