%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN015-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 03:18:44 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN015-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n016.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 10:44:22 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.44 % Refutation found
% 0.13/0.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.44 fof(f1,axiom,(
% 0.13/0.44 (![X]: (equalish(X,X) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f2,axiom,(
% 0.13/0.44 (![X,Y]: (( ~ equalish(X,Y)| equalish(Y,X) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f3,axiom,(
% 0.13/0.44 (![X,Y,Z]: (( ~ equalish(X,Y)| ~ equalish(Y,Z)| equalish(X,Z) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f4,axiom,(
% 0.13/0.44 (![A,B,C]: (( ~ equalish(A,B)| ~ element(C,A)| element(C,B) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f5,axiom,(
% 0.13/0.44 (![A,B,C]: (( ~ element(A,B)| ~ equalish(A,C)| element(C,B) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f8,negated_conjecture,(
% 0.13/0.44 (![A]: (( ~ equalish(f(A),m)| ~ element(A,m)| equalish(A,m) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f9,negated_conjecture,(
% 0.13/0.44 (![A]: (( ~ equalish(f(A),A)| ~ element(A,m)| equalish(A,m) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f10,negated_conjecture,(
% 0.13/0.44 (![A]: (( element(A,f(A))| ~ element(A,m)| equalish(A,m) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f12,negated_conjecture,(
% 0.13/0.44 (![A,B]: (( ~ element(A,B)| ~ element(B,A)| equalish(A,B)| equalish(A,m)| element(B,m)| equalish(B,m) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f13,negated_conjecture,(
% 0.13/0.44 (![A]: (( ~ equalish(g(A),n)| element(A,n)| equalish(A,n) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f14,negated_conjecture,(
% 0.13/0.44 (![A]: (( ~ equalish(g(A),A)| element(A,n)| equalish(A,n) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f15,negated_conjecture,(
% 0.13/0.44 (![A]: (( element(A,g(A))| element(A,n)| equalish(A,n) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f16,negated_conjecture,(
% 0.13/0.44 (![A]: (( element(g(A),A)| element(A,n)| equalish(A,n) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f19,negated_conjecture,(
% 0.13/0.44 (![A]: (( ~ equalish(A,n)| element(A,k)| equalish(A,k) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f20,negated_conjecture,(
% 0.13/0.44 (![A]: (( ~ element(A,k)| equalish(A,n)| equalish(A,m)| equalish(A,k) ) ))),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f22,negated_conjecture,(
% 0.13/0.44 ~ equalish(m,n) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f23,negated_conjecture,(
% 0.13/0.44 ~ equalish(n,k) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f26,negated_conjecture,(
% 0.13/0.44 equalish(m,k) ),
% 0.13/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.44 fof(f27,plain,(
% 0.13/0.44 ![X0]: (equalish(X0,X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.44 fof(f28,plain,(
% 0.13/0.44 ![X0,X1]: (~equalish(X0,X1)|equalish(X1,X0))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.44 fof(f29,plain,(
% 0.13/0.44 ![X,Z]: ((![Y]: (~equalish(X,Y)|~equalish(Y,Z)))|equalish(X,Z))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f3])).
% 0.13/0.44 fof(f30,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~equalish(X0,X1)|~equalish(X1,X2)|equalish(X0,X2))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.44 fof(f31,plain,(
% 0.13/0.44 ![B,C]: ((![A]: (~equalish(A,B)|~element(C,A)))|element(C,B))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f4])).
% 0.13/0.44 fof(f32,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~equalish(X0,X1)|~element(X2,X0)|element(X2,X1))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f31])).
% 0.13/0.44 fof(f33,plain,(
% 0.13/0.44 ![B,C]: ((![A]: (~element(A,B)|~equalish(A,C)))|element(C,B))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f5])).
% 0.13/0.44 fof(f34,plain,(
% 0.13/0.44 ![X0,X1,X2]: (~element(X0,X1)|~equalish(X0,X2)|element(X2,X1))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f33])).
% 0.13/0.44 fof(f37,plain,(
% 0.13/0.44 ![X0]: (~equalish(f(X0),m)|~element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.44 fof(f38,plain,(
% 0.13/0.44 ![X0]: (~equalish(f(X0),X0)|~element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.44 fof(f39,plain,(
% 0.13/0.44 ![X0]: (element(X0,f(X0))|~element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.44 fof(f41,plain,(
% 0.13/0.44 ![B]: (((![A]: (((~element(A,B)|~element(B,A))|equalish(A,B))|equalish(A,m)))|element(B,m))|equalish(B,m))),
% 0.13/0.44 inference(miniscoping,[status(thm)],[f12])).
% 0.13/0.44 fof(f42,plain,(
% 0.13/0.44 ![X0,X1]: (~element(X0,X1)|~element(X1,X0)|equalish(X0,X1)|equalish(X0,m)|element(X1,m)|equalish(X1,m))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f41])).
% 0.13/0.44 fof(f43,plain,(
% 0.13/0.44 ![X0]: (~equalish(g(X0),n)|element(X0,n)|equalish(X0,n))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.44 fof(f44,plain,(
% 0.13/0.44 ![X0]: (~equalish(g(X0),X0)|element(X0,n)|equalish(X0,n))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.44 fof(f45,plain,(
% 0.13/0.44 ![X0]: (element(X0,g(X0))|element(X0,n)|equalish(X0,n))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.44 fof(f46,plain,(
% 0.13/0.44 ![X0]: (element(g(X0),X0)|element(X0,n)|equalish(X0,n))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.44 fof(f50,plain,(
% 0.13/0.44 ![X0]: (~equalish(X0,n)|element(X0,k)|equalish(X0,k))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.44 fof(f51,plain,(
% 0.13/0.44 ![X0]: (~element(X0,k)|equalish(X0,n)|equalish(X0,m)|equalish(X0,k))),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/0.44 fof(f53,plain,(
% 0.13/0.44 ~equalish(m,n)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f22])).
% 0.13/0.44 fof(f54,plain,(
% 0.13/0.44 ~equalish(n,k)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f23])).
% 0.13/0.44 fof(f57,plain,(
% 0.13/0.44 equalish(m,k)),
% 0.13/0.44 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/0.44 fof(f64,plain,(
% 0.13/0.44 ![X0]: (~equalish(X0,m)|equalish(X0,k))),
% 0.13/0.44 inference(resolution,[status(thm)],[f57,f30])).
% 0.13/0.44 fof(f65,plain,(
% 0.13/0.44 equalish(k,m)),
% 0.13/0.44 inference(resolution,[status(thm)],[f57,f28])).
% 0.13/0.44 fof(f66,plain,(
% 0.13/0.44 ![X0]: (~equalish(X0,k)|equalish(X0,m))),
% 0.13/0.44 inference(resolution,[status(thm)],[f65,f30])).
% 0.13/0.44 fof(f104,plain,(
% 0.13/0.44 element(n,k)|equalish(n,k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f50,f27])).
% 0.13/0.44 fof(f105,plain,(
% 0.13/0.44 element(n,k)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f104,f54])).
% 0.13/0.44 fof(f107,plain,(
% 0.13/0.44 ![X0]: (~equalish(k,X0)|element(n,X0))),
% 0.13/0.44 inference(resolution,[status(thm)],[f105,f32])).
% 0.13/0.44 fof(f108,plain,(
% 0.13/0.44 ![X0,X1]: (~element(X0,X1)|~element(X1,X0)|equalish(X0,X1)|element(X1,m)|equalish(X1,m))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f42,f32])).
% 0.13/0.44 fof(f115,plain,(
% 0.13/0.44 element(n,m)),
% 0.13/0.44 inference(resolution,[status(thm)],[f107,f65])).
% 0.13/0.44 fof(f120,plain,(
% 0.13/0.44 element(m,n)|equalish(m,n)|~equalish(g(m),k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f44,f66])).
% 0.13/0.44 fof(f122,plain,(
% 0.13/0.44 element(m,n)|~equalish(g(m),k)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f120,f53])).
% 0.13/0.44 fof(f124,plain,(
% 0.13/0.44 element(n,f(n))|equalish(n,m)),
% 0.13/0.44 inference(resolution,[status(thm)],[f115,f39])).
% 0.13/0.44 fof(f125,plain,(
% 0.13/0.44 ~equalish(f(n),n)|equalish(n,m)),
% 0.13/0.44 inference(resolution,[status(thm)],[f115,f38])).
% 0.13/0.44 fof(f126,plain,(
% 0.13/0.44 ~equalish(f(n),m)|equalish(n,m)),
% 0.13/0.44 inference(resolution,[status(thm)],[f115,f37])).
% 0.13/0.44 fof(f128,plain,(
% 0.13/0.44 ![X0]: (~equalish(n,X0)|element(X0,m))),
% 0.13/0.44 inference(resolution,[status(thm)],[f115,f34])).
% 0.13/0.44 fof(f137,plain,(
% 0.13/0.44 ![X0]: (element(X0,n)|equalish(X0,n)|~element(g(X0),X0)|equalish(g(X0),X0)|element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(resolution,[status(thm)],[f45,f108])).
% 0.13/0.44 fof(f140,plain,(
% 0.13/0.44 ![X0]: (element(X0,n)|equalish(X0,n)|~element(g(X0),X0)|element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f137,f44])).
% 0.13/0.44 fof(f147,plain,(
% 0.13/0.44 ![X0,X1]: (element(X0,n)|equalish(X0,n)|~equalish(X0,X1)|element(g(X0),X1))),
% 0.13/0.44 inference(resolution,[status(thm)],[f46,f32])).
% 0.13/0.44 fof(f162,plain,(
% 0.13/0.44 equalish(n,m)|~equalish(f(n),k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f126,f66])).
% 0.13/0.44 fof(f167,plain,(
% 0.13/0.44 ![X0]: (~element(X0,k)|equalish(X0,n)|equalish(X0,k))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f51,f64])).
% 0.13/0.44 fof(f199,plain,(
% 0.13/0.44 ![X0]: (element(X0,n)|equalish(X0,n)|element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f140,f46])).
% 0.13/0.44 fof(f218,plain,(
% 0.13/0.44 ![X0]: (element(X0,n)|element(X0,m)|equalish(X0,m)|equalish(n,X0))),
% 0.13/0.44 inference(resolution,[status(thm)],[f199,f28])).
% 0.13/0.44 fof(f223,plain,(
% 0.13/0.44 ![X0]: (element(X0,n)|element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f218,f128])).
% 0.13/0.44 fof(f240,plain,(
% 0.13/0.44 ![X0]: (element(X0,n)|element(X0,m)|equalish(m,X0))),
% 0.13/0.44 inference(resolution,[status(thm)],[f223,f28])).
% 0.13/0.44 fof(f394,plain,(
% 0.13/0.44 element(m,n)|equalish(m,n)|element(g(m),k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f147,f57])).
% 0.13/0.44 fof(f403,plain,(
% 0.13/0.44 element(m,n)|element(g(m),k)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f394,f53])).
% 0.13/0.44 fof(f408,plain,(
% 0.13/0.44 element(m,n)|equalish(g(m),n)|equalish(g(m),k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f403,f167])).
% 0.13/0.44 fof(f412,plain,(
% 0.13/0.44 element(m,n)|equalish(g(m),n)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f408,f122])).
% 0.13/0.44 fof(f413,plain,(
% 0.13/0.44 element(m,n)|element(m,n)|equalish(m,n)),
% 0.13/0.44 inference(resolution,[status(thm)],[f412,f43])).
% 0.13/0.44 fof(f420,plain,(
% 0.13/0.44 element(m,n)|equalish(m,n)),
% 0.13/0.44 inference(duplicate_literals_removal,[status(thm)],[f413])).
% 0.13/0.44 fof(f421,plain,(
% 0.13/0.44 element(m,n)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f420,f53])).
% 0.13/0.44 fof(f437,plain,(
% 0.13/0.44 ![X0]: (~equalish(m,X0)|element(X0,n))),
% 0.13/0.44 inference(resolution,[status(thm)],[f421,f34])).
% 0.13/0.44 fof(f449,plain,(
% 0.13/0.44 ![X0]: (element(X0,n)|element(X0,m))),
% 0.13/0.44 inference(backward_subsumption_resolution,[status(thm)],[f240,f437])).
% 0.13/0.44 fof(f481,plain,(
% 0.13/0.44 ![X0]: (element(X0,m)|~element(n,X0)|equalish(n,X0)|element(X0,m)|equalish(X0,m))),
% 0.13/0.44 inference(resolution,[status(thm)],[f449,f108])).
% 0.13/0.44 fof(f484,plain,(
% 0.13/0.44 ![X0]: (element(X0,m)|~element(n,X0)|equalish(n,X0)|equalish(X0,m))),
% 0.13/0.44 inference(duplicate_literals_removal,[status(thm)],[f481])).
% 0.13/0.44 fof(f485,plain,(
% 0.13/0.44 ![X0]: (element(X0,m)|~element(n,X0)|equalish(X0,m))),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f484,f128])).
% 0.13/0.44 fof(f505,plain,(
% 0.13/0.44 element(f(n),m)|equalish(f(n),m)|equalish(n,m)),
% 0.13/0.44 inference(resolution,[status(thm)],[f485,f124])).
% 0.13/0.44 fof(f511,plain,(
% 0.13/0.44 element(f(n),m)|equalish(n,m)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f505,f126])).
% 0.13/0.44 fof(f519,plain,(
% 0.13/0.44 ![X0]: (equalish(n,m)|~equalish(m,X0)|element(f(n),X0))),
% 0.13/0.44 inference(resolution,[status(thm)],[f511,f32])).
% 0.13/0.44 fof(f563,plain,(
% 0.13/0.44 equalish(n,m)|element(f(n),k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f519,f57])).
% 0.13/0.44 fof(f569,plain,(
% 0.13/0.44 equalish(n,m)|equalish(f(n),n)|equalish(f(n),k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f563,f167])).
% 0.13/0.44 fof(f573,plain,(
% 0.13/0.44 equalish(n,m)|equalish(f(n),k)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f569,f125])).
% 0.13/0.44 fof(f574,plain,(
% 0.13/0.44 equalish(n,m)),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f573,f162])).
% 0.13/0.44 fof(f580,plain,(
% 0.13/0.44 equalish(n,k)),
% 0.13/0.44 inference(resolution,[status(thm)],[f574,f64])).
% 0.13/0.44 fof(f587,plain,(
% 0.13/0.44 $false),
% 0.13/0.44 inference(forward_subsumption_resolution,[status(thm)],[f580,f54])).
% 0.13/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.46 % Elapsed time: 0.091938 seconds
% 0.13/0.46 % CPU time: 0.501126 seconds
% 0.13/0.46 % Total memory used: 23.077 MB
% 0.13/0.46 % Net memory used: 22.145 MB
%------------------------------------------------------------------------------