%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET041-3 : 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 : n018.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:19 PM UTC 2026
% Result : Unsatisfiable 9.74s 1.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET041-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n018.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 04:48:58 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 9.74/1.81 % Refutation found
% 9.74/1.81 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.74/1.81 % SZS output start CNFRefutation for theBenchmark
% 9.74/1.81 fof(f68,axiom,(
% 9.74/1.81 (![X,Y]: (( subset(X,Y)| member(f17(X,Y),X) ) ))),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f69,axiom,(
% 9.74/1.81 (![X,Y]: (( subset(X,Y)| ~ member(f17(X,Y),Y) ) ))),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f145,axiom,(
% 9.74/1.81 (![X,Y]: (( ~ subset(X,Y)| ~ subset(Y,X)| X = Y ) ))),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f153,axiom,(
% 9.74/1.81 (![X,Y,Z]: (( ~ subset(X,Y)| ~ subset(Y,Z)| subset(X,Z) ) ))),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f165,axiom,(
% 9.74/1.81 (![Xf,X,Xg]: (( ~ function(Xf)| ~ member(X,domain_of(Xf))| subset(apply(Xg,apply(Xf,X)),apply(compose(Xg,Xf),X)) ) ))),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f166,axiom,(
% 9.74/1.81 (![Xf,Xg,X]: (( ~ function(Xf)| subset(apply(compose(Xg,Xf),X),apply(Xg,apply(Xf,X))) ) ))),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f167,hypothesis,(
% 9.74/1.81 function(a_function) ),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f168,hypothesis,(
% 9.74/1.81 member(a,domain_of(a_function)) ),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f169,negated_conjecture,(
% 9.74/1.81 apply(another_function,apply(a_function,a)) != apply(compose(another_function,a_function),a) ),
% 9.74/1.81 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.74/1.81 fof(f256,plain,(
% 9.74/1.81 ![X0,X1]: (subset(X0,X1)|member(f17(X0,X1),X0))),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f68])).
% 9.74/1.81 fof(f257,plain,(
% 9.74/1.81 ![X0,X1]: (subset(X0,X1)|~member(f17(X0,X1),X1))),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f69])).
% 9.74/1.81 fof(f353,plain,(
% 9.74/1.81 ![X0,X1]: (~subset(X0,X1)|~subset(X1,X0)|X0=X1)),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f145])).
% 9.74/1.81 fof(f361,plain,(
% 9.74/1.81 ![X,Z]: ((![Y]: (~subset(X,Y)|~subset(Y,Z)))|subset(X,Z))),
% 9.74/1.81 inference(miniscoping,[status(thm)],[f153])).
% 9.74/1.81 fof(f362,plain,(
% 9.74/1.81 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X1,X2)|subset(X0,X2))),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f361])).
% 9.74/1.81 fof(f377,plain,(
% 9.74/1.81 ![Xf,X]: ((~function(Xf)|~member(X,domain_of(Xf)))|(![Xg]: subset(apply(Xg,apply(Xf,X)),apply(compose(Xg,Xf),X))))),
% 9.74/1.81 inference(miniscoping,[status(thm)],[f165])).
% 9.74/1.81 fof(f378,plain,(
% 9.74/1.81 ![X0,X1,X2]: (~function(X0)|~member(X1,domain_of(X0))|subset(apply(X2,apply(X0,X1)),apply(compose(X2,X0),X1)))),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f377])).
% 9.74/1.81 fof(f379,plain,(
% 9.74/1.81 ![Xf]: (~function(Xf)|(![Xg,X]: subset(apply(compose(Xg,Xf),X),apply(Xg,apply(Xf,X)))))),
% 9.74/1.81 inference(miniscoping,[status(thm)],[f166])).
% 9.74/1.81 fof(f380,plain,(
% 9.74/1.81 ![X0,X1,X2]: (~function(X0)|subset(apply(compose(X1,X0),X2),apply(X1,apply(X0,X2))))),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f379])).
% 9.74/1.81 fof(f381,plain,(
% 9.74/1.81 function(a_function)),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f167])).
% 9.74/1.81 fof(f382,plain,(
% 9.74/1.81 member(a,domain_of(a_function))),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f168])).
% 9.74/1.81 fof(f383,plain,(
% 9.74/1.81 ~apply(another_function,apply(a_function,a))=apply(compose(another_function,a_function),a)),
% 9.74/1.81 inference(cnf_transformation,[status(thm)],[f169])).
% 9.74/1.81 fof(f2098,plain,(
% 9.74/1.81 ![X0,X1,X2,X3]: (~subset(X0,apply(compose(X1,X2),X3))|subset(X0,apply(X1,apply(X2,X3)))|~function(X2))),
% 9.74/1.81 inference(resolution,[status(thm)],[f362,f380])).
% 9.74/1.81 fof(f2156,plain,(
% 9.74/1.81 ![X0,X1,X2]: (~subset(X0,apply(compose(X1,a_function),X2))|subset(X0,apply(X1,apply(a_function,X2))))),
% 9.74/1.81 inference(resolution,[status(thm)],[f2098,f381])).
% 9.74/1.81 fof(f4580,plain,(
% 9.74/1.81 ![X0]: (subset(X0,X0)|subset(X0,X0))),
% 9.74/1.81 inference(resolution,[status(thm)],[f256,f257])).
% 9.74/1.81 fof(f4612,plain,(
% 9.74/1.81 ![X0]: (subset(X0,X0))),
% 9.74/1.81 inference(duplicate_literals_removal,[status(thm)],[f4580])).
% 9.74/1.81 fof(f4616,plain,(
% 9.74/1.81 ![X0,X1]: (subset(apply(compose(X0,a_function),X1),apply(X0,apply(a_function,X1))))),
% 9.74/1.81 inference(resolution,[status(thm)],[f4612,f2156])).
% 9.74/1.81 fof(f4821,plain,(
% 9.74/1.81 ![X0,X1]: (~member(X0,domain_of(a_function))|subset(apply(X1,apply(a_function,X0)),apply(compose(X1,a_function),X0)))),
% 9.74/1.81 inference(resolution,[status(thm)],[f378,f381])).
% 7.86/1.84 fof(f4833,plain,(
% 7.86/1.84 ![X0,X1]: (~member(X0,domain_of(a_function))|~subset(apply(compose(X1,a_function),X0),apply(X1,apply(a_function,X0)))|apply(compose(X1,a_function),X0)=apply(X1,apply(a_function,X0)))),
% 7.86/1.84 inference(resolution,[status(thm)],[f4821,f353])).
% 7.86/1.84 fof(f4846,plain,(
% 7.86/1.84 ![X0,X1]: (~member(X0,domain_of(a_function))|apply(compose(X1,a_function),X0)=apply(X1,apply(a_function,X0)))),
% 7.86/1.84 inference(forward_subsumption_resolution,[status(thm)],[f4833,f4616])).
% 7.86/1.84 fof(f5947,plain,(
% 7.86/1.84 ![X0]: (apply(compose(X0,a_function),a)=apply(X0,apply(a_function,a)))),
% 7.86/1.84 inference(resolution,[status(thm)],[f4846,f382])).
% 7.86/1.84 fof(f5961,plain,(
% 7.86/1.84 ~apply(another_function,apply(a_function,a))=apply(another_function,apply(a_function,a))),
% 7.86/1.84 inference(backward_demodulation,[status(thm)],[f5947,f383])).
% 7.86/1.84 fof(f5969,plain,(
% 7.86/1.84 $false),
% 7.86/1.84 inference(trivial_equality_resolution,[status(thm)],[f5961])).
% 7.86/1.84 % SZS output end CNFRefutation for theBenchmark.p
% 7.86/1.86 % Elapsed time: 1.406550 seconds
% 7.86/1.86 % CPU time: 10.692354 seconds
% 7.86/1.86 % Total memory used: 220.052 MB
% 7.86/1.86 % Net memory used: 212.504 MB
%------------------------------------------------------------------------------