%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV547-1.007 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 5.67s 1.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV547-1.007 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.54 % Computer : n017.cluster.edu
% 0.10/0.54 % Model : x86_64 x86_64
% 0.10/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.54 % Memory : 8046.5625MB
% 0.10/0.54 % OS : Linux 6.8.0-71-generic
% 0.10/0.54 % CPULimit : 300
% 0.10/0.54 % WCLimit : 300
% 0.10/0.54 % DateTime : Mon Sep 21 09:00:59 UTC 2026
% 0.10/0.54 % CPUTime :
% 0.10/0.55 % Drodi V4.1.1
% 5.67/1.39 % Refutation found
% 5.67/1.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 5.67/1.39 % SZS output start CNFRefutation for theBenchmark
% 5.67/1.39 fof(f1,axiom,(
% 5.67/1.39 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f3,axiom,(
% 5.67/1.39 (![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)) ))),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f6,hypothesis,(
% 5.67/1.39 a_838 = store(a_836,i2,e_837) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f7,hypothesis,(
% 5.67/1.39 a_840 = store(a_838,i1,e_839) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f8,hypothesis,(
% 5.67/1.39 a_842 = store(a_840,i0,e_841) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f9,hypothesis,(
% 5.67/1.39 a_844 = store(a_842,i5,e_843) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f10,hypothesis,(
% 5.67/1.39 a_846 = store(a_844,i2,e_845) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f11,hypothesis,(
% 5.67/1.39 a_848 = store(a_846,i5,e_847) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f12,hypothesis,(
% 5.67/1.39 a_850 = store(a_848,i1,e_849) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f13,hypothesis,(
% 5.67/1.39 a_851 = store(a_850,i1,e_849) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f14,hypothesis,(
% 5.67/1.39 a_853 = store(a_851,i5,e_852) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f15,hypothesis,(
% 5.67/1.39 a_855 = store(a_853,i2,e_854) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f16,hypothesis,(
% 5.67/1.39 a_857 = store(a_855,i5,e_856) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f17,hypothesis,(
% 5.67/1.39 a_859 = store(a_857,i2,e_858) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f18,hypothesis,(
% 5.67/1.39 a_860 = store(a_836,i1,e_839) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f19,hypothesis,(
% 5.67/1.39 a_861 = store(a_860,i2,e_837) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f20,hypothesis,(
% 5.67/1.39 a_863 = store(a_861,i5,e_862) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f21,hypothesis,(
% 5.67/1.39 a_865 = store(a_863,i0,e_864) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f22,hypothesis,(
% 5.67/1.39 a_867 = store(a_865,i5,e_866) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f23,hypothesis,(
% 5.67/1.39 a_869 = store(a_867,i2,e_868) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f24,hypothesis,(
% 5.67/1.39 a_871 = store(a_869,i1,e_870) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f25,hypothesis,(
% 5.67/1.39 a_872 = store(a_871,i1,e_870) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f26,hypothesis,(
% 5.67/1.39 a_874 = store(a_872,i5,e_873) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f27,hypothesis,(
% 5.67/1.39 a_876 = store(a_874,i2,e_875) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f28,hypothesis,(
% 5.67/1.39 a_878 = store(a_876,i5,e_877) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f29,hypothesis,(
% 5.67/1.39 a_880 = store(a_878,i2,e_879) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f32,hypothesis,(
% 5.67/1.39 e_837 = select(a_836,i1) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f33,hypothesis,(
% 5.67/1.39 e_839 = select(a_836,i2) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f34,hypothesis,(
% 5.67/1.39 e_841 = select(a_840,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f35,hypothesis,(
% 5.67/1.39 e_843 = select(a_840,i0) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f36,hypothesis,(
% 5.67/1.39 e_845 = select(a_844,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f37,hypothesis,(
% 5.67/1.39 e_847 = select(a_844,i2) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f38,hypothesis,(
% 5.67/1.39 e_849 = select(a_848,i1) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f39,hypothesis,(
% 5.67/1.39 e_852 = select(a_851,i2) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f40,hypothesis,(
% 5.67/1.39 e_854 = select(a_851,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f41,hypothesis,(
% 5.67/1.39 e_856 = select(a_855,i2) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f42,hypothesis,(
% 5.67/1.39 e_858 = select(a_855,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f43,hypothesis,(
% 5.67/1.39 e_862 = select(a_861,i0) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f44,hypothesis,(
% 5.67/1.39 e_864 = select(a_861,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f45,hypothesis,(
% 5.67/1.39 e_866 = select(a_865,i2) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f46,hypothesis,(
% 5.67/1.39 e_868 = select(a_865,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f47,hypothesis,(
% 5.67/1.39 e_870 = select(a_869,i1) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f48,hypothesis,(
% 5.67/1.39 e_873 = select(a_872,i2) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f49,hypothesis,(
% 5.67/1.39 e_875 = select(a_872,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f50,hypothesis,(
% 5.67/1.39 e_877 = select(a_876,i2) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f51,hypothesis,(
% 5.67/1.39 e_879 = select(a_876,i5) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f52,hypothesis,(
% 5.67/1.39 e_882 = select(a_859,i_881) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f53,hypothesis,(
% 5.67/1.39 e_883 = select(a_880,i_881) ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f55,negated_conjecture,(
% 5.67/1.39 e_882 != e_883 ),
% 5.67/1.39 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 5.67/1.39 fof(f56,plain,(
% 5.67/1.39 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f1])).
% 5.67/1.39 fof(f59,plain,(
% 5.67/1.39 ![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)))),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f3])).
% 5.67/1.39 fof(f62,plain,(
% 5.67/1.39 a_838=store(a_836,i2,e_837)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f6])).
% 5.67/1.39 fof(f63,plain,(
% 5.67/1.39 a_840=store(a_838,i1,e_839)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f7])).
% 5.67/1.39 fof(f64,plain,(
% 5.67/1.39 a_842=store(a_840,i0,e_841)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f8])).
% 5.67/1.39 fof(f65,plain,(
% 5.67/1.39 a_844=store(a_842,i5,e_843)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f9])).
% 5.67/1.39 fof(f66,plain,(
% 5.67/1.39 a_846=store(a_844,i2,e_845)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f10])).
% 5.67/1.39 fof(f67,plain,(
% 5.67/1.39 a_848=store(a_846,i5,e_847)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f11])).
% 5.67/1.39 fof(f68,plain,(
% 5.67/1.39 a_850=store(a_848,i1,e_849)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f12])).
% 5.67/1.39 fof(f69,plain,(
% 5.67/1.39 a_851=store(a_850,i1,e_849)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f13])).
% 5.67/1.39 fof(f70,plain,(
% 5.67/1.39 a_853=store(a_851,i5,e_852)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f14])).
% 5.67/1.39 fof(f71,plain,(
% 5.67/1.39 a_855=store(a_853,i2,e_854)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f15])).
% 5.67/1.39 fof(f72,plain,(
% 5.67/1.39 a_857=store(a_855,i5,e_856)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f16])).
% 5.67/1.39 fof(f73,plain,(
% 5.67/1.39 a_859=store(a_857,i2,e_858)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f17])).
% 5.67/1.39 fof(f74,plain,(
% 5.67/1.39 a_860=store(a_836,i1,e_839)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f18])).
% 5.67/1.39 fof(f75,plain,(
% 5.67/1.39 a_861=store(a_860,i2,e_837)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f19])).
% 5.67/1.39 fof(f76,plain,(
% 5.67/1.39 a_863=store(a_861,i5,e_862)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f20])).
% 5.67/1.39 fof(f77,plain,(
% 5.67/1.39 a_865=store(a_863,i0,e_864)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f21])).
% 5.67/1.39 fof(f78,plain,(
% 5.67/1.39 a_867=store(a_865,i5,e_866)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f22])).
% 5.67/1.39 fof(f79,plain,(
% 5.67/1.39 a_869=store(a_867,i2,e_868)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f23])).
% 5.67/1.39 fof(f80,plain,(
% 5.67/1.39 a_871=store(a_869,i1,e_870)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f24])).
% 5.67/1.39 fof(f81,plain,(
% 5.67/1.39 a_872=store(a_871,i1,e_870)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f25])).
% 5.67/1.39 fof(f82,plain,(
% 5.67/1.39 a_874=store(a_872,i5,e_873)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f26])).
% 5.67/1.39 fof(f83,plain,(
% 5.67/1.39 a_876=store(a_874,i2,e_875)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f27])).
% 5.67/1.39 fof(f84,plain,(
% 5.67/1.39 a_878=store(a_876,i5,e_877)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f28])).
% 5.67/1.39 fof(f85,plain,(
% 5.67/1.39 a_880=store(a_878,i2,e_879)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f29])).
% 5.67/1.39 fof(f88,plain,(
% 5.67/1.39 e_837=select(a_836,i1)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f32])).
% 5.67/1.39 fof(f89,plain,(
% 5.67/1.39 e_839=select(a_836,i2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f33])).
% 5.67/1.39 fof(f90,plain,(
% 5.67/1.39 e_841=select(a_840,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f34])).
% 5.67/1.39 fof(f91,plain,(
% 5.67/1.39 e_843=select(a_840,i0)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f35])).
% 5.67/1.39 fof(f92,plain,(
% 5.67/1.39 e_845=select(a_844,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f36])).
% 5.67/1.39 fof(f93,plain,(
% 5.67/1.39 e_847=select(a_844,i2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f37])).
% 5.67/1.39 fof(f94,plain,(
% 5.67/1.39 e_849=select(a_848,i1)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f38])).
% 5.67/1.39 fof(f95,plain,(
% 5.67/1.39 e_852=select(a_851,i2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f39])).
% 5.67/1.39 fof(f96,plain,(
% 5.67/1.39 e_854=select(a_851,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f40])).
% 5.67/1.39 fof(f97,plain,(
% 5.67/1.39 e_856=select(a_855,i2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f41])).
% 5.67/1.39 fof(f98,plain,(
% 5.67/1.39 e_858=select(a_855,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f42])).
% 5.67/1.39 fof(f99,plain,(
% 5.67/1.39 e_862=select(a_861,i0)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f43])).
% 5.67/1.39 fof(f100,plain,(
% 5.67/1.39 e_864=select(a_861,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f44])).
% 5.67/1.39 fof(f101,plain,(
% 5.67/1.39 e_866=select(a_865,i2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f45])).
% 5.67/1.39 fof(f102,plain,(
% 5.67/1.39 e_868=select(a_865,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f46])).
% 5.67/1.39 fof(f103,plain,(
% 5.67/1.39 e_870=select(a_869,i1)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f47])).
% 5.67/1.39 fof(f104,plain,(
% 5.67/1.39 e_873=select(a_872,i2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f48])).
% 5.67/1.39 fof(f105,plain,(
% 5.67/1.39 e_875=select(a_872,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f49])).
% 5.67/1.39 fof(f106,plain,(
% 5.67/1.39 e_877=select(a_876,i2)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f50])).
% 5.67/1.39 fof(f107,plain,(
% 5.67/1.39 e_879=select(a_876,i5)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f51])).
% 5.67/1.39 fof(f108,plain,(
% 5.67/1.39 e_882=select(a_859,i_881)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f52])).
% 5.67/1.39 fof(f109,plain,(
% 5.67/1.39 e_883=select(a_880,i_881)),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f53])).
% 5.67/1.39 fof(f111,plain,(
% 5.67/1.39 ~e_882=e_883),
% 5.67/1.39 inference(cnf_transformation,[status(thm)],[f55])).
% 5.67/1.39 fof(f177,plain,(
% 5.67/1.39 ![X0]: (store(store(a_836,X0,select(a_836,i2)),i2,select(a_836,X0))=store(store(a_836,i2,select(a_836,X0)),X0,e_839))),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f89,f59])).
% 5.67/1.39 fof(f181,plain,(
% 5.67/1.39 ![X0]: (store(store(a_836,X0,e_839),i2,select(a_836,X0))=store(store(a_836,i2,select(a_836,X0)),X0,e_839))),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f89,f177])).
% 5.67/1.39 fof(f204,plain,(
% 5.67/1.39 select(a_844,i5)=e_843),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f65,f56])).
% 5.67/1.39 fof(f234,plain,(
% 5.67/1.39 ![X0]: (store(store(a_840,X0,select(a_840,i0)),i0,select(a_840,X0))=store(store(a_840,i0,select(a_840,X0)),X0,e_843))),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f91,f59])).
% 5.67/1.39 fof(f238,plain,(
% 5.67/1.39 ![X0]: (store(store(a_840,X0,e_843),i0,select(a_840,X0))=store(store(a_840,i0,select(a_840,X0)),X0,e_843))),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f91,f234])).
% 5.67/1.39 fof(f250,plain,(
% 5.67/1.39 ![X0]: (store(store(a_844,X0,select(a_844,i2)),i2,select(a_844,X0))=store(store(a_844,i2,select(a_844,X0)),X0,e_847))),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f93,f59])).
% 5.67/1.39 fof(f254,plain,(
% 5.67/1.39 ![X0]: (store(store(a_844,X0,e_847),i2,select(a_844,X0))=store(store(a_844,i2,select(a_844,X0)),X0,e_847))),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f93,f250])).
% 5.67/1.39 fof(f269,plain,(
% 5.67/1.39 select(a_855,i2)=e_854),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f71,f56])).
% 5.67/1.39 fof(f512,plain,(
% 5.67/1.39 select(a_876,i2)=e_875),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f83,f56])).
% 5.67/1.39 fof(f2969,plain,(
% 5.67/1.39 e_845=e_843),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f204,f92])).
% 5.67/1.39 fof(f2978,plain,(
% 5.67/1.39 a_846=store(a_844,i2,e_843)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f2969,f66])).
% 5.67/1.39 fof(f4148,plain,(
% 5.67/1.39 e_856=e_854),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f269,f97])).
% 5.67/1.39 fof(f4163,plain,(
% 5.67/1.39 a_857=store(a_855,i5,e_854)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f4148,f72])).
% 5.67/1.39 fof(f4206,plain,(
% 5.67/1.39 store(store(a_836,i1,e_839),i2,select(a_836,i1))=store(store(a_836,i2,e_837),i1,e_839)),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f88,f181])).
% 5.67/1.39 fof(f4218,plain,(
% 5.67/1.39 store(a_860,i2,select(a_836,i1))=store(store(a_836,i2,e_837),i1,e_839)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f74,f4206])).
% 5.67/1.39 fof(f4219,plain,(
% 5.67/1.39 store(a_860,i2,e_837)=store(store(a_836,i2,e_837),i1,e_839)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f88,f4218])).
% 5.67/1.39 fof(f4220,plain,(
% 5.67/1.39 a_861=store(store(a_836,i2,e_837),i1,e_839)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f75,f4219])).
% 5.67/1.39 fof(f4221,plain,(
% 5.67/1.39 a_861=store(a_838,i1,e_839)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f62,f4220])).
% 5.67/1.39 fof(f4222,plain,(
% 5.67/1.39 a_861=a_840),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f63,f4221])).
% 5.67/1.39 fof(f4312,plain,(
% 5.67/1.39 e_864=select(a_840,i5)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f4222,f100])).
% 5.67/1.39 fof(f4313,plain,(
% 5.67/1.39 e_862=select(a_840,i0)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f4222,f99])).
% 5.67/1.39 fof(f4314,plain,(
% 5.67/1.39 a_863=store(a_840,i5,e_862)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f4222,f76])).
% 5.67/1.39 fof(f4316,plain,(
% 5.67/1.39 e_864=e_841),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f90,f4312])).
% 5.67/1.39 fof(f4317,plain,(
% 5.67/1.39 e_862=e_843),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f91,f4313])).
% 5.67/1.39 fof(f4318,plain,(
% 5.67/1.39 a_865=store(a_863,i0,e_841)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f4316,f77])).
% 5.67/1.39 fof(f4319,plain,(
% 5.67/1.39 a_863=store(a_840,i5,e_843)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f4317,f4314])).
% 5.67/1.39 fof(f5333,plain,(
% 5.67/1.39 store(store(a_840,i5,e_843),i0,select(a_840,i5))=store(store(a_840,i0,e_841),i5,e_843)),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f90,f238])).
% 5.67/1.39 fof(f5347,plain,(
% 5.67/1.39 store(a_863,i0,select(a_840,i5))=store(store(a_840,i0,e_841),i5,e_843)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f4319,f5333])).
% 5.67/1.39 fof(f5348,plain,(
% 5.67/1.39 store(a_863,i0,e_841)=store(store(a_840,i0,e_841),i5,e_843)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f90,f5347])).
% 5.67/1.39 fof(f5349,plain,(
% 5.67/1.39 a_865=store(store(a_840,i0,e_841),i5,e_843)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f4318,f5348])).
% 5.67/1.39 fof(f5350,plain,(
% 5.67/1.39 a_865=store(a_842,i5,e_843)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f64,f5349])).
% 5.67/1.39 fof(f5351,plain,(
% 5.67/1.39 a_865=a_844),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f65,f5350])).
% 5.67/1.39 fof(f5501,plain,(
% 5.67/1.39 e_868=select(a_844,i5)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f5351,f102])).
% 5.67/1.39 fof(f5502,plain,(
% 5.67/1.39 e_866=select(a_844,i2)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f5351,f101])).
% 5.67/1.39 fof(f5503,plain,(
% 5.67/1.39 a_867=store(a_844,i5,e_866)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f5351,f78])).
% 5.67/1.39 fof(f5504,plain,(
% 5.67/1.39 e_868=e_843),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f204,f5501])).
% 5.67/1.39 fof(f5505,plain,(
% 5.67/1.39 e_866=e_847),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f93,f5502])).
% 5.67/1.39 fof(f5506,plain,(
% 5.67/1.39 a_869=store(a_867,i2,e_843)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f5504,f79])).
% 5.67/1.39 fof(f5547,plain,(
% 5.67/1.39 a_867=store(a_844,i5,e_847)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f5505,f5503])).
% 5.67/1.39 fof(f5940,plain,(
% 5.67/1.39 store(store(a_844,i5,e_847),i2,select(a_844,i5))=store(store(a_844,i2,e_843),i5,e_847)),
% 5.67/1.39 inference(paramodulation,[status(thm)],[f204,f254])).
% 5.67/1.39 fof(f5952,plain,(
% 5.67/1.39 store(a_867,i2,select(a_844,i5))=store(store(a_844,i2,e_843),i5,e_847)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f5547,f5940])).
% 5.67/1.39 fof(f5953,plain,(
% 5.67/1.39 store(a_867,i2,e_843)=store(store(a_844,i2,e_843),i5,e_847)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f204,f5952])).
% 5.67/1.39 fof(f5954,plain,(
% 5.67/1.39 a_869=store(store(a_844,i2,e_843),i5,e_847)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f5506,f5953])).
% 5.67/1.39 fof(f5955,plain,(
% 5.67/1.39 a_869=store(a_846,i5,e_847)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f2978,f5954])).
% 5.67/1.39 fof(f5956,plain,(
% 5.67/1.39 a_869=a_848),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f67,f5955])).
% 5.67/1.39 fof(f6117,plain,(
% 5.67/1.39 e_870=select(a_848,i1)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f5956,f103])).
% 5.67/1.39 fof(f6118,plain,(
% 5.67/1.39 a_871=store(a_848,i1,e_870)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f5956,f80])).
% 5.67/1.39 fof(f6119,plain,(
% 5.67/1.39 e_870=e_849),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f94,f6117])).
% 5.67/1.39 fof(f6121,plain,(
% 5.67/1.39 a_872=store(a_871,i1,e_849)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6119,f81])).
% 5.67/1.39 fof(f6177,plain,(
% 5.67/1.39 a_871=store(a_848,i1,e_849)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f6119,f6118])).
% 5.67/1.39 fof(f6178,plain,(
% 5.67/1.39 a_871=a_850),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f68,f6177])).
% 5.67/1.39 fof(f6179,plain,(
% 5.67/1.39 a_872=store(a_850,i1,e_849)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f6178,f6121])).
% 5.67/1.39 fof(f6181,plain,(
% 5.67/1.39 e_875=select(a_851,i5)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6184,f105])).
% 5.67/1.39 fof(f6182,plain,(
% 5.67/1.39 e_873=select(a_851,i2)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6184,f104])).
% 5.67/1.39 fof(f6183,plain,(
% 5.67/1.39 a_874=store(a_851,i5,e_873)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6184,f82])).
% 5.67/1.39 fof(f6184,plain,(
% 5.67/1.39 a_872=a_851),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f69,f6179])).
% 5.67/1.39 fof(f6185,plain,(
% 5.67/1.39 e_875=e_854),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f96,f6181])).
% 5.67/1.39 fof(f6186,plain,(
% 5.67/1.39 e_873=e_852),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f95,f6182])).
% 5.67/1.39 fof(f6187,plain,(
% 5.67/1.39 a_876=store(a_874,i2,e_854)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6185,f83])).
% 5.67/1.39 fof(f6188,plain,(
% 5.67/1.39 a_874=store(a_851,i5,e_852)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f6186,f6183])).
% 5.67/1.39 fof(f6189,plain,(
% 5.67/1.39 a_874=a_853),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f70,f6188])).
% 5.67/1.39 fof(f6338,plain,(
% 5.67/1.39 e_877=e_854),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6339,f106])).
% 5.67/1.39 fof(f6339,plain,(
% 5.67/1.39 select(a_876,i2)=e_854),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f6185,f512])).
% 5.67/1.39 fof(f6354,plain,(
% 5.67/1.39 a_878=store(a_876,i5,e_854)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6338,f84])).
% 5.67/1.39 fof(f6355,plain,(
% 5.67/1.39 a_876=store(a_853,i2,e_854)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f6189,f6187])).
% 5.67/1.39 fof(f6357,plain,(
% 5.67/1.39 e_879=select(a_855,i5)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6358,f107])).
% 5.67/1.39 fof(f6358,plain,(
% 5.67/1.39 a_876=a_855),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f71,f6355])).
% 5.67/1.39 fof(f6359,plain,(
% 5.67/1.39 e_879=e_858),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f98,f6357])).
% 5.67/1.39 fof(f6360,plain,(
% 5.67/1.39 a_878=store(a_855,i5,e_854)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f6358,f6354])).
% 5.67/1.39 fof(f6361,plain,(
% 5.67/1.39 a_880=store(a_857,i2,e_879)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6362,f85])).
% 5.67/1.39 fof(f6362,plain,(
% 5.67/1.39 a_878=a_857),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f4163,f6360])).
% 5.67/1.39 fof(f6363,plain,(
% 5.67/1.39 a_880=store(a_857,i2,e_858)),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f6359,f6361])).
% 5.67/1.39 fof(f6403,plain,(
% 5.67/1.39 e_883=select(a_859,i_881)),
% 5.67/1.39 inference(backward_demodulation,[status(thm)],[f6404,f109])).
% 5.67/1.39 fof(f6404,plain,(
% 5.67/1.39 a_880=a_859),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f73,f6363])).
% 5.67/1.39 fof(f6661,plain,(
% 5.67/1.39 e_883=e_882),
% 5.67/1.39 inference(forward_demodulation,[status(thm)],[f108,f6403])).
% 5.67/1.39 fof(f6662,plain,(
% 5.67/1.39 $false),
% 5.67/1.39 inference(forward_subsumption_resolution,[status(thm)],[f6661,f111])).
% 5.67/1.39 % SZS output end CNFRefutation for theBenchmark.p
% 5.37/1.41 % Elapsed time: 0.858194 seconds
% 5.37/1.41 % CPU time: 6.487909 seconds
% 5.37/1.41 % Total memory used: 217.790 MB
% 5.37/1.41 % Net memory used: 214.181 MB
%------------------------------------------------------------------------------