%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG006-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 11:49:26 AM UTC 2026
% Result : Unsatisfiable 0.15s 0.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG006-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n010.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 21 12:52:42 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 0.15/0.71 % Refutation found
% 0.15/0.71 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/0.71 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.71 fof(f1,axiom,(
% 0.15/0.71 (![X,Y]: (difference(X,difference(Y,X)) = X ))),
% 0.15/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.71 fof(f2,axiom,(
% 0.15/0.71 (![X,Y]: (difference(X,difference(X,Y)) = difference(Y,difference(Y,X)) ))),
% 0.15/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.71 fof(f3,axiom,(
% 0.15/0.71 (![X,Y,Z]: (difference(difference(X,Y),Z) = difference(difference(X,Z),difference(Y,Z)) ))),
% 0.15/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.71 fof(f4,negated_conjecture,(
% 0.15/0.71 difference(difference(a,c),b) != difference(difference(a,b),c) ),
% 0.15/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/0.71 fof(f5,plain,(
% 0.15/0.71 ![X0,X1]: (difference(X0,difference(X1,X0))=X0)),
% 0.15/0.71 inference(cnf_transformation,[status(thm)],[f1])).
% 0.15/0.71 fof(f6,plain,(
% 0.15/0.71 ![X0,X1]: (difference(X0,difference(X0,X1))=difference(X1,difference(X1,X0)))),
% 0.15/0.71 inference(cnf_transformation,[status(thm)],[f2])).
% 0.15/0.71 fof(f7,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,X1),X2)=difference(difference(X0,X2),difference(X1,X2)))),
% 0.15/0.71 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/0.71 fof(f8,plain,(
% 0.15/0.71 ~difference(difference(a,c),b)=difference(difference(a,b),c)),
% 0.15/0.71 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/0.71 fof(f14,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(X0,X1),X1)=difference(X0,X1))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f5,f5])).
% 0.15/0.71 fof(f20,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(X0,X1),difference(X0,X1))=difference(X1,difference(X1,difference(X0,X1))))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f14,f6])).
% 0.15/0.71 fof(f25,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(X0,X1),difference(X1,difference(X1,X0)))=difference(X0,X1))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f6,f5])).
% 0.15/0.71 fof(f28,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(X0,X0),X1)=difference(X1,difference(X1,difference(X0,X1))))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f7,f20])).
% 0.15/0.71 fof(f29,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(X0,X0),X1)=difference(X1,X1))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f5,f28])).
% 0.15/0.71 fof(f34,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(difference(X0,X0),X1),X2)=difference(X2,X2))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f29,f29])).
% 0.15/0.71 fof(f62,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(X0,difference(X0,difference(difference(X1,X1),X2)))=difference(difference(difference(X1,X1),X2),difference(X0,X0)))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f34,f6])).
% 0.15/0.71 fof(f81,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(difference(X0,X1),X2),X1)=difference(difference(X0,X1),difference(X2,X1)))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f14,f7])).
% 0.15/0.71 fof(f89,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X1)),X2)=difference(difference(X0,X2),difference(X2,X2)))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f29,f7])).
% 0.15/0.71 fof(f115,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(difference(X0,X1),X2),X1)=difference(difference(X0,X2),X1))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f7,f81])).
% 0.15/0.71 fof(f121,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X1)),X2)=difference(difference(X0,X2),X2))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f7,f89])).
% 0.15/0.71 fof(f122,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,difference(X1,X1)),X2)=difference(X0,X2))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f14,f121])).
% 0.15/0.71 fof(f147,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X2,X2))=difference(X0,difference(X1,difference(X2,X2))))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f7,f122])).
% 0.15/0.71 fof(f152,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(X0,difference(X1,X1))=difference(X0,difference(X2,difference(X0,difference(X1,X1)))))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f5,f122])).
% 0.15/0.71 fof(f175,plain,(
% 0.15/0.71 ![X0,X1,X2,X3]: (difference(difference(X0,difference(X1,difference(X2,X2))),X3)=difference(difference(X0,X3),difference(X1,X3)))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f122,f7])).
% 0.15/0.71 fof(f185,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(X0,difference(X0,difference(difference(X1,X1),X2)))=difference(difference(X1,X1),difference(X2,difference(X0,X0))))),
% 0.15/0.71 inference(backward_demodulation,[status(thm)],[f147,f62])).
% 0.15/0.71 fof(f197,plain,(
% 0.15/0.71 ![X0,X1,X2,X3]: (difference(difference(X0,difference(X1,difference(X2,X2))),X3)=difference(difference(X0,X1),X3))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f7,f175])).
% 0.15/0.71 fof(f206,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,X0),difference(X0,difference(X0,difference(difference(X1,X1),X2))))=difference(difference(difference(X1,X1),X2),X0))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f34,f25])).
% 0.15/0.71 fof(f217,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,difference(X1,difference(X2,X2))),difference(X1,difference(difference(X1,difference(X2,X2)),X0)))=difference(X0,difference(X1,difference(X2,X2))))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f122,f25])).
% 0.15/0.71 fof(f256,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X1,difference(difference(X1,difference(X2,X2)),X0)))=difference(X0,difference(X1,difference(X2,X2))))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f197,f217])).
% 0.15/0.71 fof(f257,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,X1),difference(X1,difference(X1,X0)))=difference(X0,difference(X1,difference(X2,X2))))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f122,f256])).
% 0.15/0.71 fof(f259,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(X0,difference(X0,difference(difference(X1,X1),X2)))=difference(difference(X1,X1),X2))),
% 0.15/0.71 inference(backward_demodulation,[status(thm)],[f269,f185])).
% 0.15/0.71 fof(f266,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(X0,difference(X1,X1))=difference(X0,difference(X2,X0)))),
% 0.15/0.71 inference(backward_demodulation,[status(thm)],[f269,f152])).
% 0.15/0.71 fof(f269,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(X0,X1)=difference(X0,difference(X1,difference(X2,X2))))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f25,f257])).
% 0.15/0.71 fof(f291,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,X0),difference(difference(X1,X1),X2))=difference(difference(difference(X1,X1),X2),X0))),
% 0.15/0.71 inference(backward_demodulation,[status(thm)],[f259,f206])).
% 0.15/0.71 fof(f299,plain,(
% 0.15/0.71 ![X0,X1]: (difference(X0,difference(X1,X1))=X0)),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f5,f266])).
% 0.15/0.71 fof(f331,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(X0,X0),difference(difference(X0,X0),X1))=difference(X1,X1))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f299,f6])).
% 0.15/0.71 fof(f355,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(difference(X0,X0),X1),X0)=difference(X1,X1))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f291,f331])).
% 0.15/0.71 fof(f356,plain,(
% 0.15/0.71 ![X0,X1]: (difference(difference(X0,X1),X0)=difference(X1,X1))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f115,f355])).
% 0.15/0.71 fof(f464,plain,(
% 0.15/0.71 ![X0,X1]: (difference(X0,difference(X0,difference(X0,X1)))=difference(difference(X0,X1),difference(X1,X1)))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f356,f6])).
% 0.15/0.71 fof(f473,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(X0,difference(difference(X1,X2),X1))=X0)),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f356,f299])).
% 0.15/0.71 fof(f503,plain,(
% 0.15/0.71 ![X0,X1]: (difference(X0,difference(X0,difference(X0,X1)))=difference(difference(X0,X1),X1))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f7,f464])).
% 0.15/0.71 fof(f505,plain,(
% 0.15/0.71 ![X0,X1]: (difference(X0,difference(X0,difference(X0,X1)))=difference(X0,X1))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f14,f503])).
% 0.15/0.71 fof(f1878,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(difference(X0,X1),X2),difference(difference(difference(X0,X1),X2),difference(difference(X0,X2),X1)))=difference(difference(difference(X0,X1),X2),X1))),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f115,f505])).
% 0.15/0.71 fof(f1880,plain,(
% 0.15/0.71 ![X0,X1,X2,X3]: (difference(X0,difference(difference(difference(X1,X2),X3),difference(difference(X1,X3),X2)))=X0)),
% 0.15/0.71 inference(paramodulation,[status(thm)],[f115,f473])).
% 0.15/0.71 fof(f1928,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(difference(X0,X1),X2),difference(difference(difference(X0,X1),X2),difference(difference(X0,X2),X1)))=difference(difference(X0,X2),X1))),
% 0.15/0.71 inference(forward_demodulation,[status(thm)],[f115,f1878])).
% 0.15/0.71 fof(f1929,plain,(
% 0.15/0.71 ![X0,X1,X2]: (difference(difference(X0,X1),X2)=difference(difference(X0,X2),X1))),
% 0.15/0.71 inference(backward_demodulation,[status(thm)],[f1880,f1928])).
% 0.15/0.71 fof(f1940,plain,(
% 0.15/0.72 $false),
% 0.15/0.72 inference(backward_subsumption_resolution,[status(thm)],[f8,f1929])).
% 0.15/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 26.01/26.91 % Elapsed time: 26.521669 seconds
% 26.01/26.91 % CPU time: 208.147356 seconds
% 26.01/26.91 % Total memory used: 127.121 GB
% 26.01/26.91 % Net memory used: 127.120 GB
%------------------------------------------------------------------------------