%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV557-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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:52:47 PM UTC 2026
% Result : Unsatisfiable 0.16s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV557-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n001.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 09:13:43 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.49 % Refutation found
% 0.16/0.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.49 fof(f1,axiom,(
% 0.16/0.49 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f3,axiom,(
% 0.16/0.49 (![A,I]: (store(A,I,select(A,I)) = A ))),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f4,axiom,(
% 0.16/0.49 (![A,I,E,F]: (store(store(A,I,E),I,F) = store(A,I,F) ))),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f6,hypothesis,(
% 0.16/0.49 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)) = store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)) ),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f7,negated_conjecture,(
% 0.16/0.49 a1 != a2 ),
% 0.16/0.49 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.16/0.49 fof(f8,plain,(
% 0.16/0.49 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.49 fof(f11,plain,(
% 0.16/0.49 ![X0,X1]: (store(X0,X1,select(X0,X1))=X0)),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f3])).
% 0.16/0.49 fof(f12,plain,(
% 0.16/0.49 ![X0,X1,X2,X3]: (store(store(X0,X1,X2),X1,X3)=store(X0,X1,X3))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.49 fof(f15,plain,(
% 0.16/0.49 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4))=store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f6])).
% 0.16/0.49 fof(f16,plain,(
% 0.16/0.49 ~a1=a2),
% 0.16/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.16/0.49 fof(f25,plain,(
% 0.16/0.49 ![X0]: (store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i4,X0)=store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,X0))),
% 0.16/0.49 inference(paramodulation,[status(thm)],[f15,f12])).
% 0.16/0.49 fof(f26,plain,(
% 0.16/0.49 select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),
% 0.16/0.49 inference(paramodulation,[status(thm)],[f15,f8])).
% 0.16/0.49 fof(f28,plain,(
% 0.16/0.49 ![X0]: (store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,X0)=store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,X0))),
% 0.16/0.50 inference(forward_demodulation,[status(thm)],[f12,f25])).
% 0.16/0.50 fof(f29,plain,(
% 0.16/0.50 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),
% 0.16/0.50 inference(forward_demodulation,[status(thm)],[f8,f26])).
% 0.16/0.50 fof(f30,plain,(
% 0.16/0.50 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4))=store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))),
% 0.16/0.50 inference(paramodulation,[status(thm)],[f11,f28])).
% 0.16/0.50 fof(f34,plain,(
% 0.16/0.50 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))=store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))),
% 0.16/0.50 inference(forward_demodulation,[status(thm)],[f29,f30])).
% 0.16/0.50 fof(f37,plain,(
% 0.16/0.50 store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3))=store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))),
% 0.16/0.50 inference(forward_demodulation,[status(thm)],[f11,f34])).
% 0.16/0.50 fof(f41,plain,(
% 0.16/0.50 ![X0]: (store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i3,X0)=store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,X0))),
% 0.16/0.50 inference(paramodulation,[status(thm)],[f37,f12])).
% 0.16/0.50 fof(f42,plain,(
% 0.16/0.50 select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i3)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),
% 0.16/0.50 inference(paramodulation,[status(thm)],[f37,f8])).
% 0.16/0.50 fof(f44,plain,(
% 0.16/0.50 ![X0]: (store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,X0)=store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,X0))),
% 0.16/0.50 inference(forward_demodulation,[status(thm)],[f12,f41])).
% 0.16/0.50 fof(f45,plain,(
% 0.16/0.50 select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),
% 0.16/0.50 inference(forward_demodulation,[status(thm)],[f8,f42])).
% 0.16/0.50 fof(f46,plain,(
% 0.16/0.50 store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))=store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2))),
% 0.16/0.50 inference(paramodulation,[status(thm)],[f45,f11])).
% 0.16/0.50 fof(f47,plain,(
% 0.16/0.50 store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3))=store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2))),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f44,f46])).
% 0.16/0.51 fof(f50,plain,(
% 0.16/0.51 store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2))=store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2))),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f11,f47])).
% 0.16/0.51 fof(f51,plain,(
% 0.16/0.51 ![X0]: (store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2,X0)=store(store(a2,i1,select(a1,i1)),i2,X0))),
% 0.16/0.51 inference(paramodulation,[status(thm)],[f50,f12])).
% 0.16/0.51 fof(f52,plain,(
% 0.16/0.51 select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i2)=select(store(a1,i1,select(a2,i1)),i2)),
% 0.16/0.51 inference(paramodulation,[status(thm)],[f50,f8])).
% 0.16/0.51 fof(f54,plain,(
% 0.16/0.51 ![X0]: (store(store(a1,i1,select(a2,i1)),i2,X0)=store(store(a2,i1,select(a1,i1)),i2,X0))),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f12,f51])).
% 0.16/0.51 fof(f55,plain,(
% 0.16/0.51 select(store(a2,i1,select(a1,i1)),i2)=select(store(a1,i1,select(a2,i1)),i2)),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f8,f52])).
% 0.16/0.51 fof(f56,plain,(
% 0.16/0.51 store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2))=store(a2,i1,select(a1,i1))),
% 0.16/0.51 inference(paramodulation,[status(thm)],[f11,f54])).
% 0.16/0.51 fof(f60,plain,(
% 0.16/0.51 store(store(a1,i1,select(a2,i1)),i2,select(store(a1,i1,select(a2,i1)),i2))=store(a2,i1,select(a1,i1))),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f55,f56])).
% 0.16/0.51 fof(f63,plain,(
% 0.16/0.51 store(a1,i1,select(a2,i1))=store(a2,i1,select(a1,i1))),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f11,f60])).
% 0.16/0.51 fof(f67,plain,(
% 0.16/0.51 ![X0]: (store(store(a1,i1,select(a2,i1)),i1,X0)=store(a2,i1,X0))),
% 0.16/0.51 inference(paramodulation,[status(thm)],[f63,f12])).
% 0.16/0.51 fof(f68,plain,(
% 0.16/0.51 select(store(a1,i1,select(a2,i1)),i1)=select(a1,i1)),
% 0.16/0.51 inference(paramodulation,[status(thm)],[f63,f8])).
% 0.16/0.51 fof(f70,plain,(
% 0.16/0.51 ![X0]: (store(a1,i1,X0)=store(a2,i1,X0))),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f12,f67])).
% 0.16/0.51 fof(f71,plain,(
% 0.16/0.51 select(a2,i1)=select(a1,i1)),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f8,f68])).
% 0.16/0.51 fof(f72,plain,(
% 0.16/0.51 store(a1,i1,select(a2,i1))=a2),
% 0.16/0.51 inference(paramodulation,[status(thm)],[f11,f70])).
% 0.16/0.51 fof(f76,plain,(
% 0.16/0.51 store(a1,i1,select(a1,i1))=a2),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f71,f72])).
% 0.16/0.51 fof(f77,plain,(
% 0.16/0.51 a1=a2),
% 0.16/0.51 inference(forward_demodulation,[status(thm)],[f11,f76])).
% 0.16/0.51 fof(f78,plain,(
% 0.16/0.51 $false),
% 0.16/0.51 inference(forward_subsumption_resolution,[status(thm)],[f77,f16])).
% 0.16/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.53 % Elapsed time: 0.083291 seconds
% 0.16/0.53 % CPU time: 0.444945 seconds
% 0.16/0.53 % Total memory used: 108.832 MB
% 0.16/0.53 % Net memory used: 107.851 MB
%------------------------------------------------------------------------------