%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV553-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 : n008.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:24 PM UTC 2026
% Result : Unsatisfiable 104.32s 13.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV553-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.09/0.35 % Computer : n008.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % 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:08 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 104.32/13.60 % Refutation found
% 104.32/13.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 104.32/13.60 % SZS output start CNFRefutation for theBenchmark
% 104.32/13.60 fof(f1,axiom,(
% 104.32/13.60 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 104.32/13.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.32/13.60 fof(f2,axiom,(
% 104.32/13.60 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 104.32/13.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.32/13.60 fof(f3,hypothesis,(
% 104.32/13.60 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)) = store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)) ),
% 104.32/13.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.32/13.60 fof(f4,negated_conjecture,(
% 104.32/13.60 select(a1,sk(a1,a2)) != select(a2,sk(a1,a2)) ),
% 104.32/13.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 104.32/13.60 fof(f5,plain,(
% 104.32/13.60 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 104.32/13.60 inference(cnf_transformation,[status(thm)],[f1])).
% 104.32/13.60 fof(f6,plain,(
% 104.32/13.60 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 104.32/13.60 inference(miniscoping,[status(thm)],[f2])).
% 104.32/13.60 fof(f7,plain,(
% 104.32/13.60 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 104.32/13.60 inference(cnf_transformation,[status(thm)],[f6])).
% 104.32/13.60 fof(f8,plain,(
% 104.32/13.60 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4))=store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))),
% 104.32/13.60 inference(cnf_transformation,[status(thm)],[f3])).
% 104.32/13.60 fof(f9,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,sk(a1,a2))),
% 104.32/13.60 inference(cnf_transformation,[status(thm)],[f4])).
% 104.32/13.60 fof(f12,plain,(
% 104.32/13.60 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4))=store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f8])).
% 104.32/13.60 fof(f19,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),X0)=select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0))),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f8,f7])).
% 104.32/13.60 fof(f20,plain,(
% 104.32/13.60 select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f8,f5])).
% 104.32/13.60 fof(f21,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f20])).
% 104.32/13.60 fof(f23,plain,(
% 104.32/13.60 select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)|i3=i4),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f21])).
% 104.32/13.60 fof(f24,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f21])).
% 104.32/13.60 fof(f25,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f21])).
% 104.32/13.60 fof(f26,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f21])).
% 104.32/13.60 fof(f28,plain,(
% 104.32/13.60 select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4)|i3=i4|i3=i4),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f23])).
% 104.32/13.60 fof(f33,plain,(
% 104.32/13.60 select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4)|i3=i4),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f28])).
% 104.32/13.60 fof(f45,plain,(
% 104.32/13.60 select(store(a2,i1,select(a1,i1)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4)|i3=i4|i2=i4),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f33])).
% 104.32/13.60 fof(f46,plain,(
% 104.32/13.60 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4)|i3=i4|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f33])).
% 104.32/13.60 fof(f48,plain,(
% 104.32/13.60 select(store(a2,i1,select(a1,i1)),i4)=select(store(a1,i1,select(a2,i1)),i4)|i3=i4|i2=i4|i2=i4),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f45])).
% 104.32/13.60 fof(f51,plain,(
% 104.32/13.60 select(store(a2,i1,select(a1,i1)),i4)=select(store(a1,i1,select(a2,i1)),i4)|i3=i4|i2=i4),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f48])).
% 104.32/13.60 fof(f53,plain,(
% 104.32/13.60 select(a2,i4)=select(store(a1,i1,select(a2,i1)),i4)|i3=i4|i2=i4|i1=i4),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f51])).
% 104.32/13.60 fof(f55,plain,(
% 104.32/13.60 select(a2,i4)=select(a1,i4)|i3=i4|i2=i4|i1=i4|i1=i4),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f53])).
% 104.32/13.60 fof(f57,plain,(
% 104.32/13.60 select(a2,i4)=select(a1,i4)|i3=i4|i2=i4|i1=i4),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f55])).
% 104.32/13.60 fof(f65,plain,(
% 104.32/13.60 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f46])).
% 104.32/13.60 fof(f69,plain,(
% 104.32/13.60 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f65])).
% 104.32/13.60 fof(f75,plain,(
% 104.32/13.60 store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))=store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4))|i1=i2),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f21,f12])).
% 104.32/13.60 fof(f84,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0)|i1=i2)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f75,f7])).
% 104.32/13.60 fof(f259,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)|i2=i3|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f25])).
% 104.32/13.60 fof(f260,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f25])).
% 104.32/13.60 fof(f270,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f260])).
% 104.32/13.60 fof(f323,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f270])).
% 104.32/13.60 fof(f428,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),X0)=select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0))),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f21,f19])).
% 104.32/13.60 fof(f447,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0)|i4=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f428,f7])).
% 104.32/13.60 fof(f450,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f447])).
% 104.32/13.60 fof(f565,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i2=i3|i1=i3|i1=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f323])).
% 104.32/13.60 fof(f571,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i2=i3|i1=i3),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f565])).
% 104.32/13.60 fof(f576,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i2=i3|i1=i3|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f571])).
% 104.32/13.60 fof(f658,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f259])).
% 104.32/13.60 fof(f663,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f658])).
% 104.32/13.60 fof(f770,plain,(
% 104.32/13.60 select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f270,f663])).
% 104.32/13.60 fof(f780,plain,(
% 104.32/13.60 select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f770])).
% 104.32/13.60 fof(f993,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)|i1=i2|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f25,f24])).
% 104.32/13.60 fof(f1068,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4)|i1=i2|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f26])).
% 104.32/13.60 fof(f1085,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4)|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f1068])).
% 104.32/13.60 fof(f1457,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)|i1=i2|i2=i3|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f993])).
% 104.32/13.60 fof(f1466,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)|i1=i2|i2=i3),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f1457])).
% 104.32/13.60 fof(f1974,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0)|i1=i2|i4=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f84])).
% 104.32/13.60 fof(f1993,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0)|i1=i2)),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f1974])).
% 104.32/13.60 fof(f2150,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4)|i1=i2|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f1085])).
% 104.32/13.60 fof(f2163,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i4)|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f2150])).
% 104.32/13.60 fof(f2324,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),X0)|i1=i2|i3=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f1993])).
% 104.32/13.60 fof(f2325,plain,(
% 104.32/13.60 i4=i3|select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f5,f1993])).
% 104.32/13.60 fof(f2354,plain,(
% 104.32/13.60 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)|i1=i2),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f2325])).
% 104.32/13.60 fof(f2358,plain,(
% 104.32/13.60 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i1=i2|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f2354])).
% 104.32/13.60 fof(f2359,plain,(
% 104.32/13.60 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f2354])).
% 104.32/13.60 fof(f2404,plain,(
% 104.32/13.60 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f2359])).
% 104.32/13.60 fof(f2439,plain,(
% 104.32/13.60 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i1=i2|i2=i3|i2=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f2358])).
% 104.32/13.60 fof(f2457,plain,(
% 104.32/13.60 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i1=i2|i2=i3),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f2439])).
% 104.32/13.60 fof(f2473,plain,(
% 104.32/13.60 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(a2,i3)|i1=i2|i2=i3|i1=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f2457])).
% 104.32/13.60 fof(f2585,plain,(
% 104.32/13.60 i4=i3|select(a1,i3)=select(a2,i3)|i1=i2|i2=i3|i1=i3|i1=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f2473])).
% 104.32/13.60 fof(f2602,plain,(
% 104.32/13.60 i4=i3|select(a1,i3)=select(a2,i3)|i1=i2|i2=i3|i1=i3),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f2585])).
% 104.32/13.60 fof(f2701,plain,(
% 104.32/13.60 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f2404])).
% 104.32/13.60 fof(f2720,plain,(
% 104.32/13.60 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f2701])).
% 104.32/13.60 fof(f4408,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),X0)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),X0)|i1=i2|i3=X0|i3=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f2324])).
% 104.32/13.60 fof(f4423,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),X0)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),X0)|i1=i2|i3=X0)),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f4408])).
% 104.32/13.60 fof(f4433,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),X0)=select(store(a1,i1,select(a2,i1)),X0)|i1=i2|i3=X0|i2=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f4423])).
% 104.32/13.60 fof(f4434,plain,(
% 104.32/13.60 i4=i2|select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2)=select(store(a2,i1,select(a1,i1)),i2)|i1=i2|i3=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f5,f4423])).
% 104.32/13.60 fof(f4460,plain,(
% 104.32/13.60 i4=i2|select(a1,i2)=select(store(a2,i1,select(a1,i1)),i2)|i1=i2|i3=i2),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f4434])).
% 104.32/13.60 fof(f4463,plain,(
% 104.32/13.60 i4=i2|select(a1,i2)=select(a2,i2)|i1=i2|i3=i2|i1=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f4460])).
% 104.32/13.60 fof(f4575,plain,(
% 104.32/13.60 i4=i2|select(a1,i2)=select(a2,i2)|i1=i2|i3=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f4463])).
% 104.32/13.60 fof(f4925,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(a2,i1,select(a1,i1)),X0)=select(store(a1,i1,select(a2,i1)),X0)|i1=i2|i3=X0|i2=X0|i2=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f4433])).
% 104.32/13.60 fof(f4953,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(store(a2,i1,select(a1,i1)),X0)=select(store(a1,i1,select(a2,i1)),X0)|i1=i2|i3=X0|i2=X0)),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f4925])).
% 104.32/13.60 fof(f4958,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(a2,X0)=select(store(a1,i1,select(a2,i1)),X0)|i1=i2|i3=X0|i2=X0|i1=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f4953])).
% 104.32/13.60 fof(f4959,plain,(
% 104.32/13.60 i4=i1|select(a1,i1)=select(store(a1,i1,select(a2,i1)),i1)|i1=i2|i3=i1|i2=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f5,f4953])).
% 104.32/13.60 fof(f5105,plain,(
% 104.32/13.60 i4=i1|select(a1,i1)=select(a2,i1)|i1=i2|i3=i1|i2=i1),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f4959])).
% 104.32/13.60 fof(f5106,plain,(
% 104.32/13.60 i4=i1|select(a1,i1)=select(a2,i1)|i1=i2|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f5105])).
% 104.32/13.60 fof(f5707,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(a2,X0)=select(a1,X0)|i1=i2|i3=X0|i2=X0|i1=X0|i1=X0)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7,f4958])).
% 104.32/13.60 fof(f5851,plain,(
% 104.32/13.60 ![X0]: (i4=X0|select(a2,X0)=select(a1,X0)|i1=i2|i3=X0|i2=X0|i1=X0)),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f5707])).
% 104.32/13.60 fof(f5854,plain,(
% 104.32/13.60 i4=sk(a1,a2)|i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.60 inference(resolution,[status(thm)],[f5851,f9])).
% 104.32/13.60 fof(f6283,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,i4)|i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f5854,f9])).
% 104.32/13.60 fof(f6284,plain,(
% 104.32/13.60 i1=i2|i2=sk(a1,a2)|i1=sk(a1,a2)|~i4=i3|sk(a1,a2)=i3),
% 104.32/13.60 inference(equality_factoring,[status(thm)],[f5854])).
% 104.32/13.60 fof(f6285,plain,(
% 104.32/13.60 i1=i2|i3=sk(a1,a2)|i1=sk(a1,a2)|~i4=i2|sk(a1,a2)=i2),
% 104.32/13.60 inference(equality_factoring,[status(thm)],[f5854])).
% 104.32/13.60 fof(f6286,plain,(
% 104.32/13.60 i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|~i4=i1|sk(a1,a2)=i1),
% 104.32/13.60 inference(equality_factoring,[status(thm)],[f5854])).
% 104.32/13.60 fof(f6360,plain,(
% 104.32/13.60 ~select(a1,i4)=select(a2,i4)|i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)|i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f5854,f6283])).
% 104.32/13.60 fof(f6361,plain,(
% 104.32/13.60 ~select(a1,i4)=select(a2,i4)|i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f6360])).
% 104.32/13.60 fof(f6362,plain,(
% 104.32/13.60 i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)|i3=i4|i2=i4|i1=i4),
% 104.32/13.60 inference(resolution,[status(thm)],[f6361,f57])).
% 104.32/13.60 fof(f6366,plain,(
% 104.32/13.60 i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)|i2=i4|i1=i4),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f6362,f6284])).
% 104.32/13.60 fof(f6369,plain,(
% 104.32/13.60 i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(backward_subsumption_resolution,[status(thm)],[f6286,f6370])).
% 104.32/13.60 fof(f6370,plain,(
% 104.32/13.60 i1=i2|i3=sk(a1,a2)|i2=sk(a1,a2)|i1=sk(a1,a2)|i1=i4),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f6366,f6285])).
% 104.32/13.60 fof(f6380,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,i3)|i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6369,f9])).
% 104.32/13.60 fof(f6381,plain,(
% 104.32/13.60 i1=i2|sk(a1,a2)=i1|~i3=i2|sk(a1,a2)=i2),
% 104.32/13.60 inference(equality_factoring,[status(thm)],[f6369])).
% 104.32/13.60 fof(f6382,plain,(
% 104.32/13.60 i1=i2|i2=sk(a1,a2)|~i3=i1|sk(a1,a2)=i1),
% 104.32/13.60 inference(equality_factoring,[status(thm)],[f6369])).
% 104.32/13.60 fof(f6383,plain,(
% 104.32/13.60 ~select(a1,i3)=select(a2,i3)|i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1|i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6369,f6380])).
% 104.32/13.60 fof(f6384,plain,(
% 104.32/13.60 ~select(a1,i3)=select(a2,i3)|i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f6383])).
% 104.32/13.60 fof(f6385,plain,(
% 104.32/13.60 i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1|i4=i3|i1=i2|i2=i3|i1=i3),
% 104.32/13.60 inference(resolution,[status(thm)],[f6384,f2602])).
% 104.32/13.60 fof(f6389,plain,(
% 104.32/13.60 i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1|i4=i3|i2=i3|i1=i3),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f6385])).
% 104.32/13.60 fof(f6390,plain,(
% 104.32/13.60 i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1|i4=i3|i1=i3),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f6389,f6381])).
% 104.32/13.60 fof(f6394,plain,(
% 104.32/13.60 i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1|i4=i3),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f6390,f6382])).
% 104.32/13.60 fof(f6398,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,i2)|i1=i2|sk(a1,a2)=i1|i4=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6394,f9])).
% 104.32/13.60 fof(f6403,plain,(
% 104.32/13.60 ~select(a1,i2)=select(a2,i2)|i1=i2|sk(a1,a2)=i1|i4=i3|i1=i2|sk(a1,a2)=i1|i4=i3),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6394,f6398])).
% 104.32/13.60 fof(f6405,plain,(
% 104.32/13.60 ~select(a1,i2)=select(a2,i2)|i1=i2|sk(a1,a2)=i1|i4=i3),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f6403])).
% 104.32/13.60 fof(f6407,plain,(
% 104.32/13.60 i1=i2|sk(a1,a2)=i1|i4=i3|i4=i2|i1=i2|i3=i2),
% 104.32/13.60 inference(resolution,[status(thm)],[f6405,f4575])).
% 104.32/13.60 fof(f6411,plain,(
% 104.32/13.60 i1=i2|sk(a1,a2)=i1|i4=i3|i4=i2|i3=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f6407])).
% 104.32/13.60 fof(f6420,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,i1)|i1=i2|i4=i3|i4=i2|i3=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6411,f9])).
% 104.32/13.60 fof(f6427,plain,(
% 104.32/13.60 ~select(a1,i1)=select(a2,i1)|i1=i2|i4=i3|i4=i2|i3=i2|i1=i2|i4=i3|i4=i2|i3=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6411,f6420])).
% 104.32/13.60 fof(f6430,plain,(
% 104.32/13.60 ~select(a1,i1)=select(a2,i1)|i1=i2|i4=i3|i4=i2|i3=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f6427])).
% 104.32/13.60 fof(f6433,plain,(
% 104.32/13.60 i1=i2|i4=i3|i4=i2|i3=i2|i4=i1|i1=i2|i3=i1),
% 104.32/13.60 inference(resolution,[status(thm)],[f6430,f5106])).
% 104.32/13.60 fof(f6437,plain,(
% 104.32/13.60 i1=i2|i4=i3|i4=i2|i3=i2|i4=i1|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f6433])).
% 104.32/13.60 fof(f6620,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i3)|i2=i3|i1=i3|i1=i2|i1=i2|i4=i2|i3=i2|i4=i1|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6437,f576])).
% 104.32/13.60 fof(f7014,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i4)=select(a2,i3)|i2=i3|i1=i3|i1=i2|i1=i2|i4=i2|i3=i2|i4=i1|i3=i1),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f6620])).
% 104.32/13.60 fof(f7015,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i4)=select(a2,i3)|i2=i3|i1=i3|i1=i2|i4=i2|i4=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f7014])).
% 104.32/13.60 fof(f7854,plain,(
% 104.32/13.60 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a1,i3)),i3)=select(a2,i3)|i2=i3|i1=i3|i1=i2|i4=i2|i4=i1|i1=i2|i4=i2|i3=i2|i4=i1|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f6437,f7015])).
% 104.32/13.60 fof(f7866,plain,(
% 104.32/13.60 select(a1,i3)=select(a2,i3)|i2=i3|i1=i3|i1=i2|i4=i2|i4=i1|i1=i2|i4=i2|i3=i2|i4=i1|i3=i1),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f7854])).
% 104.32/13.60 fof(f7867,plain,(
% 104.32/13.60 select(a1,i3)=select(a2,i3)|i2=i3|i1=i3|i1=i2|i4=i2|i4=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f7866])).
% 104.32/13.60 fof(f7873,plain,(
% 104.32/13.60 i2=i3|i1=i3|i1=i2|i4=i2|i4=i1|i1=i2|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(resolution,[status(thm)],[f7867,f6384])).
% 104.32/13.60 fof(f7902,plain,(
% 104.32/13.60 i2=i3|i1=i3|i1=i2|i4=i2|i4=i1|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f7873])).
% 104.32/13.60 fof(f7903,plain,(
% 104.32/13.60 i1=i3|i1=i2|i4=i2|i4=i1|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f7902,f6381])).
% 104.32/13.60 fof(f7928,plain,(
% 104.32/13.60 i1=i2|i4=i2|i4=i1|i2=sk(a1,a2)|sk(a1,a2)=i1),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f7903,f6382])).
% 104.32/13.60 fof(f7938,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,i2)|i1=i2|i4=i2|i4=i1|sk(a1,a2)=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7928,f9])).
% 104.32/13.60 fof(f7947,plain,(
% 104.32/13.60 ~select(a1,i2)=select(a2,i2)|i1=i2|i4=i2|i4=i1|sk(a1,a2)=i1|i1=i2|i4=i2|i4=i1|sk(a1,a2)=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7928,f7938])).
% 104.32/13.60 fof(f7951,plain,(
% 104.32/13.60 ~select(a1,i2)=select(a2,i2)|i1=i2|i4=i2|i4=i1|sk(a1,a2)=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f7947])).
% 104.32/13.60 fof(f7955,plain,(
% 104.32/13.60 i1=i2|i4=i2|i4=i1|sk(a1,a2)=i1|i4=i2|i1=i2|i3=i2),
% 104.32/13.60 inference(resolution,[status(thm)],[f7951,f4575])).
% 104.32/13.60 fof(f7959,plain,(
% 104.32/13.60 i1=i2|i4=i2|i4=i1|sk(a1,a2)=i1|i3=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f7955])).
% 104.32/13.60 fof(f8011,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,i1)|i1=i2|i4=i2|i4=i1|i3=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7959,f9])).
% 104.32/13.60 fof(f8022,plain,(
% 104.32/13.60 ~select(a1,i1)=select(a2,i1)|i1=i2|i4=i2|i4=i1|i3=i2|i1=i2|i4=i2|i4=i1|i3=i2),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f7959,f8011])).
% 104.32/13.60 fof(f8027,plain,(
% 104.32/13.60 ~select(a1,i1)=select(a2,i1)|i1=i2|i4=i2|i4=i1|i3=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f8022])).
% 104.32/13.60 fof(f8032,plain,(
% 104.32/13.60 i1=i2|i4=i2|i4=i1|i3=i2|i4=i1|i1=i2|i3=i1),
% 104.32/13.60 inference(resolution,[status(thm)],[f8027,f5106])).
% 104.32/13.60 fof(f8036,plain,(
% 104.32/13.60 i1=i2|i4=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f8032])).
% 104.32/13.60 fof(f8270,plain,(
% 104.32/13.60 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2)=select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f8036,f69])).
% 104.32/13.60 fof(f8519,plain,(
% 104.32/13.60 select(a1,i2)=select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f8270])).
% 104.32/13.60 fof(f8520,plain,(
% 104.32/13.60 select(a1,i2)=select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f8519])).
% 104.32/13.60 fof(f8542,plain,(
% 104.32/13.60 select(a1,i2)=select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2)|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f8036,f8520])).
% 104.32/13.60 fof(f8549,plain,(
% 104.32/13.60 select(a1,i2)=select(a2,i2)|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f8542])).
% 104.32/13.60 fof(f8550,plain,(
% 104.32/13.60 select(a1,i2)=select(a2,i2)|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f8549])).
% 104.32/13.60 fof(f8553,plain,(
% 104.32/13.60 i3=i4|i1=i2|i4=i1|i3=i2|i3=i1|i1=i2|sk(a1,a2)=i1|i4=i3),
% 104.32/13.60 inference(resolution,[status(thm)],[f8550,f6405])).
% 104.32/13.60 fof(f8638,plain,(
% 104.32/13.60 i3=i4|i1=i2|i4=i1|i3=i2|i3=i1|sk(a1,a2)=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f8553])).
% 104.32/13.60 fof(f8735,plain,(
% 104.32/13.60 ~select(a1,sk(a1,a2))=select(a2,i1)|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f8638,f9])).
% 104.32/13.60 fof(f8747,plain,(
% 104.32/13.60 ~select(a1,i1)=select(a2,i1)|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f8638,f8735])).
% 104.32/13.60 fof(f8753,plain,(
% 104.32/13.60 ~select(a1,i1)=select(a2,i1)|i3=i4|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f8747])).
% 104.32/13.60 fof(f8754,plain,(
% 104.32/13.60 i3=i4|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f8753,f5106])).
% 104.32/13.60 fof(f8760,plain,(
% 104.32/13.60 i3=i2|i1=i2|i4=i1|i3=i2|i3=i1|i1=i2|i4=i1|i3=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f8036,f8754])).
% 104.32/13.60 fof(f9011,plain,(
% 104.32/13.60 i3=i2|i1=i2|i4=i1|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f8760])).
% 104.32/13.60 fof(f9686,plain,(
% 104.32/13.60 select(store(a2,i1,select(a1,i1)),i1)=select(store(a1,i1,select(a2,i1)),i4)|i3=i4|i2=i4|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f9011,f51])).
% 104.32/13.60 fof(f9930,plain,(
% 104.32/13.60 select(a1,i1)=select(store(a1,i1,select(a2,i1)),i4)|i3=i4|i2=i4|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f9686])).
% 104.32/13.60 fof(f9937,plain,(
% 104.32/13.60 select(a1,i1)=select(store(a1,i1,select(a2,i1)),i1)|i3=i4|i2=i4|i3=i2|i1=i2|i3=i1|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f9011,f9930])).
% 104.32/13.60 fof(f9944,plain,(
% 104.32/13.60 select(a1,i1)=select(a2,i1)|i3=i4|i2=i4|i3=i2|i1=i2|i3=i1|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(forward_demodulation,[status(thm)],[f5,f9937])).
% 104.32/13.60 fof(f9945,plain,(
% 104.32/13.60 select(a1,i1)=select(a2,i1)|i3=i4|i2=i4|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f9944])).
% 104.32/13.60 fof(f9946,plain,(
% 104.32/13.60 i3=i4|i2=i4|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(forward_subsumption_resolution,[status(thm)],[f9945,f6430])).
% 104.32/13.60 fof(f9948,plain,(
% 104.32/13.60 i3=i1|i2=i4|i3=i2|i1=i2|i3=i1|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f9011,f9946])).
% 104.32/13.60 fof(f10199,plain,(
% 104.32/13.60 i3=i1|i2=i4|i3=i2|i1=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f9948])).
% 104.32/13.60 fof(f10635,plain,(
% 104.32/13.60 i3=i1|i2=i1|i3=i2|i1=i2|i3=i2|i1=i2|i3=i1),
% 104.32/13.60 inference(paramodulation,[status(thm)],[f9011,f10199])).
% 104.32/13.60 fof(f10885,plain,(
% 104.32/13.60 i3=i1|i2=i1|i3=i2),
% 104.32/13.60 inference(duplicate_literals_removal,[status(thm)],[f10635])).
% 104.32/13.60 fof(f11132,plain,(
% 104.32/13.60 i3=i1|i2=i1|i1=i2|sk(a1,a2)=i1|sk(a1,a2)=i2),
% 104.32/13.60 inference(resolution,[status(thm)],[f10885,f6381])).
% 104.32/13.60 fof(f11247,plain,(
% 104.32/13.60 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2)|i1=i2|i3=i1|i2=i1),
% 104.32/13.61 inference(paramodulation,[status(thm)],[f10885,f2720])).
% 104.32/13.61 fof(f11489,plain,(
% 104.32/13.61 i3=i1|i2=i1|sk(a1,a2)=i1|sk(a1,a2)=i2),
% 104.32/13.61 inference(duplicate_literals_removal,[status(thm)],[f11132])).
% 104.32/13.61 fof(f11490,plain,(
% 104.32/13.61 i2=i1|sk(a1,a2)=i1|sk(a1,a2)=i2),
% 104.32/13.61 inference(forward_subsumption_resolution,[status(thm)],[f11489,f6382])).
% 104.32/13.61 fof(f11634,plain,(
% 104.32/13.61 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(a1,i2)|i1=i2|i3=i1|i2=i1),
% 104.32/13.61 inference(forward_demodulation,[status(thm)],[f5,f11247])).
% 104.32/13.61 fof(f11635,plain,(
% 104.32/13.61 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(a1,i2)|i1=i2|i3=i1),
% 104.32/13.61 inference(duplicate_literals_removal,[status(thm)],[f11634])).
% 104.32/13.61 fof(f11936,plain,(
% 104.32/13.61 ~select(a1,sk(a1,a2))=select(a2,i2)|i2=i1|sk(a1,a2)=i1),
% 104.32/13.61 inference(paramodulation,[status(thm)],[f11490,f9])).
% 104.32/13.61 fof(f11946,plain,(
% 104.32/13.61 ~select(a1,i2)=select(a2,i2)|i2=i1|sk(a1,a2)=i1|i2=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f11490,f11936])).
% 104.32/13.63 fof(f11949,plain,(
% 104.32/13.63 ~select(a1,i2)=select(a2,i2)|i2=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f11946])).
% 104.32/13.63 fof(f11952,plain,(
% 104.32/13.63 i2=i1|sk(a1,a2)=i1|i4=i2|i1=i2|i3=i2),
% 104.32/13.63 inference(resolution,[status(thm)],[f11949,f4575])).
% 104.32/13.63 fof(f11956,plain,(
% 104.32/13.63 i2=i1|sk(a1,a2)=i1|i4=i2|i3=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f11952])).
% 104.32/13.63 fof(f11964,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i1)|i2=i1|i4=i2|i3=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f11956,f9])).
% 104.32/13.63 fof(f11970,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i2=i1|i4=i2|i3=i2|i2=i1|i4=i2|i3=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f11956,f11964])).
% 104.32/13.63 fof(f11972,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i2=i1|i4=i2|i3=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f11970])).
% 104.32/13.63 fof(f11988,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2)=select(a1,i2)|i1=i2|i3=i1|i3=i1|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f10885,f11635])).
% 104.32/13.63 fof(f12019,plain,(
% 104.32/13.63 i4=i3|select(a2,i2)=select(a1,i2)|i1=i2|i3=i1|i3=i1|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f11988])).
% 104.32/13.63 fof(f12020,plain,(
% 104.32/13.63 i4=i3|select(a2,i2)=select(a1,i2)|i1=i2|i3=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f12019])).
% 104.32/13.63 fof(f12233,plain,(
% 104.32/13.63 i4=i3|i1=i2|i3=i1|i2=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(resolution,[status(thm)],[f12020,f11949])).
% 104.32/13.63 fof(f12297,plain,(
% 104.32/13.63 i4=i3|i1=i2|i3=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f12233])).
% 104.32/13.63 fof(f12364,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i1)|i4=i3|i1=i2|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f12297,f9])).
% 104.32/13.63 fof(f12369,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i4=i3|i1=i2|i3=i1|i4=i3|i1=i2|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f12297,f12364])).
% 104.32/13.63 fof(f12372,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i4=i3|i1=i2|i3=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f12369])).
% 104.32/13.63 fof(f12375,plain,(
% 104.32/13.63 i4=i3|i1=i2|i3=i1|i4=i1|i1=i2|i3=i1),
% 104.32/13.63 inference(resolution,[status(thm)],[f12372,f5106])).
% 104.32/13.63 fof(f12379,plain,(
% 104.32/13.63 i4=i3|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f12375])).
% 104.32/13.63 fof(f12454,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)),i3)|i1=i2|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f12379,f2163])).
% 104.32/13.63 fof(f12679,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f12454])).
% 104.32/13.63 fof(f12680,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i4)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f12679])).
% 104.32/13.63 fof(f19891,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2|i3=i1|i4=i1|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f12379,f12680])).
% 104.32/13.63 fof(f19918,plain,(
% 104.32/13.63 select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2|i3=i1|i4=i1|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f19891])).
% 104.32/13.63 fof(f19919,plain,(
% 104.32/13.63 select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3)|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f19918])).
% 104.32/13.63 fof(f19940,plain,(
% 104.32/13.63 select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2)|i1=i2|i3=i1|i4=i1|i3=i1|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f10885,f19919])).
% 104.32/13.63 fof(f19985,plain,(
% 104.32/13.63 select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(a1,i2)|i1=i2|i3=i1|i4=i1|i3=i1|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f19940])).
% 104.32/13.63 fof(f19986,plain,(
% 104.32/13.63 select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(a1,i2)|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f19985])).
% 104.32/13.63 fof(f20035,plain,(
% 104.32/13.63 select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i2)=select(a1,i2)|i1=i2|i3=i1|i4=i1|i3=i1|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f10885,f19986])).
% 104.32/13.63 fof(f20087,plain,(
% 104.32/13.63 select(a2,i2)=select(a1,i2)|i1=i2|i3=i1|i4=i1|i3=i1|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f20035])).
% 104.32/13.63 fof(f20088,plain,(
% 104.32/13.63 select(a2,i2)=select(a1,i2)|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f20087])).
% 104.32/13.63 fof(f20124,plain,(
% 104.32/13.63 i1=i2|i3=i1|i4=i1|i2=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(resolution,[status(thm)],[f20088,f11949])).
% 104.32/13.63 fof(f20281,plain,(
% 104.32/13.63 i1=i2|i3=i1|i4=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f20124])).
% 104.32/13.63 fof(f20434,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i1)|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f20281,f9])).
% 104.32/13.63 fof(f20440,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i1=i2|i3=i1|i4=i1|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f20281,f20434])).
% 104.32/13.63 fof(f20444,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f20440])).
% 104.32/13.63 fof(f20445,plain,(
% 104.32/13.63 i1=i2|i3=i1|i4=i1),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f20444,f5106])).
% 104.32/13.63 fof(f20776,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i1)=select(store(a1,i1,select(a2,i1)),i4)|i3=i4|i2=i4|i1=i2|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f20445,f51])).
% 104.32/13.63 fof(f21068,plain,(
% 104.32/13.63 select(a1,i1)=select(store(a1,i1,select(a2,i1)),i4)|i3=i4|i2=i4|i1=i2|i3=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f20776])).
% 104.32/13.63 fof(f21073,plain,(
% 104.32/13.63 select(a1,i1)=select(store(a1,i1,select(a2,i1)),i1)|i3=i4|i2=i4|i1=i2|i3=i1|i1=i2|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f20445,f21068])).
% 104.32/13.63 fof(f21078,plain,(
% 104.32/13.63 select(a1,i1)=select(a2,i1)|i3=i4|i2=i4|i1=i2|i3=i1|i1=i2|i3=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f21073])).
% 104.32/13.63 fof(f21079,plain,(
% 104.32/13.63 select(a1,i1)=select(a2,i1)|i3=i4|i2=i4|i1=i2|i3=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f21078])).
% 104.32/13.63 fof(f21080,plain,(
% 104.32/13.63 i3=i4|i2=i4|i1=i2|i3=i1),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f21079,f12372])).
% 104.32/13.63 fof(f21082,plain,(
% 104.32/13.63 i3=i1|i2=i4|i1=i2|i3=i1|i1=i2|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f20445,f21080])).
% 104.32/13.63 fof(f21416,plain,(
% 104.32/13.63 i3=i1|i2=i4|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f21082])).
% 104.32/13.63 fof(f21906,plain,(
% 104.32/13.63 i3=i1|i2=i1|i1=i2|i1=i2|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f20445,f21416])).
% 104.32/13.63 fof(f22239,plain,(
% 104.32/13.63 i3=i1|i2=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f21906])).
% 104.32/13.63 fof(f22824,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1)|i1=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f2720])).
% 104.32/13.63 fof(f22844,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(store(a2,i1,select(a1,i1)),i1)|i1=i2|i2=i3|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f2457])).
% 104.32/13.63 fof(f23297,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1)|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f22824])).
% 104.32/13.63 fof(f23311,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(a1,i1)|i1=i2|i2=i3|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f22844])).
% 104.32/13.63 fof(f23312,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(a1,i1)|i1=i2|i2=i3),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f23311])).
% 104.32/13.63 fof(f23578,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i1)=select(a1,i1)|i1=i2|i2=i3|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f23312])).
% 104.32/13.63 fof(f23607,plain,(
% 104.32/13.63 i4=i3|select(a2,i1)=select(a1,i1)|i1=i2|i2=i3|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f23578])).
% 104.32/13.63 fof(f23608,plain,(
% 104.32/13.63 i4=i3|select(a2,i1)=select(a1,i1)|i1=i2|i2=i3),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f23607])).
% 104.32/13.63 fof(f23635,plain,(
% 104.32/13.63 i4=i3|i1=i2|i2=i3|i2=i1|i4=i2|i3=i2),
% 104.32/13.63 inference(resolution,[status(thm)],[f23608,f11972])).
% 104.32/13.63 fof(f24056,plain,(
% 104.32/13.63 i4=i3|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f23635])).
% 104.32/13.63 fof(f24629,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i3)|i1=i2|i2=i3|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f24056,f1466])).
% 104.32/13.63 fof(f24659,plain,(
% 104.32/13.63 select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f24056,f780])).
% 104.32/13.63 fof(f24660,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f24056,f663])).
% 104.32/13.63 fof(f24975,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f24629])).
% 104.32/13.63 fof(f24976,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i3)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f24975])).
% 104.32/13.63 fof(f25031,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f24659])).
% 104.32/13.63 fof(f25032,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f25031])).
% 104.32/13.63 fof(f25033,plain,(
% 104.32/13.63 select(store(a1,i1,select(a2,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f24660])).
% 104.32/13.63 fof(f25034,plain,(
% 104.32/13.63 select(store(a1,i1,select(a2,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i3)),i4)|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f25033])).
% 104.32/13.63 fof(f25979,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(store(a2,i1,select(a1,i1)),i1)|i1=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f23297])).
% 104.32/13.63 fof(f25990,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(a1,i1)|i1=i2|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f25979])).
% 104.32/13.63 fof(f25991,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3)=select(a1,i1)|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f25990])).
% 104.32/13.63 fof(f26007,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1)=select(a1,i1)|i1=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f25991])).
% 104.32/13.63 fof(f26040,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i1)=select(a1,i1)|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f26007])).
% 104.32/13.63 fof(f26070,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i1)=select(a1,i1)|i1=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f26040])).
% 104.32/13.63 fof(f26081,plain,(
% 104.32/13.63 i4=i3|select(a2,i1)=select(a1,i1)|i1=i2|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f26070])).
% 104.32/13.63 fof(f26082,plain,(
% 104.32/13.63 i4=i3|select(a2,i1)=select(a1,i1)|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f26081])).
% 104.32/13.63 fof(f26509,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4)|i3=i4|i1=i2|i4=i3|i1=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f26082,f46])).
% 104.32/13.63 fof(f26899,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(store(a1,i1,select(a1,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i4)|i3=i4|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f26509])).
% 104.32/13.63 fof(f29343,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i1=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f26899])).
% 104.32/13.63 fof(f29351,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f29343])).
% 104.32/13.63 fof(f30093,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(store(a1,i1,select(a2,i1)),i1)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f24976])).
% 104.32/13.63 fof(f30112,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a2,i1)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f30093])).
% 104.32/13.63 fof(f30113,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a2,i1)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30112])).
% 104.32/13.63 fof(f30121,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f30113])).
% 104.32/13.63 fof(f30124,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i3,select(a2,i1)),i3)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f24056,f30113])).
% 104.32/13.63 fof(f30128,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i1,select(a2,i1)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30121])).
% 104.32/13.63 fof(f30130,plain,(
% 104.32/13.63 select(a2,i1)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f30124])).
% 104.32/13.63 fof(f30131,plain,(
% 104.32/13.63 select(a2,i1)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30130])).
% 104.32/13.63 fof(f30204,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f30128])).
% 104.32/13.63 fof(f30221,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4|i2=i4),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f30204])).
% 104.32/13.63 fof(f30235,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i4)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30221])).
% 104.32/13.63 fof(f30247,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f24056,f30235])).
% 104.32/13.63 fof(f30256,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30247])).
% 104.32/13.63 fof(f30492,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i1)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f30256])).
% 104.32/13.63 fof(f30530,plain,(
% 104.32/13.63 select(a1,i1)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f30492])).
% 104.32/13.63 fof(f30531,plain,(
% 104.32/13.63 select(a1,i1)=select(store(a1,i1,select(a2,i1)),i3)|i1=i2|i2=i3|i4=i2|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30530])).
% 104.32/13.63 fof(f30561,plain,(
% 104.32/13.63 select(a1,i1)=select(a2,i1)|i1=i2|i2=i3|i4=i2|i1=i4|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f30131,f30531])).
% 104.32/13.63 fof(f30605,plain,(
% 104.32/13.63 select(a1,i1)=select(a2,i1)|i1=i2|i2=i3|i4=i2|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30561])).
% 104.32/13.63 fof(f30606,plain,(
% 104.32/13.63 i1=i2|i2=i3|i4=i2|i1=i4),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f30605,f11972])).
% 104.32/13.63 fof(f30661,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i2,select(a1,i2)),i2)=select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f30606,f29351])).
% 104.32/13.63 fof(f30969,plain,(
% 104.32/13.63 select(a1,i2)=select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f30661])).
% 104.32/13.63 fof(f30970,plain,(
% 104.32/13.63 select(a1,i2)=select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i4)|i3=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f30969])).
% 104.32/13.63 fof(f31271,plain,(
% 104.32/13.63 select(a1,i2)=select(store(store(a1,i1,select(a1,i1)),i2,select(a2,i2)),i2)|i3=i4|i1=i2|i2=i3|i1=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f30606,f30970])).
% 104.32/13.63 fof(f31280,plain,(
% 104.32/13.63 select(a1,i2)=select(a2,i2)|i3=i4|i1=i2|i2=i3|i1=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f31271])).
% 104.32/13.63 fof(f31281,plain,(
% 104.32/13.63 select(a1,i2)=select(a2,i2)|i3=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f31280])).
% 104.32/13.63 fof(f31285,plain,(
% 104.32/13.63 i3=i4|i1=i2|i2=i3|i1=i4|i2=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(resolution,[status(thm)],[f31281,f11949])).
% 104.32/13.63 fof(f31402,plain,(
% 104.32/13.63 i3=i4|i1=i2|i2=i3|i1=i4|sk(a1,a2)=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f31285])).
% 104.32/13.63 fof(f31521,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i1)|i3=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f31402,f9])).
% 104.32/13.63 fof(f31526,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i3=i4|i1=i2|i2=i3|i1=i4|i3=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f31402,f31521])).
% 104.32/13.63 fof(f31529,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i3=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f31526])).
% 104.32/13.63 fof(f31530,plain,(
% 104.32/13.63 i3=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f31529,f26082])).
% 104.32/13.63 fof(f31533,plain,(
% 104.32/13.63 i3=i2|i1=i2|i2=i3|i1=i4|i1=i2|i2=i3|i1=i4),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f30606,f31530])).
% 104.32/13.63 fof(f31843,plain,(
% 104.32/13.63 i3=i2|i1=i2|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f31533])).
% 104.32/13.63 fof(f34529,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(store(a2,i1,select(a1,i1)),i1)),i4)|i2=i3|i1=i2|i4=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f25032])).
% 104.32/13.63 fof(f34548,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(a1,i1)),i4)|i2=i3|i1=i2|i4=i2|i2=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f34529])).
% 104.32/13.63 fof(f34549,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(a1,i1)),i4)|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f34548])).
% 104.32/13.63 fof(f34563,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(a2,i2)),i3,select(a1,i1)),i3)|i2=i3|i1=i2|i4=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f24056,f34549])).
% 104.32/13.63 fof(f34571,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(a1,i1)|i2=i3|i1=i2|i4=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f34563])).
% 104.32/13.63 fof(f34572,plain,(
% 104.32/13.63 select(store(a2,i1,select(a1,i1)),i3)=select(a1,i1)|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f34571])).
% 104.32/13.63 fof(f34732,plain,(
% 104.32/13.63 select(store(a1,i1,select(a2,i1)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i2=i3|i1=i2|i4=i2|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f25032,f25034])).
% 104.32/13.63 fof(f34760,plain,(
% 104.32/13.63 select(store(a1,i1,select(a2,i1)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f34732])).
% 104.32/13.63 fof(f34783,plain,(
% 104.32/13.63 select(store(a1,i1,select(a2,i1)),i3)=select(a1,i1)|i2=i3|i1=i2|i4=i2|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f34572,f34760])).
% 104.32/13.63 fof(f34831,plain,(
% 104.32/13.63 select(store(a1,i1,select(a2,i1)),i3)=select(a1,i1)|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f34783])).
% 104.32/13.63 fof(f34870,plain,(
% 104.32/13.63 select(a2,i1)=select(a1,i1)|i2=i3|i1=i2|i4=i2|i1=i2|i2=i3|i4=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f30131,f34831])).
% 104.32/13.63 fof(f34913,plain,(
% 104.32/13.63 select(a2,i1)=select(a1,i1)|i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f34870])).
% 104.32/13.63 fof(f34914,plain,(
% 104.32/13.63 i2=i3|i1=i2|i4=i2),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f34913,f11972])).
% 104.32/13.63 fof(f34951,plain,(
% 104.32/13.63 i2=i3|i1=i2|i1=i2|i3=i2|i1=i2),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f31843,f34914])).
% 104.32/13.63 fof(f35290,plain,(
% 104.32/13.63 i2=i3|i1=i2),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f34951])).
% 104.32/13.63 fof(f35650,plain,(
% 104.32/13.63 i2=i1|i1=i2|i2=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f22239,f35290])).
% 104.32/13.63 fof(f36051,plain,(
% 104.32/13.63 i2=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f35650])).
% 104.32/13.63 fof(f36693,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i1=i3|i1=i3),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f36051,f571])).
% 104.32/13.63 fof(f36718,plain,(
% 104.32/13.63 select(a2,i4)=select(a1,i4)|i3=i4|i1=i4|i1=i4),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f36051,f57])).
% 104.32/13.63 fof(f36722,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i1)),i4)|i3=i4),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f36051,f33])).
% 104.32/13.63 fof(f36725,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f36051,f21])).
% 104.32/13.63 fof(f37076,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i2)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i1=i3|i1=i3),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f36693])).
% 104.32/13.63 fof(f37077,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i1=i3|i1=i3),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37076])).
% 104.32/13.63 fof(f37078,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i1=i3|i1=i3),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37077])).
% 104.32/13.63 fof(f37079,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i2)),i3,select(a2,i3)),i4)|i1=i3|i1=i3),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37078])).
% 104.32/13.63 fof(f37080,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(a2,i3)),i4)|i1=i3|i1=i3),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37079])).
% 104.32/13.63 fof(f37081,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i4)|i1=i3|i1=i3),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37080])).
% 104.32/13.63 fof(f37082,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i4)|i1=i3),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f37081])).
% 104.32/13.63 fof(f37212,plain,(
% 104.32/13.63 select(a2,i4)=select(a1,i4)|i3=i4|i1=i4),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f36718])).
% 104.32/13.63 fof(f37217,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i2)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i1)),i4)|i3=i4),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f36722])).
% 104.32/13.63 fof(f37218,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i1)),i4)|i3=i4),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37217])).
% 104.32/13.63 fof(f37219,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i4)=select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i1)),i4)|i3=i4),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37218])).
% 104.32/13.63 fof(f37220,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i4)=select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i4)|i3=i4),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37219])).
% 104.32/13.63 fof(f37221,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i4)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i4)|i3=i4),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37220])).
% 104.32/13.63 fof(f37253,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f36725])).
% 104.32/13.63 fof(f37254,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37253])).
% 104.32/13.63 fof(f37255,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37254])).
% 104.32/13.63 fof(f37256,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37255])).
% 104.32/13.63 fof(f37257,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37256])).
% 104.32/13.63 fof(f37258,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37257])).
% 104.32/13.63 fof(f37259,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37258])).
% 104.32/13.63 fof(f37260,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37259])).
% 104.32/13.63 fof(f37261,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37260])).
% 104.32/13.63 fof(f37262,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37261])).
% 104.32/13.63 fof(f37263,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37262])).
% 104.32/13.63 fof(f37542,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f450])).
% 104.32/13.63 fof(f37543,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37542])).
% 104.32/13.63 fof(f37544,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37543])).
% 104.32/13.63 fof(f37545,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i2)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37544])).
% 104.32/13.63 fof(f37546,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37545])).
% 104.32/13.63 fof(f37547,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37546])).
% 104.32/13.63 fof(f37548,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37547])).
% 104.32/13.63 fof(f37549,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(store(a2,i1,select(a1,i1)),i1)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37548])).
% 104.32/13.63 fof(f37550,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37549])).
% 104.32/13.63 fof(f37551,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i2)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37550])).
% 104.32/13.63 fof(f37552,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(store(a1,i1,select(a2,i1)),i1)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f36051,f37551])).
% 104.32/13.63 fof(f37553,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),X0))),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37552])).
% 104.32/13.63 fof(f37555,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),X0)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),X0)|i3=X0)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f37553])).
% 104.32/13.63 fof(f37556,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),i3)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f5,f37553])).
% 104.32/13.63 fof(f37561,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)=select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f37556])).
% 104.32/13.63 fof(f37574,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i1=i3),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f37561])).
% 104.32/13.63 fof(f37591,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i1=i3|i1=i3),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f37574])).
% 104.32/13.63 fof(f37596,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(store(a2,i1,select(a1,i1)),i3)|i1=i3),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f37591])).
% 104.32/13.63 fof(f37598,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(a2,i3)|i1=i3|i1=i3),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f37596])).
% 104.32/13.63 fof(f37602,plain,(
% 104.32/13.63 i4=i3|select(store(a1,i1,select(a2,i1)),i3)=select(a2,i3)|i1=i3),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f37598])).
% 104.32/13.63 fof(f37606,plain,(
% 104.32/13.63 i4=i3|select(a1,i3)=select(a2,i3)|i1=i3|i1=i3),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f37602])).
% 104.32/13.63 fof(f37608,plain,(
% 104.32/13.63 i4=i3|select(a1,i3)=select(a2,i3)|i1=i3),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f37606])).
% 104.32/13.63 fof(f39489,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),X0)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),X0)|i3=X0|i3=X0)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f37555])).
% 104.32/13.63 fof(f39510,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),X0)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),X0)|i3=X0)),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f39489])).
% 104.32/13.63 fof(f39514,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(a2,i1,select(a1,i1)),X0)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),X0)|i3=X0|i1=X0)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f39510])).
% 104.32/13.63 fof(f39515,plain,(
% 104.32/13.63 i4=i1|select(a2,i1)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1)|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f5,f39510])).
% 104.32/13.63 fof(f39544,plain,(
% 104.32/13.63 i4=i1|select(a2,i1)=select(a1,i1)|i3=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f39515])).
% 104.32/13.63 fof(f39748,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(a2,i1,select(a1,i1)),X0)=select(store(a1,i1,select(a2,i1)),X0)|i3=X0|i1=X0|i1=X0)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f39514])).
% 104.32/13.63 fof(f39769,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(store(a2,i1,select(a1,i1)),X0)=select(store(a1,i1,select(a2,i1)),X0)|i3=X0|i1=X0)),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f39748])).
% 104.32/13.63 fof(f39845,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(a2,X0)=select(store(a1,i1,select(a2,i1)),X0)|i3=X0|i1=X0|i1=X0)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f39769])).
% 104.32/13.63 fof(f39864,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(a2,X0)=select(store(a1,i1,select(a2,i1)),X0)|i3=X0|i1=X0)),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f39845])).
% 104.32/13.63 fof(f39868,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(a2,X0)=select(a1,X0)|i3=X0|i1=X0|i1=X0)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f7,f39864])).
% 104.32/13.63 fof(f39882,plain,(
% 104.32/13.63 ![X0]: (i4=X0|select(a2,X0)=select(a1,X0)|i3=X0|i1=X0)),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f39868])).
% 104.32/13.63 fof(f39884,plain,(
% 104.32/13.63 i4=sk(a1,a2)|i3=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.63 inference(resolution,[status(thm)],[f39882,f9])).
% 104.32/13.63 fof(f40013,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i4)|i3=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f39884,f9])).
% 104.32/13.63 fof(f40014,plain,(
% 104.32/13.63 i1=sk(a1,a2)|~i4=i3|sk(a1,a2)=i3),
% 104.32/13.63 inference(equality_factoring,[status(thm)],[f39884])).
% 104.32/13.63 fof(f40015,plain,(
% 104.32/13.63 i3=sk(a1,a2)|~i4=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(equality_factoring,[status(thm)],[f39884])).
% 104.32/13.63 fof(f40033,plain,(
% 104.32/13.63 ~select(a1,i4)=select(a2,i4)|i3=sk(a1,a2)|i1=sk(a1,a2)|i3=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f39884,f40013])).
% 104.32/13.63 fof(f40034,plain,(
% 104.32/13.63 ~select(a1,i4)=select(a2,i4)|i3=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40033])).
% 104.32/13.63 fof(f40035,plain,(
% 104.32/13.63 i3=sk(a1,a2)|i1=sk(a1,a2)|i3=i4|i1=i4),
% 104.32/13.63 inference(resolution,[status(thm)],[f40034,f37212])).
% 104.32/13.63 fof(f40039,plain,(
% 104.32/13.63 i3=sk(a1,a2)|i1=sk(a1,a2)|i1=i4),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f40035,f40014])).
% 104.32/13.63 fof(f40042,plain,(
% 104.32/13.63 i3=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f40039,f40015])).
% 104.32/13.63 fof(f40043,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i3)|i1=sk(a1,a2)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40042,f9])).
% 104.32/13.63 fof(f40044,plain,(
% 104.32/13.63 ~i3=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(equality_factoring,[status(thm)],[f40042])).
% 104.32/13.63 fof(f40045,plain,(
% 104.32/13.63 ~select(a1,i3)=select(a2,i3)|i1=sk(a1,a2)|i1=sk(a1,a2)),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40042,f40043])).
% 104.32/13.63 fof(f40046,plain,(
% 104.32/13.63 ~select(a1,i3)=select(a2,i3)|i1=sk(a1,a2)),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40045])).
% 104.32/13.63 fof(f40047,plain,(
% 104.32/13.63 i1=sk(a1,a2)|i4=i3|i1=i3),
% 104.32/13.63 inference(resolution,[status(thm)],[f40046,f37608])).
% 104.32/13.63 fof(f40051,plain,(
% 104.32/13.63 i1=sk(a1,a2)|i4=i3),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f40047,f40044])).
% 104.32/13.63 fof(f40057,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i1)|i4=i3),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40051,f9])).
% 104.32/13.63 fof(f40085,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i4=i3|i4=i3),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40051,f40057])).
% 104.32/13.63 fof(f40087,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i4=i3),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40085])).
% 104.32/13.63 fof(f40088,plain,(
% 104.32/13.63 i4=i3|i4=i1|i3=i1),
% 104.32/13.63 inference(resolution,[status(thm)],[f40087,f39544])).
% 104.32/13.63 fof(f40122,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(a1,i3)),i3)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i4)|i1=i3|i4=i1|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40088,f37082])).
% 104.32/13.63 fof(f40207,plain,(
% 104.32/13.63 select(a1,i3)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i4)|i1=i3|i4=i1|i3=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40122])).
% 104.32/13.63 fof(f40208,plain,(
% 104.32/13.63 select(a1,i3)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i4)|i1=i3|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40207])).
% 104.32/13.63 fof(f40268,plain,(
% 104.32/13.63 select(a1,i3)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(a2,i3)),i3)|i1=i3|i4=i1|i4=i1|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40088,f40208])).
% 104.32/13.63 fof(f40274,plain,(
% 104.32/13.63 select(a1,i3)=select(a2,i3)|i1=i3|i4=i1|i4=i1|i3=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40268])).
% 104.32/13.63 fof(f40275,plain,(
% 104.32/13.63 select(a1,i3)=select(a2,i3)|i1=i3|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40274])).
% 104.32/13.63 fof(f40277,plain,(
% 104.32/13.63 i1=i3|i4=i1|i1=sk(a1,a2)),
% 104.32/13.63 inference(resolution,[status(thm)],[f40275,f40046])).
% 104.32/13.63 fof(f40286,plain,(
% 104.32/13.63 i4=i1|i1=sk(a1,a2)),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f40277,f40044])).
% 104.32/13.63 fof(f40298,plain,(
% 104.32/13.63 ~select(a1,sk(a1,a2))=select(a2,i1)|i4=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40286,f9])).
% 104.32/13.63 fof(f40299,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i4=i1|i4=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40286,f40298])).
% 104.32/13.63 fof(f40302,plain,(
% 104.32/13.63 ~select(a1,i1)=select(a2,i1)|i4=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40299])).
% 104.32/13.63 fof(f40303,plain,(
% 104.32/13.63 i4=i1|i3=i1),
% 104.32/13.63 inference(backward_subsumption_resolution,[status(thm)],[f39544,f40302])).
% 104.32/13.63 fof(f40361,plain,(
% 104.32/13.63 select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i4)|i3=i4|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40303,f37221])).
% 104.32/13.63 fof(f40426,plain,(
% 104.32/13.63 select(a2,i1)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i4)|i3=i4|i3=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40361])).
% 104.32/13.63 fof(f40438,plain,(
% 104.32/13.63 select(a2,i1)=select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1)|i3=i4|i3=i1|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40303,f40426])).
% 104.32/13.63 fof(f40446,plain,(
% 104.32/13.63 select(a2,i1)=select(a1,i1)|i3=i4|i3=i1|i3=i1),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40438])).
% 104.32/13.63 fof(f40447,plain,(
% 104.32/13.63 select(a2,i1)=select(a1,i1)|i3=i4|i3=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40446])).
% 104.32/13.63 fof(f40448,plain,(
% 104.32/13.63 i3=i4|i3=i1),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f40447,f40087])).
% 104.32/13.63 fof(f40453,plain,(
% 104.32/13.63 i3=i1|i3=i1|i3=i1),
% 104.32/13.63 inference(paramodulation,[status(thm)],[f40303,f40448])).
% 104.32/13.63 fof(f40507,plain,(
% 104.32/13.63 i3=i1),
% 104.32/13.63 inference(duplicate_literals_removal,[status(thm)],[f40453])).
% 104.32/13.63 fof(f40572,plain,(
% 104.32/13.63 ~i1=i1|sk(a1,a2)=i1),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f40507,f40044])).
% 104.32/13.63 fof(f40597,plain,(
% 104.32/13.63 i4=i3|select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)=select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f40507,f37561])).
% 104.32/13.63 fof(f40605,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i3,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),i4)),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f40507,f37263])).
% 104.32/13.63 fof(f40614,plain,(
% 104.32/13.63 sk(a1,a2)=i1),
% 104.32/13.63 inference(trivial_equality_resolution,[status(thm)],[f40572])).
% 104.32/13.63 fof(f40647,plain,(
% 104.32/13.63 i4=i1|select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)=select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f40507,f40597])).
% 104.32/13.63 fof(f40648,plain,(
% 104.32/13.63 i4=i1|select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1)=select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f40507,f40647])).
% 104.32/13.63 fof(f40649,plain,(
% 104.32/13.63 i4=i1|select(a1,i1)=select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40648])).
% 104.32/13.63 fof(f40650,plain,(
% 104.32/13.63 i4=i1|select(a1,i1)=select(a2,i1)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40649])).
% 104.32/13.63 fof(f40651,plain,(
% 104.32/13.63 i4=i1),
% 104.32/13.63 inference(forward_subsumption_resolution,[status(thm)],[f40650,f40302])).
% 104.32/13.63 fof(f40665,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f40507,f40605])).
% 104.32/13.63 fof(f40666,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f40507,f40665])).
% 104.32/13.63 fof(f40667,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(a1,i1)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i3,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40666])).
% 104.32/13.63 fof(f40668,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(a1,i1)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f40507,f40667])).
% 104.32/13.63 fof(f40669,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(a1,i1)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(a2,i1)),i4)),
% 104.32/13.63 inference(forward_demodulation,[status(thm)],[f5,f40668])).
% 104.32/13.63 fof(f40711,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(a1,i1)),i4)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(a2,i1)),i1)),
% 104.32/13.63 inference(backward_demodulation,[status(thm)],[f40651,f40669])).
% 104.32/13.63 fof(f40716,plain,(
% 104.32/13.63 select(store(store(store(a2,i1,select(a1,i1)),i1,select(a2,i1)),i1,select(a1,i1)),i1)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(a2,i1)),i1)),
% 104.32/13.68 inference(forward_demodulation,[status(thm)],[f40651,f40711])).
% 104.32/13.68 fof(f40717,plain,(
% 104.32/13.68 select(a1,i1)=select(store(store(store(a1,i1,select(a2,i1)),i1,select(a1,i1)),i1,select(a2,i1)),i1)),
% 104.32/13.68 inference(forward_demodulation,[status(thm)],[f5,f40716])).
% 104.32/13.68 fof(f40718,plain,(
% 104.32/13.68 select(a1,i1)=select(a2,i1)),
% 104.32/13.68 inference(forward_demodulation,[status(thm)],[f5,f40717])).
% 104.32/13.68 fof(f40724,plain,(
% 104.32/13.68 ~select(a1,sk(a1,a2))=select(a2,i1)),
% 104.32/13.68 inference(backward_demodulation,[status(thm)],[f40614,f9])).
% 104.32/13.68 fof(f40725,plain,(
% 104.32/13.68 ~select(a1,i1)=select(a2,i1)),
% 104.32/13.68 inference(forward_demodulation,[status(thm)],[f40614,f40724])).
% 104.32/13.68 fof(f40726,plain,(
% 104.32/13.68 ~select(a1,i1)=select(a1,i1)),
% 104.32/13.68 inference(forward_demodulation,[status(thm)],[f40718,f40725])).
% 104.32/13.68 fof(f40727,plain,(
% 104.32/13.68 $false),
% 104.32/13.68 inference(trivial_equality_resolution,[status(thm)],[f40726])).
% 104.32/13.68 % SZS output end CNFRefutation for theBenchmark.p
% 6.14/13.82 % Elapsed time: 13.447455 seconds
% 6.14/13.82 % CPU time: 105.813966 seconds
% 6.14/13.82 % Total memory used: 1.302 GB
% 6.14/13.82 % Net memory used: 1.282 GB
%------------------------------------------------------------------------------