%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV547-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 : n015.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:51:39 PM UTC 2026
% Result : Unsatisfiable 1.36s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV547-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:08:51 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 1.36/0.65 % Refutation found
% 1.36/0.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.36/0.65 % SZS output start CNFRefutation for theBenchmark
% 1.36/0.65 fof(f1,axiom,(
% 1.36/0.65 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f3,axiom,(
% 1.36/0.65 (![A,I,J]: (store(store(A,I,select(A,J)),J,select(A,I)) = store(store(A,J,select(A,I)),I,select(A,J)) ))),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f6,hypothesis,(
% 1.36/0.65 a_469 = store(a_467,i0,e_468) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f7,hypothesis,(
% 1.36/0.65 a_471 = store(a_469,i3,e_470) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f8,hypothesis,(
% 1.36/0.65 a_473 = store(a_471,i3,e_472) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f9,hypothesis,(
% 1.36/0.65 a_475 = store(a_473,i2,e_474) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f10,hypothesis,(
% 1.36/0.65 a_477 = store(a_475,i2,e_476) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f11,hypothesis,(
% 1.36/0.65 a_479 = store(a_477,i0,e_478) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f12,hypothesis,(
% 1.36/0.65 a_480 = store(a_467,i3,e_470) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f13,hypothesis,(
% 1.36/0.65 a_481 = store(a_480,i0,e_468) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f14,hypothesis,(
% 1.36/0.65 a_483 = store(a_481,i3,e_482) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f15,hypothesis,(
% 1.36/0.65 a_485 = store(a_483,i2,e_484) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f16,hypothesis,(
% 1.36/0.65 a_487 = store(a_485,i0,e_486) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f17,hypothesis,(
% 1.36/0.65 a_489 = store(a_487,i2,e_488) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f19,hypothesis,(
% 1.36/0.65 e_468 = select(a_467,i3) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f20,hypothesis,(
% 1.36/0.65 e_470 = select(a_467,i0) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f21,hypothesis,(
% 1.36/0.65 e_472 = select(a_471,i2) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f22,hypothesis,(
% 1.36/0.65 e_474 = select(a_471,i3) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f23,hypothesis,(
% 1.36/0.65 e_476 = select(a_475,i0) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f24,hypothesis,(
% 1.36/0.65 e_478 = select(a_475,i2) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f25,hypothesis,(
% 1.36/0.65 e_482 = select(a_481,i2) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f26,hypothesis,(
% 1.36/0.65 e_484 = select(a_481,i3) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f27,hypothesis,(
% 1.36/0.65 e_486 = select(a_485,i2) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f28,hypothesis,(
% 1.36/0.65 e_488 = select(a_485,i0) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f29,hypothesis,(
% 1.36/0.65 e_491 = select(a_479,i_490) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f30,hypothesis,(
% 1.36/0.65 e_492 = select(a_489,i_490) ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f32,negated_conjecture,(
% 1.36/0.65 e_491 != e_492 ),
% 1.36/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.36/0.65 fof(f33,plain,(
% 1.36/0.65 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f1])).
% 1.36/0.65 fof(f36,plain,(
% 1.36/0.65 ![X0,X1,X2]: (store(store(X0,X1,select(X0,X2)),X2,select(X0,X1))=store(store(X0,X2,select(X0,X1)),X1,select(X0,X2)))),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f3])).
% 1.36/0.65 fof(f39,plain,(
% 1.36/0.65 a_469=store(a_467,i0,e_468)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f6])).
% 1.36/0.65 fof(f40,plain,(
% 1.36/0.65 a_471=store(a_469,i3,e_470)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f7])).
% 1.36/0.65 fof(f41,plain,(
% 1.36/0.65 a_473=store(a_471,i3,e_472)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f8])).
% 1.36/0.65 fof(f42,plain,(
% 1.36/0.65 a_475=store(a_473,i2,e_474)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f9])).
% 1.36/0.65 fof(f43,plain,(
% 1.36/0.65 a_477=store(a_475,i2,e_476)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f10])).
% 1.36/0.65 fof(f44,plain,(
% 1.36/0.65 a_479=store(a_477,i0,e_478)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f11])).
% 1.36/0.65 fof(f45,plain,(
% 1.36/0.65 a_480=store(a_467,i3,e_470)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f12])).
% 1.36/0.65 fof(f46,plain,(
% 1.36/0.65 a_481=store(a_480,i0,e_468)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f13])).
% 1.36/0.65 fof(f47,plain,(
% 1.36/0.65 a_483=store(a_481,i3,e_482)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f14])).
% 1.36/0.65 fof(f48,plain,(
% 1.36/0.65 a_485=store(a_483,i2,e_484)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f15])).
% 1.36/0.65 fof(f49,plain,(
% 1.36/0.65 a_487=store(a_485,i0,e_486)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f16])).
% 1.36/0.65 fof(f50,plain,(
% 1.36/0.65 a_489=store(a_487,i2,e_488)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f17])).
% 1.36/0.65 fof(f52,plain,(
% 1.36/0.65 e_468=select(a_467,i3)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f19])).
% 1.36/0.65 fof(f53,plain,(
% 1.36/0.65 e_470=select(a_467,i0)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f20])).
% 1.36/0.65 fof(f54,plain,(
% 1.36/0.65 e_472=select(a_471,i2)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f21])).
% 1.36/0.65 fof(f55,plain,(
% 1.36/0.65 e_474=select(a_471,i3)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f22])).
% 1.36/0.65 fof(f56,plain,(
% 1.36/0.65 e_476=select(a_475,i0)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f23])).
% 1.36/0.65 fof(f57,plain,(
% 1.36/0.65 e_478=select(a_475,i2)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f24])).
% 1.36/0.65 fof(f58,plain,(
% 1.36/0.65 e_482=select(a_481,i2)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f25])).
% 1.36/0.65 fof(f59,plain,(
% 1.36/0.65 e_484=select(a_481,i3)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f26])).
% 1.36/0.65 fof(f60,plain,(
% 1.36/0.65 e_486=select(a_485,i2)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f27])).
% 1.36/0.65 fof(f61,plain,(
% 1.36/0.65 e_488=select(a_485,i0)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f28])).
% 1.36/0.65 fof(f62,plain,(
% 1.36/0.65 e_491=select(a_479,i_490)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f29])).
% 1.36/0.65 fof(f63,plain,(
% 1.36/0.65 e_492=select(a_489,i_490)),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f30])).
% 1.36/0.65 fof(f65,plain,(
% 1.36/0.65 ~e_491=e_492),
% 1.36/0.65 inference(cnf_transformation,[status(thm)],[f32])).
% 1.36/0.65 fof(f71,plain,(
% 1.36/0.65 ![X0]: (store(store(a_481,X0,e_482),i2,select(a_481,X0))=store(store(a_481,i2,select(a_481,X0)),X0,select(a_481,i2)))),
% 1.36/0.65 inference(paramodulation,[status(thm)],[f58,f36])).
% 1.36/0.65 fof(f72,plain,(
% 1.36/0.65 ![X0]: (store(store(a_475,X0,e_478),i2,select(a_475,X0))=store(store(a_475,i2,select(a_475,X0)),X0,select(a_475,i2)))),
% 1.36/0.65 inference(paramodulation,[status(thm)],[f57,f36])).
% 1.36/0.65 fof(f75,plain,(
% 1.36/0.65 ![X0]: (store(store(a_471,X0,e_472),i2,select(a_471,X0))=store(store(a_471,i2,select(a_471,X0)),X0,select(a_471,i2)))),
% 1.36/0.65 inference(paramodulation,[status(thm)],[f54,f36])).
% 1.36/0.65 fof(f77,plain,(
% 1.36/0.65 ![X0]: (store(store(a_467,X0,e_468),i3,select(a_467,X0))=store(store(a_467,i3,select(a_467,X0)),X0,select(a_467,i3)))),
% 1.36/0.65 inference(paramodulation,[status(thm)],[f52,f36])).
% 1.36/0.65 fof(f129,plain,(
% 1.36/0.65 ![X0]: (store(store(a_481,X0,e_482),i2,select(a_481,X0))=store(store(a_481,i2,select(a_481,X0)),X0,e_482))),
% 1.36/0.65 inference(forward_demodulation,[status(thm)],[f58,f71])).
% 1.36/0.65 fof(f130,plain,(
% 1.36/0.65 ![X0]: (store(store(a_475,X0,e_478),i2,select(a_475,X0))=store(store(a_475,i2,select(a_475,X0)),X0,e_478))),
% 1.36/0.65 inference(forward_demodulation,[status(thm)],[f57,f72])).
% 1.36/0.65 fof(f133,plain,(
% 1.36/0.65 ![X0]: (store(store(a_471,X0,e_472),i2,select(a_471,X0))=store(store(a_471,i2,select(a_471,X0)),X0,e_472))),
% 1.36/0.65 inference(forward_demodulation,[status(thm)],[f54,f75])).
% 1.36/0.65 fof(f135,plain,(
% 1.36/0.65 ![X0]: (store(store(a_467,X0,e_468),i3,select(a_467,X0))=store(store(a_467,i3,select(a_467,X0)),X0,e_468))),
% 1.36/0.65 inference(forward_demodulation,[status(thm)],[f52,f77])).
% 1.36/0.65 fof(f223,plain,(
% 1.36/0.65 select(a_471,i3)=e_470),
% 1.36/0.65 inference(paramodulation,[status(thm)],[f40,f33])).
% 1.36/0.65 fof(f224,plain,(
% 1.36/0.65 a_471=store(a_469,i3,e_474)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f228,f40])).
% 1.36/0.65 fof(f225,plain,(
% 1.36/0.65 e_474=select(a_467,i0)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f228,f53])).
% 1.36/0.65 fof(f227,plain,(
% 1.36/0.65 a_480=store(a_467,i3,e_474)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f228,f45])).
% 1.36/0.65 fof(f228,plain,(
% 1.36/0.65 e_474=e_470),
% 1.36/0.65 inference(forward_demodulation,[status(thm)],[f55,f223])).
% 1.36/0.65 fof(f241,plain,(
% 1.36/0.65 select(a_475,i2)=e_474),
% 1.36/0.65 inference(paramodulation,[status(thm)],[f42,f33])).
% 1.36/0.65 fof(f242,plain,(
% 1.36/0.65 a_475=store(a_473,i2,e_478)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f250,f42])).
% 1.36/0.65 fof(f243,plain,(
% 1.36/0.65 e_478=select(a_467,i0)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f250,f225])).
% 1.36/0.65 fof(f245,plain,(
% 1.36/0.65 e_478=select(a_471,i3)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f250,f55])).
% 1.36/0.65 fof(f246,plain,(
% 1.36/0.65 a_480=store(a_467,i3,e_478)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f250,f227])).
% 1.36/0.65 fof(f248,plain,(
% 1.36/0.65 a_471=store(a_469,i3,e_478)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f250,f224])).
% 1.36/0.65 fof(f250,plain,(
% 1.36/0.65 e_478=e_474),
% 1.36/0.65 inference(forward_demodulation,[status(thm)],[f57,f241])).
% 1.36/0.65 fof(f543,plain,(
% 1.36/0.65 select(a_485,i2)=e_484),
% 1.36/0.65 inference(paramodulation,[status(thm)],[f48,f33])).
% 1.36/0.65 fof(f544,plain,(
% 1.36/0.65 a_485=store(a_483,i2,e_486)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f547,f48])).
% 1.36/0.65 fof(f545,plain,(
% 1.36/0.65 e_486=select(a_481,i3)),
% 1.36/0.65 inference(backward_demodulation,[status(thm)],[f547,f59])).
% 1.36/0.66 fof(f547,plain,(
% 1.36/0.66 e_486=e_484),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f60,f543])).
% 1.36/0.66 fof(f1045,plain,(
% 1.36/0.66 store(store(a_481,i3,e_482),i2,select(a_481,i3))=store(store(a_481,i2,e_486),i3,e_482)),
% 1.36/0.66 inference(paramodulation,[status(thm)],[f545,f129])).
% 1.36/0.66 fof(f1050,plain,(
% 1.36/0.66 store(a_483,i2,select(a_481,i3))=store(store(a_481,i2,e_486),i3,e_482)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f47,f1045])).
% 1.36/0.66 fof(f1051,plain,(
% 1.36/0.66 store(a_483,i2,e_486)=store(store(a_481,i2,e_486),i3,e_482)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f545,f1050])).
% 1.36/0.66 fof(f1052,plain,(
% 1.36/0.66 a_485=store(store(a_481,i2,e_486),i3,e_482)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f544,f1051])).
% 1.36/0.66 fof(f1055,plain,(
% 1.36/0.66 store(store(a_475,i0,e_478),i2,select(a_475,i0))=store(store(a_475,i2,e_476),i0,e_478)),
% 1.36/0.66 inference(paramodulation,[status(thm)],[f56,f130])).
% 1.36/0.66 fof(f1058,plain,(
% 1.36/0.66 store(store(a_475,i0,e_478),i2,e_476)=store(store(a_475,i2,e_476),i0,e_478)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f56,f1055])).
% 1.36/0.66 fof(f1059,plain,(
% 1.36/0.66 store(store(a_475,i0,e_478),i2,e_476)=store(a_477,i0,e_478)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f43,f1058])).
% 1.36/0.66 fof(f1060,plain,(
% 1.36/0.66 store(store(a_475,i0,e_478),i2,e_476)=a_479),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f44,f1059])).
% 1.36/0.66 fof(f1487,plain,(
% 1.36/0.66 store(store(a_471,i3,e_472),i2,select(a_471,i3))=store(store(a_471,i2,e_478),i3,e_472)),
% 1.36/0.66 inference(paramodulation,[status(thm)],[f245,f133])).
% 1.36/0.66 fof(f1492,plain,(
% 1.36/0.66 store(a_473,i2,select(a_471,i3))=store(store(a_471,i2,e_478),i3,e_472)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f41,f1487])).
% 1.36/0.66 fof(f1493,plain,(
% 1.36/0.66 store(a_473,i2,e_478)=store(store(a_471,i2,e_478),i3,e_472)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f245,f1492])).
% 1.36/0.66 fof(f1494,plain,(
% 1.36/0.66 a_475=store(store(a_471,i2,e_478),i3,e_472)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f242,f1493])).
% 1.36/0.66 fof(f1495,plain,(
% 1.36/0.66 store(store(a_467,i0,e_468),i3,select(a_467,i0))=store(store(a_467,i3,e_478),i0,e_468)),
% 1.36/0.66 inference(paramodulation,[status(thm)],[f243,f135])).
% 1.36/0.66 fof(f1501,plain,(
% 1.36/0.66 store(a_469,i3,select(a_467,i0))=store(store(a_467,i3,e_478),i0,e_468)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f39,f1495])).
% 1.36/0.66 fof(f1502,plain,(
% 1.36/0.66 store(a_469,i3,e_478)=store(store(a_467,i3,e_478),i0,e_468)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f243,f1501])).
% 1.36/0.66 fof(f1503,plain,(
% 1.36/0.66 a_471=store(store(a_467,i3,e_478),i0,e_468)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f248,f1502])).
% 1.36/0.66 fof(f1504,plain,(
% 1.36/0.66 a_471=store(a_480,i0,e_468)),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f246,f1503])).
% 1.36/0.66 fof(f1510,plain,(
% 1.36/0.66 e_478=select(a_481,i3)),
% 1.36/0.66 inference(backward_demodulation,[status(thm)],[f1526,f245])).
% 1.36/0.66 fof(f1512,plain,(
% 1.36/0.66 e_472=select(a_481,i2)),
% 1.36/0.66 inference(backward_demodulation,[status(thm)],[f1526,f54])).
% 1.36/0.66 fof(f1516,plain,(
% 1.36/0.66 a_475=store(store(a_481,i2,e_478),i3,e_472)),
% 1.36/0.66 inference(backward_demodulation,[status(thm)],[f1526,f1494])).
% 1.36/0.66 fof(f1526,plain,(
% 1.36/0.66 a_471=a_481),
% 1.36/0.66 inference(forward_demodulation,[status(thm)],[f46,f1504])).
% 1.36/0.66 fof(f1609,plain,(
% 1.36/0.66 store(store(a_475,i0,e_486),i2,e_476)=a_479),
% 1.36/0.67 inference(backward_demodulation,[status(thm)],[f1622,f1060])).
% 1.36/0.67 fof(f1622,plain,(
% 1.36/0.67 e_478=e_486),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f545,f1510])).
% 1.36/0.67 fof(f1635,plain,(
% 1.36/0.67 e_472=e_482),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f58,f1512])).
% 1.36/0.67 fof(f1647,plain,(
% 1.36/0.67 a_475=store(store(a_481,i2,e_486),i3,e_472)),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f1622,f1516])).
% 1.36/0.67 fof(f1648,plain,(
% 1.36/0.67 a_475=store(store(a_481,i2,e_486),i3,e_482)),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f1635,f1647])).
% 1.36/0.67 fof(f1652,plain,(
% 1.36/0.67 e_476=select(a_485,i0)),
% 1.36/0.67 inference(backward_demodulation,[status(thm)],[f1661,f56])).
% 1.36/0.67 fof(f1661,plain,(
% 1.36/0.67 a_475=a_485),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f1052,f1648])).
% 1.36/0.67 fof(f1763,plain,(
% 1.36/0.67 store(store(a_485,i0,e_486),i2,e_476)=a_479),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f1661,f1609])).
% 1.36/0.67 fof(f1764,plain,(
% 1.36/0.67 store(a_487,i2,e_476)=a_479),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f49,f1763])).
% 1.36/0.67 fof(f1842,plain,(
% 1.36/0.67 store(a_487,i2,e_488)=a_479),
% 1.36/0.67 inference(backward_demodulation,[status(thm)],[f1885,f1764])).
% 1.36/0.67 fof(f1885,plain,(
% 1.36/0.67 e_476=e_488),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f61,f1652])).
% 1.36/0.67 fof(f1942,plain,(
% 1.36/0.67 e_491=select(a_489,i_490)),
% 1.36/0.67 inference(backward_demodulation,[status(thm)],[f2010,f62])).
% 1.36/0.67 fof(f2010,plain,(
% 1.36/0.67 a_489=a_479),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f50,f1842])).
% 1.36/0.67 fof(f2108,plain,(
% 1.36/0.67 e_491=e_492),
% 1.36/0.67 inference(forward_demodulation,[status(thm)],[f63,f1942])).
% 1.36/0.67 fof(f2109,plain,(
% 1.36/0.67 $false),
% 1.36/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2108,f65])).
% 1.36/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 1.36/0.69 % Elapsed time: 0.311120 seconds
% 1.36/0.69 % CPU time: 2.209054 seconds
% 1.36/0.69 % Total memory used: 156.074 MB
% 1.36/0.69 % Net memory used: 154.482 MB
%------------------------------------------------------------------------------