%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV537-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 : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:51:36 PM UTC 2026
% Result : Unsatisfiable 0.16s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV537-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.41 % Computer : n016.cluster.edu
% 0.12/0.41 % Model : x86_64 x86_64
% 0.12/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.41 % Memory : 8046.5625MB
% 0.12/0.41 % OS : Linux 6.8.0-71-generic
% 0.12/0.41 % CPULimit : 300
% 0.12/0.41 % WCLimit : 300
% 0.12/0.41 % DateTime : Mon Sep 21 09:08:22 UTC 2026
% 0.12/0.42 % CPUTime :
% 0.16/0.43 % Drodi V4.1.1
% 0.16/0.84 % Refutation found
% 0.16/0.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/0.84 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.84 fof(f1,axiom,(
% 0.16/0.84 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f2,axiom,(
% 0.16/0.84 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f5,hypothesis,(
% 0.16/0.84 a_469 = store(a_467,i0,e_468) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f6,hypothesis,(
% 0.16/0.84 a_471 = store(a_469,i3,e_470) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f7,hypothesis,(
% 0.16/0.84 a_473 = store(a_471,i3,e_472) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f8,hypothesis,(
% 0.16/0.84 a_475 = store(a_473,i2,e_474) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f9,hypothesis,(
% 0.16/0.84 a_477 = store(a_475,i2,e_476) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f10,hypothesis,(
% 0.16/0.84 a_479 = store(a_477,i0,e_478) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f11,hypothesis,(
% 0.16/0.84 a_480 = store(a_467,i3,e_470) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f12,hypothesis,(
% 0.16/0.84 a_481 = store(a_480,i0,e_468) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f13,hypothesis,(
% 0.16/0.84 a_483 = store(a_481,i3,e_482) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f14,hypothesis,(
% 0.16/0.84 a_485 = store(a_483,i2,e_484) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f15,hypothesis,(
% 0.16/0.84 a_487 = store(a_485,i0,e_486) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f16,hypothesis,(
% 0.16/0.84 a_489 = store(a_487,i2,e_488) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f18,hypothesis,(
% 0.16/0.84 e_468 = select(a_467,i3) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f19,hypothesis,(
% 0.16/0.84 e_470 = select(a_467,i0) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f20,hypothesis,(
% 0.16/0.84 e_472 = select(a_471,i2) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f21,hypothesis,(
% 0.16/0.84 e_474 = select(a_471,i3) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f22,hypothesis,(
% 0.16/0.84 e_476 = select(a_475,i0) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f23,hypothesis,(
% 0.16/0.84 e_478 = select(a_475,i2) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f24,hypothesis,(
% 0.16/0.84 e_482 = select(a_481,i2) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f25,hypothesis,(
% 0.16/0.84 e_484 = select(a_481,i3) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f26,hypothesis,(
% 0.16/0.84 e_486 = select(a_485,i2) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f27,hypothesis,(
% 0.16/0.84 e_488 = select(a_485,i0) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f28,hypothesis,(
% 0.16/0.84 e_491 = select(a_479,i_490) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f29,hypothesis,(
% 0.16/0.84 e_492 = select(a_489,i_490) ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f31,negated_conjecture,(
% 0.16/0.84 e_491 != e_492 ),
% 0.16/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.84 fof(f32,plain,(
% 0.16/0.84 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f1])).
% 0.16/0.84 fof(f33,plain,(
% 0.16/0.84 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 0.16/0.84 inference(miniscoping,[status(thm)],[f2])).
% 0.16/0.84 fof(f34,plain,(
% 0.16/0.84 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f33])).
% 0.16/0.84 fof(f37,plain,(
% 0.16/0.84 a_469=store(a_467,i0,e_468)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f5])).
% 0.16/0.84 fof(f38,plain,(
% 0.16/0.84 a_471=store(a_469,i3,e_470)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f6])).
% 0.16/0.84 fof(f39,plain,(
% 0.16/0.84 a_473=store(a_471,i3,e_472)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f7])).
% 0.16/0.84 fof(f40,plain,(
% 0.16/0.84 a_475=store(a_473,i2,e_474)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f8])).
% 0.16/0.84 fof(f41,plain,(
% 0.16/0.84 a_477=store(a_475,i2,e_476)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f9])).
% 0.16/0.84 fof(f42,plain,(
% 0.16/0.84 a_479=store(a_477,i0,e_478)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f10])).
% 0.16/0.84 fof(f43,plain,(
% 0.16/0.84 a_480=store(a_467,i3,e_470)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f11])).
% 0.16/0.84 fof(f44,plain,(
% 0.16/0.84 a_481=store(a_480,i0,e_468)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f12])).
% 0.16/0.84 fof(f45,plain,(
% 0.16/0.84 a_483=store(a_481,i3,e_482)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f13])).
% 0.16/0.84 fof(f46,plain,(
% 0.16/0.84 a_485=store(a_483,i2,e_484)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f14])).
% 0.16/0.84 fof(f47,plain,(
% 0.16/0.84 a_487=store(a_485,i0,e_486)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f15])).
% 0.16/0.84 fof(f48,plain,(
% 0.16/0.84 a_489=store(a_487,i2,e_488)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f16])).
% 0.16/0.84 fof(f50,plain,(
% 0.16/0.84 e_468=select(a_467,i3)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f18])).
% 0.16/0.84 fof(f51,plain,(
% 0.16/0.84 e_470=select(a_467,i0)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f19])).
% 0.16/0.84 fof(f52,plain,(
% 0.16/0.84 e_472=select(a_471,i2)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f20])).
% 0.16/0.84 fof(f53,plain,(
% 0.16/0.84 e_474=select(a_471,i3)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f21])).
% 0.16/0.84 fof(f54,plain,(
% 0.16/0.84 e_476=select(a_475,i0)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f22])).
% 0.16/0.84 fof(f55,plain,(
% 0.16/0.84 e_478=select(a_475,i2)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f23])).
% 0.16/0.84 fof(f56,plain,(
% 0.16/0.84 e_482=select(a_481,i2)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f24])).
% 0.16/0.84 fof(f57,plain,(
% 0.16/0.84 e_484=select(a_481,i3)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f25])).
% 0.16/0.84 fof(f58,plain,(
% 0.16/0.84 e_486=select(a_485,i2)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f26])).
% 0.16/0.84 fof(f59,plain,(
% 0.16/0.84 e_488=select(a_485,i0)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f27])).
% 0.16/0.84 fof(f60,plain,(
% 0.16/0.84 e_491=select(a_479,i_490)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f28])).
% 0.16/0.84 fof(f61,plain,(
% 0.16/0.84 e_492=select(a_489,i_490)),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f29])).
% 0.16/0.84 fof(f63,plain,(
% 0.16/0.84 ~e_491=e_492),
% 0.16/0.84 inference(cnf_transformation,[status(thm)],[f31])).
% 0.16/0.84 fof(f66,plain,(
% 0.16/0.84 select(a_469,i0)=e_468),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f37,f32])).
% 0.16/0.84 fof(f67,plain,(
% 0.16/0.84 select(a_471,i3)=e_470),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f38,f32])).
% 0.16/0.84 fof(f68,plain,(
% 0.16/0.84 e_474=e_470),
% 0.16/0.84 inference(backward_demodulation,[status(thm)],[f67,f53])).
% 0.16/0.84 fof(f69,plain,(
% 0.16/0.84 select(a_473,i3)=e_472),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f39,f32])).
% 0.16/0.84 fof(f70,plain,(
% 0.16/0.84 a_475=store(a_473,i2,e_470)),
% 0.16/0.84 inference(forward_demodulation,[status(thm)],[f68,f40])).
% 0.16/0.84 fof(f71,plain,(
% 0.16/0.84 select(a_475,i2)=e_470),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f70,f32])).
% 0.16/0.84 fof(f72,plain,(
% 0.16/0.84 select(a_477,i2)=e_476),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f41,f32])).
% 0.16/0.84 fof(f73,plain,(
% 0.16/0.84 select(a_479,i0)=e_478),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f42,f32])).
% 0.16/0.84 fof(f75,plain,(
% 0.16/0.84 ![X0]: (i0=X0|select(a_479,X0)=select(a_477,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f42,f34])).
% 0.16/0.84 fof(f76,plain,(
% 0.16/0.84 ![X0]: (i2=X0|select(a_477,X0)=select(a_475,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f41,f34])).
% 0.16/0.84 fof(f77,plain,(
% 0.16/0.84 ![X0]: (i2=X0|select(a_475,X0)=select(a_473,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f70,f34])).
% 0.16/0.84 fof(f78,plain,(
% 0.16/0.84 ![X0]: (i3=X0|select(a_473,X0)=select(a_471,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f39,f34])).
% 0.16/0.84 fof(f79,plain,(
% 0.16/0.84 ![X0]: (i3=X0|select(a_471,X0)=select(a_469,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f38,f34])).
% 0.16/0.84 fof(f80,plain,(
% 0.16/0.84 ![X0]: (i0=X0|select(a_469,X0)=select(a_467,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f37,f34])).
% 0.16/0.84 fof(f84,plain,(
% 0.16/0.84 ![X0]: (i2=X0|select(a_479,X0)=select(a_475,X0)|i0=X0)),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f75,f76])).
% 0.16/0.84 fof(f86,plain,(
% 0.16/0.84 i2=i3|select(a_475,i3)=e_472),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f69,f77])).
% 0.16/0.84 fof(f89,plain,(
% 0.16/0.84 ![X0]: (i3=X0|select(a_475,X0)=select(a_471,X0)|i2=X0)),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f77,f78])).
% 0.16/0.84 fof(f92,plain,(
% 0.16/0.84 i3=i0|select(a_471,i0)=e_468),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f66,f79])).
% 0.16/0.84 fof(f95,plain,(
% 0.16/0.84 ![X0]: (i0=X0|select(a_471,X0)=select(a_467,X0)|i3=X0)),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f79,f80])).
% 0.16/0.84 fof(f102,plain,(
% 0.16/0.84 i2=i_490|e_491=select(a_475,i_490)|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f60,f84])).
% 0.16/0.84 fof(f104,plain,(
% 0.16/0.84 i3=i_490|e_491=select(a_471,i_490)|i2=i_490|i2=i_490|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f102,f89])).
% 0.16/0.84 fof(f107,plain,(
% 0.16/0.84 i3=i0|e_476=select(a_471,i0)|i2=i0),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f54,f89])).
% 0.16/0.84 fof(f112,plain,(
% 0.16/0.84 i3=i_490|e_491=select(a_471,i_490)|i2=i_490|i0=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f104])).
% 0.16/0.84 fof(f114,plain,(
% 0.16/0.84 i0=i_490|e_491=select(a_467,i_490)|i3=i_490|i3=i_490|i2=i_490|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f112,f95])).
% 0.16/0.84 fof(f117,plain,(
% 0.16/0.84 i0=i2|e_472=select(a_467,i2)|i3=i2),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f52,f95])).
% 0.16/0.84 fof(f122,plain,(
% 0.16/0.84 i0=i_490|e_491=select(a_467,i_490)|i3=i_490|i2=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f114])).
% 0.16/0.84 fof(f124,plain,(
% 0.16/0.84 i3=i0|e_476=e_468|i2=i0|i3=i0),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f92,f107])).
% 0.16/0.84 fof(f128,plain,(
% 0.16/0.84 i3=i0|e_476=e_468|i2=i0),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f124])).
% 0.16/0.84 fof(f130,plain,(
% 0.16/0.84 a_477=store(a_475,i2,e_468)|i3=i0|i2=i0),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f128,f41])).
% 0.16/0.84 fof(f132,plain,(
% 0.16/0.84 select(a_477,i2)=e_468|i3=i0|i2=i0),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f130,f32])).
% 0.16/0.84 fof(f134,plain,(
% 0.16/0.84 select(a_479,i2)=e_468|i3=i0|i2=i0|i0=i2),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f75,f132])).
% 0.16/0.84 fof(f137,plain,(
% 0.16/0.84 select(a_479,i2)=e_468|i3=i0|i2=i0),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f134])).
% 0.16/0.84 fof(f141,plain,(
% 0.16/0.84 e_478=e_470),
% 0.16/0.84 inference(backward_demodulation,[status(thm)],[f71,f55])).
% 0.16/0.84 fof(f147,plain,(
% 0.16/0.84 select(a_479,i2)=e_476|i0=i2),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f75,f72])).
% 0.16/0.84 fof(f156,plain,(
% 0.16/0.84 select(a_479,i0)=e_470),
% 0.16/0.84 inference(forward_demodulation,[status(thm)],[f141,f73])).
% 0.16/0.84 fof(f159,plain,(
% 0.16/0.84 ![X0]: (i3=X0|select(a_480,X0)=select(a_467,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f43,f34])).
% 0.16/0.84 fof(f160,plain,(
% 0.16/0.84 select(a_480,i3)=e_470),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f43,f32])).
% 0.16/0.84 fof(f163,plain,(
% 0.16/0.84 ![X0]: (i0=X0|select(a_481,X0)=select(a_480,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f44,f34])).
% 0.16/0.84 fof(f164,plain,(
% 0.16/0.84 select(a_481,i0)=e_468),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f44,f32])).
% 0.16/0.84 fof(f165,plain,(
% 0.16/0.84 i0=i3|select(a_481,i3)=e_470),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f160,f163])).
% 0.16/0.84 fof(f166,plain,(
% 0.16/0.84 ![X0]: (i0=X0|select(a_481,X0)=select(a_467,X0)|i3=X0)),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f159,f163])).
% 0.16/0.84 fof(f169,plain,(
% 0.16/0.84 i0=i3|e_484=e_470),
% 0.16/0.84 inference(forward_demodulation,[status(thm)],[f57,f165])).
% 0.16/0.84 fof(f172,plain,(
% 0.16/0.84 i0=i2|e_482=select(a_467,i2)|i3=i2),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f56,f166])).
% 0.16/0.84 fof(f175,plain,(
% 0.16/0.84 i0=i2|e_482=e_472|i3=i2|i0=i2|i3=i2),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f117,f172])).
% 0.16/0.84 fof(f177,plain,(
% 0.16/0.84 i0=i2|e_482=e_472|i3=i2),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f175])).
% 0.16/0.84 fof(f180,plain,(
% 0.16/0.84 ![X0]: (i3=X0|select(a_483,X0)=select(a_481,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f45,f34])).
% 0.16/0.84 fof(f181,plain,(
% 0.16/0.84 select(a_483,i3)=e_482),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f45,f32])).
% 0.16/0.84 fof(f187,plain,(
% 0.16/0.84 ![X0]: (i2=X0|select(a_485,X0)=select(a_483,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f46,f34])).
% 0.16/0.84 fof(f188,plain,(
% 0.16/0.84 select(a_485,i2)=e_484),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f46,f32])).
% 0.16/0.84 fof(f190,plain,(
% 0.16/0.84 ![X0]: (i2=X0|select(a_485,X0)=select(a_481,X0)|i3=X0)),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f180,f187])).
% 0.16/0.84 fof(f199,plain,(
% 0.16/0.84 i2=i0|e_488=select(a_481,i0)|i3=i0),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f59,f190])).
% 0.16/0.84 fof(f206,plain,(
% 0.16/0.84 i2=i0|e_488=e_468|i3=i0),
% 0.16/0.84 inference(backward_demodulation,[status(thm)],[f164,f199])).
% 0.16/0.84 fof(f210,plain,(
% 0.16/0.84 select(a_485,i3)=e_482|i2=i3),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f187,f181])).
% 0.16/0.84 fof(f220,plain,(
% 0.16/0.84 e_486=e_484),
% 0.16/0.84 inference(backward_demodulation,[status(thm)],[f188,f58])).
% 0.16/0.84 fof(f224,plain,(
% 0.16/0.84 a_487=store(a_485,i0,e_484)),
% 0.16/0.84 inference(forward_demodulation,[status(thm)],[f220,f47])).
% 0.16/0.84 fof(f226,plain,(
% 0.16/0.84 ![X0]: (i0=X0|select(a_487,X0)=select(a_485,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f224,f34])).
% 0.16/0.84 fof(f227,plain,(
% 0.16/0.84 select(a_487,i0)=e_484),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f224,f32])).
% 0.16/0.84 fof(f236,plain,(
% 0.16/0.84 ![X0]: (i2=X0|select(a_489,X0)=select(a_487,X0))),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f48,f34])).
% 0.16/0.84 fof(f237,plain,(
% 0.16/0.84 select(a_489,i2)=e_488),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f48,f32])).
% 0.16/0.84 fof(f238,plain,(
% 0.16/0.84 i2=i0|select(a_489,i0)=e_484),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f227,f236])).
% 0.16/0.84 fof(f239,plain,(
% 0.16/0.84 ![X0]: (i2=X0|select(a_489,X0)=select(a_485,X0)|i0=X0)),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f226,f236])).
% 0.16/0.84 fof(f243,plain,(
% 0.16/0.84 i2=i_490|e_492=select(a_485,i_490)|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f61,f239])).
% 0.16/0.84 fof(f246,plain,(
% 0.16/0.84 i2=i_490|e_492=select(a_481,i_490)|i0=i_490|i2=i_490|i3=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f190,f243])).
% 0.16/0.84 fof(f248,plain,(
% 0.16/0.84 i2=i_490|e_492=select(a_481,i_490)|i0=i_490|i3=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f246])).
% 0.16/0.84 fof(f254,plain,(
% 0.16/0.84 i2=i_490|e_492=select(a_467,i_490)|i0=i_490|i3=i_490|i0=i_490|i3=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f166,f248])).
% 0.16/0.84 fof(f256,plain,(
% 0.16/0.84 i2=i_490|e_492=select(a_467,i_490)|i0=i_490|i3=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f254])).
% 0.16/0.84 fof(f258,plain,(
% 0.16/0.84 i2=i_490|e_492=e_491|i0=i_490|i3=i_490|i0=i_490|i3=i_490|i2=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f122,f256])).
% 0.16/0.84 fof(f260,plain,(
% 0.16/0.84 i2=i_490|e_492=e_491|i0=i_490|i3=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f258])).
% 0.16/0.84 fof(f261,plain,(
% 0.16/0.84 i2=i_490|i0=i_490|i3=i_490),
% 0.16/0.84 inference(forward_subsumption_resolution,[status(thm)],[f260,f63])).
% 0.16/0.84 fof(f264,plain,(
% 0.16/0.84 i2=i_490|e_492=select(a_485,i3)|i0=i_490|i2=i_490|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f261,f243])).
% 0.16/0.84 fof(f265,plain,(
% 0.16/0.84 i2=i_490|e_491=select(a_475,i3)|i0=i_490|i2=i_490|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f261,f102])).
% 0.16/0.84 fof(f268,plain,(
% 0.16/0.84 i0=i_490|~i3=i2|i_490=i2),
% 0.16/0.84 inference(equality_factoring,[status(thm)],[f261])).
% 0.16/0.84 fof(f269,plain,(
% 0.16/0.84 i2=i_490|~i3=i0|i_490=i0),
% 0.16/0.84 inference(equality_factoring,[status(thm)],[f261])).
% 0.16/0.84 fof(f270,plain,(
% 0.16/0.84 i2=i_490|e_492=select(a_485,i3)|i0=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f264])).
% 0.16/0.84 fof(f271,plain,(
% 0.16/0.84 i2=i_490|e_491=select(a_475,i3)|i0=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f265])).
% 0.16/0.84 fof(f272,plain,(
% 0.16/0.84 i2=i_490|e_492=e_482|i0=i_490|i2=i3),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f210,f270])).
% 0.16/0.84 fof(f278,plain,(
% 0.16/0.84 i2=i_490|e_492=e_482|i0=i_490),
% 0.16/0.84 inference(forward_subsumption_resolution,[status(thm)],[f272,f268])).
% 0.16/0.84 fof(f282,plain,(
% 0.16/0.84 ~e_491=e_482|i2=i_490|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f278,f63])).
% 0.16/0.84 fof(f283,plain,(
% 0.16/0.84 i2=i_490|e_491=e_472|i0=i_490|i2=i3),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f86,f271])).
% 0.16/0.84 fof(f287,plain,(
% 0.16/0.84 i2=i_490|e_491=e_472|i0=i_490),
% 0.16/0.84 inference(forward_subsumption_resolution,[status(thm)],[f283,f268])).
% 0.16/0.84 fof(f289,plain,(
% 0.16/0.84 ~e_472=e_482|i2=i_490|i0=i_490|i2=i_490|i0=i_490),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f287,f282])).
% 0.16/0.84 fof(f290,plain,(
% 0.16/0.84 ~e_472=e_482|i2=i_490|i0=i_490),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f289])).
% 0.16/0.84 fof(f291,plain,(
% 0.16/0.84 i2=i_490|i0=i_490|i0=i2|i3=i2),
% 0.16/0.84 inference(resolution,[status(thm)],[f290,f177])).
% 0.16/0.84 fof(f293,plain,(
% 0.16/0.84 i2=i_490|i0=i_490|i0=i2),
% 0.16/0.84 inference(forward_subsumption_resolution,[status(thm)],[f291,f268])).
% 0.16/0.84 fof(f300,plain,(
% 0.16/0.84 e_492=select(a_489,i0)|i2=i_490|i0=i2),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f293,f61])).
% 0.16/0.84 fof(f301,plain,(
% 0.16/0.84 e_491=select(a_479,i0)|i2=i_490|i0=i2),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f293,f60])).
% 0.16/0.84 fof(f309,plain,(
% 0.16/0.84 e_491=e_470|i2=i_490|i0=i2),
% 0.16/0.84 inference(forward_demodulation,[status(thm)],[f156,f301])).
% 0.16/0.84 fof(f320,plain,(
% 0.16/0.84 e_492=e_484|i2=i_490|i0=i2|i2=i0),
% 0.16/0.84 inference(paramodulation,[status(thm)],[f238,f300])).
% 0.16/0.84 fof(f324,plain,(
% 0.16/0.84 e_492=e_484|i2=i_490|i0=i2),
% 0.16/0.84 inference(duplicate_literals_removal,[status(thm)],[f320])).
% 0.16/0.85 fof(f328,plain,(
% 0.16/0.85 ~e_491=e_484|i2=i_490|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f324,f63])).
% 0.16/0.85 fof(f331,plain,(
% 0.16/0.85 ~e_470=e_484|i2=i_490|i0=i2|i2=i_490|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f309,f328])).
% 0.16/0.85 fof(f333,plain,(
% 0.16/0.85 ~e_470=e_484|i2=i_490|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f331])).
% 0.16/0.85 fof(f335,plain,(
% 0.16/0.85 i2=i_490|i0=i2|i0=i3),
% 0.16/0.85 inference(resolution,[status(thm)],[f333,f169])).
% 0.16/0.85 fof(f344,plain,(
% 0.16/0.85 e_492=select(a_489,i2)|i0=i2|i0=i3),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f335,f61])).
% 0.16/0.85 fof(f345,plain,(
% 0.16/0.85 e_491=select(a_479,i2)|i0=i2|i0=i3),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f335,f60])).
% 0.16/0.85 fof(f355,plain,(
% 0.16/0.85 e_492=e_488|i0=i2|i0=i3),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f237,f344])).
% 0.16/0.85 fof(f360,plain,(
% 0.16/0.85 ~e_491=e_488|i0=i2|i0=i3),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f355,f63])).
% 0.16/0.85 fof(f367,plain,(
% 0.16/0.85 e_491=e_468|i0=i2|i0=i3|i3=i0|i2=i0),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f137,f345])).
% 0.16/0.85 fof(f373,plain,(
% 0.16/0.85 e_491=e_468|i0=i2|i0=i3),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f367])).
% 0.16/0.85 fof(f391,plain,(
% 0.16/0.85 ~e_468=e_488|i0=i2|i0=i3|i0=i2|i0=i3),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f373,f360])).
% 0.16/0.85 fof(f399,plain,(
% 0.16/0.85 ~e_468=e_488|i0=i2|i0=i3),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f391])).
% 0.16/0.85 fof(f400,plain,(
% 0.16/0.85 i0=i2|i0=i3),
% 0.16/0.85 inference(forward_subsumption_resolution,[status(thm)],[f399,f206])).
% 0.16/0.85 fof(f416,plain,(
% 0.16/0.85 a_480=store(a_467,i0,e_470)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f400,f43])).
% 0.16/0.85 fof(f421,plain,(
% 0.16/0.85 a_471=store(a_469,i0,e_470)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f400,f38])).
% 0.16/0.85 fof(f422,plain,(
% 0.16/0.85 e_484=select(a_481,i0)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f400,f57])).
% 0.16/0.85 fof(f423,plain,(
% 0.16/0.85 e_468=select(a_467,i0)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f400,f50])).
% 0.16/0.85 fof(f433,plain,(
% 0.16/0.85 e_484=e_468|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f164,f422])).
% 0.16/0.85 fof(f434,plain,(
% 0.16/0.85 e_468=e_470|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f51,f423])).
% 0.16/0.85 fof(f436,plain,(
% 0.16/0.85 ~e_470=e_468|i2=i_490|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f433,f333])).
% 0.16/0.85 fof(f440,plain,(
% 0.16/0.85 ~e_470=e_468|i2=i_490|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f436])).
% 0.16/0.85 fof(f482,plain,(
% 0.16/0.85 i2=i_490|i0=i2),
% 0.16/0.85 inference(forward_subsumption_resolution,[status(thm)],[f440,f434])).
% 0.16/0.85 fof(f487,plain,(
% 0.16/0.85 e_492=select(a_489,i2)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f482,f61])).
% 0.16/0.85 fof(f488,plain,(
% 0.16/0.85 e_491=select(a_479,i2)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f482,f60])).
% 0.16/0.85 fof(f491,plain,(
% 0.16/0.85 e_492=e_488|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f237,f487])).
% 0.16/0.85 fof(f494,plain,(
% 0.16/0.85 ~e_491=e_488|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f491,f63])).
% 0.16/0.85 fof(f502,plain,(
% 0.16/0.85 a_480=store(a_467,i0,e_468)|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f434,f416])).
% 0.16/0.85 fof(f505,plain,(
% 0.16/0.85 a_480=a_469|i0=i2|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f37,f502])).
% 0.16/0.85 fof(f506,plain,(
% 0.16/0.85 a_480=a_469|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f505])).
% 0.16/0.85 fof(f509,plain,(
% 0.16/0.85 a_481=store(a_469,i0,e_468)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f506,f44])).
% 0.16/0.85 fof(f514,plain,(
% 0.16/0.85 e_491=e_476|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f147,f488])).
% 0.16/0.85 fof(f518,plain,(
% 0.16/0.85 e_491=e_476|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f514])).
% 0.16/0.85 fof(f521,plain,(
% 0.16/0.85 ~e_476=e_488|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f518,f494])).
% 0.16/0.85 fof(f524,plain,(
% 0.16/0.85 ~e_476=e_488|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f521])).
% 0.16/0.85 fof(f536,plain,(
% 0.16/0.85 a_471=store(a_469,i0,e_468)|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f434,f421])).
% 0.16/0.85 fof(f539,plain,(
% 0.16/0.85 a_471=store(a_469,i0,e_468)|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f536])).
% 0.16/0.85 fof(f586,plain,(
% 0.16/0.85 a_471=a_481|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f509,f539])).
% 0.16/0.85 fof(f590,plain,(
% 0.16/0.85 a_471=a_481|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f586])).
% 0.16/0.85 fof(f596,plain,(
% 0.16/0.85 a_483=store(a_471,i3,e_482)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f590,f45])).
% 0.16/0.85 fof(f598,plain,(
% 0.16/0.85 e_484=select(a_471,i3)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f590,f57])).
% 0.16/0.85 fof(f599,plain,(
% 0.16/0.85 e_482=select(a_471,i2)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f590,f56])).
% 0.16/0.85 fof(f604,plain,(
% 0.16/0.85 e_484=e_470|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f67,f598])).
% 0.16/0.85 fof(f605,plain,(
% 0.16/0.85 e_482=e_472|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f52,f599])).
% 0.16/0.85 fof(f610,plain,(
% 0.16/0.85 a_485=store(a_483,i2,e_470)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f604,f46])).
% 0.16/0.85 fof(f648,plain,(
% 0.16/0.85 a_483=store(a_471,i3,e_472)|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f605,f596])).
% 0.16/0.85 fof(f652,plain,(
% 0.16/0.85 a_483=a_473|i0=i2|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f39,f648])).
% 0.16/0.85 fof(f653,plain,(
% 0.16/0.85 a_483=a_473|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f652])).
% 0.16/0.85 fof(f701,plain,(
% 0.16/0.85 a_485=store(a_473,i2,e_470)|i0=i2|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f653,f610])).
% 0.16/0.85 fof(f706,plain,(
% 0.16/0.85 a_485=a_475|i0=i2|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f70,f701])).
% 0.16/0.85 fof(f707,plain,(
% 0.16/0.85 a_485=a_475|i0=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f706])).
% 0.16/0.85 fof(f720,plain,(
% 0.16/0.85 e_488=select(a_475,i0)|i0=i2),
% 0.16/0.85 inference(paramodulation,[status(thm)],[f707,f59])).
% 0.16/0.85 fof(f725,plain,(
% 0.16/0.85 e_488=e_476|i0=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f54,f720])).
% 0.16/0.85 fof(f1433,plain,(
% 0.16/0.85 ~e_472=e_482|i2=i_490|i2=i_490),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f290])).
% 0.16/0.85 fof(f1439,plain,(
% 0.16/0.85 i2=i_490|~i3=i0|i_490=i2),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f269])).
% 0.16/0.85 fof(f1449,plain,(
% 0.16/0.85 select(a_481,i2)=e_468),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f164])).
% 0.16/0.85 fof(f1453,plain,(
% 0.16/0.85 i2=i3|e_484=e_470),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f169])).
% 0.16/0.85 fof(f1456,plain,(
% 0.16/0.85 select(a_479,i2)=e_470),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f156])).
% 0.16/0.85 fof(f1462,plain,(
% 0.16/0.85 i3=i0|select(a_471,i2)=e_468),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f92])).
% 0.16/0.85 fof(f1466,plain,(
% 0.16/0.85 e_488=select(a_485,i2)),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f59])).
% 0.16/0.85 fof(f1468,plain,(
% 0.16/0.85 e_470=select(a_467,i2)),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1469,f51])).
% 0.16/0.85 fof(f1469,plain,(
% 0.16/0.85 i0=i2),
% 0.16/0.85 inference(forward_subsumption_resolution,[status(thm)],[f524,f725])).
% 0.16/0.85 fof(f1472,plain,(
% 0.16/0.85 ~e_472=e_482|i2=i_490),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f1433])).
% 0.16/0.85 fof(f1478,plain,(
% 0.16/0.85 i2=i_490|~i3=i2|i_490=i2),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f1469,f1439])).
% 0.16/0.85 fof(f1479,plain,(
% 0.16/0.85 i2=i_490|~i3=i2),
% 0.16/0.85 inference(duplicate_literals_removal,[status(thm)],[f1478])).
% 0.16/0.85 fof(f1487,plain,(
% 0.16/0.85 i3=i2|select(a_471,i2)=e_468),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f1469,f1462])).
% 0.16/0.85 fof(f1488,plain,(
% 0.16/0.85 i3=i2|e_472=e_468),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f52,f1487])).
% 0.16/0.85 fof(f1489,plain,(
% 0.16/0.85 e_488=e_484),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f188,f1466])).
% 0.16/0.85 fof(f1491,plain,(
% 0.16/0.85 select(a_489,i2)=e_484),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1489,f237])).
% 0.16/0.85 fof(f1499,plain,(
% 0.16/0.85 e_482=e_468),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1449,f56])).
% 0.16/0.85 fof(f1501,plain,(
% 0.16/0.85 ~e_472=e_468|i2=i_490),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1499,f1472])).
% 0.16/0.85 fof(f1553,plain,(
% 0.16/0.85 i3=i2|i2=i_490),
% 0.16/0.85 inference(resolution,[status(thm)],[f1488,f1501])).
% 0.16/0.85 fof(f1556,plain,(
% 0.16/0.85 i2=i_490),
% 0.16/0.85 inference(forward_subsumption_resolution,[status(thm)],[f1553,f1479])).
% 0.16/0.85 fof(f1655,plain,(
% 0.16/0.85 e_492=select(a_489,i2)),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1556,f61])).
% 0.16/0.85 fof(f1656,plain,(
% 0.16/0.85 e_491=select(a_479,i2)),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1556,f60])).
% 0.16/0.85 fof(f1657,plain,(
% 0.16/0.85 e_492=e_484),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f1491,f1655])).
% 0.16/0.85 fof(f1658,plain,(
% 0.16/0.85 e_491=e_470),
% 0.16/0.85 inference(forward_demodulation,[status(thm)],[f1456,f1656])).
% 0.16/0.85 fof(f1659,plain,(
% 0.16/0.85 ~e_491=e_484),
% 0.16/0.85 inference(backward_demodulation,[status(thm)],[f1657,f63])).
% 0.51/0.89 fof(f1660,plain,(
% 0.51/0.89 i2=i3),
% 0.51/0.89 inference(backward_subsumption_resolution,[status(thm)],[f1453,f1661])).
% 0.51/0.89 fof(f1661,plain,(
% 0.51/0.89 ~e_470=e_484),
% 0.51/0.89 inference(forward_demodulation,[status(thm)],[f1658,f1659])).
% 0.51/0.89 fof(f1685,plain,(
% 0.51/0.89 e_484=select(a_481,i2)),
% 0.51/0.89 inference(backward_demodulation,[status(thm)],[f1660,f57])).
% 0.51/0.89 fof(f1686,plain,(
% 0.51/0.89 e_468=select(a_467,i2)),
% 0.51/0.89 inference(backward_demodulation,[status(thm)],[f1660,f50])).
% 0.51/0.89 fof(f1691,plain,(
% 0.51/0.89 e_484=e_468),
% 0.51/0.89 inference(forward_demodulation,[status(thm)],[f1449,f1685])).
% 0.51/0.89 fof(f1718,plain,(
% 0.51/0.89 ~e_470=e_468),
% 0.51/0.89 inference(backward_demodulation,[status(thm)],[f1691,f1661])).
% 0.51/0.89 fof(f1751,plain,(
% 0.51/0.89 e_470=e_468),
% 0.51/0.89 inference(backward_demodulation,[status(thm)],[f1686,f1468])).
% 0.51/0.89 fof(f1752,plain,(
% 0.51/0.89 $false),
% 0.51/0.89 inference(forward_subsumption_resolution,[status(thm)],[f1751,f1718])).
% 0.51/0.89 % SZS output end CNFRefutation for theBenchmark.p
% 0.51/0.89 % Elapsed time: 0.462700 seconds
% 0.51/0.89 % CPU time: 3.143360 seconds
% 0.51/0.89 % Total memory used: 128.745 MB
% 0.51/0.89 % Net memory used: 127.009 MB
%------------------------------------------------------------------------------