%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV558-1.010 : 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 : 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:52:47 PM UTC 2026
% Result : Unsatisfiable 0.15s 5.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV558-1.010 : 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/5.38 % Computer : n015.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 09:11:56 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.40 % Drodi V4.1.1
% 0.15/5.44 % Refutation found
% 0.15/5.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.44 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.44 fof(f1,axiom,(
% 0.15/5.44 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f3,axiom,(
% 0.15/5.44 (![A,I]: (store(A,I,select(A,I)) = A ))),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f6,hypothesis,(
% 0.15/5.44 a_41 = store(a1,i1,e_40) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f7,hypothesis,(
% 0.15/5.44 a_43 = store(a2,i1,e_42) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f8,hypothesis,(
% 0.15/5.44 a_45 = store(a_41,i2,e_44) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f9,hypothesis,(
% 0.15/5.44 a_47 = store(a_43,i2,e_46) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f10,hypothesis,(
% 0.15/5.44 a_49 = store(a_45,i3,e_48) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f11,hypothesis,(
% 0.15/5.44 a_51 = store(a_47,i3,e_50) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f12,hypothesis,(
% 0.15/5.44 a_53 = store(a_49,i4,e_52) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f13,hypothesis,(
% 0.15/5.44 a_55 = store(a_51,i4,e_54) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f14,hypothesis,(
% 0.15/5.44 a_57 = store(a_53,i5,e_56) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f15,hypothesis,(
% 0.15/5.44 a_59 = store(a_55,i5,e_58) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f16,hypothesis,(
% 0.15/5.44 a_61 = store(a_57,i6,e_60) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f17,hypothesis,(
% 0.15/5.44 a_63 = store(a_59,i6,e_62) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f18,hypothesis,(
% 0.15/5.44 a_65 = store(a_61,i7,e_64) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f19,hypothesis,(
% 0.15/5.44 a_67 = store(a_63,i7,e_66) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f20,hypothesis,(
% 0.15/5.44 a_69 = store(a_65,i8,e_68) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f21,hypothesis,(
% 0.15/5.44 a_71 = store(a_67,i8,e_70) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f22,hypothesis,(
% 0.15/5.44 a_73 = store(a_69,i9,e_72) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f23,hypothesis,(
% 0.15/5.44 a_75 = store(a_71,i9,e_74) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f24,hypothesis,(
% 0.15/5.44 a_77 = store(a_73,i10,e_76) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f25,hypothesis,(
% 0.15/5.44 a_79 = store(a_75,i10,e_78) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f26,hypothesis,(
% 0.15/5.44 e_40 = select(a2,i1) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f27,hypothesis,(
% 0.15/5.44 e_42 = select(a1,i1) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f28,hypothesis,(
% 0.15/5.44 e_44 = select(a_43,i2) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f29,hypothesis,(
% 0.15/5.44 e_46 = select(a_41,i2) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f30,hypothesis,(
% 0.15/5.44 e_48 = select(a_47,i3) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f31,hypothesis,(
% 0.15/5.44 e_50 = select(a_45,i3) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f32,hypothesis,(
% 0.15/5.44 e_52 = select(a_51,i4) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f33,hypothesis,(
% 0.15/5.44 e_54 = select(a_49,i4) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f34,hypothesis,(
% 0.15/5.44 e_56 = select(a_55,i5) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f35,hypothesis,(
% 0.15/5.44 e_58 = select(a_53,i5) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f36,hypothesis,(
% 0.15/5.44 e_60 = select(a_59,i6) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f37,hypothesis,(
% 0.15/5.44 e_62 = select(a_57,i6) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f38,hypothesis,(
% 0.15/5.44 e_64 = select(a_63,i7) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f39,hypothesis,(
% 0.15/5.44 e_66 = select(a_61,i7) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f40,hypothesis,(
% 0.15/5.44 e_68 = select(a_67,i8) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f41,hypothesis,(
% 0.15/5.44 e_70 = select(a_65,i8) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f42,hypothesis,(
% 0.15/5.44 e_72 = select(a_71,i9) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f43,hypothesis,(
% 0.15/5.44 e_74 = select(a_69,i9) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f44,hypothesis,(
% 0.15/5.44 e_76 = select(a_75,i10) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f45,hypothesis,(
% 0.15/5.44 e_78 = select(a_73,i10) ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f46,hypothesis,(
% 0.15/5.44 a_77 = a_79 ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f47,negated_conjecture,(
% 0.15/5.44 a1 != a2 ),
% 0.15/5.44 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.15/5.44 fof(f48,plain,(
% 0.15/5.44 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f1])).
% 0.15/5.44 fof(f51,plain,(
% 0.15/5.44 ![X0,X1]: (store(X0,X1,select(X0,X1))=X0)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.15/5.44 fof(f55,plain,(
% 0.15/5.44 a_41=store(a1,i1,e_40)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.15/5.44 fof(f56,plain,(
% 0.15/5.44 a_43=store(a2,i1,e_42)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f7])).
% 0.15/5.44 fof(f57,plain,(
% 0.15/5.44 a_45=store(a_41,i2,e_44)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f8])).
% 0.15/5.44 fof(f58,plain,(
% 0.15/5.44 a_47=store(a_43,i2,e_46)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f9])).
% 0.15/5.44 fof(f59,plain,(
% 0.15/5.44 a_49=store(a_45,i3,e_48)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f10])).
% 0.15/5.44 fof(f60,plain,(
% 0.15/5.44 a_51=store(a_47,i3,e_50)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f11])).
% 0.15/5.44 fof(f61,plain,(
% 0.15/5.44 a_53=store(a_49,i4,e_52)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f12])).
% 0.15/5.44 fof(f62,plain,(
% 0.15/5.44 a_55=store(a_51,i4,e_54)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f13])).
% 0.15/5.44 fof(f63,plain,(
% 0.15/5.44 a_57=store(a_53,i5,e_56)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f14])).
% 0.15/5.44 fof(f64,plain,(
% 0.15/5.44 a_59=store(a_55,i5,e_58)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f15])).
% 0.15/5.44 fof(f65,plain,(
% 0.15/5.44 a_61=store(a_57,i6,e_60)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/5.44 fof(f66,plain,(
% 0.15/5.44 a_63=store(a_59,i6,e_62)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f17])).
% 0.15/5.44 fof(f67,plain,(
% 0.15/5.44 a_65=store(a_61,i7,e_64)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f18])).
% 0.15/5.44 fof(f68,plain,(
% 0.15/5.44 a_67=store(a_63,i7,e_66)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.44 fof(f69,plain,(
% 0.15/5.44 a_69=store(a_65,i8,e_68)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f20])).
% 0.15/5.44 fof(f70,plain,(
% 0.15/5.44 a_71=store(a_67,i8,e_70)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f21])).
% 0.15/5.44 fof(f71,plain,(
% 0.15/5.44 a_73=store(a_69,i9,e_72)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f22])).
% 0.15/5.44 fof(f72,plain,(
% 0.15/5.44 a_75=store(a_71,i9,e_74)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f23])).
% 0.15/5.44 fof(f73,plain,(
% 0.15/5.44 a_77=store(a_73,i10,e_76)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f24])).
% 0.15/5.44 fof(f74,plain,(
% 0.15/5.44 a_79=store(a_75,i10,e_78)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f25])).
% 0.15/5.44 fof(f75,plain,(
% 0.15/5.44 e_40=select(a2,i1)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f26])).
% 0.15/5.44 fof(f76,plain,(
% 0.15/5.44 e_42=select(a1,i1)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f27])).
% 0.15/5.44 fof(f77,plain,(
% 0.15/5.44 e_44=select(a_43,i2)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f28])).
% 0.15/5.44 fof(f78,plain,(
% 0.15/5.44 e_46=select(a_41,i2)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f29])).
% 0.15/5.44 fof(f79,plain,(
% 0.15/5.44 e_48=select(a_47,i3)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f30])).
% 0.15/5.44 fof(f80,plain,(
% 0.15/5.44 e_50=select(a_45,i3)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/5.44 fof(f81,plain,(
% 0.15/5.44 e_52=select(a_51,i4)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f32])).
% 0.15/5.44 fof(f82,plain,(
% 0.15/5.44 e_54=select(a_49,i4)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f33])).
% 0.15/5.44 fof(f83,plain,(
% 0.15/5.44 e_56=select(a_55,i5)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f34])).
% 0.15/5.44 fof(f84,plain,(
% 0.15/5.44 e_58=select(a_53,i5)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f35])).
% 0.15/5.44 fof(f85,plain,(
% 0.15/5.44 e_60=select(a_59,i6)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/5.44 fof(f86,plain,(
% 0.15/5.44 e_62=select(a_57,i6)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f37])).
% 0.15/5.44 fof(f87,plain,(
% 0.15/5.44 e_64=select(a_63,i7)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f38])).
% 0.15/5.44 fof(f88,plain,(
% 0.15/5.44 e_66=select(a_61,i7)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f39])).
% 0.15/5.44 fof(f89,plain,(
% 0.15/5.44 e_68=select(a_67,i8)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f40])).
% 0.15/5.44 fof(f90,plain,(
% 0.15/5.44 e_70=select(a_65,i8)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f41])).
% 0.15/5.44 fof(f91,plain,(
% 0.15/5.44 e_72=select(a_71,i9)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f42])).
% 0.15/5.44 fof(f92,plain,(
% 0.15/5.44 e_74=select(a_69,i9)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f43])).
% 0.15/5.44 fof(f93,plain,(
% 0.15/5.44 e_76=select(a_75,i10)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f44])).
% 0.15/5.44 fof(f94,plain,(
% 0.15/5.44 e_78=select(a_73,i10)),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f45])).
% 0.15/5.44 fof(f95,plain,(
% 0.15/5.44 a_77=a_79),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f46])).
% 0.15/5.44 fof(f96,plain,(
% 0.15/5.44 ~a1=a2),
% 0.15/5.44 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/5.44 fof(f99,plain,(
% 0.15/5.44 store(a_63,i7,e_64)=a_63),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f87,f51])).
% 0.15/5.44 fof(f100,plain,(
% 0.15/5.44 store(a_57,i6,e_62)=a_57),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f86,f51])).
% 0.15/5.44 fof(f101,plain,(
% 0.15/5.44 store(a_59,i6,e_60)=a_59),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f85,f51])).
% 0.15/5.44 fof(f102,plain,(
% 0.15/5.44 store(a_53,i5,e_58)=a_53),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f84,f51])).
% 0.15/5.44 fof(f103,plain,(
% 0.15/5.44 store(a_55,i5,e_56)=a_55),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f83,f51])).
% 0.15/5.44 fof(f104,plain,(
% 0.15/5.44 store(a_49,i4,e_54)=a_49),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f82,f51])).
% 0.15/5.44 fof(f105,plain,(
% 0.15/5.44 store(a_51,i4,e_52)=a_51),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f81,f51])).
% 0.15/5.44 fof(f106,plain,(
% 0.15/5.44 store(a_45,i3,e_50)=a_45),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f80,f51])).
% 0.15/5.44 fof(f107,plain,(
% 0.15/5.44 store(a_47,i3,e_48)=a_47),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f79,f51])).
% 0.15/5.44 fof(f108,plain,(
% 0.15/5.44 store(a_41,i2,e_46)=a_41),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f78,f51])).
% 0.15/5.44 fof(f111,plain,(
% 0.15/5.44 store(a_43,i2,e_44)=a_43),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f77,f51])).
% 0.15/5.44 fof(f112,plain,(
% 0.15/5.44 store(a1,i1,e_42)=a1),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f76,f51])).
% 0.15/5.44 fof(f113,plain,(
% 0.15/5.44 store(a2,i1,e_40)=a2),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f75,f51])).
% 0.15/5.44 fof(f116,plain,(
% 0.15/5.44 store(a_61,i7,e_66)=a_61),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f88,f51])).
% 0.15/5.44 fof(f117,plain,(
% 0.15/5.44 store(a_67,i8,e_68)=a_67),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f89,f51])).
% 0.15/5.44 fof(f118,plain,(
% 0.15/5.44 store(a_65,i8,e_70)=a_65),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f90,f51])).
% 0.15/5.44 fof(f119,plain,(
% 0.15/5.44 store(a_71,i9,e_72)=a_71),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f91,f51])).
% 0.15/5.44 fof(f120,plain,(
% 0.15/5.44 store(a_69,i9,e_74)=a_69),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f92,f51])).
% 0.15/5.44 fof(f122,plain,(
% 0.15/5.44 store(a_73,i10,e_78)=a_73),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f94,f51])).
% 0.15/5.44 fof(f124,plain,(
% 0.15/5.44 select(a_41,i1)=e_40),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f55,f48])).
% 0.15/5.44 fof(f127,plain,(
% 0.15/5.44 select(a_43,i1)=e_42),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f56,f48])).
% 0.15/5.44 fof(f130,plain,(
% 0.15/5.44 select(a_45,i2)=e_44),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f57,f48])).
% 0.15/5.44 fof(f133,plain,(
% 0.15/5.44 select(a_47,i2)=e_46),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f58,f48])).
% 0.15/5.44 fof(f180,plain,(
% 0.15/5.44 select(a_49,i3)=e_48),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f59,f48])).
% 0.15/5.44 fof(f186,plain,(
% 0.15/5.44 select(a_51,i3)=e_50),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f60,f48])).
% 0.15/5.44 fof(f192,plain,(
% 0.15/5.44 select(a_53,i4)=e_52),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f61,f48])).
% 0.15/5.44 fof(f198,plain,(
% 0.15/5.44 select(a_55,i4)=e_54),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f62,f48])).
% 0.15/5.44 fof(f204,plain,(
% 0.15/5.44 select(a_57,i5)=e_56),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f63,f48])).
% 0.15/5.44 fof(f210,plain,(
% 0.15/5.44 select(a_59,i5)=e_58),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f64,f48])).
% 0.15/5.44 fof(f216,plain,(
% 0.15/5.44 select(a_61,i6)=e_60),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f65,f48])).
% 0.15/5.44 fof(f222,plain,(
% 0.15/5.44 select(a_63,i6)=e_62),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f66,f48])).
% 0.15/5.44 fof(f228,plain,(
% 0.15/5.44 select(a_65,i7)=e_64),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f67,f48])).
% 0.15/5.44 fof(f233,plain,(
% 0.15/5.44 select(a_67,i7)=e_66),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f68,f48])).
% 0.15/5.44 fof(f238,plain,(
% 0.15/5.44 select(a_69,i8)=e_68),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f69,f48])).
% 0.15/5.44 fof(f246,plain,(
% 0.15/5.44 select(a_71,i8)=e_70),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f70,f48])).
% 0.15/5.44 fof(f252,plain,(
% 0.15/5.44 select(a_73,i9)=e_72),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f71,f48])).
% 0.15/5.44 fof(f258,plain,(
% 0.15/5.44 select(a_75,i9)=e_74),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f72,f48])).
% 0.15/5.44 fof(f260,plain,(
% 0.15/5.44 a_79=store(a_73,i10,e_76)),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f95,f73])).
% 0.15/5.44 fof(f265,plain,(
% 0.15/5.44 select(a_79,i10)=e_76),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f260,f48])).
% 0.15/5.44 fof(f271,plain,(
% 0.15/5.44 select(a_79,i10)=e_78),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f74,f48])).
% 0.15/5.44 fof(f272,plain,(
% 0.15/5.44 e_78=e_76),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f271,f265])).
% 0.15/5.44 fof(f274,plain,(
% 0.15/5.44 a_79=store(a_73,i10,e_78)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f272,f260])).
% 0.15/5.44 fof(f275,plain,(
% 0.15/5.44 e_78=select(a_75,i10)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f272,f93])).
% 0.15/5.44 fof(f276,plain,(
% 0.15/5.44 store(a_75,i10,e_78)=a_75),
% 0.15/5.44 inference(paramodulation,[status(thm)],[f275,f51])).
% 0.15/5.44 fof(f277,plain,(
% 0.15/5.44 a_79=a_75),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f74,f276])).
% 0.15/5.44 fof(f295,plain,(
% 0.15/5.44 select(a_79,i9)=e_74),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f277,f258])).
% 0.15/5.44 fof(f296,plain,(
% 0.15/5.44 a_79=store(a_71,i9,e_74)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f277,f72])).
% 0.15/5.44 fof(f527,plain,(
% 0.15/5.44 select(a_79,i9)=e_72),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f530,f252])).
% 0.15/5.44 fof(f528,plain,(
% 0.15/5.44 a_79=store(a_69,i9,e_72)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f530,f71])).
% 0.15/5.44 fof(f530,plain,(
% 0.15/5.44 a_79=a_73),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f274,f122])).
% 0.15/5.44 fof(f531,plain,(
% 0.15/5.44 e_74=e_72),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f295,f527])).
% 0.15/5.44 fof(f532,plain,(
% 0.15/5.44 store(a_71,i9,e_74)=a_71),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f531,f119])).
% 0.15/5.44 fof(f534,plain,(
% 0.15/5.44 a_79=a_71),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f296,f532])).
% 0.15/5.44 fof(f536,plain,(
% 0.15/5.44 select(a_79,i8)=e_70),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f534,f246])).
% 0.15/5.44 fof(f537,plain,(
% 0.15/5.44 a_79=store(a_67,i8,e_70)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f534,f70])).
% 0.15/5.44 fof(f583,plain,(
% 0.15/5.44 a_79=a_69),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f584,f120])).
% 0.15/5.44 fof(f584,plain,(
% 0.15/5.44 a_79=store(a_69,i9,e_74)),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f531,f528])).
% 0.15/5.44 fof(f607,plain,(
% 0.15/5.44 select(a_79,i8)=e_68),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f583,f238])).
% 0.15/5.44 fof(f608,plain,(
% 0.15/5.44 a_79=store(a_65,i8,e_68)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f583,f69])).
% 0.15/5.44 fof(f610,plain,(
% 0.15/5.44 e_70=e_68),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f536,f607])).
% 0.15/5.44 fof(f611,plain,(
% 0.15/5.44 store(a_67,i8,e_70)=a_67),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f610,f117])).
% 0.15/5.44 fof(f613,plain,(
% 0.15/5.44 a_79=a_67),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f537,f611])).
% 0.15/5.44 fof(f615,plain,(
% 0.15/5.44 select(a_79,i7)=e_66),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f613,f233])).
% 0.15/5.44 fof(f616,plain,(
% 0.15/5.44 a_79=store(a_63,i7,e_66)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f613,f68])).
% 0.15/5.44 fof(f620,plain,(
% 0.15/5.44 a_79=a_65),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f621,f118])).
% 0.15/5.44 fof(f621,plain,(
% 0.15/5.44 a_79=store(a_65,i8,e_70)),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f610,f608])).
% 0.15/5.44 fof(f630,plain,(
% 0.15/5.44 select(a_79,i7)=e_64),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f620,f228])).
% 0.15/5.44 fof(f631,plain,(
% 0.15/5.44 a_79=store(a_61,i7,e_64)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f620,f67])).
% 0.15/5.44 fof(f633,plain,(
% 0.15/5.44 e_66=e_64),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f615,f630])).
% 0.15/5.44 fof(f634,plain,(
% 0.15/5.44 store(a_63,i7,e_66)=a_63),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f633,f99])).
% 0.15/5.44 fof(f717,plain,(
% 0.15/5.44 a_79=a_61),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f718,f116])).
% 0.15/5.44 fof(f718,plain,(
% 0.15/5.44 a_79=store(a_61,i7,e_66)),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f633,f631])).
% 0.15/5.44 fof(f728,plain,(
% 0.15/5.44 select(a_79,i6)=e_60),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f717,f216])).
% 0.15/5.44 fof(f729,plain,(
% 0.15/5.44 a_79=store(a_57,i6,e_60)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f717,f65])).
% 0.15/5.44 fof(f737,plain,(
% 0.15/5.44 select(a_79,i6)=e_62),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f739,f222])).
% 0.15/5.44 fof(f738,plain,(
% 0.15/5.44 a_79=store(a_59,i6,e_62)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f739,f66])).
% 0.15/5.44 fof(f739,plain,(
% 0.15/5.44 a_79=a_63),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f616,f634])).
% 0.15/5.44 fof(f755,plain,(
% 0.15/5.44 e_62=e_60),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f737,f728])).
% 0.15/5.44 fof(f758,plain,(
% 0.15/5.44 a_79=store(a_57,i6,e_62)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f755,f729])).
% 0.15/5.44 fof(f759,plain,(
% 0.15/5.44 store(a_59,i6,e_62)=a_59),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f755,f101])).
% 0.15/5.44 fof(f761,plain,(
% 0.15/5.44 a_79=a_59),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f738,f759])).
% 0.15/5.44 fof(f764,plain,(
% 0.15/5.44 select(a_79,i5)=e_58),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f761,f210])).
% 0.15/5.44 fof(f765,plain,(
% 0.15/5.44 a_79=store(a_55,i5,e_58)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f761,f64])).
% 0.15/5.44 fof(f768,plain,(
% 0.15/5.44 a_79=a_57),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f758,f100])).
% 0.15/5.44 fof(f778,plain,(
% 0.15/5.44 select(a_79,i5)=e_56),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f768,f204])).
% 0.15/5.44 fof(f779,plain,(
% 0.15/5.44 a_79=store(a_53,i5,e_56)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f768,f63])).
% 0.15/5.44 fof(f784,plain,(
% 0.15/5.44 store(a_55,i5,e_58)=a_55),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f786,f103])).
% 0.15/5.44 fof(f786,plain,(
% 0.15/5.44 e_58=e_56),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f764,f778])).
% 0.15/5.44 fof(f815,plain,(
% 0.15/5.44 a_79=a_53),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f816,f102])).
% 0.15/5.44 fof(f816,plain,(
% 0.15/5.44 a_79=store(a_53,i5,e_58)),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f786,f779])).
% 0.15/5.44 fof(f826,plain,(
% 0.15/5.44 select(a_79,i4)=e_52),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f815,f192])).
% 0.15/5.44 fof(f827,plain,(
% 0.15/5.44 a_79=store(a_49,i4,e_52)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f815,f61])).
% 0.15/5.44 fof(f835,plain,(
% 0.15/5.44 select(a_79,i4)=e_54),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f837,f198])).
% 0.15/5.44 fof(f836,plain,(
% 0.15/5.44 a_79=store(a_51,i4,e_54)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f837,f62])).
% 0.15/5.44 fof(f837,plain,(
% 0.15/5.44 a_79=a_55),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f765,f784])).
% 0.15/5.44 fof(f839,plain,(
% 0.15/5.44 e_54=e_52),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f835,f826])).
% 0.15/5.44 fof(f842,plain,(
% 0.15/5.44 store(a_51,i4,e_54)=a_51),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f839,f105])).
% 0.15/5.44 fof(f856,plain,(
% 0.15/5.44 a_79=a_49),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f857,f104])).
% 0.15/5.44 fof(f857,plain,(
% 0.15/5.44 a_79=store(a_49,i4,e_54)),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f839,f827])).
% 0.15/5.44 fof(f867,plain,(
% 0.15/5.44 select(a_79,i3)=e_48),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f856,f180])).
% 0.15/5.44 fof(f868,plain,(
% 0.15/5.44 a_79=store(a_45,i3,e_48)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f856,f59])).
% 0.15/5.44 fof(f940,plain,(
% 0.15/5.44 select(a_79,i3)=e_50),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f942,f186])).
% 0.15/5.44 fof(f941,plain,(
% 0.15/5.44 a_79=store(a_47,i3,e_50)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f942,f60])).
% 0.15/5.44 fof(f942,plain,(
% 0.15/5.44 a_79=a_51),
% 0.15/5.44 inference(forward_demodulation,[status(thm)],[f836,f842])).
% 0.15/5.44 fof(f944,plain,(
% 0.15/5.44 e_50=e_48),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f940,f867])).
% 0.15/5.44 fof(f947,plain,(
% 0.15/5.44 a_79=store(a_45,i3,e_50)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f944,f868])).
% 0.15/5.44 fof(f948,plain,(
% 0.15/5.44 store(a_47,i3,e_50)=a_47),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f944,f107])).
% 0.15/5.44 fof(f996,plain,(
% 0.15/5.44 a_79=a_45),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f947,f106])).
% 0.15/5.44 fof(f1006,plain,(
% 0.15/5.44 select(a_79,i2)=e_44),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f996,f130])).
% 0.15/5.44 fof(f1007,plain,(
% 0.15/5.44 a_79=store(a_41,i2,e_44)),
% 0.15/5.44 inference(backward_demodulation,[status(thm)],[f996,f57])).
% 0.15/5.44 fof(f1015,plain,(
% 0.15/5.45 select(a_79,i2)=e_46),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1017,f133])).
% 0.15/5.45 fof(f1016,plain,(
% 0.15/5.45 a_79=store(a_43,i2,e_46)),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1017,f58])).
% 0.15/5.45 fof(f1017,plain,(
% 0.15/5.45 a_79=a_47),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f941,f948])).
% 0.15/5.45 fof(f1019,plain,(
% 0.15/5.45 e_46=e_44),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1015,f1006])).
% 0.15/5.45 fof(f1026,plain,(
% 0.15/5.45 store(a_43,i2,e_46)=a_43),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1019,f111])).
% 0.15/5.45 fof(f1029,plain,(
% 0.15/5.45 a_79=a_41),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1030,f108])).
% 0.15/5.45 fof(f1030,plain,(
% 0.15/5.45 a_79=store(a_41,i2,e_46)),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f1019,f1007])).
% 0.15/5.45 fof(f1089,plain,(
% 0.15/5.45 select(a_79,i1)=e_40),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f1029,f124])).
% 0.15/5.45 fof(f1090,plain,(
% 0.15/5.45 a_79=store(a1,i1,e_40)),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f1029,f55])).
% 0.15/5.45 fof(f1110,plain,(
% 0.15/5.45 a_79=a_43),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1016,f1026])).
% 0.15/5.45 fof(f1119,plain,(
% 0.15/5.45 select(a_79,i1)=e_42),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1110,f127])).
% 0.15/5.45 fof(f1121,plain,(
% 0.15/5.45 e_42=e_40),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1119,f1089])).
% 0.15/5.45 fof(f1137,plain,(
% 0.15/5.45 store(a2,i1,e_42)=a2),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f1121,f113])).
% 0.15/5.45 fof(f1145,plain,(
% 0.15/5.45 a_79=a2),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1146,f1137])).
% 0.15/5.45 fof(f1146,plain,(
% 0.15/5.45 a_79=store(a2,i1,e_42)),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f1110,f56])).
% 0.15/5.45 fof(f1154,plain,(
% 0.15/5.45 a_79=store(a1,i1,e_42)),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f1121,f1090])).
% 0.15/5.45 fof(f1175,plain,(
% 0.15/5.45 ~a1=a_79),
% 0.15/5.45 inference(backward_demodulation,[status(thm)],[f1145,f96])).
% 0.15/5.45 fof(f1176,plain,(
% 0.15/5.45 a_79=a1),
% 0.15/5.45 inference(forward_demodulation,[status(thm)],[f1154,f112])).
% 0.15/5.45 fof(f1177,plain,(
% 0.15/5.45 $false),
% 0.15/5.45 inference(forward_subsumption_resolution,[status(thm)],[f1176,f1175])).
% 0.15/5.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.47 % Elapsed time: 0.072749 seconds
% 0.15/5.47 % CPU time: 0.265731 seconds
% 0.15/5.47 % Total memory used: 106.100 MB
% 0.15/5.47 % Net memory used: 105.716 MB
%------------------------------------------------------------------------------