%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ITP004+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 12:51:46 PM UTC 2026
% Result : Theorem 66.41s 8.98s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ITP004+2 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n017.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 20 21:35:56 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 66.41/8.98 % Refutation found
% 66.41/8.98 % SZS status Theorem for theBenchmark: Theorem is valid
% 66.41/8.98 % SZS output start CNFRefutation for theBenchmark
% 66.41/8.98 fof(f4,axiom,(
% 66.41/8.98 (! [A,B,F] :( mem(F,arr(A,B))=> (! [X] :( mem(X,A)=> mem(ap(F,X),B) ) )) )),
% 66.41/8.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.41/8.98 fof(f17,axiom,(
% 66.41/8.98 (! [A_27a] :( ne(A_27a)=> mem(c_2Epred__set_2ECHOICE(A_27a),arr(arr(A_27a,bool),A_27a)) ) )),
% 66.41/8.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.41/8.98 fof(f19,axiom,(
% 66.41/8.98 (! [A_27a] :( ne(A_27a)=> mem(c_2Epred__set_2EREST(A_27a),arr(arr(A_27a,bool),arr(A_27a,bool))) ) )),
% 66.41/8.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.41/8.98 fof(f24,axiom,(
% 66.41/8.98 (! [A_27a] :( ne(A_27a)=> (! [V0s] :( mem(V0s,arr(A_27a,bool))=> (! [V1t] :( mem(V1t,arr(A_27a,bool))=> ( p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))<=> (! [V2x] :( mem(V2x,A_27a)=> ( p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))=> p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t)) ) ) )) ) )) )) )),
% 66.41/8.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.41/8.98 fof(f25,axiom,(
% 66.41/8.98 (! [A_27a] :( ne(A_27a)=> (! [V0s] :( mem(V0s,arr(A_27a,bool))=> (! [V1x] :( mem(V1x,A_27a)=> (! [V2y] :( mem(V2y,A_27a)=> ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),V2y)))<=> ( p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V0s))& V1x != V2y ) ) ) )) )) )) )),
% 66.41/8.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.41/8.98 fof(f26,axiom,(
% 66.41/8.98 (! [A_27a] :( ne(A_27a)=> (! [V0s] :( mem(V0s,arr(A_27a,bool))=> ap(c_2Epred__set_2EREST(A_27a),V0s) = ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),ap(c_2Epred__set_2ECHOICE(A_27a),V0s)) ) )) )),
% 66.41/8.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.41/8.98 fof(f27,conjecture,(
% 66.41/8.98 (! [A_27a] :( ne(A_27a)=> (! [V0s] :( mem(V0s,arr(A_27a,bool))=> p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Epred__set_2EREST(A_27a),V0s)),V0s)) ) )) )),
% 66.41/8.98 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 66.41/8.98 fof(f28,negated_conjecture,(
% 66.41/8.98 ~((! [A_27a] :( ne(A_27a)=> (! [V0s] :( mem(V0s,arr(A_27a,bool))=> p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Epred__set_2EREST(A_27a),V0s)),V0s)) ) )) ))),
% 66.41/8.98 inference(negated_conjecture,[status(cth)],[f27])).
% 66.41/8.98 fof(f33,plain,(
% 66.41/8.98 ![A,B,F]: (~mem(F,arr(A,B))|(![X]: (~mem(X,A)|mem(ap(F,X),B))))),
% 66.41/8.98 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 66.41/8.98 fof(f34,plain,(
% 66.41/8.98 ![X0,X1,X2,X3]: (~mem(X0,arr(X1,X2))|~mem(X3,X1)|mem(ap(X0,X3),X2))),
% 66.41/8.98 inference(cnf_transformation,[status(thm)],[f33])).
% 66.41/8.98 fof(f69,plain,(
% 66.41/8.98 ![A_27a]: (~ne(A_27a)|mem(c_2Epred__set_2ECHOICE(A_27a),arr(arr(A_27a,bool),A_27a)))),
% 66.41/8.98 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 66.41/8.98 fof(f70,plain,(
% 66.41/8.98 ![X0]: (~ne(X0)|mem(c_2Epred__set_2ECHOICE(X0),arr(arr(X0,bool),X0)))),
% 66.41/8.98 inference(cnf_transformation,[status(thm)],[f69])).
% 66.41/8.98 fof(f73,plain,(
% 66.41/8.98 ![A_27a]: (~ne(A_27a)|mem(c_2Epred__set_2EREST(A_27a),arr(arr(A_27a,bool),arr(A_27a,bool))))),
% 66.41/8.98 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 66.41/8.98 fof(f74,plain,(
% 66.41/8.98 ![X0]: (~ne(X0)|mem(c_2Epred__set_2EREST(X0),arr(arr(X0,bool),arr(X0,bool))))),
% 66.41/8.98 inference(cnf_transformation,[status(thm)],[f73])).
% 66.41/8.98 fof(f89,plain,(
% 66.41/8.98 ![A_27a]: (~ne(A_27a)|(![V0s]: (~mem(V0s,arr(A_27a,bool))|(![V1t]: (~mem(V1t,arr(A_27a,bool))|(p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))<=>(![V2x]: (~mem(V2x,A_27a)|(~p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))|p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t)))))))))))),
% 66.41/8.98 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 66.41/8.98 fof(f90,plain,(
% 66.41/8.98 ![A_27a]: (~ne(A_27a)|(![V0s]: (~mem(V0s,arr(A_27a,bool))|(![V1t]: (~mem(V1t,arr(A_27a,bool))|((~p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))|(![V2x]: (~mem(V2x,A_27a)|(~p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))|p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t))))))&(p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))|(?[V2x]: (mem(V2x,A_27a)&(p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))&~p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t))))))))))))),
% 66.41/8.98 inference(NNF_transformation,[status(thm)],[f89])).
% 66.41/8.98 fof(f91,plain,(
% 66.41/8.98 ![A_27a]: (~ne(A_27a)|(![V0s]: (~mem(V0s,arr(A_27a,bool))|(![V1t]: (~mem(V1t,arr(A_27a,bool))|((~p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))|(![V2x]: (~mem(V2x,A_27a)|(~p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V0s))|p(ap(ap(c_2Ebool_2EIN(A_27a),V2x),V1t))))))&(p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),V0s),V1t))|(mem(sK2_skl(V1t,V0s,A_27a),A_27a)&(p(ap(ap(c_2Ebool_2EIN(A_27a),sK2_skl(V1t,V0s,A_27a)),V0s))&~p(ap(ap(c_2Ebool_2EIN(A_27a),sK2_skl(V1t,V0s,A_27a)),V1t)))))))))))),
% 66.41/8.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(V2x,sK2_skl(V1t,V0s,A_27a))],[f90])).
% 66.41/8.99 fof(f93,plain,(
% 66.41/8.99 ![X0,X1,X2]: (~ne(X0)|~mem(X1,arr(X0,bool))|~mem(X2,arr(X0,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))|mem(sK2_skl(X2,X1,X0),X0))),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f91])).
% 66.41/8.99 fof(f94,plain,(
% 66.41/8.99 ![X0,X1,X2]: (~ne(X0)|~mem(X1,arr(X0,bool))|~mem(X2,arr(X0,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))|p(ap(ap(c_2Ebool_2EIN(X0),sK2_skl(X2,X1,X0)),X1)))),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f91])).
% 66.41/8.99 fof(f95,plain,(
% 66.41/8.99 ![X0,X1,X2]: (~ne(X0)|~mem(X1,arr(X0,bool))|~mem(X2,arr(X0,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(X0),X1),X2))|~p(ap(ap(c_2Ebool_2EIN(X0),sK2_skl(X2,X1,X0)),X2)))),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f91])).
% 66.41/8.99 fof(f96,plain,(
% 66.41/8.99 ![A_27a]: (~ne(A_27a)|(![V0s]: (~mem(V0s,arr(A_27a,bool))|(![V1x]: (~mem(V1x,A_27a)|(![V2y]: (~mem(V2y,A_27a)|(p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),V2y)))<=>(p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V0s))&~V1x=V2y)))))))))),
% 66.41/8.99 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 66.41/8.99 fof(f97,plain,(
% 66.41/8.99 ![A_27a]: (~ne(A_27a)|(![V0s]: (~mem(V0s,arr(A_27a,bool))|(![V1x]: (~mem(V1x,A_27a)|(![V2y]: (~mem(V2y,A_27a)|((~p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),V2y)))|(p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V0s))&~V1x=V2y))&(p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),V2y)))|(~p(ap(ap(c_2Ebool_2EIN(A_27a),V1x),V0s))|V1x=V2y))))))))))),
% 66.41/8.99 inference(NNF_transformation,[status(thm)],[f96])).
% 66.41/8.99 fof(f98,plain,(
% 66.41/8.99 ![X0,X1,X2,X3]: (~ne(X0)|~mem(X1,arr(X0,bool))|~mem(X2,X0)|~mem(X3,X0)|~p(ap(ap(c_2Ebool_2EIN(X0),X2),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)))|p(ap(ap(c_2Ebool_2EIN(X0),X2),X1)))),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f97])).
% 66.41/8.99 fof(f101,plain,(
% 66.41/8.99 ![A_27a]: (~ne(A_27a)|(![V0s]: (~mem(V0s,arr(A_27a,bool))|ap(c_2Epred__set_2EREST(A_27a),V0s)=ap(ap(c_2Epred__set_2EDELETE(A_27a),V0s),ap(c_2Epred__set_2ECHOICE(A_27a),V0s)))))),
% 66.41/8.99 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 66.41/8.99 fof(f102,plain,(
% 66.41/8.99 ![X0,X1]: (~ne(X0)|~mem(X1,arr(X0,bool))|ap(c_2Epred__set_2EREST(X0),X1)=ap(ap(c_2Epred__set_2EDELETE(X0),X1),ap(c_2Epred__set_2ECHOICE(X0),X1)))),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f101])).
% 66.41/8.99 fof(f103,plain,(
% 66.41/8.99 (?[A_27a]: (ne(A_27a)&(?[V0s]: (mem(V0s,arr(A_27a,bool))&~p(ap(ap(c_2Epred__set_2ESUBSET(A_27a),ap(c_2Epred__set_2EREST(A_27a),V0s)),V0s))))))),
% 66.41/8.99 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 66.41/8.99 fof(f104,plain,(
% 66.41/8.99 (ne(sK3_skl)&(mem(sK4_skl,arr(sK3_skl,bool))&~p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)),sK4_skl))))),
% 66.41/8.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(A_27a,sK3_skl),skolemize(V0s,sK4_skl)],[f103])).
% 66.41/8.99 fof(f105,plain,(
% 66.41/8.99 ne(sK3_skl)),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f104])).
% 66.41/8.99 fof(f106,plain,(
% 66.41/8.99 mem(sK4_skl,arr(sK3_skl,bool))),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f104])).
% 66.41/8.99 fof(f107,plain,(
% 66.41/8.99 ~p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)),sK4_skl))),
% 66.41/8.99 inference(cnf_transformation,[status(thm)],[f104])).
% 66.41/8.99 fof(f113,plain,(
% 66.41/8.99 ![X0,X1]: (~ne(X0)|~mem(X1,arr(X0,bool))|mem(ap(c_2Epred__set_2EREST(X0),X1),arr(X0,bool)))),
% 66.41/8.99 inference(resolution,[status(thm)],[f74,f34])).
% 66.41/8.99 fof(f156,definition,(
% 66.41/8.99 sQ1_spl <=> (ne(sK3_skl))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f158,plain,(
% 66.41/8.99 ~ne(sK3_skl)|sQ1_spl),
% 66.41/8.99 inference(component_clause,[status(thm)],[f156])).
% 66.41/8.99 fof(f180,plain,(
% 66.41/8.99 $false|sQ1_spl),
% 66.41/8.99 inference(forward_subsumption_resolution,[status(thm)],[f158,f105])).
% 66.41/8.99 fof(f181,plain,(
% 66.41/8.99 sQ1_spl),
% 66.41/8.99 inference(contradiction_clause,[status(thm)],[f180])).
% 66.41/8.99 fof(f202,plain,(
% 66.41/8.99 mem(c_2Epred__set_2ECHOICE(sK3_skl),arr(arr(sK3_skl,bool),sK3_skl))),
% 66.41/8.99 inference(resolution,[status(thm)],[f70,f105])).
% 66.41/8.99 fof(f219,plain,(
% 66.41/8.99 ![X0]: (~mem(X0,arr(sK3_skl,bool))|mem(ap(c_2Epred__set_2ECHOICE(sK3_skl),X0),sK3_skl))),
% 66.41/8.99 inference(resolution,[status(thm)],[f202,f34])).
% 66.41/8.99 fof(f255,plain,(
% 66.41/8.99 mem(ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl),sK3_skl)),
% 66.41/8.99 inference(resolution,[status(thm)],[f219,f106])).
% 66.41/8.99 fof(f584,definition,(
% 66.41/8.99 sQ52_spl <=> (mem(sK4_skl,arr(sK3_skl,bool)))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f586,plain,(
% 66.41/8.99 ~mem(sK4_skl,arr(sK3_skl,bool))|sQ52_spl),
% 66.41/8.99 inference(component_clause,[status(thm)],[f584])).
% 66.41/8.99 fof(f591,plain,(
% 66.41/8.99 $false|sQ52_spl),
% 66.41/8.99 inference(forward_subsumption_resolution,[status(thm)],[f586,f106])).
% 66.41/8.99 fof(f592,plain,(
% 66.41/8.99 sQ52_spl),
% 66.41/8.99 inference(contradiction_clause,[status(thm)],[f591])).
% 66.41/8.99 fof(f718,plain,(
% 66.41/8.99 ![X0,X1,X2,X3]: (~ne(X0)|~mem(X1,arr(X0,bool))|~mem(sK2_skl(X2,ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3),X0),X0)|~mem(X3,X0)|p(ap(ap(c_2Ebool_2EIN(X0),sK2_skl(X2,ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3),X0)),X1))|~ne(X0)|~mem(ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3),arr(X0,bool))|~mem(X2,arr(X0,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)),X2)))),
% 66.41/8.99 inference(resolution,[status(thm)],[f98,f94])).
% 66.41/8.99 fof(f720,plain,(
% 66.41/8.99 ![X0,X1,X2,X3]: (~ne(X0)|~mem(X1,arr(X0,bool))|~mem(sK2_skl(X2,ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3),X0),X0)|~mem(X3,X0)|p(ap(ap(c_2Ebool_2EIN(X0),sK2_skl(X2,ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3),X0)),X1))|~mem(ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3),arr(X0,bool))|~mem(X2,arr(X0,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X3)),X2)))),
% 66.41/8.99 inference(duplicate_literals_removal,[status(thm)],[f718])).
% 66.41/8.99 fof(f721,plain,(
% 66.41/8.99 ![X0,X1,X2,X3]: (~ne(X0)|~mem(X1,arr(X0,bool))|~mem(X2,X0)|p(ap(ap(c_2Ebool_2EIN(X0),sK2_skl(X3,ap(ap(c_2Epred__set_2EDELETE(X0),X1),X2),X0)),X1))|~mem(ap(ap(c_2Epred__set_2EDELETE(X0),X1),X2),arr(X0,bool))|~mem(X3,arr(X0,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(X0),ap(ap(c_2Epred__set_2EDELETE(X0),X1),X2)),X3)))),
% 66.41/8.99 inference(forward_subsumption_resolution,[status(thm)],[f720,f93])).
% 66.41/8.99 fof(f931,plain,(
% 66.41/8.99 ![X0]: (~mem(X0,arr(sK3_skl,bool))|ap(c_2Epred__set_2EREST(sK3_skl),X0)=ap(ap(c_2Epred__set_2EDELETE(sK3_skl),X0),ap(c_2Epred__set_2ECHOICE(sK3_skl),X0)))),
% 66.41/8.99 inference(resolution,[status(thm)],[f102,f105])).
% 66.41/8.99 fof(f997,plain,(
% 66.41/8.99 ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)=ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl))),
% 66.41/8.99 inference(resolution,[status(thm)],[f931,f106])).
% 66.41/8.99 fof(f6411,plain,(
% 66.41/8.99 ![X0]: (~ne(sK3_skl)|~mem(sK4_skl,arr(sK3_skl,bool))|~mem(ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl),sK3_skl)|p(ap(ap(c_2Ebool_2EIN(sK3_skl),sK2_skl(X0,ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl)),sK3_skl)),sK4_skl))|~mem(ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl),arr(sK3_skl,bool))|~mem(X0,arr(sK3_skl,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl))),X0)))),
% 66.41/8.99 inference(paramodulation,[status(thm)],[f997,f721])).
% 66.41/8.99 fof(f6416,definition,(
% 66.41/8.99 sQ513_spl <=> (mem(ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl),sK3_skl))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ513_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f6418,plain,(
% 66.41/8.99 ~mem(ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl),sK3_skl)|sQ513_spl),
% 66.41/8.99 inference(component_clause,[status(thm)],[f6416])).
% 66.41/8.99 fof(f6419,definition,(
% 66.41/8.99 ![X0]: (sQ514_spl <=> (p(ap(ap(c_2Ebool_2EIN(sK3_skl),sK2_skl(X0,ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl)),sK3_skl)),sK4_skl))|~mem(X0,arr(sK3_skl,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl))),X0))))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f6420,plain,(
% 66.41/8.99 ![X0]: (p(ap(ap(c_2Ebool_2EIN(sK3_skl),sK2_skl(X0,ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl)),sK3_skl)),sK4_skl))|~mem(X0,arr(sK3_skl,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl))),X0))|~sQ514_spl)),
% 66.41/8.99 inference(component_clause,[status(thm)],[f6419])).
% 66.41/8.99 fof(f6422,definition,(
% 66.41/8.99 sQ515_spl <=> (mem(ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl),arr(sK3_skl,bool)))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ515_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f6424,plain,(
% 66.41/8.99 ~mem(ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl),arr(sK3_skl,bool))|sQ515_spl),
% 66.41/8.99 inference(component_clause,[status(thm)],[f6422])).
% 66.41/8.99 fof(f6425,plain,(
% 66.41/8.99 ~sQ1_spl|~sQ52_spl|~sQ513_spl|sQ514_spl|~sQ515_spl),
% 66.41/8.99 inference(split_clause,[status(thm)],[f6411,f156,f584,f6416,f6419,f6422])).
% 66.41/8.99 fof(f6442,plain,(
% 66.41/8.99 $false|sQ513_spl),
% 66.41/8.99 inference(forward_subsumption_resolution,[status(thm)],[f6418,f255])).
% 66.41/8.99 fof(f6443,plain,(
% 66.41/8.99 sQ513_spl),
% 66.41/8.99 inference(contradiction_clause,[status(thm)],[f6442])).
% 66.41/8.99 fof(f6446,plain,(
% 66.41/8.99 ![X0]: (p(ap(ap(c_2Ebool_2EIN(sK3_skl),sK2_skl(X0,ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl),sK3_skl)),sK4_skl))|~mem(X0,arr(sK3_skl,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(ap(c_2Epred__set_2EDELETE(sK3_skl),sK4_skl),ap(c_2Epred__set_2ECHOICE(sK3_skl),sK4_skl))),X0))|~sQ514_spl)),
% 66.41/8.99 inference(forward_demodulation,[status(thm)],[f997,f6420])).
% 66.41/8.99 fof(f6447,plain,(
% 66.41/8.99 ![X0]: (p(ap(ap(c_2Ebool_2EIN(sK3_skl),sK2_skl(X0,ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl),sK3_skl)),sK4_skl))|~mem(X0,arr(sK3_skl,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)),X0))|~sQ514_spl)),
% 66.41/8.99 inference(forward_demodulation,[status(thm)],[f997,f6446])).
% 66.41/8.99 fof(f6448,plain,(
% 66.41/8.99 ~ne(sK3_skl)|~mem(sK4_skl,arr(sK3_skl,bool))|sQ515_spl),
% 66.41/8.99 inference(resolution,[status(thm)],[f6424,f113])).
% 66.41/8.99 fof(f6449,plain,(
% 66.41/8.99 ~sQ1_spl|~sQ52_spl|sQ515_spl),
% 66.41/8.99 inference(split_clause,[status(thm)],[f6448,f156,f584,f6422])).
% 66.41/8.99 fof(f7430,definition,(
% 66.41/8.99 sQ580_spl <=> (p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)),sK4_skl)))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ580_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f7431,plain,(
% 66.41/8.99 p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)),sK4_skl))|~sQ580_spl),
% 66.41/8.99 inference(component_clause,[status(thm)],[f7430])).
% 66.41/8.99 fof(f7458,plain,(
% 66.41/8.99 $false|~sQ580_spl),
% 66.41/8.99 inference(forward_subsumption_resolution,[status(thm)],[f7431,f107])).
% 66.41/8.99 fof(f7459,plain,(
% 66.41/8.99 ~sQ580_spl),
% 66.41/8.99 inference(contradiction_clause,[status(thm)],[f7458])).
% 66.41/8.99 fof(f7800,definition,(
% 66.41/8.99 sQ607_spl <=> (ap(c_2Epred__set_2EDELETE(bool),sK0_skl(c_2Epred__set_2EDELETE(bool),c_2Epred__set_2EDELETE(bool),arr(bool,arr(bool,bool)),arr(bool,bool)))=ap(c_2Epred__set_2EDELETE(bool),sK0_skl(c_2Epred__set_2EDELETE(bool),c_2Epred__set_2EDELETE(bool),arr(bool,arr(bool,bool)),arr(bool,bool))))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ607_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f7802,plain,(
% 66.41/8.99 ~ap(c_2Epred__set_2EDELETE(bool),sK0_skl(c_2Epred__set_2EDELETE(bool),c_2Epred__set_2EDELETE(bool),arr(bool,arr(bool,bool)),arr(bool,bool)))=ap(c_2Epred__set_2EDELETE(bool),sK0_skl(c_2Epred__set_2EDELETE(bool),c_2Epred__set_2EDELETE(bool),arr(bool,arr(bool,bool)),arr(bool,bool)))|sQ607_spl),
% 66.41/8.99 inference(component_clause,[status(thm)],[f7800])).
% 66.41/8.99 fof(f7807,plain,(
% 66.41/8.99 $false|sQ607_spl),
% 66.41/8.99 inference(trivial_equality_resolution,[status(thm)],[f7802])).
% 66.41/8.99 fof(f7808,plain,(
% 66.41/8.99 sQ607_spl),
% 66.41/8.99 inference(contradiction_clause,[status(thm)],[f7807])).
% 66.41/8.99 fof(f8782,definition,(
% 66.41/8.99 sQ679_spl <=> (ap(c_2Epred__set_2EDELETE(ind),sK0_skl(c_2Epred__set_2EDELETE(ind),c_2Epred__set_2EDELETE(ind),arr(ind,arr(ind,bool)),arr(ind,bool)))=ap(c_2Epred__set_2EDELETE(ind),sK0_skl(c_2Epred__set_2EDELETE(ind),c_2Epred__set_2EDELETE(ind),arr(ind,arr(ind,bool)),arr(ind,bool))))),
% 66.41/8.99 introduced(definition,[new_symbols(definition,[sQ679_spl])],[split_symbol_definition])).
% 66.41/8.99 fof(f8784,plain,(
% 66.41/8.99 ~ap(c_2Epred__set_2EDELETE(ind),sK0_skl(c_2Epred__set_2EDELETE(ind),c_2Epred__set_2EDELETE(ind),arr(ind,arr(ind,bool)),arr(ind,bool)))=ap(c_2Epred__set_2EDELETE(ind),sK0_skl(c_2Epred__set_2EDELETE(ind),c_2Epred__set_2EDELETE(ind),arr(ind,arr(ind,bool)),arr(ind,bool)))|sQ679_spl),
% 61.39/9.06 inference(component_clause,[status(thm)],[f8782])).
% 61.39/9.06 fof(f8789,plain,(
% 61.39/9.06 $false|sQ679_spl),
% 61.39/9.06 inference(trivial_equality_resolution,[status(thm)],[f8784])).
% 61.39/9.06 fof(f8790,plain,(
% 61.39/9.06 sQ679_spl),
% 61.39/9.06 inference(contradiction_clause,[status(thm)],[f8789])).
% 61.39/9.06 fof(f16904,plain,(
% 61.39/9.06 ~mem(sK4_skl,arr(sK3_skl,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)),sK4_skl))|~ne(sK3_skl)|~mem(ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl),arr(sK3_skl,bool))|~mem(sK4_skl,arr(sK3_skl,bool))|p(ap(ap(c_2Epred__set_2ESUBSET(sK3_skl),ap(c_2Epred__set_2EREST(sK3_skl),sK4_skl)),sK4_skl))|~sQ514_spl),
% 61.39/9.06 inference(resolution,[status(thm)],[f6447,f95])).
% 61.39/9.06 fof(f16907,plain,(
% 61.39/9.06 ~sQ52_spl|sQ580_spl|~sQ1_spl|~sQ515_spl|~sQ514_spl),
% 61.39/9.06 inference(split_clause,[status(thm)],[f16904,f584,f7430,f156,f6422,f6419])).
% 61.39/9.06 fof(f16916,plain,(
% 61.39/9.06 $false),
% 61.39/9.06 inference(sat_refutation,[status(thm)],[f181,f592,f6425,f6443,f6449,f7459,f7808,f8790,f16907])).
% 61.39/9.06 % SZS output end CNFRefutation for theBenchmark.p
% 9.27/9.15 % Elapsed time: 8.696112 seconds
% 9.27/9.15 % CPU time: 67.831030 seconds
% 9.27/9.15 % Total memory used: 701.112 MB
% 9.27/9.15 % Net memory used: 626.359 MB
%------------------------------------------------------------------------------