%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV565-1.004 : 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 : n004.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:49 PM UTC 2026
% Result : Unsatisfiable 11.00s 1.90s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV565-1.004 : 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.36 % Computer : n004.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 09:10:04 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 11.00/1.90 % Refutation found
% 11.00/1.90 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.00/1.90 % SZS output start CNFRefutation for theBenchmark
% 11.00/1.90 fof(f1,axiom,(
% 11.00/1.90 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f2,axiom,(
% 11.00/1.90 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f3,axiom,(
% 11.00/1.90 (![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)) ))),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f4,hypothesis,(
% 11.00/1.90 a_20 = store(a1,i1,e_19) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f5,hypothesis,(
% 11.00/1.90 a_22 = store(a2,i1,e_21) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f6,hypothesis,(
% 11.00/1.90 a_24 = store(a_20,i2,e_23) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f7,hypothesis,(
% 11.00/1.90 a_26 = store(a_22,i2,e_25) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f8,hypothesis,(
% 11.00/1.90 a_28 = store(a_24,i3,e_27) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f9,hypothesis,(
% 11.00/1.90 a_30 = store(a_26,i3,e_29) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f10,hypothesis,(
% 11.00/1.90 a_32 = store(a_28,i4,e_31) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f11,hypothesis,(
% 11.00/1.90 a_34 = store(a_30,i4,e_33) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f12,hypothesis,(
% 11.00/1.90 e_19 = select(a2,i1) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f13,hypothesis,(
% 11.00/1.90 e_21 = select(a1,i1) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f14,hypothesis,(
% 11.00/1.90 e_23 = select(a_22,i2) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f15,hypothesis,(
% 11.00/1.90 e_25 = select(a_20,i2) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f16,hypothesis,(
% 11.00/1.90 e_27 = select(a_26,i3) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f17,hypothesis,(
% 11.00/1.90 e_29 = select(a_24,i3) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f18,hypothesis,(
% 11.00/1.90 e_31 = select(a_30,i4) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f19,hypothesis,(
% 11.00/1.90 e_33 = select(a_28,i4) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f20,hypothesis,(
% 11.00/1.90 e_36 = select(a1,i_35) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f21,hypothesis,(
% 11.00/1.90 e_37 = select(a2,i_35) ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f23,hypothesis,(
% 11.00/1.90 a_32 = a_34 ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f24,negated_conjecture,(
% 11.00/1.90 e_36 != e_37 ),
% 11.00/1.90 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.00/1.90 fof(f25,plain,(
% 11.00/1.90 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f1])).
% 11.00/1.90 fof(f26,plain,(
% 11.00/1.90 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 11.00/1.90 inference(miniscoping,[status(thm)],[f2])).
% 11.00/1.90 fof(f27,plain,(
% 11.00/1.90 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f26])).
% 11.00/1.90 fof(f28,plain,(
% 11.00/1.90 ![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)))),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f3])).
% 11.00/1.90 fof(f29,plain,(
% 11.00/1.90 a_20=store(a1,i1,e_19)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f4])).
% 11.00/1.90 fof(f30,plain,(
% 11.00/1.90 a_22=store(a2,i1,e_21)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f5])).
% 11.00/1.90 fof(f31,plain,(
% 11.00/1.90 a_24=store(a_20,i2,e_23)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f6])).
% 11.00/1.90 fof(f32,plain,(
% 11.00/1.90 a_26=store(a_22,i2,e_25)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f7])).
% 11.00/1.90 fof(f33,plain,(
% 11.00/1.90 a_28=store(a_24,i3,e_27)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f8])).
% 11.00/1.90 fof(f34,plain,(
% 11.00/1.90 a_30=store(a_26,i3,e_29)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f9])).
% 11.00/1.90 fof(f35,plain,(
% 11.00/1.90 a_32=store(a_28,i4,e_31)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f10])).
% 11.00/1.90 fof(f36,plain,(
% 11.00/1.90 a_34=store(a_30,i4,e_33)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f11])).
% 11.00/1.90 fof(f37,plain,(
% 11.00/1.90 e_19=select(a2,i1)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f12])).
% 11.00/1.90 fof(f38,plain,(
% 11.00/1.90 e_21=select(a1,i1)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f13])).
% 11.00/1.90 fof(f39,plain,(
% 11.00/1.90 e_23=select(a_22,i2)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f14])).
% 11.00/1.90 fof(f40,plain,(
% 11.00/1.90 e_25=select(a_20,i2)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f15])).
% 11.00/1.90 fof(f41,plain,(
% 11.00/1.90 e_27=select(a_26,i3)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f16])).
% 11.00/1.90 fof(f42,plain,(
% 11.00/1.90 e_29=select(a_24,i3)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f17])).
% 11.00/1.90 fof(f43,plain,(
% 11.00/1.90 e_31=select(a_30,i4)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f18])).
% 11.00/1.90 fof(f44,plain,(
% 11.00/1.90 e_33=select(a_28,i4)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f19])).
% 11.00/1.90 fof(f45,plain,(
% 11.00/1.90 e_36=select(a1,i_35)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f20])).
% 11.00/1.90 fof(f46,plain,(
% 11.00/1.90 e_37=select(a2,i_35)),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f21])).
% 11.00/1.90 fof(f48,plain,(
% 11.00/1.90 a_32=a_34),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f23])).
% 11.00/1.90 fof(f49,plain,(
% 11.00/1.90 ~e_36=e_37),
% 11.00/1.90 inference(cnf_transformation,[status(thm)],[f24])).
% 11.00/1.90 fof(f50,plain,(
% 11.00/1.90 select(a_20,i1)=e_19),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f29,f25])).
% 11.00/1.90 fof(f51,plain,(
% 11.00/1.90 select(a_22,i1)=e_21),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f30,f25])).
% 11.00/1.90 fof(f52,plain,(
% 11.00/1.90 select(a_24,i2)=e_23),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f31,f25])).
% 11.00/1.90 fof(f54,plain,(
% 11.00/1.90 ![X0]: (i2=X0|select(a_24,X0)=select(a_20,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f31,f27])).
% 11.00/1.90 fof(f55,plain,(
% 11.00/1.90 ![X0]: (i1=X0|select(a_22,X0)=select(a2,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f30,f27])).
% 11.00/1.90 fof(f56,plain,(
% 11.00/1.90 ![X0]: (i1=X0|select(a_20,X0)=select(a1,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f29,f27])).
% 11.00/1.90 fof(f71,plain,(
% 11.00/1.90 ![X0]: (store(store(a2,X0,e_37),i_35,select(a2,X0))=store(store(a2,i_35,select(a2,X0)),X0,select(a2,i_35)))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f46,f28])).
% 11.00/1.90 fof(f132,plain,(
% 11.00/1.90 ![X0]: (store(store(a2,X0,e_37),i_35,select(a2,X0))=store(store(a2,i_35,select(a2,X0)),X0,e_37))),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f46,f71])).
% 11.00/1.90 fof(f182,plain,(
% 11.00/1.90 ![X0]: (i2=X0|select(a_26,X0)=select(a_22,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f32,f27])).
% 11.00/1.90 fof(f183,plain,(
% 11.00/1.90 select(a_26,i2)=e_25),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f32,f25])).
% 11.00/1.90 fof(f192,plain,(
% 11.00/1.90 ![X0]: (i3=X0|select(a_28,X0)=select(a_24,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f33,f27])).
% 11.00/1.90 fof(f193,plain,(
% 11.00/1.90 select(a_28,i3)=e_27),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f33,f25])).
% 11.00/1.90 fof(f202,plain,(
% 11.00/1.90 ![X0]: (i3=X0|select(a_30,X0)=select(a_26,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f34,f27])).
% 11.00/1.90 fof(f203,plain,(
% 11.00/1.90 select(a_30,i3)=e_29),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f34,f25])).
% 11.00/1.90 fof(f212,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_32,X0)=select(a_28,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f35,f27])).
% 11.00/1.90 fof(f213,plain,(
% 11.00/1.90 select(a_32,i4)=e_31),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f35,f25])).
% 11.00/1.90 fof(f222,plain,(
% 11.00/1.90 a_32=store(a_30,i4,e_33)),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f48,f36])).
% 11.00/1.90 fof(f223,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_32,X0)=select(a_30,X0))),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f222,f27])).
% 11.00/1.90 fof(f224,plain,(
% 11.00/1.90 select(a_32,i4)=e_33),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f222,f25])).
% 11.00/1.90 fof(f225,plain,(
% 11.00/1.90 e_31=e_33),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f213,f224])).
% 11.00/1.90 fof(f227,plain,(
% 11.00/1.90 e_31=select(a_28,i4)),
% 11.00/1.90 inference(backward_demodulation,[status(thm)],[f225,f44])).
% 11.00/1.90 fof(f239,plain,(
% 11.00/1.90 i2=i3|e_29=select(a_20,i3)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f42,f54])).
% 11.00/1.90 fof(f251,plain,(
% 11.00/1.90 i1=i_35|select(a_22,i_35)=e_37),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f46,f55])).
% 11.00/1.90 fof(f258,plain,(
% 11.00/1.90 ![X0]: (store(store(a_22,X0,select(a_22,i_35)),i_35,select(a_22,X0))=store(store(a_22,i_35,select(a_22,X0)),X0,e_37)|i1=i_35)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f251,f28])).
% 11.00/1.90 fof(f263,plain,(
% 11.00/1.90 i1=i_35|select(a_20,i_35)=e_36),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f45,f56])).
% 11.00/1.90 fof(f286,plain,(
% 11.00/1.90 ![X0]: (store(store(a_20,X0,select(a_20,i_35)),i_35,select(a_20,X0))=store(store(a_20,i_35,select(a_20,X0)),X0,e_36)|i1=i_35)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f263,f28])).
% 11.00/1.90 fof(f294,plain,(
% 11.00/1.90 ![X0]: (select(store(store(a2,X0,e_37),i_35,select(a2,X0)),X0)=e_37)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f132,f25])).
% 11.00/1.90 fof(f298,plain,(
% 11.00/1.90 select(store(store(a2,i1,e_37),i_35,e_19),i1)=e_37),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f37,f294])).
% 11.00/1.90 fof(f418,plain,(
% 11.00/1.90 i2=i3|e_27=select(a_22,i3)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f41,f182])).
% 11.00/1.90 fof(f430,plain,(
% 11.00/1.90 i3=i4|e_31=select(a_24,i4)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f227,f192])).
% 11.00/1.90 fof(f439,plain,(
% 11.00/1.90 i3=i4|e_31=select(a_20,i4)|i2=i4),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f54,f430])).
% 11.00/1.90 fof(f446,plain,(
% 11.00/1.90 i3=i4|e_31=select(a_26,i4)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f43,f202])).
% 11.00/1.90 fof(f454,plain,(
% 11.00/1.90 i3=i4|e_31=select(a_22,i4)|i2=i4),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f182,f446])).
% 11.00/1.90 fof(f467,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_28,X0)=select(a_30,X0)|i4=X0)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f212,f223])).
% 11.00/1.90 fof(f474,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_28,X0)=select(a_30,X0))),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f467])).
% 11.00/1.90 fof(f476,plain,(
% 11.00/1.90 i4=i3|select(a_28,i3)=e_29),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f203,f474])).
% 11.00/1.90 fof(f478,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_28,X0)=select(a_26,X0)|i3=X0)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f202,f474])).
% 11.00/1.90 fof(f487,plain,(
% 11.00/1.90 i4=i3|e_27=e_29),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f193,f476])).
% 11.00/1.90 fof(f494,plain,(
% 11.00/1.90 e_31=select(a_28,i3)|e_27=e_29),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f487,f227])).
% 11.00/1.90 fof(f497,plain,(
% 11.00/1.90 e_31=select(a_30,i3)|e_27=e_29),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f487,f43])).
% 11.00/1.90 fof(f500,plain,(
% 11.00/1.90 e_31=e_27|e_27=e_29),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f193,f494])).
% 11.00/1.90 fof(f501,plain,(
% 11.00/1.90 e_31=e_29|e_27=e_29),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f203,f497])).
% 11.00/1.90 fof(f506,plain,(
% 11.00/1.90 e_27=e_29|e_27=e_29|e_27=e_29),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f500,f501])).
% 11.00/1.90 fof(f512,plain,(
% 11.00/1.90 e_27=e_29),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f506])).
% 11.00/1.90 fof(f518,plain,(
% 11.00/1.90 i2=i3|e_27=select(a_20,i3)),
% 11.00/1.90 inference(backward_demodulation,[status(thm)],[f512,f239])).
% 11.00/1.90 fof(f521,plain,(
% 11.00/1.90 e_27=select(a_24,i3)),
% 11.00/1.90 inference(backward_demodulation,[status(thm)],[f512,f42])).
% 11.00/1.90 fof(f670,plain,(
% 11.00/1.90 ![X0]: (store(store(a_22,X0,e_37),i_35,select(a_22,X0))=store(store(a_22,i_35,select(a_22,X0)),X0,e_37)|i1=i_35|i1=i_35)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f251,f258])).
% 11.00/1.90 fof(f679,plain,(
% 11.00/1.90 ![X0]: (store(store(a_22,X0,e_37),i_35,select(a_22,X0))=store(store(a_22,i_35,select(a_22,X0)),X0,e_37)|i1=i_35)),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f670])).
% 11.00/1.90 fof(f934,plain,(
% 11.00/1.90 ![X0]: (select(store(store(a_20,i_35,select(a_20,X0)),X0,e_36),i_35)=select(a_20,X0)|i1=i_35)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f286,f25])).
% 11.00/1.90 fof(f941,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_24,X0)=select(a_26,X0)|i3=X0|i3=X0)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f192,f478])).
% 11.00/1.90 fof(f950,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_24,X0)=select(a_26,X0)|i3=X0)),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f941])).
% 11.00/1.90 fof(f953,plain,(
% 11.00/1.90 i4=i2|select(a_24,i2)=e_25|i3=i2),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f183,f950])).
% 11.00/1.90 fof(f955,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_24,X0)=select(a_22,X0)|i3=X0|i2=X0)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f182,f950])).
% 11.00/1.90 fof(f965,plain,(
% 11.00/1.90 i4=i2|e_23=e_25|i3=i2),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f52,f953])).
% 11.00/1.90 fof(f973,plain,(
% 11.00/1.90 i3=i4|e_31=select(a_26,i2)|e_23=e_25|i3=i2),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f965,f446])).
% 11.00/1.90 fof(f974,plain,(
% 11.00/1.90 i3=i4|e_31=select(a_24,i2)|e_23=e_25|i3=i2),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f965,f430])).
% 11.00/1.90 fof(f984,plain,(
% 11.00/1.90 i3=i4|e_31=e_25|e_23=e_25|i3=i2),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f183,f973])).
% 11.00/1.90 fof(f985,plain,(
% 11.00/1.90 i3=i4|e_31=e_23|e_23=e_25|i3=i2),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f52,f974])).
% 11.00/1.90 fof(f994,plain,(
% 11.00/1.90 i3=i4|e_25=e_23|e_23=e_25|i3=i2|i3=i4|e_23=e_25|i3=i2),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f984,f985])).
% 11.00/1.90 fof(f1002,plain,(
% 11.00/1.90 i3=i4|e_25=e_23|i3=i2),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f994])).
% 11.00/1.90 fof(f1006,plain,(
% 11.00/1.90 i3=i2|e_25=e_23|i3=i2|e_23=e_25|i3=i2),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f965,f1002])).
% 11.00/1.90 fof(f1023,plain,(
% 11.00/1.90 i3=i2|e_25=e_23),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f1006])).
% 11.00/1.90 fof(f1040,plain,(
% 11.00/1.90 e_27=select(a_24,i2)|e_25=e_23),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f1023,f521])).
% 11.00/1.90 fof(f1045,plain,(
% 11.00/1.90 e_27=select(a_26,i2)|e_25=e_23),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f1023,f41])).
% 11.00/1.90 fof(f1047,plain,(
% 11.00/1.90 e_27=e_23|e_25=e_23),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f52,f1040])).
% 11.00/1.90 fof(f1049,plain,(
% 11.00/1.90 e_27=e_25|e_25=e_23),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f183,f1045])).
% 11.00/1.90 fof(f1058,plain,(
% 11.00/1.90 e_23=e_25|e_25=e_23|e_25=e_23),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f1047,f1049])).
% 11.00/1.90 fof(f1068,plain,(
% 11.00/1.90 e_23=e_25),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f1058])).
% 11.00/1.90 fof(f1078,plain,(
% 11.00/1.90 e_23=select(a_20,i2)),
% 11.00/1.90 inference(backward_demodulation,[status(thm)],[f1068,f40])).
% 11.00/1.90 fof(f1761,plain,(
% 11.00/1.90 select(store(store(a_20,i_35,e_23),i2,e_36),i_35)=select(a_20,i2)|i1=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f1078,f934])).
% 11.00/1.90 fof(f1775,plain,(
% 11.00/1.90 select(store(store(a_20,i_35,e_23),i2,e_36),i_35)=e_23|i1=i_35),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f1078,f1761])).
% 11.00/1.90 fof(f2145,plain,(
% 11.00/1.90 ![X0]: (select(store(store(a_22,X0,e_37),i_35,select(a_22,X0)),X0)=e_37|i1=i_35)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f679,f25])).
% 11.00/1.90 fof(f2153,plain,(
% 11.00/1.90 select(store(store(a_22,i3,e_37),i_35,e_27),i3)=e_37|i1=i_35|i2=i3),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f418,f2145])).
% 11.00/1.90 fof(f2156,plain,(
% 11.00/1.90 select(store(store(a_22,i2,e_37),i_35,e_23),i2)=e_37|i1=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f39,f2145])).
% 11.00/1.90 fof(f2328,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_20,X0)=select(a_22,X0)|i3=X0|i2=X0|i2=X0)),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f54,f955])).
% 11.00/1.90 fof(f2338,plain,(
% 11.00/1.90 ![X0]: (i4=X0|select(a_20,X0)=select(a_22,X0)|i3=X0|i2=X0)),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2328])).
% 11.00/1.90 fof(f2342,plain,(
% 11.00/1.90 i4=i_35|select(a_20,i_35)=e_37|i3=i_35|i2=i_35|i1=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f251,f2338])).
% 11.00/1.90 fof(f2343,plain,(
% 11.00/1.90 i4=i1|select(a_20,i1)=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f51,f2338])).
% 11.00/1.90 fof(f2369,plain,(
% 11.00/1.90 i4=i1|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f50,f2343])).
% 11.00/1.90 fof(f2384,plain,(
% 11.00/1.90 e_31=select(a_28,i1)|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2369,f227])).
% 11.00/1.90 fof(f2387,plain,(
% 11.00/1.90 e_31=select(a_30,i1)|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2369,f43])).
% 11.00/1.90 fof(f2391,plain,(
% 11.00/1.90 e_31=select(a_24,i1)|e_19=e_21|i3=i1|i2=i1|i3=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f192,f2384])).
% 11.00/1.90 fof(f2400,plain,(
% 11.00/1.90 e_31=select(a_24,i1)|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2391])).
% 11.00/1.90 fof(f2413,plain,(
% 11.00/1.90 e_31=select(a_26,i1)|e_19=e_21|i3=i1|i2=i1|i3=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f202,f2387])).
% 11.00/1.90 fof(f2421,plain,(
% 11.00/1.90 e_31=select(a_26,i1)|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2413])).
% 11.00/1.90 fof(f2425,plain,(
% 11.00/1.90 e_31=select(a_20,i1)|e_19=e_21|i3=i1|i2=i1|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f54,f2400])).
% 11.00/1.90 fof(f2435,plain,(
% 11.00/1.90 e_31=e_19|e_19=e_21|i3=i1|i2=i1|i2=i1),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f50,f2425])).
% 11.00/1.90 fof(f2436,plain,(
% 11.00/1.90 e_31=e_19|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2435])).
% 11.00/1.90 fof(f2449,plain,(
% 11.00/1.90 e_31=select(a_22,i1)|e_19=e_21|i3=i1|i2=i1|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f182,f2421])).
% 11.00/1.90 fof(f2458,plain,(
% 11.00/1.90 e_31=e_21|e_19=e_21|i3=i1|i2=i1|i2=i1),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f51,f2449])).
% 11.00/1.90 fof(f2459,plain,(
% 11.00/1.90 e_31=e_21|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2458])).
% 11.00/1.90 fof(f2463,plain,(
% 11.00/1.90 e_19=e_21|e_19=e_21|i3=i1|i2=i1|e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2436,f2459])).
% 11.00/1.90 fof(f2472,plain,(
% 11.00/1.90 e_19=e_21|i3=i1|i2=i1),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2463])).
% 11.00/1.90 fof(f2488,plain,(
% 11.00/1.90 e_27=select(a_24,i1)|e_19=e_21|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2472,f521])).
% 11.00/1.90 fof(f2490,plain,(
% 11.00/1.90 i2=i3|e_27=select(a_22,i1)|e_19=e_21|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2472,f418])).
% 11.00/1.90 fof(f2495,plain,(
% 11.00/1.90 i2=i3|e_27=e_21|e_19=e_21|i2=i1),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f51,f2490])).
% 11.00/1.90 fof(f2533,plain,(
% 11.00/1.90 i4=i_35|e_36=e_37|i3=i_35|i2=i_35|i1=i_35|i1=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f263,f2342])).
% 11.00/1.90 fof(f2546,plain,(
% 11.00/1.90 i4=i_35|e_36=e_37|i3=i_35|i2=i_35|i1=i_35),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2533])).
% 11.00/1.90 fof(f2547,plain,(
% 11.00/1.90 i4=i_35|i3=i_35|i2=i_35|i1=i_35),
% 11.00/1.90 inference(forward_subsumption_resolution,[status(thm)],[f2546,f49])).
% 11.00/1.90 fof(f2653,plain,(
% 11.00/1.90 i1=i_35|select(a_20,i4)=e_36|i3=i_35|i2=i_35|i1=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2547,f263])).
% 11.00/1.90 fof(f2654,plain,(
% 11.00/1.90 i1=i_35|select(a_22,i4)=e_37|i3=i_35|i2=i_35|i1=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2547,f251])).
% 11.00/1.90 fof(f2657,plain,(
% 11.00/1.90 i2=i_35|i1=i_35|~i4=i3|i_35=i3),
% 11.00/1.90 inference(equality_factoring,[status(thm)],[f2547])).
% 11.00/1.90 fof(f2658,plain,(
% 11.00/1.90 i3=i_35|i1=i_35|~i4=i2|i_35=i2),
% 11.00/1.90 inference(equality_factoring,[status(thm)],[f2547])).
% 11.00/1.90 fof(f2707,plain,(
% 11.00/1.90 i1=i_35|select(a_20,i4)=e_36|i3=i_35|i2=i_35),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2653])).
% 11.00/1.90 fof(f2708,plain,(
% 11.00/1.90 i1=i_35|select(a_22,i4)=e_37|i3=i_35|i2=i_35),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f2654])).
% 11.00/1.90 fof(f2721,plain,(
% 11.00/1.90 i1=i_35|e_31=e_36|i3=i_35|i2=i_35|i3=i4|i2=i4),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f439,f2707])).
% 11.00/1.90 fof(f2733,plain,(
% 11.00/1.90 i1=i_35|e_31=e_36|i3=i_35|i2=i_35|i2=i4),
% 11.00/1.90 inference(forward_subsumption_resolution,[status(thm)],[f2721,f2657])).
% 11.00/1.90 fof(f2740,plain,(
% 11.00/1.90 i1=i_35|e_31=e_37|i3=i_35|i2=i_35|i3=i4|i2=i4),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f454,f2708])).
% 11.00/1.90 fof(f2759,plain,(
% 11.00/1.90 i1=i_35|e_31=e_37|i3=i_35|i2=i_35|i2=i4),
% 11.00/1.90 inference(forward_subsumption_resolution,[status(thm)],[f2740,f2657])).
% 11.00/1.90 fof(f2799,plain,(
% 11.00/1.90 i1=i_35|e_31=e_36|i3=i_35|i2=i_35),
% 11.00/1.90 inference(forward_subsumption_resolution,[status(thm)],[f2733,f2658])).
% 11.00/1.90 fof(f2961,plain,(
% 11.00/1.90 i1=i_35|e_31=e_37|i3=i_35|i2=i_35),
% 11.00/1.90 inference(forward_subsumption_resolution,[status(thm)],[f2759,f2658])).
% 11.00/1.90 fof(f2999,plain,(
% 11.00/1.90 ~e_36=e_31|i1=i_35|i3=i_35|i2=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f2961,f49])).
% 11.00/1.90 fof(f3020,plain,(
% 11.00/1.90 i1=i_35|i3=i_35|i2=i_35),
% 11.00/1.90 inference(forward_subsumption_resolution,[status(thm)],[f2999,f2799])).
% 11.00/1.90 fof(f3034,plain,(
% 11.00/1.90 select(store(store(a_22,i3,e_37),i3,e_27),i3)=e_37|i1=i_35|i2=i3|i1=i_35|i2=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f3020,f2153])).
% 11.00/1.90 fof(f3114,plain,(
% 11.00/1.90 i1=i_35|select(a_20,i3)=e_36|i1=i_35|i2=i_35),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f3020,f263])).
% 11.00/1.90 fof(f3119,plain,(
% 11.00/1.90 i1=i_35|~i3=i2|i_35=i2),
% 11.00/1.90 inference(equality_factoring,[status(thm)],[f3020])).
% 11.00/1.90 fof(f3133,plain,(
% 11.00/1.90 e_27=e_37|i1=i_35|i2=i3|i1=i_35|i2=i_35),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f25,f3034])).
% 11.00/1.90 fof(f3134,plain,(
% 11.00/1.90 e_27=e_37|i1=i_35|i2=i3|i2=i_35),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f3133])).
% 11.00/1.90 fof(f3170,plain,(
% 11.00/1.90 i1=i_35|select(a_20,i3)=e_36|i2=i_35),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f3114])).
% 11.00/1.90 fof(f3312,plain,(
% 11.00/1.90 e_27=select(a_20,i1)|e_19=e_21|i2=i1|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f54,f2488])).
% 11.00/1.90 fof(f3322,plain,(
% 11.00/1.90 e_27=e_19|e_19=e_21|i2=i1|i2=i1),
% 11.00/1.90 inference(forward_demodulation,[status(thm)],[f50,f3312])).
% 11.00/1.90 fof(f3323,plain,(
% 11.00/1.90 e_27=e_19|e_19=e_21|i2=i1),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f3322])).
% 11.00/1.90 fof(f3340,plain,(
% 11.00/1.90 i2=i3|e_19=e_21|e_19=e_21|i2=i1|e_19=e_21|i2=i1),
% 11.00/1.90 inference(paramodulation,[status(thm)],[f3323,f2495])).
% 11.00/1.90 fof(f3353,plain,(
% 11.00/1.90 i2=i3|e_19=e_21|i2=i1),
% 11.00/1.90 inference(duplicate_literals_removal,[status(thm)],[f3340])).
% 11.00/1.90 fof(f3363,plain,(
% 11.00/1.90 i2=i1|e_19=e_21|i2=i1|e_19=e_21|i2=i1),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f2472,f3353])).
% 11.00/1.91 fof(f3387,plain,(
% 11.00/1.91 i2=i1|e_19=e_21),
% 11.00/1.91 inference(duplicate_literals_removal,[status(thm)],[f3363])).
% 11.00/1.91 fof(f3413,plain,(
% 11.00/1.91 e_23=select(a_20,i1)|e_19=e_21),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f3387,f1078])).
% 11.00/1.91 fof(f3428,plain,(
% 11.00/1.91 e_23=select(a_22,i1)|e_19=e_21),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f3387,f39])).
% 11.00/1.91 fof(f3431,plain,(
% 11.00/1.91 e_23=e_19|e_19=e_21),
% 11.00/1.91 inference(forward_demodulation,[status(thm)],[f50,f3413])).
% 11.00/1.91 fof(f3434,plain,(
% 11.00/1.91 e_23=e_21|e_19=e_21),
% 11.00/1.91 inference(forward_demodulation,[status(thm)],[f51,f3428])).
% 11.00/1.91 fof(f3459,plain,(
% 11.00/1.91 e_19=e_21|e_19=e_21|e_19=e_21),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f3431,f3434])).
% 11.00/1.91 fof(f3485,plain,(
% 11.00/1.91 e_19=e_21),
% 11.00/1.91 inference(duplicate_literals_removal,[status(thm)],[f3459])).
% 11.00/1.91 fof(f3505,plain,(
% 11.00/1.91 e_19=select(a1,i1)),
% 11.00/1.91 inference(backward_demodulation,[status(thm)],[f3485,f38])).
% 11.00/1.91 fof(f4129,plain,(
% 11.00/1.91 e_27=e_37|i1=i_35|i2=i_35),
% 11.00/1.91 inference(forward_subsumption_resolution,[status(thm)],[f3134,f3119])).
% 11.00/1.91 fof(f4165,plain,(
% 11.00/1.91 ~e_36=e_27|i1=i_35|i2=i_35),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f4129,f49])).
% 11.00/1.91 fof(f4183,plain,(
% 11.00/1.91 i1=i_35|e_27=e_36|i2=i_35|i2=i3),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f518,f3170])).
% 11.00/1.91 fof(f4195,plain,(
% 11.00/1.91 i1=i_35|i2=i_35|i2=i3),
% 11.00/1.91 inference(forward_subsumption_resolution,[status(thm)],[f4183,f4165])).
% 11.00/1.91 fof(f4202,plain,(
% 11.00/1.91 i1=i_35|i2=i_35),
% 11.00/1.91 inference(forward_subsumption_resolution,[status(thm)],[f4195,f3119])).
% 11.00/1.91 fof(f4214,plain,(
% 11.00/1.91 select(store(store(a_22,i2,e_37),i2,e_23),i2)=e_37|i1=i_35|i1=i_35),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f4202,f2156])).
% 11.00/1.91 fof(f4237,plain,(
% 11.00/1.91 select(store(store(a_20,i_35,e_23),i2,e_36),i2)=e_23|i1=i_35|i1=i_35),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f4202,f1775])).
% 11.00/1.91 fof(f4301,plain,(
% 11.00/1.91 e_23=e_37|i1=i_35|i1=i_35),
% 11.00/1.91 inference(forward_demodulation,[status(thm)],[f25,f4214])).
% 11.00/1.91 fof(f4302,plain,(
% 11.00/1.91 e_23=e_37|i1=i_35),
% 11.00/1.91 inference(duplicate_literals_removal,[status(thm)],[f4301])).
% 11.00/1.91 fof(f4310,plain,(
% 11.00/1.91 e_36=e_23|i1=i_35|i1=i_35),
% 11.00/1.91 inference(forward_demodulation,[status(thm)],[f25,f4237])).
% 11.00/1.91 fof(f4311,plain,(
% 11.00/1.91 e_36=e_23|i1=i_35),
% 11.00/1.91 inference(duplicate_literals_removal,[status(thm)],[f4310])).
% 11.00/1.91 fof(f4379,plain,(
% 11.00/1.91 ~e_36=e_23|i1=i_35),
% 11.00/1.91 inference(paramodulation,[status(thm)],[f4302,f49])).
% 11.00/1.91 fof(f4562,plain,(
% 11.00/1.91 select(store(store(a2,i1,e_37),i1,e_19),i1)=e_37),
% 11.00/1.91 inference(backward_demodulation,[status(thm)],[f4570,f298])).
% 11.00/1.91 fof(f4569,plain,(
% 11.00/1.91 e_36=select(a1,i1)),
% 11.00/1.91 inference(backward_demodulation,[status(thm)],[f4570,f45])).
% 11.00/1.91 fof(f4570,plain,(
% 11.00/1.91 i1=i_35),
% 11.00/1.91 inference(forward_subsumption_resolution,[status(thm)],[f4379,f4311])).
% 11.00/1.91 fof(f4617,plain,(
% 11.00/1.91 e_19=e_37),
% 11.00/1.91 inference(forward_demodulation,[status(thm)],[f25,f4562])).
% 11.00/1.91 fof(f4620,plain,(
% 11.00/1.91 e_36=e_19),
% 11.00/1.91 inference(forward_demodulation,[status(thm)],[f3505,f4569])).
% 11.00/1.91 fof(f4621,plain,(
% 11.00/1.91 ~e_36=e_19),
% 11.00/1.91 inference(backward_demodulation,[status(thm)],[f4617,f49])).
% 11.00/1.91 fof(f4622,plain,(
% 11.00/1.91 ~e_19=e_19),
% 11.00/1.91 inference(forward_demodulation,[status(thm)],[f4620,f4621])).
% 11.00/1.91 fof(f4623,plain,(
% 11.00/1.91 $false),
% 11.00/1.91 inference(trivial_equality_resolution,[status(thm)],[f4622])).
% 11.00/1.91 % SZS output end CNFRefutation for theBenchmark.p
% 10.91/1.95 % Elapsed time: 1.572277 seconds
% 10.91/1.95 % CPU time: 12.050343 seconds
% 10.91/1.95 % Total memory used: 261.798 MB
% 10.91/1.95 % Net memory used: 255.585 MB
%------------------------------------------------------------------------------