%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET787-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:12:36 PM UTC 2026
% Result : Unsatisfiable 0.13s 5.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET787-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.35 % Computer : n004.cluster.edu
% 0.10/5.35 % Model : x86_64 x86_64
% 0.10/5.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.35 % Memory : 8046.5625MB
% 0.10/5.35 % OS : Linux 6.8.0-71-generic
% 0.10/5.35 % CPULimit : 300
% 0.10/5.35 % WCLimit : 300
% 0.10/5.35 % DateTime : Mon Sep 21 05:37:54 UTC 2026
% 0.10/5.36 % CPUTime :
% 0.10/5.37 % Drodi V4.1.1
% 0.13/5.44 % Refutation found
% 0.13/5.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/5.44 % SZS output start CNFRefutation for theBenchmark
% 0.13/5.44 fof(f16,axiom,(
% 0.13/5.44 (![U,V,W]: (( ~ member(U,V)| member(U,un(W,V)) ) ))),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f17,axiom,(
% 0.13/5.44 (![U,V,W]: (( ~ member(U,V)| member(U,un(V,W)) ) ))),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f94,axiom,(
% 0.13/5.44 (![U,V]: (( ~ member(U,cons(V,eptset))| U = V ) ))),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f95,axiom,(
% 0.13/5.44 (![U,V,W]: (( ~ member(U,cons(V,W))| U = V| member(U,W) ) ))),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f102,axiom,(
% 0.13/5.44 (![U,V]: (( ~ member(U,union(V))| member(U,unionE_sk1(U,V)) ) ))),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f103,axiom,(
% 0.13/5.44 (![U,V]: (( ~ member(U,union(V))| member(unionE_sk1(U,V),V) ) ))),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f148,negated_conjecture,(
% 0.13/5.44 member(sk2,union(cons(a,cons(b,eptset)))) ),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f149,negated_conjecture,(
% 0.13/5.44 ~ member(sk2,un(a,b)) ),
% 0.13/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/5.44 fof(f170,plain,(
% 0.13/5.44 ![U,V]: (~member(U,V)|(![W]: member(U,un(W,V))))),
% 0.13/5.44 inference(miniscoping,[status(thm)],[f16])).
% 0.13/5.44 fof(f171,plain,(
% 0.13/5.44 ![X0,X1,X2]: (~member(X0,X1)|member(X0,un(X2,X1)))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f170])).
% 0.13/5.44 fof(f172,plain,(
% 0.13/5.44 ![U,V]: (~member(U,V)|(![W]: member(U,un(V,W))))),
% 0.13/5.44 inference(miniscoping,[status(thm)],[f17])).
% 0.13/5.44 fof(f173,plain,(
% 0.13/5.44 ![X0,X1,X2]: (~member(X0,X1)|member(X0,un(X1,X2)))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f172])).
% 0.13/5.44 fof(f282,plain,(
% 0.13/5.44 ![X0,X1]: (~member(X0,cons(X1,eptset))|X0=X1)),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f94])).
% 0.13/5.44 fof(f283,plain,(
% 0.13/5.44 ![U,W]: ((![V]: (~member(U,cons(V,W))|U=V))|member(U,W))),
% 0.13/5.44 inference(miniscoping,[status(thm)],[f95])).
% 0.13/5.44 fof(f284,plain,(
% 0.13/5.44 ![X0,X1,X2]: (~member(X0,cons(X1,X2))|X0=X1|member(X0,X2))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f283])).
% 0.13/5.44 fof(f297,plain,(
% 0.13/5.44 ![X0,X1]: (~member(X0,union(X1))|member(X0,unionE_sk1(X0,X1)))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f102])).
% 0.13/5.44 fof(f298,plain,(
% 0.13/5.44 ![X0,X1]: (~member(X0,union(X1))|member(unionE_sk1(X0,X1),X1))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f103])).
% 0.13/5.44 fof(f360,plain,(
% 0.13/5.44 member(sk2,union(cons(a,cons(b,eptset))))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f148])).
% 0.13/5.44 fof(f361,plain,(
% 0.13/5.44 ~member(sk2,un(a,b))),
% 0.13/5.44 inference(cnf_transformation,[status(thm)],[f149])).
% 0.13/5.44 fof(f368,plain,(
% 0.13/5.44 ~member(sk2,b)),
% 0.13/5.44 inference(resolution,[status(thm)],[f171,f361])).
% 0.13/5.44 fof(f370,plain,(
% 0.13/5.44 ~member(sk2,a)),
% 0.13/5.44 inference(resolution,[status(thm)],[f173,f361])).
% 0.13/5.44 fof(f381,plain,(
% 0.13/5.44 ![X0,X1,X2]: (unionE_sk1(X0,cons(X1,X2))=X1|member(unionE_sk1(X0,cons(X1,X2)),X2)|~member(X0,union(cons(X1,X2))))),
% 0.13/5.44 inference(resolution,[status(thm)],[f284,f298])).
% 0.13/5.44 fof(f514,plain,(
% 0.13/5.44 unionE_sk1(sk2,cons(a,cons(b,eptset)))=a|member(unionE_sk1(sk2,cons(a,cons(b,eptset))),cons(b,eptset))),
% 0.13/5.44 inference(resolution,[status(thm)],[f381,f360])).
% 0.13/5.44 fof(f516,definition,(
% 0.13/5.44 sQ2_spl <=> (unionE_sk1(sk2,cons(a,cons(b,eptset)))=a)),
% 0.13/5.44 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/5.44 fof(f517,plain,(
% 0.13/5.44 unionE_sk1(sk2,cons(a,cons(b,eptset)))=a|~sQ2_spl),
% 0.13/5.44 inference(component_clause,[status(thm)],[f516])).
% 0.13/5.44 fof(f519,definition,(
% 0.13/5.44 sQ3_spl <=> (member(unionE_sk1(sk2,cons(a,cons(b,eptset))),cons(b,eptset)))),
% 0.13/5.44 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/5.44 fof(f520,plain,(
% 0.13/5.44 member(unionE_sk1(sk2,cons(a,cons(b,eptset))),cons(b,eptset))|~sQ3_spl),
% 0.13/5.44 inference(component_clause,[status(thm)],[f519])).
% 0.13/5.44 fof(f522,plain,(
% 0.13/5.44 sQ2_spl|sQ3_spl),
% 0.13/5.44 inference(split_clause,[status(thm)],[f514,f516,f519])).
% 0.13/5.44 fof(f524,plain,(
% 0.13/5.44 ~member(sk2,union(cons(a,cons(b,eptset))))|member(sk2,a)|~sQ2_spl),
% 0.13/5.44 inference(paramodulation,[status(thm)],[f517,f297])).
% 0.13/5.44 fof(f525,definition,(
% 0.13/5.44 sQ4_spl <=> (member(sk2,union(cons(a,cons(b,eptset)))))),
% 0.13/5.44 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/5.45 fof(f527,plain,(
% 0.13/5.45 ~member(sk2,union(cons(a,cons(b,eptset))))|sQ4_spl),
% 0.13/5.45 inference(component_clause,[status(thm)],[f525])).
% 0.13/5.45 fof(f532,definition,(
% 0.13/5.45 sQ6_spl <=> (member(sk2,a))),
% 0.13/5.45 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/5.45 fof(f533,plain,(
% 0.13/5.45 member(sk2,a)|~sQ6_spl),
% 0.13/5.45 inference(component_clause,[status(thm)],[f532])).
% 0.13/5.45 fof(f535,plain,(
% 0.13/5.45 ~sQ4_spl|sQ6_spl|~sQ2_spl),
% 0.13/5.45 inference(split_clause,[status(thm)],[f524,f525,f532,f516])).
% 0.13/5.45 fof(f536,plain,(
% 0.13/5.45 $false|sQ4_spl),
% 0.13/5.45 inference(forward_subsumption_resolution,[status(thm)],[f527,f360])).
% 0.13/5.45 fof(f537,plain,(
% 0.13/5.45 sQ4_spl),
% 0.13/5.45 inference(contradiction_clause,[status(thm)],[f536])).
% 0.13/5.45 fof(f538,plain,(
% 0.13/5.45 $false|~sQ6_spl),
% 0.13/5.45 inference(forward_subsumption_resolution,[status(thm)],[f533,f370])).
% 0.13/5.45 fof(f539,plain,(
% 0.13/5.45 ~sQ6_spl),
% 0.13/5.45 inference(contradiction_clause,[status(thm)],[f538])).
% 0.13/5.45 fof(f540,plain,(
% 0.13/5.45 unionE_sk1(sk2,cons(a,cons(b,eptset)))=b|~sQ3_spl),
% 0.13/5.45 inference(resolution,[status(thm)],[f520,f282])).
% 0.13/5.45 fof(f551,plain,(
% 0.13/5.45 ~member(sk2,union(cons(a,cons(b,eptset))))|member(sk2,b)|~sQ3_spl),
% 0.13/5.45 inference(paramodulation,[status(thm)],[f540,f297])).
% 0.13/5.45 fof(f556,definition,(
% 0.13/5.45 sQ10_spl <=> (member(sk2,b))),
% 0.13/5.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/5.45 fof(f557,plain,(
% 0.13/5.45 member(sk2,b)|~sQ10_spl),
% 0.13/5.45 inference(component_clause,[status(thm)],[f556])).
% 0.13/5.45 fof(f559,plain,(
% 0.13/5.45 ~sQ4_spl|sQ10_spl|~sQ3_spl),
% 0.13/5.45 inference(split_clause,[status(thm)],[f551,f525,f556,f519])).
% 0.13/5.45 fof(f560,plain,(
% 0.13/5.45 $false|~sQ10_spl),
% 0.13/5.45 inference(forward_subsumption_resolution,[status(thm)],[f557,f368])).
% 0.13/5.45 fof(f561,plain,(
% 0.13/5.45 ~sQ10_spl),
% 0.13/5.45 inference(contradiction_clause,[status(thm)],[f560])).
% 0.13/5.45 fof(f562,plain,(
% 0.13/5.45 $false),
% 0.13/5.45 inference(sat_refutation,[status(thm)],[f522,f535,f537,f539,f559,f561])).
% 0.13/5.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.48 % Elapsed time: 0.113861 seconds
% 0.13/5.48 % CPU time: 0.593306 seconds
% 0.13/5.48 % Total memory used: 113.646 MB
% 0.13/5.48 % Net memory used: 112.909 MB
%------------------------------------------------------------------------------