%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV555-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:52:46 PM UTC 2026
% Result : Unsatisfiable 0.10s 6.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV555-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.98 % Computer : n004.cluster.edu
% 0.10/5.98 % Model : x86_64 x86_64
% 0.10/5.98 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.98 % Memory : 8046.5625MB
% 0.10/5.98 % OS : Linux 6.8.0-71-generic
% 0.10/5.98 % CPULimit : 300
% 0.10/5.98 % WCLimit : 300
% 0.10/5.98 % DateTime : Mon Sep 21 09:07:56 UTC 2026
% 0.10/5.98 % CPUTime :
% 0.10/6.00 % Drodi V4.1.1
% 0.10/6.03 % Refutation found
% 0.10/6.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/6.03 % SZS output start CNFRefutation for theBenchmark
% 0.10/6.03 fof(f1,axiom,(
% 0.10/6.03 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f2,axiom,(
% 0.10/6.03 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f3,hypothesis,(
% 0.10/6.03 a_20 = store(a1,i1,e_19) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f4,hypothesis,(
% 0.10/6.03 a_22 = store(a2,i1,e_21) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f5,hypothesis,(
% 0.10/6.03 a_24 = store(a_20,i2,e_23) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f6,hypothesis,(
% 0.10/6.03 a_26 = store(a_22,i2,e_25) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f7,hypothesis,(
% 0.10/6.03 a_28 = store(a_24,i3,e_27) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f8,hypothesis,(
% 0.10/6.03 a_30 = store(a_26,i3,e_29) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f9,hypothesis,(
% 0.10/6.03 a_32 = store(a_28,i4,e_31) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f10,hypothesis,(
% 0.10/6.03 a_34 = store(a_30,i4,e_33) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f11,hypothesis,(
% 0.10/6.03 e_19 = select(a2,i1) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f12,hypothesis,(
% 0.10/6.03 e_21 = select(a1,i1) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f13,hypothesis,(
% 0.10/6.03 e_23 = select(a_22,i2) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f14,hypothesis,(
% 0.10/6.03 e_25 = select(a_20,i2) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f15,hypothesis,(
% 0.10/6.03 e_27 = select(a_26,i3) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f16,hypothesis,(
% 0.10/6.03 e_29 = select(a_24,i3) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f17,hypothesis,(
% 0.10/6.03 e_31 = select(a_30,i4) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f18,hypothesis,(
% 0.10/6.03 e_33 = select(a_28,i4) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f19,hypothesis,(
% 0.10/6.03 e_36 = select(a1,i_35) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f20,hypothesis,(
% 0.10/6.03 e_37 = select(a2,i_35) ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f22,hypothesis,(
% 0.10/6.03 a_32 = a_34 ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f23,negated_conjecture,(
% 0.10/6.03 e_36 != e_37 ),
% 0.10/6.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/6.03 fof(f24,plain,(
% 0.10/6.03 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.10/6.03 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/6.03 fof(f25,plain,(
% 0.10/6.03 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 0.10/6.03 inference(miniscoping,[status(thm)],[f2])).
% 0.10/6.03 fof(f26,plain,(
% 0.10/6.03 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 0.10/6.03 inference(cnf_transformation,[status(thm)],[f25])).
% 0.10/6.03 fof(f27,plain,(
% 0.10/6.03 a_20=store(a1,i1,e_19)),
% 0.10/6.03 inference(cnf_transformation,[status(thm)],[f3])).
% 0.16/6.03 fof(f28,plain,(
% 0.16/6.03 a_22=store(a2,i1,e_21)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/6.03 fof(f29,plain,(
% 0.16/6.03 a_24=store(a_20,i2,e_23)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/6.03 fof(f30,plain,(
% 0.16/6.03 a_26=store(a_22,i2,e_25)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f6])).
% 0.16/6.03 fof(f31,plain,(
% 0.16/6.03 a_28=store(a_24,i3,e_27)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f7])).
% 0.16/6.03 fof(f32,plain,(
% 0.16/6.03 a_30=store(a_26,i3,e_29)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f8])).
% 0.16/6.03 fof(f33,plain,(
% 0.16/6.03 a_32=store(a_28,i4,e_31)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f9])).
% 0.16/6.03 fof(f34,plain,(
% 0.16/6.03 a_34=store(a_30,i4,e_33)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f10])).
% 0.16/6.03 fof(f35,plain,(
% 0.16/6.03 e_19=select(a2,i1)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f11])).
% 0.16/6.03 fof(f36,plain,(
% 0.16/6.03 e_21=select(a1,i1)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f12])).
% 0.16/6.03 fof(f37,plain,(
% 0.16/6.03 e_23=select(a_22,i2)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f13])).
% 0.16/6.03 fof(f38,plain,(
% 0.16/6.03 e_25=select(a_20,i2)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f14])).
% 0.16/6.03 fof(f39,plain,(
% 0.16/6.03 e_27=select(a_26,i3)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f15])).
% 0.16/6.03 fof(f40,plain,(
% 0.16/6.03 e_29=select(a_24,i3)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f16])).
% 0.16/6.03 fof(f41,plain,(
% 0.16/6.03 e_31=select(a_30,i4)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f17])).
% 0.16/6.03 fof(f42,plain,(
% 0.16/6.03 e_33=select(a_28,i4)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f18])).
% 0.16/6.03 fof(f43,plain,(
% 0.16/6.03 e_36=select(a1,i_35)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f19])).
% 0.16/6.03 fof(f44,plain,(
% 0.16/6.03 e_37=select(a2,i_35)),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f20])).
% 0.16/6.03 fof(f46,plain,(
% 0.16/6.03 a_32=a_34),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f22])).
% 0.16/6.03 fof(f47,plain,(
% 0.16/6.03 ~e_36=e_37),
% 0.16/6.03 inference(cnf_transformation,[status(thm)],[f23])).
% 0.16/6.03 fof(f48,plain,(
% 0.16/6.03 a_32=store(a_30,i4,e_33)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f46,f34])).
% 0.16/6.03 fof(f51,plain,(
% 0.16/6.03 ![X0]: (i1=X0|select(a_20,X0)=select(a1,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f27,f26])).
% 0.16/6.03 fof(f52,plain,(
% 0.16/6.03 select(a_20,i1)=e_19),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f27,f24])).
% 0.16/6.03 fof(f53,plain,(
% 0.16/6.03 ![X0]: (i1=X0|select(a_22,X0)=select(a2,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f28,f26])).
% 0.16/6.03 fof(f54,plain,(
% 0.16/6.03 select(a_22,i1)=e_21),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f28,f24])).
% 0.16/6.03 fof(f55,plain,(
% 0.16/6.03 ![X0]: (i2=X0|select(a_24,X0)=select(a_20,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f29,f26])).
% 0.16/6.03 fof(f56,plain,(
% 0.16/6.03 select(a_24,i2)=e_23),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f29,f24])).
% 0.16/6.03 fof(f57,plain,(
% 0.16/6.03 ![X0]: (i2=X0|select(a_26,X0)=select(a_22,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f30,f26])).
% 0.16/6.03 fof(f58,plain,(
% 0.16/6.03 select(a_26,i2)=e_25),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f30,f24])).
% 0.16/6.03 fof(f59,plain,(
% 0.16/6.03 ![X0]: (i3=X0|select(a_28,X0)=select(a_24,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f31,f26])).
% 0.16/6.03 fof(f60,plain,(
% 0.16/6.03 select(a_28,i3)=e_27),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f31,f24])).
% 0.16/6.03 fof(f61,plain,(
% 0.16/6.03 ![X0]: (i3=X0|select(a_30,X0)=select(a_26,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f32,f26])).
% 0.16/6.03 fof(f62,plain,(
% 0.16/6.03 select(a_30,i3)=e_29),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f32,f24])).
% 0.16/6.03 fof(f63,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_32,X0)=select(a_28,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f33,f26])).
% 0.16/6.03 fof(f64,plain,(
% 0.16/6.03 select(a_32,i4)=e_31),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f33,f24])).
% 0.16/6.03 fof(f65,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_32,X0)=select(a_30,X0))),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f48,f26])).
% 0.16/6.03 fof(f66,plain,(
% 0.16/6.03 select(a_32,i4)=e_33),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f48,f24])).
% 0.16/6.03 fof(f68,plain,(
% 0.16/6.03 e_31=select(a_28,i4)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f69,f42])).
% 0.16/6.03 fof(f69,plain,(
% 0.16/6.03 e_31=e_33),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f64,f66])).
% 0.16/6.03 fof(f73,plain,(
% 0.16/6.03 i1=i_35|select(a_20,i_35)=e_36),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f43,f51])).
% 0.16/6.03 fof(f77,plain,(
% 0.16/6.03 i1=i_35|select(a_22,i_35)=e_37),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f44,f53])).
% 0.16/6.03 fof(f81,plain,(
% 0.16/6.03 i2=i3|e_29=select(a_20,i3)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f40,f55])).
% 0.16/6.03 fof(f85,plain,(
% 0.16/6.03 i2=i3|e_27=select(a_22,i3)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f39,f57])).
% 0.16/6.03 fof(f88,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_24,i4)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f68,f59])).
% 0.16/6.03 fof(f92,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_20,i4)|i2=i4),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f55,f88])).
% 0.16/6.03 fof(f95,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_26,i4)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f41,f61])).
% 0.16/6.03 fof(f100,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_22,i4)|i2=i4),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f57,f95])).
% 0.16/6.03 fof(f103,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_28,X0)=select(a_30,X0)|i4=X0)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f63,f65])).
% 0.16/6.03 fof(f106,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_28,X0)=select(a_30,X0))),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f103])).
% 0.16/6.03 fof(f108,plain,(
% 0.16/6.03 i4=i3|select(a_28,i3)=e_29),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f62,f106])).
% 0.16/6.03 fof(f110,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_28,X0)=select(a_26,X0)|i3=X0)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f61,f106])).
% 0.16/6.03 fof(f114,plain,(
% 0.16/6.03 i4=i3|e_27=e_29),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f60,f108])).
% 0.16/6.03 fof(f119,plain,(
% 0.16/6.03 e_31=select(a_28,i3)|e_27=e_29),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f114,f68])).
% 0.16/6.03 fof(f122,plain,(
% 0.16/6.03 e_31=select(a_30,i3)|e_27=e_29),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f114,f41])).
% 0.16/6.03 fof(f125,plain,(
% 0.16/6.03 e_31=e_27|e_27=e_29),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f60,f119])).
% 0.16/6.03 fof(f126,plain,(
% 0.16/6.03 e_31=e_29|e_27=e_29),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f62,f122])).
% 0.16/6.03 fof(f129,plain,(
% 0.16/6.03 e_27=e_29|e_27=e_29|e_27=e_29),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f125,f126])).
% 0.16/6.03 fof(f136,plain,(
% 0.16/6.03 i2=i3|e_27=select(a_20,i3)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f145,f81])).
% 0.16/6.03 fof(f139,plain,(
% 0.16/6.03 e_27=select(a_24,i3)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f145,f40])).
% 0.16/6.03 fof(f145,plain,(
% 0.16/6.03 e_27=e_29),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f129])).
% 0.16/6.03 fof(f158,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_24,X0)=select(a_26,X0)|i3=X0|i3=X0)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f59,f110])).
% 0.16/6.03 fof(f162,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_24,X0)=select(a_26,X0)|i3=X0)),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f158])).
% 0.16/6.03 fof(f165,plain,(
% 0.16/6.03 i4=i2|select(a_24,i2)=e_25|i3=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f58,f162])).
% 0.16/6.03 fof(f167,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_24,X0)=select(a_22,X0)|i3=X0|i2=X0)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f57,f162])).
% 0.16/6.03 fof(f172,plain,(
% 0.16/6.03 i4=i2|e_23=e_25|i3=i2),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f56,f165])).
% 0.16/6.03 fof(f176,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_26,i2)|e_23=e_25|i3=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f172,f95])).
% 0.16/6.03 fof(f177,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_24,i2)|e_23=e_25|i3=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f172,f88])).
% 0.16/6.03 fof(f185,plain,(
% 0.16/6.03 i3=i4|e_31=e_25|e_23=e_25|i3=i2),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f58,f176])).
% 0.16/6.03 fof(f186,plain,(
% 0.16/6.03 i3=i4|e_31=e_23|e_23=e_25|i3=i2),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f56,f177])).
% 0.16/6.03 fof(f190,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_20,X0)=select(a_22,X0)|i3=X0|i2=X0|i2=X0)),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f55,f167])).
% 0.16/6.03 fof(f195,plain,(
% 0.16/6.03 ![X0]: (i4=X0|select(a_20,X0)=select(a_22,X0)|i3=X0|i2=X0)),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f190])).
% 0.16/6.03 fof(f199,plain,(
% 0.16/6.03 i3=i4|e_25=e_23|e_23=e_25|i3=i2|i3=i4|e_23=e_25|i3=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f185,f186])).
% 0.16/6.03 fof(f203,plain,(
% 0.16/6.03 i3=i4|e_25=e_23|i3=i2),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f199])).
% 0.16/6.03 fof(f205,plain,(
% 0.16/6.03 i3=i2|e_25=e_23|i3=i2|e_23=e_25|i3=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f172,f203])).
% 0.16/6.03 fof(f216,plain,(
% 0.16/6.03 i3=i2|e_25=e_23),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f205])).
% 0.16/6.03 fof(f224,plain,(
% 0.16/6.03 e_27=select(a_24,i2)|e_25=e_23),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f216,f139])).
% 0.16/6.03 fof(f229,plain,(
% 0.16/6.03 e_27=select(a_26,i2)|e_25=e_23),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f216,f39])).
% 0.16/6.03 fof(f231,plain,(
% 0.16/6.03 e_27=e_23|e_25=e_23),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f56,f224])).
% 0.16/6.03 fof(f233,plain,(
% 0.16/6.03 e_27=e_25|e_25=e_23),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f58,f229])).
% 0.16/6.03 fof(f236,plain,(
% 0.16/6.03 e_23=e_25|e_25=e_23|e_25=e_23),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f231,f233])).
% 0.16/6.03 fof(f245,plain,(
% 0.16/6.03 e_23=select(a_20,i2)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f252,f38])).
% 0.16/6.03 fof(f252,plain,(
% 0.16/6.03 e_23=e_25),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f236])).
% 0.16/6.03 fof(f263,plain,(
% 0.16/6.03 i4=i_35|select(a_20,i_35)=e_37|i3=i_35|i2=i_35|i1=i_35),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f77,f195])).
% 0.16/6.03 fof(f264,plain,(
% 0.16/6.03 i4=i1|select(a_20,i1)=e_21|i3=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f54,f195])).
% 0.16/6.03 fof(f271,plain,(
% 0.16/6.03 i4=i1|e_19=e_21|i3=i1|i2=i1),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f52,f264])).
% 0.16/6.03 fof(f273,plain,(
% 0.16/6.03 i4=i_35|e_36=e_37|i3=i_35|i2=i_35|i1=i_35|i1=i_35),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f73,f263])).
% 0.16/6.03 fof(f275,plain,(
% 0.16/6.03 i4=i_35|e_36=e_37|i3=i_35|i2=i_35|i1=i_35),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f273])).
% 0.16/6.03 fof(f276,plain,(
% 0.16/6.03 i4=i_35|i3=i_35|i2=i_35|i1=i_35),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f275,f47])).
% 0.16/6.03 fof(f278,plain,(
% 0.16/6.03 i1=i_35|select(a_22,i4)=e_37|i3=i_35|i2=i_35|i1=i_35),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f276,f77])).
% 0.16/6.03 fof(f279,plain,(
% 0.16/6.03 i1=i_35|select(a_20,i4)=e_36|i3=i_35|i2=i_35|i1=i_35),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f276,f73])).
% 0.16/6.03 fof(f282,plain,(
% 0.16/6.03 i2=i_35|i1=i_35|~i4=i3|i_35=i3),
% 0.16/6.03 inference(equality_factoring,[status(thm)],[f276])).
% 0.16/6.03 fof(f283,plain,(
% 0.16/6.03 i3=i_35|i1=i_35|~i4=i2|i_35=i2),
% 0.16/6.03 inference(equality_factoring,[status(thm)],[f276])).
% 0.16/6.03 fof(f285,plain,(
% 0.16/6.03 i1=i_35|select(a_22,i4)=e_37|i3=i_35|i2=i_35),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f278])).
% 0.16/6.03 fof(f286,plain,(
% 0.16/6.03 i1=i_35|select(a_20,i4)=e_36|i3=i_35|i2=i_35),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f279])).
% 0.16/6.03 fof(f290,plain,(
% 0.16/6.03 i1=i_35|e_31=e_37|i3=i_35|i2=i_35|i3=i4|i2=i4),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f100,f285])).
% 0.16/6.03 fof(f294,plain,(
% 0.16/6.03 i1=i_35|e_31=e_37|i3=i_35|i2=i_35|i2=i4),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f290,f282])).
% 0.16/6.03 fof(f295,plain,(
% 0.16/6.03 i1=i_35|e_31=e_36|i3=i_35|i2=i_35|i3=i4|i2=i4),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f92,f286])).
% 0.16/6.03 fof(f297,plain,(
% 0.16/6.03 i1=i_35|e_31=e_36|i3=i_35|i2=i_35|i2=i4),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f295,f282])).
% 0.16/6.03 fof(f303,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_22,i1)|i2=i4|e_19=e_21|i3=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f271,f100])).
% 0.16/6.03 fof(f304,plain,(
% 0.16/6.03 i3=i4|e_31=select(a_20,i1)|i2=i4|e_19=e_21|i3=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f271,f92])).
% 0.16/6.03 fof(f315,plain,(
% 0.16/6.03 i3=i4|e_31=e_21|i2=i4|e_19=e_21|i3=i1|i2=i1),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f54,f303])).
% 0.16/6.03 fof(f316,plain,(
% 0.16/6.03 i3=i4|e_31=e_19|i2=i4|e_19=e_21|i3=i1|i2=i1),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f52,f304])).
% 0.16/6.03 fof(f328,plain,(
% 0.16/6.03 ~e_36=e_31|i1=i_35|i3=i_35|i2=i_35|i2=i4),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f294,f47])).
% 0.16/6.03 fof(f329,plain,(
% 0.16/6.03 i3=i_35|i1=i_35|i_35=i2),
% 0.16/6.03 inference(backward_subsumption_resolution,[status(thm)],[f283,f330])).
% 0.16/6.03 fof(f330,plain,(
% 0.16/6.03 i1=i_35|i3=i_35|i2=i_35|i2=i4),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f328,f297])).
% 0.16/6.03 fof(f333,plain,(
% 0.16/6.03 i3=i4|e_21=e_19|i2=i4|e_19=e_21|i3=i1|i2=i1|i3=i4|i2=i4|e_19=e_21|i3=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f315,f316])).
% 0.16/6.03 fof(f337,plain,(
% 0.16/6.03 i3=i4|e_21=e_19|i2=i4|i3=i1|i2=i1),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f333])).
% 0.16/6.03 fof(f350,plain,(
% 0.16/6.03 i1=i_35|select(a_22,i3)=e_37|i1=i_35|i_35=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f329,f77])).
% 0.16/6.03 fof(f351,plain,(
% 0.16/6.03 i1=i_35|select(a_20,i3)=e_36|i1=i_35|i_35=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f329,f73])).
% 0.16/6.03 fof(f355,plain,(
% 0.16/6.03 i1=i_35|~i3=i2|i_35=i2),
% 0.16/6.03 inference(equality_factoring,[status(thm)],[f329])).
% 0.16/6.03 fof(f357,plain,(
% 0.16/6.03 i1=i_35|select(a_22,i3)=e_37|i_35=i2),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f350])).
% 0.16/6.03 fof(f358,plain,(
% 0.16/6.03 i1=i_35|select(a_20,i3)=e_36|i_35=i2),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f351])).
% 0.16/6.03 fof(f362,plain,(
% 0.16/6.03 i1=i_35|e_27=e_37|i_35=i2|i2=i3),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f85,f357])).
% 0.16/6.03 fof(f366,plain,(
% 0.16/6.03 i1=i_35|e_27=e_37|i_35=i2),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f362,f355])).
% 0.16/6.03 fof(f369,plain,(
% 0.16/6.03 ~e_36=e_27|i1=i_35|i_35=i2),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f366,f47])).
% 0.16/6.03 fof(f370,plain,(
% 0.16/6.03 i1=i_35|e_27=e_36|i_35=i2|i2=i3),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f136,f358])).
% 0.16/6.03 fof(f372,plain,(
% 0.16/6.03 i1=i_35|i_35=i2),
% 0.16/6.03 inference(backward_subsumption_resolution,[status(thm)],[f355,f373])).
% 0.16/6.03 fof(f373,plain,(
% 0.16/6.03 i1=i_35|i_35=i2|i2=i3),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f370,f369])).
% 0.16/6.03 fof(f374,plain,(
% 0.16/6.03 i1=i_35|select(a_22,i2)=e_37|i1=i_35),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f372,f77])).
% 0.16/6.03 fof(f375,plain,(
% 0.16/6.03 i1=i_35|select(a_20,i2)=e_36|i1=i_35),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f372,f73])).
% 0.16/6.03 fof(f379,plain,(
% 0.16/6.03 i1=i_35|e_23=e_37|i1=i_35),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f37,f374])).
% 0.16/6.03 fof(f380,plain,(
% 0.16/6.03 i1=i_35|e_23=e_37),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f379])).
% 0.16/6.03 fof(f381,plain,(
% 0.16/6.03 i1=i_35|e_23=e_36|i1=i_35),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f245,f375])).
% 0.16/6.03 fof(f382,plain,(
% 0.16/6.03 i1=i_35|e_23=e_36),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f381])).
% 0.16/6.03 fof(f383,plain,(
% 0.16/6.03 ~e_36=e_23|i1=i_35),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f380,f47])).
% 0.16/6.03 fof(f389,plain,(
% 0.16/6.03 e_37=select(a2,i1)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f395,f44])).
% 0.16/6.03 fof(f390,plain,(
% 0.16/6.03 e_36=select(a1,i1)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f395,f43])).
% 0.16/6.03 fof(f395,plain,(
% 0.16/6.03 i1=i_35),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f383,f382])).
% 0.16/6.03 fof(f396,plain,(
% 0.16/6.03 ~e_36=e_19),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f397,f47])).
% 0.16/6.03 fof(f397,plain,(
% 0.16/6.03 e_37=e_19),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f35,f389])).
% 0.16/6.03 fof(f398,plain,(
% 0.16/6.03 e_36=e_21),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f36,f390])).
% 0.16/6.03 fof(f399,plain,(
% 0.16/6.03 i3=i4|i2=i4|i3=i1|i2=i1),
% 0.16/6.03 inference(backward_subsumption_resolution,[status(thm)],[f337,f409])).
% 0.16/6.03 fof(f401,plain,(
% 0.16/6.03 i4=i1|i3=i1|i2=i1),
% 0.16/6.03 inference(backward_subsumption_resolution,[status(thm)],[f271,f409])).
% 0.16/6.03 fof(f409,plain,(
% 0.16/6.03 ~e_21=e_19),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f398,f396])).
% 0.16/6.03 fof(f437,plain,(
% 0.16/6.03 i3=i1|i2=i4|i3=i1|i2=i1|i3=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f401,f399])).
% 0.16/6.03 fof(f449,plain,(
% 0.16/6.03 i3=i1|i2=i4|i2=i1),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f437])).
% 0.16/6.03 fof(f457,plain,(
% 0.16/6.03 i3=i1|i2=i1|i2=i1|i3=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f401,f449])).
% 0.16/6.03 fof(f468,plain,(
% 0.16/6.03 i3=i1|i2=i1),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f457])).
% 0.16/6.03 fof(f476,plain,(
% 0.16/6.03 e_27=select(a_24,i1)|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f468,f139])).
% 0.16/6.03 fof(f478,plain,(
% 0.16/6.03 i2=i3|e_27=select(a_22,i1)|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f468,f85])).
% 0.16/6.03 fof(f483,plain,(
% 0.16/6.03 i2=i3|e_27=e_21|i2=i1),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f54,f478])).
% 0.16/6.03 fof(f491,plain,(
% 0.16/6.03 e_27=select(a_20,i1)|i2=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f55,f476])).
% 0.16/6.03 fof(f496,plain,(
% 0.16/6.03 e_27=e_19|i2=i1|i2=i1),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f52,f491])).
% 0.16/6.03 fof(f497,plain,(
% 0.16/6.03 e_27=e_19|i2=i1),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f496])).
% 0.16/6.03 fof(f508,plain,(
% 0.16/6.03 i2=i3|e_19=e_21|i2=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f497,f483])).
% 0.16/6.03 fof(f513,plain,(
% 0.16/6.03 i2=i3|e_19=e_21|i2=i1),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f508])).
% 0.16/6.03 fof(f514,plain,(
% 0.16/6.03 i2=i3|i2=i1),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f513,f409])).
% 0.16/6.03 fof(f517,plain,(
% 0.16/6.03 i2=i1|i2=i1|i2=i1),
% 0.16/6.03 inference(paramodulation,[status(thm)],[f468,f514])).
% 0.16/6.03 fof(f535,plain,(
% 0.16/6.03 e_23=select(a_20,i1)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f554,f245])).
% 0.16/6.03 fof(f546,plain,(
% 0.16/6.03 e_23=select(a_22,i1)),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f554,f37])).
% 0.16/6.03 fof(f554,plain,(
% 0.16/6.03 i2=i1),
% 0.16/6.03 inference(duplicate_literals_removal,[status(thm)],[f517])).
% 0.16/6.03 fof(f567,plain,(
% 0.16/6.03 e_23=e_19),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f52,f535])).
% 0.16/6.03 fof(f571,plain,(
% 0.16/6.03 e_19=e_21),
% 0.16/6.03 inference(backward_demodulation,[status(thm)],[f572,f54])).
% 0.16/6.03 fof(f572,plain,(
% 0.16/6.03 e_19=select(a_22,i1)),
% 0.16/6.03 inference(forward_demodulation,[status(thm)],[f567,f546])).
% 0.16/6.03 fof(f573,plain,(
% 0.16/6.03 $false),
% 0.16/6.03 inference(forward_subsumption_resolution,[status(thm)],[f571,f409])).
% 0.16/6.03 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/6.06 % Elapsed time: 0.066044 seconds
% 0.16/6.06 % CPU time: 0.225202 seconds
% 0.16/6.06 % Total memory used: 103.361 MB
% 0.16/6.06 % Net memory used: 102.974 MB
%------------------------------------------------------------------------------