%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET010-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:11:09 PM UTC 2026
% Result : Unsatisfiable 21.47s 3.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET010-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n014.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 04:41:05 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 21.47/3.13 % Refutation found
% 21.47/3.13 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 21.47/3.13 % SZS output start CNFRefutation for theBenchmark
% 21.47/3.13 fof(f10,axiom,(
% 21.47/3.13 (![Set1,Set2,Union]: (( union(Set1,Set2,Union)| member(g(Set1,Set2,Union),Set1)| member(g(Set1,Set2,Union),Set2)| member(g(Set1,Set2,Union),Union) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f11,axiom,(
% 21.47/3.13 (![Set1,Set2,Union]: (( ~ member(g(Set1,Set2,Union),Set1)| ~ member(g(Set1,Set2,Union),Union)| union(Set1,Set2,Union) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f12,axiom,(
% 21.47/3.13 (![Set1,Set2,Union]: (( ~ member(g(Set1,Set2,Union),Set2)| ~ member(g(Set1,Set2,Union),Union)| union(Set1,Set2,Union) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f13,axiom,(
% 21.47/3.13 (![Set1,Set2,Intersection,Element]: (( ~ intersection(Set1,Set2,Intersection)| ~ member(Element,Intersection)| member(Element,Set1) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f14,axiom,(
% 21.47/3.13 (![Set1,Set2,Intersection,Element]: (( ~ intersection(Set1,Set2,Intersection)| ~ member(Element,Intersection)| member(Element,Set2) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f15,axiom,(
% 21.47/3.13 (![Set1,Set2,Intersection,Element]: (( ~ intersection(Set1,Set2,Intersection)| ~ member(Element,Set2)| ~ member(Element,Set1)| member(Element,Intersection) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f19,axiom,(
% 21.47/3.13 (![Set1,Set2,Difference,Element]: (( ~ difference(Set1,Set2,Difference)| ~ member(Element,Difference)| member(Element,Set1) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f20,axiom,(
% 21.47/3.13 (![Element,Set1,Set2,A_set]: (( ~ member(Element,Set1)| ~ member(Element,Set2)| ~ difference(A_set,Set1,Set2) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f21,axiom,(
% 21.47/3.13 (![Element,Set1,Set2,Difference]: (( ~ member(Element,Set1)| ~ difference(Set1,Set2,Difference)| member(Element,Difference)| member(Element,Set2) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f22,axiom,(
% 21.47/3.13 (![Set1,Set2,Difference]: (( difference(Set1,Set2,Difference)| member(k(Set1,Set2,Difference),Set1)| member(k(Set1,Set2,Difference),Difference) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f24,axiom,(
% 21.47/3.13 (![Set1,Set2,Difference]: (( ~ member(k(Set1,Set2,Difference),Difference)| ~ member(k(Set1,Set2,Difference),Set1)| member(k(Set1,Set2,Difference),Set2)| difference(Set1,Set2,Difference) ) ))),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f25,hypothesis,(
% 21.47/3.13 intersection(a,b,aIb) ),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f26,hypothesis,(
% 21.47/3.13 difference(c,a,cDa) ),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f27,hypothesis,(
% 21.47/3.13 difference(c,b,cDb) ),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f28,hypothesis,(
% 21.47/3.13 difference(c,aIb,cD_aIb) ),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f29,negated_conjecture,(
% 21.47/3.13 ~ union(cDa,cDb,cD_aIb) ),
% 21.47/3.13 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 21.47/3.13 fof(f43,plain,(
% 21.47/3.13 ![X0,X1,X2]: (union(X0,X1,X2)|member(g(X0,X1,X2),X0)|member(g(X0,X1,X2),X1)|member(g(X0,X1,X2),X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f10])).
% 21.47/3.13 fof(f44,plain,(
% 21.47/3.13 ![X0,X1,X2]: (~member(g(X0,X1,X2),X0)|~member(g(X0,X1,X2),X2)|union(X0,X1,X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f11])).
% 21.47/3.13 fof(f45,plain,(
% 21.47/3.13 ![X0,X1,X2]: (~member(g(X0,X1,X2),X1)|~member(g(X0,X1,X2),X2)|union(X0,X1,X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f12])).
% 21.47/3.13 fof(f46,plain,(
% 21.47/3.13 ![Set1,Element]: ((![Intersection]: ((![Set2]: ~intersection(Set1,Set2,Intersection))|~member(Element,Intersection)))|member(Element,Set1))),
% 21.47/3.13 inference(miniscoping,[status(thm)],[f13])).
% 21.47/3.13 fof(f47,plain,(
% 21.47/3.13 ![X0,X1,X2,X3]: (~intersection(X0,X1,X2)|~member(X3,X2)|member(X3,X0))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f46])).
% 21.47/3.13 fof(f48,plain,(
% 21.47/3.13 ![Set2,Element]: ((![Intersection]: ((![Set1]: ~intersection(Set1,Set2,Intersection))|~member(Element,Intersection)))|member(Element,Set2))),
% 21.47/3.13 inference(miniscoping,[status(thm)],[f14])).
% 21.47/3.13 fof(f49,plain,(
% 21.47/3.13 ![X0,X1,X2,X3]: (~intersection(X0,X1,X2)|~member(X3,X2)|member(X3,X1))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f48])).
% 21.47/3.13 fof(f50,plain,(
% 21.47/3.13 ![Intersection,Element]: ((![Set1]: ((![Set2]: (~intersection(Set1,Set2,Intersection)|~member(Element,Set2)))|~member(Element,Set1)))|member(Element,Intersection))),
% 21.47/3.13 inference(miniscoping,[status(thm)],[f15])).
% 21.47/3.13 fof(f51,plain,(
% 21.47/3.13 ![X0,X1,X2,X3]: (~intersection(X0,X1,X2)|~member(X3,X1)|~member(X3,X0)|member(X3,X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f50])).
% 21.47/3.13 fof(f55,plain,(
% 21.47/3.13 ![Set1,Element]: ((![Difference]: ((![Set2]: ~difference(Set1,Set2,Difference))|~member(Element,Difference)))|member(Element,Set1))),
% 21.47/3.13 inference(miniscoping,[status(thm)],[f19])).
% 21.47/3.13 fof(f56,plain,(
% 21.47/3.13 ![X0,X1,X2,X3]: (~difference(X0,X1,X2)|~member(X3,X2)|member(X3,X0))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f55])).
% 21.47/3.13 fof(f57,plain,(
% 21.47/3.13 ![Set1,Set2]: ((![Element]: (~member(Element,Set1)|~member(Element,Set2)))|(![A_set]: ~difference(A_set,Set1,Set2)))),
% 21.47/3.13 inference(miniscoping,[status(thm)],[f20])).
% 21.47/3.13 fof(f58,plain,(
% 21.47/3.13 ![X0,X1,X2,X3]: (~member(X0,X1)|~member(X0,X2)|~difference(X3,X1,X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f57])).
% 21.47/3.13 fof(f59,plain,(
% 21.47/3.13 ![Element,Set2]: ((![Difference]: ((![Set1]: (~member(Element,Set1)|~difference(Set1,Set2,Difference)))|member(Element,Difference)))|member(Element,Set2))),
% 21.47/3.13 inference(miniscoping,[status(thm)],[f21])).
% 21.47/3.13 fof(f60,plain,(
% 21.47/3.13 ![X0,X1,X2,X3]: (~member(X0,X1)|~difference(X1,X2,X3)|member(X0,X3)|member(X0,X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f59])).
% 21.47/3.13 fof(f61,plain,(
% 21.47/3.13 ![X0,X1,X2]: (difference(X0,X1,X2)|member(k(X0,X1,X2),X0)|member(k(X0,X1,X2),X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f22])).
% 21.47/3.13 fof(f63,plain,(
% 21.47/3.13 ![X0,X1,X2]: (~member(k(X0,X1,X2),X2)|~member(k(X0,X1,X2),X0)|member(k(X0,X1,X2),X1)|difference(X0,X1,X2))),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f24])).
% 21.47/3.13 fof(f64,plain,(
% 21.47/3.13 intersection(a,b,aIb)),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f25])).
% 21.47/3.13 fof(f65,plain,(
% 21.47/3.13 difference(c,a,cDa)),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f26])).
% 21.47/3.13 fof(f66,plain,(
% 21.47/3.13 difference(c,b,cDb)),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f27])).
% 21.47/3.13 fof(f67,plain,(
% 21.47/3.13 difference(c,aIb,cD_aIb)),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f28])).
% 21.47/3.13 fof(f68,plain,(
% 21.47/3.13 ~union(cDa,cDb,cD_aIb)),
% 21.47/3.13 inference(cnf_transformation,[status(thm)],[f29])).
% 21.47/3.13 fof(f104,plain,(
% 21.47/3.13 ![X0]: (~member(X0,aIb)|~member(X0,cD_aIb))),
% 21.47/3.13 inference(resolution,[status(thm)],[f58,f67])).
% 21.47/3.13 fof(f105,plain,(
% 21.47/3.13 ![X0]: (~member(X0,b)|~member(X0,cDb))),
% 21.47/3.13 inference(resolution,[status(thm)],[f58,f66])).
% 21.47/3.13 fof(f106,plain,(
% 21.47/3.13 ![X0]: (~member(X0,a)|~member(X0,cDa))),
% 21.47/3.13 inference(resolution,[status(thm)],[f58,f65])).
% 21.47/3.13 fof(f107,plain,(
% 21.47/3.13 ![X0]: (~member(X0,b)|~member(X0,a)|member(X0,aIb))),
% 21.47/3.13 inference(resolution,[status(thm)],[f64,f51])).
% 21.47/3.13 fof(f108,plain,(
% 21.47/3.13 ![X0]: (~member(X0,aIb)|member(X0,b))),
% 21.47/3.13 inference(resolution,[status(thm)],[f64,f49])).
% 21.47/3.13 fof(f109,plain,(
% 21.47/3.13 ![X0]: (~member(X0,aIb)|member(X0,a))),
% 21.47/3.13 inference(resolution,[status(thm)],[f64,f47])).
% 21.47/3.13 fof(f217,plain,(
% 21.47/3.13 ![X0]: (~member(X0,cD_aIb)|member(X0,c))),
% 21.47/3.13 inference(resolution,[status(thm)],[f56,f67])).
% 21.47/3.13 fof(f218,plain,(
% 21.47/3.13 ![X0]: (~member(X0,cDb)|member(X0,c))),
% 21.47/3.13 inference(resolution,[status(thm)],[f56,f66])).
% 21.47/3.13 fof(f219,plain,(
% 21.47/3.13 ![X0]: (~member(X0,cDa)|member(X0,c))),
% 21.47/3.13 inference(resolution,[status(thm)],[f56,f65])).
% 21.47/3.13 fof(f230,plain,(
% 21.47/3.13 ![X0,X1]: (member(g(X0,X1,cD_aIb),c)|union(X0,X1,cD_aIb)|member(g(X0,X1,cD_aIb),X0)|member(g(X0,X1,cD_aIb),X1))),
% 21.47/3.13 inference(resolution,[status(thm)],[f217,f43])).
% 21.47/3.13 fof(f265,plain,(
% 21.47/3.13 ![X0]: (~member(X0,c)|member(X0,cD_aIb)|member(X0,aIb))),
% 21.47/3.13 inference(resolution,[status(thm)],[f60,f67])).
% 21.47/3.13 fof(f266,plain,(
% 21.47/3.13 ![X0]: (~member(X0,c)|member(X0,cDb)|member(X0,b))),
% 21.47/3.13 inference(resolution,[status(thm)],[f60,f66])).
% 21.47/3.13 fof(f267,plain,(
% 21.47/3.13 ![X0]: (~member(X0,c)|member(X0,cDa)|member(X0,a))),
% 21.47/3.13 inference(resolution,[status(thm)],[f60,f65])).
% 21.47/3.13 fof(f274,plain,(
% 21.47/3.13 ![X0]: (difference(cDa,X0,cDa)|~member(k(cDa,X0,cDa),a))),
% 21.47/3.13 inference(resolution,[status(thm)],[f61,f106])).
% 21.47/3.13 fof(f278,plain,(
% 21.47/3.13 ![X0]: (difference(cDb,X0,cDb)|~member(k(cDb,X0,cDb),b))),
% 21.47/3.13 inference(resolution,[status(thm)],[f61,f105])).
% 21.47/3.13 fof(f292,plain,(
% 21.47/3.13 ![X0,X1]: (difference(X0,X1,X0)|member(k(X0,X1,X0),X0))),
% 21.47/3.13 inference(factoring,[status(thm)],[f61])).
% 21.47/3.13 fof(f427,plain,(
% 21.47/3.13 ![X0,X1]: (~member(k(X0,X1,X0),X0)|member(k(X0,X1,X0),X1)|difference(X0,X1,X0)|difference(X0,X1,X0))),
% 21.47/3.13 inference(resolution,[status(thm)],[f63,f292])).
% 21.47/3.13 fof(f432,plain,(
% 21.47/3.13 ![X0,X1]: (~member(k(X0,X1,X0),X0)|member(k(X0,X1,X0),X1)|difference(X0,X1,X0))),
% 21.47/3.13 inference(duplicate_literals_removal,[status(thm)],[f427])).
% 21.47/3.13 fof(f433,plain,(
% 21.47/3.13 ![X0,X1]: (member(k(X0,X1,X0),X1)|difference(X0,X1,X0))),
% 21.47/3.13 inference(forward_subsumption_resolution,[status(thm)],[f432,f292])).
% 21.47/3.13 fof(f610,plain,(
% 21.47/3.13 ![X0]: (difference(X0,aIb,X0)|member(k(X0,aIb,X0),a))),
% 21.47/3.13 inference(resolution,[status(thm)],[f433,f109])).
% 21.47/3.13 fof(f611,plain,(
% 21.47/3.13 ![X0]: (difference(X0,aIb,X0)|member(k(X0,aIb,X0),b))),
% 21.47/3.13 inference(resolution,[status(thm)],[f433,f108])).
% 21.47/3.13 fof(f1906,plain,(
% 21.47/3.13 difference(cDa,aIb,cDa)|difference(cDa,aIb,cDa)),
% 21.47/3.13 inference(resolution,[status(thm)],[f274,f610])).
% 21.47/3.13 fof(f1908,plain,(
% 21.47/3.13 difference(cDa,aIb,cDa)),
% 21.47/3.13 inference(duplicate_literals_removal,[status(thm)],[f1906])).
% 21.47/3.13 fof(f1912,plain,(
% 21.47/3.13 ![X0]: (~member(X0,aIb)|~member(X0,cDa))),
% 21.47/3.13 inference(resolution,[status(thm)],[f1908,f58])).
% 21.47/3.13 fof(f2169,plain,(
% 21.47/3.13 ![X0]: (member(g(cDa,X0,cD_aIb),c)|union(cDa,X0,cD_aIb)|member(g(cDa,X0,cD_aIb),X0)|member(g(cDa,X0,cD_aIb),c))),
% 21.47/3.13 inference(resolution,[status(thm)],[f230,f219])).
% 21.47/3.13 fof(f2214,plain,(
% 21.47/3.13 ![X0]: (member(g(cDa,X0,cD_aIb),c)|union(cDa,X0,cD_aIb)|member(g(cDa,X0,cD_aIb),X0))),
% 21.47/3.13 inference(duplicate_literals_removal,[status(thm)],[f2169])).
% 21.47/3.13 fof(f2430,plain,(
% 21.47/3.13 difference(cDb,aIb,cDb)|difference(cDb,aIb,cDb)),
% 21.47/3.13 inference(resolution,[status(thm)],[f278,f611])).
% 21.47/3.13 fof(f2432,plain,(
% 21.47/3.13 difference(cDb,aIb,cDb)),
% 21.47/3.13 inference(duplicate_literals_removal,[status(thm)],[f2430])).
% 21.47/3.13 fof(f2436,plain,(
% 21.47/3.13 ![X0]: (~member(X0,aIb)|~member(X0,cDb))),
% 21.47/3.13 inference(resolution,[status(thm)],[f2432,f58])).
% 21.47/3.13 fof(f15621,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),c)|union(cDa,cDb,cD_aIb)|member(g(cDa,cDb,cD_aIb),c)),
% 21.47/3.13 inference(resolution,[status(thm)],[f2214,f218])).
% 21.47/3.13 fof(f15636,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),c)|union(cDa,cDb,cD_aIb)),
% 21.47/3.13 inference(duplicate_literals_removal,[status(thm)],[f15621])).
% 21.47/3.13 fof(f15637,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),c)),
% 21.47/3.13 inference(forward_subsumption_resolution,[status(thm)],[f15636,f68])).
% 21.47/3.13 fof(f15640,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),cDa)|member(g(cDa,cDb,cD_aIb),a)),
% 21.47/3.13 inference(resolution,[status(thm)],[f15637,f267])).
% 21.47/3.13 fof(f15641,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),cDb)|member(g(cDa,cDb,cD_aIb),b)),
% 21.47/3.13 inference(resolution,[status(thm)],[f15637,f266])).
% 21.47/3.13 fof(f15642,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),cD_aIb)|member(g(cDa,cDb,cD_aIb),aIb)),
% 21.47/3.13 inference(resolution,[status(thm)],[f15637,f265])).
% 21.47/3.13 fof(f15784,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),aIb)|~member(g(cDa,cDb,cD_aIb),cDb)|union(cDa,cDb,cD_aIb)),
% 21.47/3.13 inference(resolution,[status(thm)],[f15642,f45])).
% 21.47/3.13 fof(f15785,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),aIb)|~member(g(cDa,cDb,cD_aIb),cDa)|union(cDa,cDb,cD_aIb)),
% 21.47/3.13 inference(resolution,[status(thm)],[f15642,f44])).
% 21.47/3.13 fof(f15788,plain,(
% 21.47/3.13 ~member(g(cDa,cDb,cD_aIb),cDb)|union(cDa,cDb,cD_aIb)),
% 21.47/3.13 inference(forward_subsumption_resolution,[status(thm)],[f15784,f2436])).
% 21.47/3.13 fof(f15789,plain,(
% 21.47/3.13 ~member(g(cDa,cDb,cD_aIb),cDa)|union(cDa,cDb,cD_aIb)),
% 21.47/3.13 inference(forward_subsumption_resolution,[status(thm)],[f15785,f1912])).
% 21.47/3.13 fof(f15790,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),b)),
% 21.47/3.13 inference(backward_subsumption_resolution,[status(thm)],[f15641,f15791])).
% 21.47/3.13 fof(f15791,plain,(
% 21.47/3.13 ~member(g(cDa,cDb,cD_aIb),cDb)),
% 21.47/3.13 inference(forward_subsumption_resolution,[status(thm)],[f15788,f68])).
% 21.47/3.13 fof(f15800,plain,(
% 21.47/3.13 union(cDa,cDb,cD_aIb)|member(g(cDa,cDb,cD_aIb),cDa)|member(g(cDa,cDb,cD_aIb),cD_aIb)),
% 21.47/3.13 inference(resolution,[status(thm)],[f15791,f43])).
% 21.47/3.13 fof(f15806,plain,(
% 21.47/3.13 member(g(cDa,cDb,cD_aIb),cDa)|member(g(cDa,cDb,cD_aIb),cD_aIb)),
% 21.47/3.16 inference(forward_subsumption_resolution,[status(thm)],[f15800,f68])).
% 21.47/3.16 fof(f15808,plain,(
% 21.47/3.16 ~member(g(cDa,cDb,cD_aIb),a)|member(g(cDa,cDb,cD_aIb),aIb)),
% 21.47/3.16 inference(resolution,[status(thm)],[f15790,f107])).
% 21.47/3.16 fof(f15810,plain,(
% 21.47/3.16 member(g(cDa,cDb,cD_aIb),a)),
% 21.47/3.16 inference(backward_subsumption_resolution,[status(thm)],[f15640,f15811])).
% 21.47/3.16 fof(f15811,plain,(
% 21.47/3.16 ~member(g(cDa,cDb,cD_aIb),cDa)),
% 21.47/3.16 inference(forward_subsumption_resolution,[status(thm)],[f15789,f68])).
% 21.47/3.16 fof(f15866,plain,(
% 21.47/3.16 member(g(cDa,cDb,cD_aIb),cD_aIb)),
% 21.47/3.16 inference(forward_subsumption_resolution,[status(thm)],[f15806,f15811])).
% 21.47/3.16 fof(f15870,plain,(
% 21.47/3.16 ~member(g(cDa,cDb,cD_aIb),aIb)),
% 21.47/3.16 inference(resolution,[status(thm)],[f15866,f104])).
% 21.47/3.16 fof(f15872,plain,(
% 21.47/3.16 member(g(cDa,cDb,cD_aIb),aIb)),
% 21.47/3.16 inference(forward_subsumption_resolution,[status(thm)],[f15808,f15810])).
% 21.47/3.16 fof(f15873,plain,(
% 21.47/3.16 $false),
% 21.47/3.16 inference(backward_subsumption_resolution,[status(thm)],[f15870,f15872])).
% 21.47/3.16 % SZS output end CNFRefutation for theBenchmark.p
% 21.47/3.17 % Elapsed time: 2.798398 seconds
% 21.47/3.17 % CPU time: 21.968513 seconds
% 21.47/3.17 % Total memory used: 180.361 MB
% 21.47/3.17 % Net memory used: 161.806 MB
%------------------------------------------------------------------------------