%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV568-1.030 : 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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:52:49 PM UTC 2026
% Result : Unsatisfiable 6.63s 6.22s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/5.32 % Computer : n012.cluster.edu
% 0.04/5.32 % Model : x86_64 x86_64
% 0.04/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/5.32 % Memory : 8046.5625MB
% 0.04/5.32 % OS : Linux 6.8.0-71-generic
% 0.04/5.32 % CPULimit : 300
% 0.04/5.32 % WCLimit : 300
% 0.04/5.32 % DateTime : Mon Sep 21 09:10:30 UTC 2026
% 0.04/5.32 % CPUTime :
% 0.04/5.33 % Drodi V4.1.1
% 6.63/6.22 % Refutation found
% 6.63/6.22 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.63/6.22 % SZS output start CNFRefutation for theBenchmark
% 6.63/6.22 fof(f1,axiom,(
% 6.63/6.22 (![A,I,E]: (select(store(A,I,E),I) = E ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f2,axiom,(
% 6.63/6.22 (![I,J,A,E]: (( I = J| select(store(A,I,E),J) = select(A,J) ) ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f3,axiom,(
% 6.63/6.22 (![A,E]: (rselect_seq(rstore_seq(A,E)) = E ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f4,axiom,(
% 6.63/6.22 (![A,E]: (rselect_head(rstore_head(A,E)) = E ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f5,axiom,(
% 6.63/6.22 (![A,E]: (rselect_tail(rstore_tail(A,E)) = E ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f6,axiom,(
% 6.63/6.22 (![A,E]: (rselect_seq(rstore_head(A,E)) = rselect_seq(A) ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f7,axiom,(
% 6.63/6.22 (![A,E]: (rselect_seq(rstore_tail(A,E)) = rselect_seq(A) ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f8,axiom,(
% 6.63/6.22 (![A,E]: (rselect_head(rstore_tail(A,E)) = rselect_head(A) ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f9,axiom,(
% 6.63/6.22 (![A,E]: (rselect_head(rstore_seq(A,E)) = rselect_head(A) ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f11,axiom,(
% 6.63/6.22 (![A,E]: (rselect_tail(rstore_head(A,E)) = rselect_tail(A) ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f43,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f44,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f45,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f46,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f47,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f48,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f49,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f50,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f51,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f52,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(s(X)))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f53,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(s(X))))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f54,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(s(X)))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f55,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(s(X))))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f56,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(s(X)))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f57,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(s(X))))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f58,axiom,(
% 6.63/6.22 (![X]: (s(s(s(s(X)))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f59,axiom,(
% 6.63/6.22 (![X]: (s(s(s(X))) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f60,axiom,(
% 6.63/6.22 (![X]: (s(s(X)) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f61,axiom,(
% 6.63/6.22 (![X]: (s(X) != X ))),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.22 fof(f63,hypothesis,(
% 6.63/6.22 earray_100 = store(earray_98,index_99,e21) ),
% 6.63/6.22 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f64,hypothesis,(
% 6.63/6.23 earray_104 = rselect_seq(q22) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f65,hypothesis,(
% 6.63/6.23 earray_106 = store(earray_104,index_105,e22) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f66,hypothesis,(
% 6.63/6.23 earray_110 = rselect_seq(q23) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f67,hypothesis,(
% 6.63/6.23 earray_112 = store(earray_110,index_111,e23) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f68,hypothesis,(
% 6.63/6.23 earray_119 = rselect_seq(q24) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f69,hypothesis,(
% 6.63/6.23 earray_121 = store(earray_119,index_120,e24) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f70,hypothesis,(
% 6.63/6.23 earray_125 = rselect_seq(q25) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f71,hypothesis,(
% 6.63/6.23 earray_127 = store(earray_125,index_126,e25) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f72,hypothesis,(
% 6.63/6.23 earray_131 = rselect_seq(q26) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f73,hypothesis,(
% 6.63/6.23 earray_133 = store(earray_131,index_132,e26) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f75,hypothesis,(
% 6.63/6.23 earray_140 = rselect_seq(q27) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f76,hypothesis,(
% 6.63/6.23 earray_142 = store(earray_140,index_141,e27) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f77,hypothesis,(
% 6.63/6.23 earray_146 = rselect_seq(q28) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f78,hypothesis,(
% 6.63/6.23 earray_148 = store(earray_146,index_147,e28) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f81,hypothesis,(
% 6.63/6.23 earray_16 = store(earray_14,index_15,e10) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f82,hypothesis,(
% 6.63/6.23 earray_161 = rselect_seq(q29) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f83,hypothesis,(
% 6.63/6.23 earray_163 = store(earray_161,index_162,e29) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f95,hypothesis,(
% 6.63/6.23 earray_20 = rselect_seq(q11) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f98,hypothesis,(
% 6.63/6.23 earray_212 = rselect_seq(q30) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f99,hypothesis,(
% 6.63/6.23 earray_22 = store(earray_20,index_21,e11) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f100,hypothesis,(
% 6.63/6.23 earray_29 = rselect_seq(q12) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f101,hypothesis,(
% 6.63/6.23 earray_31 = store(earray_29,index_30,e12) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f102,hypothesis,(
% 6.63/6.23 earray_35 = rselect_seq(q13) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f103,hypothesis,(
% 6.63/6.23 earray_37 = store(earray_35,index_36,e13) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f105,hypothesis,(
% 6.63/6.23 earray_41 = rselect_seq(q14) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f106,hypothesis,(
% 6.63/6.23 earray_43 = store(earray_41,index_42,e14) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f107,hypothesis,(
% 6.63/6.23 earray_50 = rselect_seq(q15) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f108,hypothesis,(
% 6.63/6.23 earray_52 = store(earray_50,index_51,e15) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f109,hypothesis,(
% 6.63/6.23 earray_56 = rselect_seq(q16) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f110,hypothesis,(
% 6.63/6.23 earray_58 = store(earray_56,index_57,e16) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f111,hypothesis,(
% 6.63/6.23 earray_62 = rselect_seq(q17) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f112,hypothesis,(
% 6.63/6.23 earray_64 = store(earray_62,index_63,e17) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f113,hypothesis,(
% 6.63/6.23 earray_71 = rselect_seq(q18) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f114,hypothesis,(
% 6.63/6.23 earray_73 = store(earray_71,index_72,e18) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f118,hypothesis,(
% 6.63/6.23 earray_83 = rselect_seq(q19) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f119,hypothesis,(
% 6.63/6.23 earray_85 = store(earray_83,index_84,e19) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f120,hypothesis,(
% 6.63/6.23 earray_89 = rselect_seq(q20) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f121,hypothesis,(
% 6.63/6.23 earray_91 = store(earray_89,index_90,e20) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f122,hypothesis,(
% 6.63/6.23 earray_98 = rselect_seq(q21) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f123,hypothesis,(
% 6.63/6.23 elem_214 = select(earray_212,index_213) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f124,hypothesis,(
% 6.63/6.23 index_0 = rselect_tail(q) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f125,hypothesis,(
% 6.63/6.23 index_102 = s(index_99) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f126,hypothesis,(
% 6.63/6.23 index_105 = rselect_tail(q22) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f127,hypothesis,(
% 6.63/6.23 index_108 = s(index_105) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f128,hypothesis,(
% 6.63/6.23 index_111 = rselect_tail(q23) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f129,hypothesis,(
% 6.63/6.23 index_114 = s(index_111) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f130,hypothesis,(
% 6.63/6.23 index_116 = rselect_head(queue_115) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f131,hypothesis,(
% 6.63/6.23 index_117 = s(index_116) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f132,hypothesis,(
% 6.63/6.23 index_12 = s(index_9) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f133,hypothesis,(
% 6.63/6.23 index_120 = rselect_tail(q24) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f134,hypothesis,(
% 6.63/6.23 index_123 = s(index_120) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f135,hypothesis,(
% 6.63/6.23 index_126 = rselect_tail(q25) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f136,hypothesis,(
% 6.63/6.23 index_129 = s(index_126) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f137,hypothesis,(
% 6.63/6.23 index_132 = rselect_tail(q26) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f138,hypothesis,(
% 6.63/6.23 index_135 = s(index_132) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f139,hypothesis,(
% 6.63/6.23 index_137 = rselect_head(queue_136) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f140,hypothesis,(
% 6.63/6.23 index_138 = s(index_137) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f141,hypothesis,(
% 6.63/6.23 index_141 = rselect_tail(q27) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f142,hypothesis,(
% 6.63/6.23 index_144 = s(index_141) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f143,hypothesis,(
% 6.63/6.23 index_147 = rselect_tail(q28) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f144,hypothesis,(
% 6.63/6.23 index_15 = rselect_tail(q10) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f145,hypothesis,(
% 6.63/6.23 index_150 = s(index_147) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f146,hypothesis,(
% 6.63/6.23 index_153 = rselect_tail(q2) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f147,hypothesis,(
% 6.63/6.23 index_156 = s(index_153) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f148,hypothesis,(
% 6.63/6.23 index_158 = rselect_head(queue_157) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f149,hypothesis,(
% 6.63/6.23 index_159 = s(index_158) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f150,hypothesis,(
% 6.63/6.23 index_162 = rselect_tail(q29) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f152,hypothesis,(
% 6.63/6.23 index_167 = rselect_head(queue_166) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f153,hypothesis,(
% 6.63/6.23 index_168 = s(index_167) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f154,hypothesis,(
% 6.63/6.23 index_171 = rselect_tail(q3) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f155,hypothesis,(
% 6.63/6.23 index_174 = s(index_171) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f156,hypothesis,(
% 6.63/6.23 index_177 = rselect_tail(q4) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f157,hypothesis,(
% 6.63/6.23 index_18 = s(index_15) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f158,hypothesis,(
% 6.63/6.23 index_180 = s(index_177) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f159,hypothesis,(
% 6.63/6.23 index_183 = rselect_tail(q5) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f160,hypothesis,(
% 6.63/6.23 index_186 = s(index_183) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f161,hypothesis,(
% 6.63/6.23 index_188 = rselect_head(queue_187) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f162,hypothesis,(
% 6.63/6.23 index_189 = s(index_188) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f163,hypothesis,(
% 6.63/6.23 index_192 = rselect_tail(q6) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f164,hypothesis,(
% 6.63/6.23 index_195 = s(index_192) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f165,hypothesis,(
% 6.63/6.23 index_198 = rselect_tail(q7) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f166,hypothesis,(
% 6.63/6.23 index_201 = s(index_198) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f167,hypothesis,(
% 6.63/6.23 index_204 = rselect_tail(q8) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f168,hypothesis,(
% 6.63/6.23 index_207 = s(index_204) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f169,hypothesis,(
% 6.63/6.23 index_209 = rselect_head(queue_208) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f170,hypothesis,(
% 6.63/6.23 index_21 = rselect_tail(q11) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f171,hypothesis,(
% 6.63/6.23 index_210 = s(index_209) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f172,hypothesis,(
% 6.63/6.23 index_213 = rselect_head(q30) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f173,hypothesis,(
% 6.63/6.23 index_24 = s(index_21) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f174,hypothesis,(
% 6.63/6.23 index_26 = rselect_head(queue_25) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f175,hypothesis,(
% 6.63/6.23 index_27 = s(index_26) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f176,hypothesis,(
% 6.63/6.23 index_3 = rselect_tail(q0) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f177,hypothesis,(
% 6.63/6.23 index_30 = rselect_tail(q12) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f178,hypothesis,(
% 6.63/6.23 index_33 = s(index_30) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f179,hypothesis,(
% 6.63/6.23 index_36 = rselect_tail(q13) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f180,hypothesis,(
% 6.63/6.23 index_39 = s(index_36) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f181,hypothesis,(
% 6.63/6.23 index_42 = rselect_tail(q14) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f182,hypothesis,(
% 6.63/6.23 index_45 = s(index_42) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f183,hypothesis,(
% 6.63/6.23 index_47 = rselect_head(queue_46) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f184,hypothesis,(
% 6.63/6.23 index_48 = s(index_47) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f185,hypothesis,(
% 6.63/6.23 index_51 = rselect_tail(q15) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f186,hypothesis,(
% 6.63/6.23 index_54 = s(index_51) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f187,hypothesis,(
% 6.63/6.23 index_57 = rselect_tail(q16) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f188,hypothesis,(
% 6.63/6.23 index_6 = s(index_3) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f189,hypothesis,(
% 6.63/6.23 index_60 = s(index_57) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f190,hypothesis,(
% 6.63/6.23 index_63 = rselect_tail(q17) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f191,hypothesis,(
% 6.63/6.23 index_66 = s(index_63) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f192,hypothesis,(
% 6.63/6.23 index_68 = rselect_head(queue_67) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f193,hypothesis,(
% 6.63/6.23 index_69 = s(index_68) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f194,hypothesis,(
% 6.63/6.23 index_72 = rselect_tail(q18) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f195,hypothesis,(
% 6.63/6.23 index_75 = s(index_72) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f196,hypothesis,(
% 6.63/6.23 index_78 = rselect_tail(q1) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f197,hypothesis,(
% 6.63/6.23 index_81 = s(index_78) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f198,hypothesis,(
% 6.63/6.23 index_84 = rselect_tail(q19) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f199,hypothesis,(
% 6.63/6.23 index_87 = s(index_84) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f200,hypothesis,(
% 6.63/6.23 index_9 = rselect_tail(q9) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f201,hypothesis,(
% 6.63/6.23 index_90 = rselect_tail(q20) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f202,hypothesis,(
% 6.63/6.23 index_93 = s(index_90) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f203,hypothesis,(
% 6.63/6.23 index_95 = rselect_head(queue_94) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f204,hypothesis,(
% 6.63/6.23 index_96 = s(index_95) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f205,hypothesis,(
% 6.63/6.23 index_99 = rselect_tail(q21) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f206,hypothesis,(
% 6.63/6.23 queue_1 = rstore_head(q,index_0) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f207,hypothesis,(
% 6.63/6.23 queue_101 = rstore_seq(q21,earray_100) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f208,hypothesis,(
% 6.63/6.23 queue_103 = rstore_tail(queue_101,index_102) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f209,hypothesis,(
% 6.63/6.23 queue_107 = rstore_seq(q22,earray_106) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f210,hypothesis,(
% 6.63/6.23 queue_109 = rstore_tail(queue_107,index_108) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f211,hypothesis,(
% 6.63/6.23 queue_11 = rstore_seq(q9,earray_10) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f212,hypothesis,(
% 6.63/6.23 queue_113 = rstore_seq(q23,earray_112) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f213,hypothesis,(
% 6.63/6.23 queue_115 = rstore_tail(queue_113,index_114) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f214,hypothesis,(
% 6.63/6.23 queue_118 = rstore_head(queue_115,index_117) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f215,hypothesis,(
% 6.63/6.23 queue_122 = rstore_seq(q24,earray_121) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f216,hypothesis,(
% 6.63/6.23 queue_124 = rstore_tail(queue_122,index_123) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f217,hypothesis,(
% 6.63/6.23 queue_128 = rstore_seq(q25,earray_127) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f218,hypothesis,(
% 6.63/6.23 queue_13 = rstore_tail(queue_11,index_12) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f219,hypothesis,(
% 6.63/6.23 queue_130 = rstore_tail(queue_128,index_129) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f220,hypothesis,(
% 6.63/6.23 queue_134 = rstore_seq(q26,earray_133) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f221,hypothesis,(
% 6.63/6.23 queue_136 = rstore_tail(queue_134,index_135) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f222,hypothesis,(
% 6.63/6.23 queue_139 = rstore_head(queue_136,index_138) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f223,hypothesis,(
% 6.63/6.23 queue_143 = rstore_seq(q27,earray_142) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f224,hypothesis,(
% 6.63/6.23 queue_145 = rstore_tail(queue_143,index_144) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f225,hypothesis,(
% 6.63/6.23 queue_149 = rstore_seq(q28,earray_148) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f226,hypothesis,(
% 6.63/6.23 queue_151 = rstore_tail(queue_149,index_150) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f227,hypothesis,(
% 6.63/6.23 queue_155 = rstore_seq(q2,earray_154) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f228,hypothesis,(
% 6.63/6.23 queue_157 = rstore_tail(queue_155,index_156) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f229,hypothesis,(
% 6.63/6.23 queue_160 = rstore_head(queue_157,index_159) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f230,hypothesis,(
% 6.63/6.23 queue_164 = rstore_seq(q29,earray_163) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f231,hypothesis,(
% 6.63/6.23 queue_166 = rstore_tail(queue_164,index_165) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f232,hypothesis,(
% 6.63/6.23 queue_169 = rstore_head(queue_166,index_168) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f233,hypothesis,(
% 6.63/6.23 queue_17 = rstore_seq(q10,earray_16) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f234,hypothesis,(
% 6.63/6.23 queue_173 = rstore_seq(q3,earray_172) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f235,hypothesis,(
% 6.63/6.23 queue_175 = rstore_tail(queue_173,index_174) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f236,hypothesis,(
% 6.63/6.23 queue_179 = rstore_seq(q4,earray_178) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f237,hypothesis,(
% 6.63/6.23 queue_181 = rstore_tail(queue_179,index_180) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f238,hypothesis,(
% 6.63/6.23 queue_185 = rstore_seq(q5,earray_184) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f239,hypothesis,(
% 6.63/6.23 queue_187 = rstore_tail(queue_185,index_186) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f240,hypothesis,(
% 6.63/6.23 queue_19 = rstore_tail(queue_17,index_18) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f241,hypothesis,(
% 6.63/6.23 queue_190 = rstore_head(queue_187,index_189) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f242,hypothesis,(
% 6.63/6.23 queue_194 = rstore_seq(q6,earray_193) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f243,hypothesis,(
% 6.63/6.23 queue_196 = rstore_tail(queue_194,index_195) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f244,hypothesis,(
% 6.63/6.23 queue_200 = rstore_seq(q7,earray_199) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f245,hypothesis,(
% 6.63/6.23 queue_202 = rstore_tail(queue_200,index_201) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f246,hypothesis,(
% 6.63/6.23 queue_206 = rstore_seq(q8,earray_205) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f247,hypothesis,(
% 6.63/6.23 queue_208 = rstore_tail(queue_206,index_207) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f248,hypothesis,(
% 6.63/6.23 queue_211 = rstore_head(queue_208,index_210) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f249,hypothesis,(
% 6.63/6.23 queue_23 = rstore_seq(q11,earray_22) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f250,hypothesis,(
% 6.63/6.23 queue_25 = rstore_tail(queue_23,index_24) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f251,hypothesis,(
% 6.63/6.23 queue_28 = rstore_head(queue_25,index_27) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f252,hypothesis,(
% 6.63/6.23 queue_32 = rstore_seq(q12,earray_31) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f253,hypothesis,(
% 6.63/6.23 queue_34 = rstore_tail(queue_32,index_33) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f254,hypothesis,(
% 6.63/6.23 queue_38 = rstore_seq(q13,earray_37) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f255,hypothesis,(
% 6.63/6.23 queue_40 = rstore_tail(queue_38,index_39) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f256,hypothesis,(
% 6.63/6.23 queue_44 = rstore_seq(q14,earray_43) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f257,hypothesis,(
% 6.63/6.23 queue_46 = rstore_tail(queue_44,index_45) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f258,hypothesis,(
% 6.63/6.23 queue_49 = rstore_head(queue_46,index_48) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f259,hypothesis,(
% 6.63/6.23 queue_5 = rstore_seq(q0,earray_4) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f260,hypothesis,(
% 6.63/6.23 queue_53 = rstore_seq(q15,earray_52) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f261,hypothesis,(
% 6.63/6.23 queue_55 = rstore_tail(queue_53,index_54) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f262,hypothesis,(
% 6.63/6.23 queue_59 = rstore_seq(q16,earray_58) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f263,hypothesis,(
% 6.63/6.23 queue_61 = rstore_tail(queue_59,index_60) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f264,hypothesis,(
% 6.63/6.23 queue_65 = rstore_seq(q17,earray_64) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f265,hypothesis,(
% 6.63/6.23 queue_67 = rstore_tail(queue_65,index_66) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f266,hypothesis,(
% 6.63/6.23 queue_7 = rstore_tail(queue_5,index_6) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f267,hypothesis,(
% 6.63/6.23 queue_70 = rstore_head(queue_67,index_69) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f268,hypothesis,(
% 6.63/6.23 queue_74 = rstore_seq(q18,earray_73) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f269,hypothesis,(
% 6.63/6.23 queue_76 = rstore_tail(queue_74,index_75) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f270,hypothesis,(
% 6.63/6.23 queue_80 = rstore_seq(q1,earray_79) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f271,hypothesis,(
% 6.63/6.23 queue_82 = rstore_tail(queue_80,index_81) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f272,hypothesis,(
% 6.63/6.23 queue_86 = rstore_seq(q19,earray_85) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f273,hypothesis,(
% 6.63/6.23 queue_88 = rstore_tail(queue_86,index_87) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f274,hypothesis,(
% 6.63/6.23 queue_92 = rstore_seq(q20,earray_91) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f275,hypothesis,(
% 6.63/6.23 queue_94 = rstore_tail(queue_92,index_93) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f276,hypothesis,(
% 6.63/6.23 queue_97 = rstore_head(queue_94,index_96) ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f277,hypothesis,(
% 6.63/6.23 q0 = queue_1 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f278,hypothesis,(
% 6.63/6.23 q1 = queue_7 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f279,hypothesis,(
% 6.63/6.23 q10 = queue_13 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f280,hypothesis,(
% 6.63/6.23 q11 = queue_19 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f281,hypothesis,(
% 6.63/6.23 q12 = queue_28 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f282,hypothesis,(
% 6.63/6.23 q13 = queue_34 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f283,hypothesis,(
% 6.63/6.23 q14 = queue_40 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f284,hypothesis,(
% 6.63/6.23 q15 = queue_49 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f285,hypothesis,(
% 6.63/6.23 q16 = queue_55 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f286,hypothesis,(
% 6.63/6.23 q17 = queue_61 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f287,hypothesis,(
% 6.63/6.23 q18 = queue_70 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f288,hypothesis,(
% 6.63/6.23 q19 = queue_76 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f289,hypothesis,(
% 6.63/6.23 q2 = queue_82 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f290,hypothesis,(
% 6.63/6.23 q20 = queue_88 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f291,hypothesis,(
% 6.63/6.23 q21 = queue_97 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f292,hypothesis,(
% 6.63/6.23 q22 = queue_103 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f293,hypothesis,(
% 6.63/6.23 q23 = queue_109 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f294,hypothesis,(
% 6.63/6.23 q24 = queue_118 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f295,hypothesis,(
% 6.63/6.23 q25 = queue_124 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f296,hypothesis,(
% 6.63/6.23 q26 = queue_130 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f297,hypothesis,(
% 6.63/6.23 q27 = queue_139 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f298,hypothesis,(
% 6.63/6.23 q28 = queue_145 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f299,hypothesis,(
% 6.63/6.23 q29 = queue_151 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f300,hypothesis,(
% 6.63/6.23 q3 = queue_160 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f301,hypothesis,(
% 6.63/6.23 q30 = queue_169 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f302,hypothesis,(
% 6.63/6.23 q4 = queue_175 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f303,hypothesis,(
% 6.63/6.23 q5 = queue_181 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f304,hypothesis,(
% 6.63/6.23 q6 = queue_190 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f305,hypothesis,(
% 6.63/6.23 q7 = queue_196 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f306,hypothesis,(
% 6.63/6.23 q8 = queue_202 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f307,hypothesis,(
% 6.63/6.23 q9 = queue_211 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f308,negated_conjecture,(
% 6.63/6.23 elem_214 != e10 ),
% 6.63/6.23 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.63/6.23 fof(f309,plain,(
% 6.63/6.23 ![X0,X1,X2]: (select(store(X0,X1,X2),X1)=X2)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f1])).
% 6.63/6.23 fof(f310,plain,(
% 6.63/6.23 ![I,J]: (I=J|(![A,E]: select(store(A,I,E),J)=select(A,J)))),
% 6.63/6.23 inference(miniscoping,[status(thm)],[f2])).
% 6.63/6.23 fof(f311,plain,(
% 6.63/6.23 ![X0,X1,X2,X3]: (X0=X1|select(store(X2,X0,X3),X1)=select(X2,X1))),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f310])).
% 6.63/6.23 fof(f312,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_seq(rstore_seq(X0,X1))=X1)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f3])).
% 6.63/6.23 fof(f313,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_head(rstore_head(X0,X1))=X1)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f4])).
% 6.63/6.23 fof(f314,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_tail(rstore_tail(X0,X1))=X1)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f5])).
% 6.63/6.23 fof(f315,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_seq(rstore_head(X0,X1))=rselect_seq(X0))),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f6])).
% 6.63/6.23 fof(f316,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_seq(rstore_tail(X0,X1))=rselect_seq(X0))),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f7])).
% 6.63/6.23 fof(f317,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_head(rstore_tail(X0,X1))=rselect_head(X0))),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f8])).
% 6.63/6.23 fof(f318,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_head(rstore_seq(X0,X1))=rselect_head(X0))),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f9])).
% 6.63/6.23 fof(f320,plain,(
% 6.63/6.23 ![X0,X1]: (rselect_tail(rstore_head(X0,X1))=rselect_tail(X0))),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f11])).
% 6.63/6.23 fof(f352,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f43])).
% 6.63/6.23 fof(f353,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f44])).
% 6.63/6.23 fof(f354,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f45])).
% 6.63/6.23 fof(f355,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f46])).
% 6.63/6.23 fof(f356,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f47])).
% 6.63/6.23 fof(f357,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f48])).
% 6.63/6.23 fof(f358,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f49])).
% 6.63/6.23 fof(f359,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f50])).
% 6.63/6.23 fof(f360,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f51])).
% 6.63/6.23 fof(f361,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(s(X0))))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f52])).
% 6.63/6.23 fof(f362,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(s(X0)))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f53])).
% 6.63/6.23 fof(f363,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(s(X0))))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f54])).
% 6.63/6.23 fof(f364,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(s(X0)))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f55])).
% 6.63/6.23 fof(f365,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(s(X0))))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f56])).
% 6.63/6.23 fof(f366,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(s(X0)))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f57])).
% 6.63/6.23 fof(f367,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(s(X0))))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f58])).
% 6.63/6.23 fof(f368,plain,(
% 6.63/6.23 ![X0]: (~s(s(s(X0)))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f59])).
% 6.63/6.23 fof(f369,plain,(
% 6.63/6.23 ![X0]: (~s(s(X0))=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f60])).
% 6.63/6.23 fof(f370,plain,(
% 6.63/6.23 ![X0]: (~s(X0)=X0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f61])).
% 6.63/6.23 fof(f372,plain,(
% 6.63/6.23 earray_100=store(earray_98,index_99,e21)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f63])).
% 6.63/6.23 fof(f373,plain,(
% 6.63/6.23 earray_104=rselect_seq(q22)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f64])).
% 6.63/6.23 fof(f374,plain,(
% 6.63/6.23 earray_106=store(earray_104,index_105,e22)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f65])).
% 6.63/6.23 fof(f375,plain,(
% 6.63/6.23 earray_110=rselect_seq(q23)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f66])).
% 6.63/6.23 fof(f376,plain,(
% 6.63/6.23 earray_112=store(earray_110,index_111,e23)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f67])).
% 6.63/6.23 fof(f377,plain,(
% 6.63/6.23 earray_119=rselect_seq(q24)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f68])).
% 6.63/6.23 fof(f378,plain,(
% 6.63/6.23 earray_121=store(earray_119,index_120,e24)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f69])).
% 6.63/6.23 fof(f379,plain,(
% 6.63/6.23 earray_125=rselect_seq(q25)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f70])).
% 6.63/6.23 fof(f380,plain,(
% 6.63/6.23 earray_127=store(earray_125,index_126,e25)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f71])).
% 6.63/6.23 fof(f381,plain,(
% 6.63/6.23 earray_131=rselect_seq(q26)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f72])).
% 6.63/6.23 fof(f382,plain,(
% 6.63/6.23 earray_133=store(earray_131,index_132,e26)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f73])).
% 6.63/6.23 fof(f384,plain,(
% 6.63/6.23 earray_140=rselect_seq(q27)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f75])).
% 6.63/6.23 fof(f385,plain,(
% 6.63/6.23 earray_142=store(earray_140,index_141,e27)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f76])).
% 6.63/6.23 fof(f386,plain,(
% 6.63/6.23 earray_146=rselect_seq(q28)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f77])).
% 6.63/6.23 fof(f387,plain,(
% 6.63/6.23 earray_148=store(earray_146,index_147,e28)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f78])).
% 6.63/6.23 fof(f390,plain,(
% 6.63/6.23 earray_16=store(earray_14,index_15,e10)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f81])).
% 6.63/6.23 fof(f391,plain,(
% 6.63/6.23 earray_161=rselect_seq(q29)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f82])).
% 6.63/6.23 fof(f392,plain,(
% 6.63/6.23 earray_163=store(earray_161,index_162,e29)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f83])).
% 6.63/6.23 fof(f404,plain,(
% 6.63/6.23 earray_20=rselect_seq(q11)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f95])).
% 6.63/6.23 fof(f407,plain,(
% 6.63/6.23 earray_212=rselect_seq(q30)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f98])).
% 6.63/6.23 fof(f408,plain,(
% 6.63/6.23 earray_22=store(earray_20,index_21,e11)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f99])).
% 6.63/6.23 fof(f409,plain,(
% 6.63/6.23 earray_29=rselect_seq(q12)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f100])).
% 6.63/6.23 fof(f410,plain,(
% 6.63/6.23 earray_31=store(earray_29,index_30,e12)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f101])).
% 6.63/6.23 fof(f411,plain,(
% 6.63/6.23 earray_35=rselect_seq(q13)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f102])).
% 6.63/6.23 fof(f412,plain,(
% 6.63/6.23 earray_37=store(earray_35,index_36,e13)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f103])).
% 6.63/6.23 fof(f414,plain,(
% 6.63/6.23 earray_41=rselect_seq(q14)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f105])).
% 6.63/6.23 fof(f415,plain,(
% 6.63/6.23 earray_43=store(earray_41,index_42,e14)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f106])).
% 6.63/6.23 fof(f416,plain,(
% 6.63/6.23 earray_50=rselect_seq(q15)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f107])).
% 6.63/6.23 fof(f417,plain,(
% 6.63/6.23 earray_52=store(earray_50,index_51,e15)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f108])).
% 6.63/6.23 fof(f418,plain,(
% 6.63/6.23 earray_56=rselect_seq(q16)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f109])).
% 6.63/6.23 fof(f419,plain,(
% 6.63/6.23 earray_58=store(earray_56,index_57,e16)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f110])).
% 6.63/6.23 fof(f420,plain,(
% 6.63/6.23 earray_62=rselect_seq(q17)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f111])).
% 6.63/6.23 fof(f421,plain,(
% 6.63/6.23 earray_64=store(earray_62,index_63,e17)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f112])).
% 6.63/6.23 fof(f422,plain,(
% 6.63/6.23 earray_71=rselect_seq(q18)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f113])).
% 6.63/6.23 fof(f423,plain,(
% 6.63/6.23 earray_73=store(earray_71,index_72,e18)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f114])).
% 6.63/6.23 fof(f427,plain,(
% 6.63/6.23 earray_83=rselect_seq(q19)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f118])).
% 6.63/6.23 fof(f428,plain,(
% 6.63/6.23 earray_85=store(earray_83,index_84,e19)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f119])).
% 6.63/6.23 fof(f429,plain,(
% 6.63/6.23 earray_89=rselect_seq(q20)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f120])).
% 6.63/6.23 fof(f430,plain,(
% 6.63/6.23 earray_91=store(earray_89,index_90,e20)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f121])).
% 6.63/6.23 fof(f431,plain,(
% 6.63/6.23 earray_98=rselect_seq(q21)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f122])).
% 6.63/6.23 fof(f432,plain,(
% 6.63/6.23 elem_214=select(earray_212,index_213)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f123])).
% 6.63/6.23 fof(f433,plain,(
% 6.63/6.23 index_0=rselect_tail(q)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f124])).
% 6.63/6.23 fof(f434,plain,(
% 6.63/6.23 index_102=s(index_99)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f125])).
% 6.63/6.23 fof(f435,plain,(
% 6.63/6.23 index_105=rselect_tail(q22)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f126])).
% 6.63/6.23 fof(f436,plain,(
% 6.63/6.23 index_108=s(index_105)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f127])).
% 6.63/6.23 fof(f437,plain,(
% 6.63/6.23 index_111=rselect_tail(q23)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f128])).
% 6.63/6.23 fof(f438,plain,(
% 6.63/6.23 index_114=s(index_111)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f129])).
% 6.63/6.23 fof(f439,plain,(
% 6.63/6.23 index_116=rselect_head(queue_115)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f130])).
% 6.63/6.23 fof(f440,plain,(
% 6.63/6.23 index_117=s(index_116)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f131])).
% 6.63/6.23 fof(f441,plain,(
% 6.63/6.23 index_12=s(index_9)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f132])).
% 6.63/6.23 fof(f442,plain,(
% 6.63/6.23 index_120=rselect_tail(q24)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f133])).
% 6.63/6.23 fof(f443,plain,(
% 6.63/6.23 index_123=s(index_120)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f134])).
% 6.63/6.23 fof(f444,plain,(
% 6.63/6.23 index_126=rselect_tail(q25)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f135])).
% 6.63/6.23 fof(f445,plain,(
% 6.63/6.23 index_129=s(index_126)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f136])).
% 6.63/6.23 fof(f446,plain,(
% 6.63/6.23 index_132=rselect_tail(q26)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f137])).
% 6.63/6.23 fof(f447,plain,(
% 6.63/6.23 index_135=s(index_132)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f138])).
% 6.63/6.23 fof(f448,plain,(
% 6.63/6.23 index_137=rselect_head(queue_136)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f139])).
% 6.63/6.23 fof(f449,plain,(
% 6.63/6.23 index_138=s(index_137)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f140])).
% 6.63/6.23 fof(f450,plain,(
% 6.63/6.23 index_141=rselect_tail(q27)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f141])).
% 6.63/6.23 fof(f451,plain,(
% 6.63/6.23 index_144=s(index_141)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f142])).
% 6.63/6.23 fof(f452,plain,(
% 6.63/6.23 index_147=rselect_tail(q28)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f143])).
% 6.63/6.23 fof(f453,plain,(
% 6.63/6.23 index_15=rselect_tail(q10)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f144])).
% 6.63/6.23 fof(f454,plain,(
% 6.63/6.23 index_150=s(index_147)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f145])).
% 6.63/6.23 fof(f455,plain,(
% 6.63/6.23 index_153=rselect_tail(q2)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f146])).
% 6.63/6.23 fof(f456,plain,(
% 6.63/6.23 index_156=s(index_153)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f147])).
% 6.63/6.23 fof(f457,plain,(
% 6.63/6.23 index_158=rselect_head(queue_157)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f148])).
% 6.63/6.23 fof(f458,plain,(
% 6.63/6.23 index_159=s(index_158)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f149])).
% 6.63/6.23 fof(f459,plain,(
% 6.63/6.23 index_162=rselect_tail(q29)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f150])).
% 6.63/6.23 fof(f461,plain,(
% 6.63/6.23 index_167=rselect_head(queue_166)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f152])).
% 6.63/6.23 fof(f462,plain,(
% 6.63/6.23 index_168=s(index_167)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f153])).
% 6.63/6.23 fof(f463,plain,(
% 6.63/6.23 index_171=rselect_tail(q3)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f154])).
% 6.63/6.23 fof(f464,plain,(
% 6.63/6.23 index_174=s(index_171)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f155])).
% 6.63/6.23 fof(f465,plain,(
% 6.63/6.23 index_177=rselect_tail(q4)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f156])).
% 6.63/6.23 fof(f466,plain,(
% 6.63/6.23 index_18=s(index_15)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f157])).
% 6.63/6.23 fof(f467,plain,(
% 6.63/6.23 index_180=s(index_177)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f158])).
% 6.63/6.23 fof(f468,plain,(
% 6.63/6.23 index_183=rselect_tail(q5)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f159])).
% 6.63/6.23 fof(f469,plain,(
% 6.63/6.23 index_186=s(index_183)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f160])).
% 6.63/6.23 fof(f470,plain,(
% 6.63/6.23 index_188=rselect_head(queue_187)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f161])).
% 6.63/6.23 fof(f471,plain,(
% 6.63/6.23 index_189=s(index_188)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f162])).
% 6.63/6.23 fof(f472,plain,(
% 6.63/6.23 index_192=rselect_tail(q6)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f163])).
% 6.63/6.23 fof(f473,plain,(
% 6.63/6.23 index_195=s(index_192)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f164])).
% 6.63/6.23 fof(f474,plain,(
% 6.63/6.23 index_198=rselect_tail(q7)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f165])).
% 6.63/6.23 fof(f475,plain,(
% 6.63/6.23 index_201=s(index_198)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f166])).
% 6.63/6.23 fof(f476,plain,(
% 6.63/6.23 index_204=rselect_tail(q8)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f167])).
% 6.63/6.23 fof(f477,plain,(
% 6.63/6.23 index_207=s(index_204)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f168])).
% 6.63/6.23 fof(f478,plain,(
% 6.63/6.23 index_209=rselect_head(queue_208)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f169])).
% 6.63/6.23 fof(f479,plain,(
% 6.63/6.23 index_21=rselect_tail(q11)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f170])).
% 6.63/6.23 fof(f480,plain,(
% 6.63/6.23 index_210=s(index_209)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f171])).
% 6.63/6.23 fof(f481,plain,(
% 6.63/6.23 index_213=rselect_head(q30)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f172])).
% 6.63/6.23 fof(f482,plain,(
% 6.63/6.23 index_24=s(index_21)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f173])).
% 6.63/6.23 fof(f483,plain,(
% 6.63/6.23 index_26=rselect_head(queue_25)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f174])).
% 6.63/6.23 fof(f484,plain,(
% 6.63/6.23 index_27=s(index_26)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f175])).
% 6.63/6.23 fof(f485,plain,(
% 6.63/6.23 index_3=rselect_tail(q0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f176])).
% 6.63/6.23 fof(f486,plain,(
% 6.63/6.23 index_30=rselect_tail(q12)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f177])).
% 6.63/6.23 fof(f487,plain,(
% 6.63/6.23 index_33=s(index_30)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f178])).
% 6.63/6.23 fof(f488,plain,(
% 6.63/6.23 index_36=rselect_tail(q13)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f179])).
% 6.63/6.23 fof(f489,plain,(
% 6.63/6.23 index_39=s(index_36)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f180])).
% 6.63/6.23 fof(f490,plain,(
% 6.63/6.23 index_42=rselect_tail(q14)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f181])).
% 6.63/6.23 fof(f491,plain,(
% 6.63/6.23 index_45=s(index_42)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f182])).
% 6.63/6.23 fof(f492,plain,(
% 6.63/6.23 index_47=rselect_head(queue_46)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f183])).
% 6.63/6.23 fof(f493,plain,(
% 6.63/6.23 index_48=s(index_47)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f184])).
% 6.63/6.23 fof(f494,plain,(
% 6.63/6.23 index_51=rselect_tail(q15)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f185])).
% 6.63/6.23 fof(f495,plain,(
% 6.63/6.23 index_54=s(index_51)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f186])).
% 6.63/6.23 fof(f496,plain,(
% 6.63/6.23 index_57=rselect_tail(q16)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f187])).
% 6.63/6.23 fof(f497,plain,(
% 6.63/6.23 index_6=s(index_3)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f188])).
% 6.63/6.23 fof(f498,plain,(
% 6.63/6.23 index_60=s(index_57)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f189])).
% 6.63/6.23 fof(f499,plain,(
% 6.63/6.23 index_63=rselect_tail(q17)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f190])).
% 6.63/6.23 fof(f500,plain,(
% 6.63/6.23 index_66=s(index_63)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f191])).
% 6.63/6.23 fof(f501,plain,(
% 6.63/6.23 index_68=rselect_head(queue_67)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f192])).
% 6.63/6.23 fof(f502,plain,(
% 6.63/6.23 index_69=s(index_68)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f193])).
% 6.63/6.23 fof(f503,plain,(
% 6.63/6.23 index_72=rselect_tail(q18)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f194])).
% 6.63/6.23 fof(f504,plain,(
% 6.63/6.23 index_75=s(index_72)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f195])).
% 6.63/6.23 fof(f505,plain,(
% 6.63/6.23 index_78=rselect_tail(q1)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f196])).
% 6.63/6.23 fof(f506,plain,(
% 6.63/6.23 index_81=s(index_78)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f197])).
% 6.63/6.23 fof(f507,plain,(
% 6.63/6.23 index_84=rselect_tail(q19)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f198])).
% 6.63/6.23 fof(f508,plain,(
% 6.63/6.23 index_87=s(index_84)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f199])).
% 6.63/6.23 fof(f509,plain,(
% 6.63/6.23 index_9=rselect_tail(q9)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f200])).
% 6.63/6.23 fof(f510,plain,(
% 6.63/6.23 index_90=rselect_tail(q20)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f201])).
% 6.63/6.23 fof(f511,plain,(
% 6.63/6.23 index_93=s(index_90)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f202])).
% 6.63/6.23 fof(f512,plain,(
% 6.63/6.23 index_95=rselect_head(queue_94)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f203])).
% 6.63/6.23 fof(f513,plain,(
% 6.63/6.23 index_96=s(index_95)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f204])).
% 6.63/6.23 fof(f514,plain,(
% 6.63/6.23 index_99=rselect_tail(q21)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f205])).
% 6.63/6.23 fof(f515,plain,(
% 6.63/6.23 queue_1=rstore_head(q,index_0)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f206])).
% 6.63/6.23 fof(f516,plain,(
% 6.63/6.23 queue_101=rstore_seq(q21,earray_100)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f207])).
% 6.63/6.23 fof(f517,plain,(
% 6.63/6.23 queue_103=rstore_tail(queue_101,index_102)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f208])).
% 6.63/6.23 fof(f518,plain,(
% 6.63/6.23 queue_107=rstore_seq(q22,earray_106)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f209])).
% 6.63/6.23 fof(f519,plain,(
% 6.63/6.23 queue_109=rstore_tail(queue_107,index_108)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f210])).
% 6.63/6.23 fof(f520,plain,(
% 6.63/6.23 queue_11=rstore_seq(q9,earray_10)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f211])).
% 6.63/6.23 fof(f521,plain,(
% 6.63/6.23 queue_113=rstore_seq(q23,earray_112)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f212])).
% 6.63/6.23 fof(f522,plain,(
% 6.63/6.23 queue_115=rstore_tail(queue_113,index_114)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f213])).
% 6.63/6.23 fof(f523,plain,(
% 6.63/6.23 queue_118=rstore_head(queue_115,index_117)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f214])).
% 6.63/6.23 fof(f524,plain,(
% 6.63/6.23 queue_122=rstore_seq(q24,earray_121)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f215])).
% 6.63/6.23 fof(f525,plain,(
% 6.63/6.23 queue_124=rstore_tail(queue_122,index_123)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f216])).
% 6.63/6.23 fof(f526,plain,(
% 6.63/6.23 queue_128=rstore_seq(q25,earray_127)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f217])).
% 6.63/6.23 fof(f527,plain,(
% 6.63/6.23 queue_13=rstore_tail(queue_11,index_12)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f218])).
% 6.63/6.23 fof(f528,plain,(
% 6.63/6.23 queue_130=rstore_tail(queue_128,index_129)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f219])).
% 6.63/6.23 fof(f529,plain,(
% 6.63/6.23 queue_134=rstore_seq(q26,earray_133)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f220])).
% 6.63/6.23 fof(f530,plain,(
% 6.63/6.23 queue_136=rstore_tail(queue_134,index_135)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f221])).
% 6.63/6.23 fof(f531,plain,(
% 6.63/6.23 queue_139=rstore_head(queue_136,index_138)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f222])).
% 6.63/6.23 fof(f532,plain,(
% 6.63/6.23 queue_143=rstore_seq(q27,earray_142)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f223])).
% 6.63/6.23 fof(f533,plain,(
% 6.63/6.23 queue_145=rstore_tail(queue_143,index_144)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f224])).
% 6.63/6.23 fof(f534,plain,(
% 6.63/6.23 queue_149=rstore_seq(q28,earray_148)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f225])).
% 6.63/6.23 fof(f535,plain,(
% 6.63/6.23 queue_151=rstore_tail(queue_149,index_150)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f226])).
% 6.63/6.23 fof(f536,plain,(
% 6.63/6.23 queue_155=rstore_seq(q2,earray_154)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f227])).
% 6.63/6.23 fof(f537,plain,(
% 6.63/6.23 queue_157=rstore_tail(queue_155,index_156)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f228])).
% 6.63/6.23 fof(f538,plain,(
% 6.63/6.23 queue_160=rstore_head(queue_157,index_159)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f229])).
% 6.63/6.23 fof(f539,plain,(
% 6.63/6.23 queue_164=rstore_seq(q29,earray_163)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f230])).
% 6.63/6.23 fof(f540,plain,(
% 6.63/6.23 queue_166=rstore_tail(queue_164,index_165)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f231])).
% 6.63/6.23 fof(f541,plain,(
% 6.63/6.23 queue_169=rstore_head(queue_166,index_168)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f232])).
% 6.63/6.23 fof(f542,plain,(
% 6.63/6.23 queue_17=rstore_seq(q10,earray_16)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f233])).
% 6.63/6.23 fof(f543,plain,(
% 6.63/6.23 queue_173=rstore_seq(q3,earray_172)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f234])).
% 6.63/6.23 fof(f544,plain,(
% 6.63/6.23 queue_175=rstore_tail(queue_173,index_174)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f235])).
% 6.63/6.23 fof(f545,plain,(
% 6.63/6.23 queue_179=rstore_seq(q4,earray_178)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f236])).
% 6.63/6.23 fof(f546,plain,(
% 6.63/6.23 queue_181=rstore_tail(queue_179,index_180)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f237])).
% 6.63/6.23 fof(f547,plain,(
% 6.63/6.23 queue_185=rstore_seq(q5,earray_184)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f238])).
% 6.63/6.23 fof(f548,plain,(
% 6.63/6.23 queue_187=rstore_tail(queue_185,index_186)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f239])).
% 6.63/6.23 fof(f549,plain,(
% 6.63/6.23 queue_19=rstore_tail(queue_17,index_18)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f240])).
% 6.63/6.23 fof(f550,plain,(
% 6.63/6.23 queue_190=rstore_head(queue_187,index_189)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f241])).
% 6.63/6.23 fof(f551,plain,(
% 6.63/6.23 queue_194=rstore_seq(q6,earray_193)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f242])).
% 6.63/6.23 fof(f552,plain,(
% 6.63/6.23 queue_196=rstore_tail(queue_194,index_195)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f243])).
% 6.63/6.23 fof(f553,plain,(
% 6.63/6.23 queue_200=rstore_seq(q7,earray_199)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f244])).
% 6.63/6.23 fof(f554,plain,(
% 6.63/6.23 queue_202=rstore_tail(queue_200,index_201)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f245])).
% 6.63/6.23 fof(f555,plain,(
% 6.63/6.23 queue_206=rstore_seq(q8,earray_205)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f246])).
% 6.63/6.23 fof(f556,plain,(
% 6.63/6.23 queue_208=rstore_tail(queue_206,index_207)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f247])).
% 6.63/6.23 fof(f557,plain,(
% 6.63/6.23 queue_211=rstore_head(queue_208,index_210)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f248])).
% 6.63/6.23 fof(f558,plain,(
% 6.63/6.23 queue_23=rstore_seq(q11,earray_22)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f249])).
% 6.63/6.23 fof(f559,plain,(
% 6.63/6.23 queue_25=rstore_tail(queue_23,index_24)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f250])).
% 6.63/6.23 fof(f560,plain,(
% 6.63/6.23 queue_28=rstore_head(queue_25,index_27)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f251])).
% 6.63/6.23 fof(f561,plain,(
% 6.63/6.23 queue_32=rstore_seq(q12,earray_31)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f252])).
% 6.63/6.23 fof(f562,plain,(
% 6.63/6.23 queue_34=rstore_tail(queue_32,index_33)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f253])).
% 6.63/6.23 fof(f563,plain,(
% 6.63/6.23 queue_38=rstore_seq(q13,earray_37)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f254])).
% 6.63/6.23 fof(f564,plain,(
% 6.63/6.23 queue_40=rstore_tail(queue_38,index_39)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f255])).
% 6.63/6.23 fof(f565,plain,(
% 6.63/6.23 queue_44=rstore_seq(q14,earray_43)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f256])).
% 6.63/6.23 fof(f566,plain,(
% 6.63/6.23 queue_46=rstore_tail(queue_44,index_45)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f257])).
% 6.63/6.23 fof(f567,plain,(
% 6.63/6.23 queue_49=rstore_head(queue_46,index_48)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f258])).
% 6.63/6.23 fof(f568,plain,(
% 6.63/6.23 queue_5=rstore_seq(q0,earray_4)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f259])).
% 6.63/6.23 fof(f569,plain,(
% 6.63/6.23 queue_53=rstore_seq(q15,earray_52)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f260])).
% 6.63/6.23 fof(f570,plain,(
% 6.63/6.23 queue_55=rstore_tail(queue_53,index_54)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f261])).
% 6.63/6.23 fof(f571,plain,(
% 6.63/6.23 queue_59=rstore_seq(q16,earray_58)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f262])).
% 6.63/6.23 fof(f572,plain,(
% 6.63/6.23 queue_61=rstore_tail(queue_59,index_60)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f263])).
% 6.63/6.23 fof(f573,plain,(
% 6.63/6.23 queue_65=rstore_seq(q17,earray_64)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f264])).
% 6.63/6.23 fof(f574,plain,(
% 6.63/6.23 queue_67=rstore_tail(queue_65,index_66)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f265])).
% 6.63/6.23 fof(f575,plain,(
% 6.63/6.23 queue_7=rstore_tail(queue_5,index_6)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f266])).
% 6.63/6.23 fof(f576,plain,(
% 6.63/6.23 queue_70=rstore_head(queue_67,index_69)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f267])).
% 6.63/6.23 fof(f577,plain,(
% 6.63/6.23 queue_74=rstore_seq(q18,earray_73)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f268])).
% 6.63/6.23 fof(f578,plain,(
% 6.63/6.23 queue_76=rstore_tail(queue_74,index_75)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f269])).
% 6.63/6.23 fof(f579,plain,(
% 6.63/6.23 queue_80=rstore_seq(q1,earray_79)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f270])).
% 6.63/6.23 fof(f580,plain,(
% 6.63/6.23 queue_82=rstore_tail(queue_80,index_81)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f271])).
% 6.63/6.23 fof(f581,plain,(
% 6.63/6.23 queue_86=rstore_seq(q19,earray_85)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f272])).
% 6.63/6.23 fof(f582,plain,(
% 6.63/6.23 queue_88=rstore_tail(queue_86,index_87)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f273])).
% 6.63/6.23 fof(f583,plain,(
% 6.63/6.23 queue_92=rstore_seq(q20,earray_91)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f274])).
% 6.63/6.23 fof(f584,plain,(
% 6.63/6.23 queue_94=rstore_tail(queue_92,index_93)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f275])).
% 6.63/6.23 fof(f585,plain,(
% 6.63/6.23 queue_97=rstore_head(queue_94,index_96)),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f276])).
% 6.63/6.23 fof(f586,plain,(
% 6.63/6.23 q0=queue_1),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f277])).
% 6.63/6.23 fof(f587,plain,(
% 6.63/6.23 q1=queue_7),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f278])).
% 6.63/6.23 fof(f588,plain,(
% 6.63/6.23 q10=queue_13),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f279])).
% 6.63/6.23 fof(f589,plain,(
% 6.63/6.23 q11=queue_19),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f280])).
% 6.63/6.23 fof(f590,plain,(
% 6.63/6.23 q12=queue_28),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f281])).
% 6.63/6.23 fof(f591,plain,(
% 6.63/6.23 q13=queue_34),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f282])).
% 6.63/6.23 fof(f592,plain,(
% 6.63/6.23 q14=queue_40),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f283])).
% 6.63/6.23 fof(f593,plain,(
% 6.63/6.23 q15=queue_49),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f284])).
% 6.63/6.23 fof(f594,plain,(
% 6.63/6.23 q16=queue_55),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f285])).
% 6.63/6.23 fof(f595,plain,(
% 6.63/6.23 q17=queue_61),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f286])).
% 6.63/6.23 fof(f596,plain,(
% 6.63/6.23 q18=queue_70),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f287])).
% 6.63/6.23 fof(f597,plain,(
% 6.63/6.23 q19=queue_76),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f288])).
% 6.63/6.23 fof(f598,plain,(
% 6.63/6.23 q2=queue_82),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f289])).
% 6.63/6.23 fof(f599,plain,(
% 6.63/6.23 q20=queue_88),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f290])).
% 6.63/6.23 fof(f600,plain,(
% 6.63/6.23 q21=queue_97),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f291])).
% 6.63/6.23 fof(f601,plain,(
% 6.63/6.23 q22=queue_103),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f292])).
% 6.63/6.23 fof(f602,plain,(
% 6.63/6.23 q23=queue_109),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f293])).
% 6.63/6.23 fof(f603,plain,(
% 6.63/6.23 q24=queue_118),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f294])).
% 6.63/6.23 fof(f604,plain,(
% 6.63/6.23 q25=queue_124),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f295])).
% 6.63/6.23 fof(f605,plain,(
% 6.63/6.23 q26=queue_130),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f296])).
% 6.63/6.23 fof(f606,plain,(
% 6.63/6.23 q27=queue_139),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f297])).
% 6.63/6.23 fof(f607,plain,(
% 6.63/6.23 q28=queue_145),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f298])).
% 6.63/6.23 fof(f608,plain,(
% 6.63/6.23 q29=queue_151),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f299])).
% 6.63/6.23 fof(f609,plain,(
% 6.63/6.23 q3=queue_160),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f300])).
% 6.63/6.23 fof(f610,plain,(
% 6.63/6.23 q30=queue_169),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f301])).
% 6.63/6.23 fof(f611,plain,(
% 6.63/6.23 q4=queue_175),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f302])).
% 6.63/6.23 fof(f612,plain,(
% 6.63/6.23 q5=queue_181),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f303])).
% 6.63/6.23 fof(f613,plain,(
% 6.63/6.23 q6=queue_190),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f304])).
% 6.63/6.23 fof(f614,plain,(
% 6.63/6.23 q7=queue_196),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f305])).
% 6.63/6.23 fof(f615,plain,(
% 6.63/6.23 q8=queue_202),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f306])).
% 6.63/6.23 fof(f616,plain,(
% 6.63/6.23 q9=queue_211),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f307])).
% 6.63/6.23 fof(f617,plain,(
% 6.63/6.23 ~elem_214=e10),
% 6.63/6.23 inference(cnf_transformation,[status(thm)],[f308])).
% 6.63/6.23 fof(f618,plain,(
% 6.63/6.23 select(earray_16,index_15)=e10),
% 6.63/6.23 inference(paramodulation,[status(thm)],[f390,f309])).
% 6.63/6.23 fof(f775,plain,(
% 6.63/6.23 ~s(index_18)=index_15),
% 6.63/6.23 inference(paramodulation,[status(thm)],[f466,f369])).
% 6.63/6.23 fof(f776,plain,(
% 6.63/6.23 ~index_18=index_15),
% 6.63/6.23 inference(paramodulation,[status(thm)],[f466,f370])).
% 6.63/6.23 fof(f1744,plain,(
% 6.63/6.23 q0=rstore_head(q,index_0)),
% 6.63/6.23 inference(forward_demodulation,[status(thm)],[f586,f515])).
% 6.63/6.23 fof(f1745,plain,(
% 6.63/6.23 rselect_tail(q0)=rselect_tail(q)),
% 6.63/6.23 inference(paramodulation,[status(thm)],[f1744,f320])).
% 6.63/6.23 fof(f1747,plain,(
% 6.63/6.23 rselect_head(q0)=index_0),
% 6.63/6.23 inference(paramodulation,[status(thm)],[f1744,f313])).
% 6.63/6.23 fof(f1748,plain,(
% 6.63/6.23 index_3=rselect_tail(q)),
% 6.63/6.23 inference(forward_demodulation,[status(thm)],[f485,f1745])).
% 6.63/6.23 fof(f1750,plain,(
% 6.63/6.23 index_0=index_3),
% 6.63/6.23 inference(backward_demodulation,[status(thm)],[f1748,f433])).
% 6.63/6.23 fof(f1832,plain,(
% 6.63/6.24 rselect_head(q0)=index_3),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f1750,f1747])).
% 6.63/6.24 fof(f1834,plain,(
% 6.63/6.24 rselect_head(queue_101)=rselect_head(q21)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f516,f318])).
% 6.63/6.24 fof(f1835,plain,(
% 6.63/6.24 rselect_seq(queue_101)=earray_100),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f516,f312])).
% 6.63/6.24 fof(f1837,plain,(
% 6.63/6.24 q22=rstore_tail(queue_101,index_102)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f601,f517])).
% 6.63/6.24 fof(f1838,plain,(
% 6.63/6.24 rselect_head(q22)=rselect_head(queue_101)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f1837,f317])).
% 6.63/6.24 fof(f1839,plain,(
% 6.63/6.24 rselect_seq(q22)=rselect_seq(queue_101)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f1837,f316])).
% 6.63/6.24 fof(f1840,plain,(
% 6.63/6.24 rselect_tail(q22)=index_102),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f1837,f314])).
% 6.63/6.24 fof(f1841,plain,(
% 6.63/6.24 earray_104=rselect_seq(queue_101)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f373,f1839])).
% 6.63/6.24 fof(f1842,plain,(
% 6.63/6.24 earray_104=earray_100),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f1835,f1841])).
% 6.63/6.24 fof(f1843,plain,(
% 6.63/6.24 index_105=index_102),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f435,f1840])).
% 6.63/6.24 fof(f1848,plain,(
% 6.63/6.24 index_105=s(index_99)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f1843,f434])).
% 6.63/6.24 fof(f1910,plain,(
% 6.63/6.24 rselect_head(queue_107)=rselect_head(q22)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f518,f318])).
% 6.63/6.24 fof(f1911,plain,(
% 6.63/6.24 rselect_seq(queue_107)=earray_106),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f518,f312])).
% 6.63/6.24 fof(f1913,plain,(
% 6.63/6.24 q23=rstore_tail(queue_107,index_108)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f602,f519])).
% 6.63/6.24 fof(f1914,plain,(
% 6.63/6.24 rselect_head(q23)=rselect_head(queue_107)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f1913,f317])).
% 6.63/6.24 fof(f1915,plain,(
% 6.63/6.24 rselect_seq(q23)=rselect_seq(queue_107)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f1913,f316])).
% 6.63/6.24 fof(f1916,plain,(
% 6.63/6.24 rselect_tail(q23)=index_108),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f1913,f314])).
% 6.63/6.24 fof(f1917,plain,(
% 6.63/6.24 earray_110=rselect_seq(queue_107)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f375,f1915])).
% 6.63/6.24 fof(f1918,plain,(
% 6.63/6.24 earray_110=earray_106),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f1911,f1917])).
% 6.63/6.24 fof(f1919,plain,(
% 6.63/6.24 index_111=index_108),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f437,f1916])).
% 6.63/6.24 fof(f2049,plain,(
% 6.63/6.24 index_111=s(index_105)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f1919,f436])).
% 6.63/6.24 fof(f2159,plain,(
% 6.63/6.24 rselect_head(queue_11)=rselect_head(q9)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f520,f318])).
% 6.63/6.24 fof(f2163,plain,(
% 6.63/6.24 rselect_head(queue_113)=rselect_head(q23)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f521,f318])).
% 6.63/6.24 fof(f2164,plain,(
% 6.63/6.24 rselect_seq(queue_113)=earray_112),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f521,f312])).
% 6.63/6.24 fof(f2166,plain,(
% 6.63/6.24 rselect_head(queue_115)=rselect_head(queue_113)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f522,f317])).
% 6.63/6.24 fof(f2167,plain,(
% 6.63/6.24 rselect_seq(queue_115)=rselect_seq(queue_113)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f522,f316])).
% 6.63/6.24 fof(f2168,plain,(
% 6.63/6.24 rselect_tail(queue_115)=index_114),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f522,f314])).
% 6.63/6.24 fof(f2169,plain,(
% 6.63/6.24 index_116=rselect_head(queue_113)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f439,f2166])).
% 6.63/6.24 fof(f2170,plain,(
% 6.63/6.24 rselect_seq(queue_115)=earray_112),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2164,f2167])).
% 6.63/6.24 fof(f2257,plain,(
% 6.63/6.24 q24=rstore_head(queue_115,index_117)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f603,f523])).
% 6.63/6.24 fof(f2258,plain,(
% 6.63/6.24 rselect_tail(q24)=rselect_tail(queue_115)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2257,f320])).
% 6.63/6.24 fof(f2259,plain,(
% 6.63/6.24 rselect_seq(q24)=rselect_seq(queue_115)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2257,f315])).
% 6.63/6.24 fof(f2260,plain,(
% 6.63/6.24 rselect_head(q24)=index_117),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2257,f313])).
% 6.63/6.24 fof(f2261,plain,(
% 6.63/6.24 index_120=rselect_tail(queue_115)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f442,f2258])).
% 6.63/6.24 fof(f2262,plain,(
% 6.63/6.24 earray_119=rselect_seq(queue_115)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f377,f2259])).
% 6.63/6.24 fof(f2263,plain,(
% 6.63/6.24 earray_119=earray_112),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2170,f2262])).
% 6.63/6.24 fof(f2265,plain,(
% 6.63/6.24 index_120=index_114),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f2261,f2168])).
% 6.63/6.24 fof(f2272,plain,(
% 6.63/6.24 index_120=s(index_111)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f2265,f438])).
% 6.63/6.24 fof(f2347,plain,(
% 6.63/6.24 rselect_head(queue_122)=rselect_head(q24)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f524,f318])).
% 6.63/6.24 fof(f2348,plain,(
% 6.63/6.24 rselect_seq(queue_122)=earray_121),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f524,f312])).
% 6.63/6.24 fof(f2350,plain,(
% 6.63/6.24 rselect_head(queue_122)=index_117),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2260,f2347])).
% 6.63/6.24 fof(f2351,plain,(
% 6.63/6.24 q25=rstore_tail(queue_122,index_123)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f604,f525])).
% 6.63/6.24 fof(f2352,plain,(
% 6.63/6.24 rselect_head(q25)=rselect_head(queue_122)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2351,f317])).
% 6.63/6.24 fof(f2353,plain,(
% 6.63/6.24 rselect_seq(q25)=rselect_seq(queue_122)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2351,f316])).
% 6.63/6.24 fof(f2354,plain,(
% 6.63/6.24 rselect_tail(q25)=index_123),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2351,f314])).
% 6.63/6.24 fof(f2355,plain,(
% 6.63/6.24 rselect_head(q25)=index_117),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2350,f2352])).
% 6.63/6.24 fof(f2356,plain,(
% 6.63/6.24 earray_125=rselect_seq(queue_122)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f379,f2353])).
% 6.63/6.24 fof(f2357,plain,(
% 6.63/6.24 earray_125=earray_121),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2348,f2356])).
% 6.63/6.24 fof(f2358,plain,(
% 6.63/6.24 index_126=index_123),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f444,f2354])).
% 6.63/6.24 fof(f2504,plain,(
% 6.63/6.24 index_126=s(index_120)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f2358,f443])).
% 6.63/6.24 fof(f2629,plain,(
% 6.63/6.24 rselect_head(queue_128)=rselect_head(q25)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f526,f318])).
% 6.63/6.24 fof(f2630,plain,(
% 6.63/6.24 rselect_seq(queue_128)=earray_127),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f526,f312])).
% 6.63/6.24 fof(f2632,plain,(
% 6.63/6.24 rselect_head(queue_128)=index_117),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2355,f2629])).
% 6.63/6.24 fof(f2633,plain,(
% 6.63/6.24 q10=rstore_tail(queue_11,index_12)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f588,f527])).
% 6.63/6.24 fof(f2634,plain,(
% 6.63/6.24 rselect_head(q10)=rselect_head(queue_11)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2633,f317])).
% 6.63/6.24 fof(f2636,plain,(
% 6.63/6.24 rselect_tail(q10)=index_12),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2633,f314])).
% 6.63/6.24 fof(f2639,plain,(
% 6.63/6.24 index_15=index_12),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f453,f2636])).
% 6.63/6.24 fof(f2650,plain,(
% 6.63/6.24 index_15=s(index_9)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f2639,f441])).
% 6.63/6.24 fof(f2731,plain,(
% 6.63/6.24 q26=rstore_tail(queue_128,index_129)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f605,f528])).
% 6.63/6.24 fof(f2732,plain,(
% 6.63/6.24 rselect_head(q26)=rselect_head(queue_128)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2731,f317])).
% 6.63/6.24 fof(f2733,plain,(
% 6.63/6.24 rselect_seq(q26)=rselect_seq(queue_128)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2731,f316])).
% 6.63/6.24 fof(f2734,plain,(
% 6.63/6.24 rselect_tail(q26)=index_129),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f2731,f314])).
% 6.63/6.24 fof(f2735,plain,(
% 6.63/6.24 rselect_head(q26)=index_117),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2632,f2732])).
% 6.63/6.24 fof(f2736,plain,(
% 6.63/6.24 earray_131=rselect_seq(queue_128)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f381,f2733])).
% 6.63/6.24 fof(f2737,plain,(
% 6.63/6.24 earray_131=earray_127),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2630,f2736])).
% 6.63/6.24 fof(f2738,plain,(
% 6.63/6.24 index_132=index_129),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f446,f2734])).
% 6.63/6.24 fof(f2746,plain,(
% 6.63/6.24 index_132=s(index_126)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f2738,f445])).
% 6.63/6.24 fof(f2997,plain,(
% 6.63/6.24 rselect_head(queue_134)=rselect_head(q26)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f529,f318])).
% 6.63/6.24 fof(f2998,plain,(
% 6.63/6.24 rselect_seq(queue_134)=earray_133),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f529,f312])).
% 6.63/6.24 fof(f3000,plain,(
% 6.63/6.24 rselect_head(queue_134)=index_117),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2735,f2997])).
% 6.63/6.24 fof(f3001,plain,(
% 6.63/6.24 rselect_head(queue_136)=rselect_head(queue_134)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f530,f317])).
% 6.63/6.24 fof(f3002,plain,(
% 6.63/6.24 rselect_seq(queue_136)=rselect_seq(queue_134)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f530,f316])).
% 6.63/6.24 fof(f3003,plain,(
% 6.63/6.24 rselect_tail(queue_136)=index_135),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f530,f314])).
% 6.63/6.24 fof(f3004,plain,(
% 6.63/6.24 index_137=rselect_head(queue_134)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f448,f3001])).
% 6.63/6.24 fof(f3005,plain,(
% 6.63/6.24 index_137=index_117),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3000,f3004])).
% 6.63/6.24 fof(f3006,plain,(
% 6.63/6.24 rselect_seq(queue_136)=earray_133),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2998,f3002])).
% 6.63/6.24 fof(f3009,plain,(
% 6.63/6.24 index_138=s(index_117)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3005,f449])).
% 6.63/6.24 fof(f3111,plain,(
% 6.63/6.24 q27=rstore_head(queue_136,index_138)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f606,f531])).
% 6.63/6.24 fof(f3112,plain,(
% 6.63/6.24 rselect_tail(q27)=rselect_tail(queue_136)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3111,f320])).
% 6.63/6.24 fof(f3113,plain,(
% 6.63/6.24 rselect_seq(q27)=rselect_seq(queue_136)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3111,f315])).
% 6.63/6.24 fof(f3114,plain,(
% 6.63/6.24 rselect_head(q27)=index_138),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3111,f313])).
% 6.63/6.24 fof(f3115,plain,(
% 6.63/6.24 index_141=rselect_tail(queue_136)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f450,f3112])).
% 6.63/6.24 fof(f3116,plain,(
% 6.63/6.24 earray_140=rselect_seq(queue_136)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f384,f3113])).
% 6.63/6.24 fof(f3117,plain,(
% 6.63/6.24 earray_140=earray_133),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3006,f3116])).
% 6.63/6.24 fof(f3119,plain,(
% 6.63/6.24 index_141=index_135),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3115,f3003])).
% 6.63/6.24 fof(f3126,plain,(
% 6.63/6.24 index_141=s(index_132)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3119,f447])).
% 6.63/6.24 fof(f3323,plain,(
% 6.63/6.24 rselect_head(queue_143)=rselect_head(q27)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f532,f318])).
% 6.63/6.24 fof(f3324,plain,(
% 6.63/6.24 rselect_seq(queue_143)=earray_142),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f532,f312])).
% 6.63/6.24 fof(f3326,plain,(
% 6.63/6.24 rselect_head(queue_143)=index_138),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3114,f3323])).
% 6.63/6.24 fof(f3327,plain,(
% 6.63/6.24 q28=rstore_tail(queue_143,index_144)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f607,f533])).
% 6.63/6.24 fof(f3328,plain,(
% 6.63/6.24 rselect_head(q28)=rselect_head(queue_143)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3327,f317])).
% 6.63/6.24 fof(f3329,plain,(
% 6.63/6.24 rselect_seq(q28)=rselect_seq(queue_143)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3327,f316])).
% 6.63/6.24 fof(f3330,plain,(
% 6.63/6.24 rselect_tail(q28)=index_144),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3327,f314])).
% 6.63/6.24 fof(f3331,plain,(
% 6.63/6.24 rselect_head(q28)=index_138),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3326,f3328])).
% 6.63/6.24 fof(f3332,plain,(
% 6.63/6.24 earray_146=rselect_seq(queue_143)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f386,f3329])).
% 6.63/6.24 fof(f3333,plain,(
% 6.63/6.24 earray_146=earray_142),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3324,f3332])).
% 6.63/6.24 fof(f3334,plain,(
% 6.63/6.24 index_147=index_144),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f452,f3330])).
% 6.63/6.24 fof(f3342,plain,(
% 6.63/6.24 index_147=s(index_141)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3334,f451])).
% 6.63/6.24 fof(f3669,plain,(
% 6.63/6.24 rselect_head(queue_149)=rselect_head(q28)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f534,f318])).
% 6.63/6.24 fof(f3670,plain,(
% 6.63/6.24 rselect_seq(queue_149)=earray_148),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f534,f312])).
% 6.63/6.24 fof(f3672,plain,(
% 6.63/6.24 rselect_head(queue_149)=index_138),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3331,f3669])).
% 6.63/6.24 fof(f3675,plain,(
% 6.63/6.24 ![X0]: (index_99=X0|select(earray_100,X0)=select(earray_98,X0))),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f372,f311])).
% 6.63/6.24 fof(f3677,plain,(
% 6.63/6.24 q29=rstore_tail(queue_149,index_150)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f608,f535])).
% 6.63/6.24 fof(f3678,plain,(
% 6.63/6.24 rselect_head(q29)=rselect_head(queue_149)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3677,f317])).
% 6.63/6.24 fof(f3679,plain,(
% 6.63/6.24 rselect_seq(q29)=rselect_seq(queue_149)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3677,f316])).
% 6.63/6.24 fof(f3680,plain,(
% 6.63/6.24 rselect_tail(q29)=index_150),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3677,f314])).
% 6.63/6.24 fof(f3681,plain,(
% 6.63/6.24 rselect_head(q29)=index_138),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3672,f3678])).
% 6.63/6.24 fof(f3682,plain,(
% 6.63/6.24 earray_161=rselect_seq(queue_149)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f391,f3679])).
% 6.63/6.24 fof(f3683,plain,(
% 6.63/6.24 earray_161=earray_148),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3670,f3682])).
% 6.63/6.24 fof(f3684,plain,(
% 6.63/6.24 index_162=index_150),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f459,f3680])).
% 6.63/6.24 fof(f3692,plain,(
% 6.63/6.24 index_162=s(index_147)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3684,f454])).
% 6.63/6.24 fof(f3795,plain,(
% 6.63/6.24 rselect_head(queue_155)=rselect_head(q2)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f536,f318])).
% 6.63/6.24 fof(f3798,plain,(
% 6.63/6.24 rselect_head(queue_157)=rselect_head(queue_155)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f537,f317])).
% 6.63/6.24 fof(f3800,plain,(
% 6.63/6.24 rselect_tail(queue_157)=index_156),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f537,f314])).
% 6.63/6.24 fof(f3801,plain,(
% 6.63/6.24 index_158=rselect_head(queue_155)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f457,f3798])).
% 6.63/6.24 fof(f3803,plain,(
% 6.63/6.24 earray_106=store(earray_100,index_105,e22)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f1842,f374])).
% 6.63/6.24 fof(f3804,plain,(
% 6.63/6.24 ![X0]: (index_105=X0|select(earray_106,X0)=select(earray_100,X0))),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3803,f311])).
% 6.63/6.24 fof(f3806,plain,(
% 6.63/6.24 earray_112=store(earray_106,index_111,e23)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f1918,f376])).
% 6.63/6.24 fof(f3807,plain,(
% 6.63/6.24 ![X0]: (index_111=X0|select(earray_112,X0)=select(earray_106,X0))),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3806,f311])).
% 6.63/6.24 fof(f3809,plain,(
% 6.63/6.24 earray_121=store(earray_112,index_120,e24)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2263,f378])).
% 6.63/6.24 fof(f3810,plain,(
% 6.63/6.24 ![X0]: (index_120=X0|select(earray_121,X0)=select(earray_112,X0))),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3809,f311])).
% 6.63/6.24 fof(f3812,plain,(
% 6.63/6.24 q3=rstore_head(queue_157,index_159)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f609,f538])).
% 6.63/6.24 fof(f3813,plain,(
% 6.63/6.24 rselect_tail(q3)=rselect_tail(queue_157)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3812,f320])).
% 6.63/6.24 fof(f3815,plain,(
% 6.63/6.24 rselect_head(q3)=index_159),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3812,f313])).
% 6.63/6.24 fof(f3816,plain,(
% 6.63/6.24 index_171=rselect_tail(queue_157)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f463,f3813])).
% 6.63/6.24 fof(f3820,plain,(
% 6.63/6.24 index_171=index_156),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3816,f3800])).
% 6.63/6.24 fof(f3821,plain,(
% 6.63/6.24 earray_127=store(earray_121,index_126,e25)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2357,f380])).
% 6.63/6.24 fof(f3822,plain,(
% 6.63/6.24 ![X0]: (index_126=X0|select(earray_127,X0)=select(earray_121,X0))),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3821,f311])).
% 6.63/6.24 fof(f3827,plain,(
% 6.63/6.24 index_171=s(index_153)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3820,f456])).
% 6.63/6.24 fof(f3929,plain,(
% 6.63/6.24 rselect_head(queue_164)=rselect_head(q29)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f539,f318])).
% 6.63/6.24 fof(f3930,plain,(
% 6.63/6.24 rselect_seq(queue_164)=earray_163),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f539,f312])).
% 6.63/6.24 fof(f3932,plain,(
% 6.63/6.24 rselect_head(queue_164)=index_138),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3681,f3929])).
% 6.63/6.24 fof(f3933,plain,(
% 6.63/6.24 rselect_head(queue_166)=rselect_head(queue_164)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f540,f317])).
% 6.63/6.24 fof(f3934,plain,(
% 6.63/6.24 rselect_seq(queue_166)=rselect_seq(queue_164)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f540,f316])).
% 6.63/6.24 fof(f3936,plain,(
% 6.63/6.24 index_167=rselect_head(queue_164)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f461,f3933])).
% 6.63/6.24 fof(f3937,plain,(
% 6.63/6.24 index_167=index_138),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3932,f3936])).
% 6.63/6.24 fof(f3938,plain,(
% 6.63/6.24 rselect_seq(queue_166)=earray_163),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3930,f3934])).
% 6.63/6.24 fof(f3939,plain,(
% 6.63/6.24 earray_133=store(earray_127,index_132,e26)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f2737,f382])).
% 6.63/6.24 fof(f3940,plain,(
% 6.63/6.24 ![X0]: (index_132=X0|select(earray_133,X0)=select(earray_127,X0))),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3939,f311])).
% 6.63/6.24 fof(f3942,plain,(
% 6.63/6.24 earray_142=store(earray_133,index_141,e27)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3117,f385])).
% 6.63/6.24 fof(f3943,plain,(
% 6.63/6.24 ![X0]: (index_141=X0|select(earray_142,X0)=select(earray_133,X0))),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f3942,f311])).
% 6.63/6.24 fof(f3947,plain,(
% 6.63/6.24 index_168=s(index_138)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f3937,f462])).
% 6.63/6.24 fof(f4000,plain,(
% 6.63/6.24 q30=rstore_head(queue_166,index_168)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f610,f541])).
% 6.63/6.24 fof(f4002,plain,(
% 6.63/6.24 rselect_seq(q30)=rselect_seq(queue_166)),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f4000,f315])).
% 6.63/6.24 fof(f4003,plain,(
% 6.63/6.24 rselect_head(q30)=index_168),
% 6.63/6.24 inference(paramodulation,[status(thm)],[f4000,f313])).
% 6.63/6.24 fof(f4005,plain,(
% 6.63/6.24 earray_212=rselect_seq(queue_166)),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f407,f4002])).
% 6.63/6.24 fof(f4006,plain,(
% 6.63/6.24 earray_212=earray_163),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f3938,f4005])).
% 6.63/6.24 fof(f4007,plain,(
% 6.63/6.24 index_213=index_168),
% 6.63/6.24 inference(forward_demodulation,[status(thm)],[f481,f4003])).
% 6.63/6.24 fof(f4009,plain,(
% 6.63/6.24 elem_214=select(earray_163,index_213)),
% 6.63/6.24 inference(backward_demodulation,[status(thm)],[f4006,f432])).
% 6.63/6.25 fof(f4012,plain,(
% 6.63/6.25 index_213=s(index_138)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4007,f3947])).
% 6.63/6.25 fof(f4065,plain,(
% 6.63/6.25 earray_148=store(earray_142,index_147,e28)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3333,f387])).
% 6.63/6.25 fof(f4066,plain,(
% 6.63/6.25 ![X0]: (index_147=X0|select(earray_148,X0)=select(earray_142,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4065,f311])).
% 6.63/6.25 fof(f4070,plain,(
% 6.63/6.25 earray_163=store(earray_148,index_162,e29)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3683,f392])).
% 6.63/6.25 fof(f4071,plain,(
% 6.63/6.25 ![X0]: (index_162=X0|select(earray_163,X0)=select(earray_148,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4070,f311])).
% 6.63/6.25 fof(f4074,plain,(
% 6.63/6.25 rselect_head(queue_17)=rselect_head(q10)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f542,f318])).
% 6.63/6.25 fof(f4075,plain,(
% 6.63/6.25 rselect_seq(queue_17)=earray_16),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f542,f312])).
% 6.63/6.25 fof(f4078,plain,(
% 6.63/6.25 rselect_head(queue_173)=rselect_head(q3)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f543,f318])).
% 6.63/6.25 fof(f4081,plain,(
% 6.63/6.25 rselect_head(queue_173)=index_159),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3815,f4078])).
% 6.63/6.25 fof(f4085,plain,(
% 6.63/6.25 q4=rstore_tail(queue_173,index_174)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f611,f544])).
% 6.63/6.25 fof(f4086,plain,(
% 6.63/6.25 rselect_head(q4)=rselect_head(queue_173)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4085,f317])).
% 6.63/6.25 fof(f4088,plain,(
% 6.63/6.25 rselect_tail(q4)=index_174),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4085,f314])).
% 6.63/6.25 fof(f4089,plain,(
% 6.63/6.25 rselect_head(q4)=index_159),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4081,f4086])).
% 6.63/6.25 fof(f4092,plain,(
% 6.63/6.25 index_177=index_174),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f465,f4088])).
% 6.63/6.25 fof(f4099,plain,(
% 6.63/6.25 index_177=s(index_171)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4092,f464])).
% 6.63/6.25 fof(f4207,plain,(
% 6.63/6.25 rselect_head(queue_179)=rselect_head(q4)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f545,f318])).
% 6.63/6.25 fof(f4210,plain,(
% 6.63/6.25 rselect_head(queue_179)=index_159),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4089,f4207])).
% 6.63/6.25 fof(f4211,plain,(
% 6.63/6.25 q5=rstore_tail(queue_179,index_180)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f612,f546])).
% 6.63/6.25 fof(f4212,plain,(
% 6.63/6.25 rselect_head(q5)=rselect_head(queue_179)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4211,f317])).
% 6.63/6.25 fof(f4214,plain,(
% 6.63/6.25 rselect_tail(q5)=index_180),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4211,f314])).
% 6.63/6.25 fof(f4215,plain,(
% 6.63/6.25 rselect_head(q5)=index_159),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4210,f4212])).
% 6.63/6.25 fof(f4218,plain,(
% 6.63/6.25 index_183=index_180),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f468,f4214])).
% 6.63/6.25 fof(f4227,plain,(
% 6.63/6.25 index_183=s(index_177)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4218,f467])).
% 6.63/6.25 fof(f4330,plain,(
% 6.63/6.25 rselect_head(queue_185)=rselect_head(q5)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f547,f318])).
% 6.63/6.25 fof(f4333,plain,(
% 6.63/6.25 rselect_head(queue_185)=index_159),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4215,f4330])).
% 6.63/6.25 fof(f4340,plain,(
% 6.63/6.25 rselect_head(queue_187)=rselect_head(queue_185)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f548,f317])).
% 6.63/6.25 fof(f4342,plain,(
% 6.63/6.25 rselect_tail(queue_187)=index_186),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f548,f314])).
% 6.63/6.25 fof(f4343,plain,(
% 6.63/6.25 index_188=rselect_head(queue_185)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f470,f4340])).
% 6.63/6.25 fof(f4344,plain,(
% 6.63/6.25 index_188=index_159),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4333,f4343])).
% 6.63/6.25 fof(f4348,plain,(
% 6.63/6.25 index_189=s(index_159)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4344,f471])).
% 6.63/6.25 fof(f4350,plain,(
% 6.63/6.25 ![X0]: (index_21=X0|select(earray_22,X0)=select(earray_20,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f408,f311])).
% 6.63/6.25 fof(f4403,plain,(
% 6.63/6.25 q11=rstore_tail(queue_17,index_18)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f589,f549])).
% 6.63/6.25 fof(f4404,plain,(
% 6.63/6.25 rselect_head(q11)=rselect_head(queue_17)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4403,f317])).
% 6.63/6.25 fof(f4405,plain,(
% 6.63/6.25 rselect_seq(q11)=rselect_seq(queue_17)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4403,f316])).
% 6.63/6.25 fof(f4406,plain,(
% 6.63/6.25 rselect_tail(q11)=index_18),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4403,f314])).
% 6.63/6.25 fof(f4407,plain,(
% 6.63/6.25 earray_20=rselect_seq(queue_17)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f404,f4405])).
% 6.63/6.25 fof(f4408,plain,(
% 6.63/6.25 earray_20=earray_16),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4075,f4407])).
% 6.63/6.25 fof(f4409,plain,(
% 6.63/6.25 index_21=index_18),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f479,f4406])).
% 6.63/6.25 fof(f4415,plain,(
% 6.63/6.25 ~s(index_21)=index_15),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4409,f775])).
% 6.63/6.25 fof(f4416,plain,(
% 6.63/6.25 ~index_21=index_15),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4409,f776])).
% 6.63/6.25 fof(f4417,plain,(
% 6.63/6.25 index_21=s(index_15)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4409,f466])).
% 6.63/6.25 fof(f4419,plain,(
% 6.63/6.25 ~index_24=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4415])).
% 6.63/6.25 fof(f4420,plain,(
% 6.63/6.25 ![X0]: (index_30=X0|select(earray_31,X0)=select(earray_29,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f410,f311])).
% 6.63/6.25 fof(f4422,plain,(
% 6.63/6.25 ![X0]: (index_36=X0|select(earray_37,X0)=select(earray_35,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f412,f311])).
% 6.63/6.25 fof(f4424,plain,(
% 6.63/6.25 ~s(s(s(index_21)))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f367])).
% 6.63/6.25 fof(f4425,plain,(
% 6.63/6.25 ~s(s(s(s(index_21))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f366])).
% 6.63/6.25 fof(f4426,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_21)))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f365])).
% 6.63/6.25 fof(f4427,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_21))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f364])).
% 6.63/6.25 fof(f4428,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_21)))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f363])).
% 6.63/6.25 fof(f4429,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_21))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f362])).
% 6.63/6.25 fof(f4430,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_21)))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f361])).
% 6.63/6.25 fof(f4431,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_21))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f360])).
% 6.63/6.25 fof(f4432,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f359])).
% 6.63/6.25 fof(f4433,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f358])).
% 6.63/6.25 fof(f4434,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f357])).
% 6.63/6.25 fof(f4435,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f356])).
% 6.63/6.25 fof(f4436,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f355])).
% 6.63/6.25 fof(f4437,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f354])).
% 6.63/6.25 fof(f4438,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f353])).
% 6.63/6.25 fof(f4439,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f352])).
% 6.63/6.25 fof(f4446,plain,(
% 6.63/6.25 ~s(s(index_21))=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4417,f368])).
% 6.63/6.25 fof(f4474,plain,(
% 6.63/6.25 ~s(s(index_24))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4424])).
% 6.63/6.25 fof(f4475,plain,(
% 6.63/6.25 ~s(s(s(index_24)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4425])).
% 6.63/6.25 fof(f4476,plain,(
% 6.63/6.25 ~s(s(s(s(index_24))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4426])).
% 6.63/6.25 fof(f4477,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_24)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4427])).
% 6.63/6.25 fof(f4478,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_24))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4428])).
% 6.63/6.25 fof(f4479,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_24)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4429])).
% 6.63/6.25 fof(f4480,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_24))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4430])).
% 6.63/6.25 fof(f4481,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_24)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4431])).
% 6.63/6.25 fof(f4482,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_24))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4432])).
% 6.63/6.25 fof(f4483,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4433])).
% 6.63/6.25 fof(f4484,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4434])).
% 6.63/6.25 fof(f4485,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4435])).
% 6.63/6.25 fof(f4486,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4436])).
% 6.63/6.25 fof(f4487,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4437])).
% 6.63/6.25 fof(f4488,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4438])).
% 6.63/6.25 fof(f4489,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4439])).
% 6.63/6.25 fof(f4496,plain,(
% 6.63/6.25 ~s(index_24)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f482,f4446])).
% 6.63/6.25 fof(f4523,plain,(
% 6.63/6.25 q6=rstore_head(queue_187,index_189)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f613,f550])).
% 6.63/6.25 fof(f4524,plain,(
% 6.63/6.25 rselect_tail(q6)=rselect_tail(queue_187)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4523,f320])).
% 6.63/6.25 fof(f4526,plain,(
% 6.63/6.25 rselect_head(q6)=index_189),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4523,f313])).
% 6.63/6.25 fof(f4527,plain,(
% 6.63/6.25 index_192=rselect_tail(queue_187)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f472,f4524])).
% 6.63/6.25 fof(f4532,plain,(
% 6.63/6.25 index_192=index_186),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4527,f4342])).
% 6.63/6.25 fof(f4539,plain,(
% 6.63/6.25 index_192=s(index_183)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4532,f469])).
% 6.63/6.25 fof(f4642,plain,(
% 6.63/6.25 rselect_head(queue_194)=rselect_head(q6)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f551,f318])).
% 6.63/6.25 fof(f4645,plain,(
% 6.63/6.25 rselect_head(queue_194)=index_189),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4526,f4642])).
% 6.63/6.25 fof(f4648,plain,(
% 6.63/6.25 ![X0]: (index_42=X0|select(earray_43,X0)=select(earray_41,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f415,f311])).
% 6.63/6.25 fof(f4650,plain,(
% 6.63/6.25 ![X0]: (index_51=X0|select(earray_52,X0)=select(earray_50,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f417,f311])).
% 6.63/6.25 fof(f4652,plain,(
% 6.63/6.25 q7=rstore_tail(queue_194,index_195)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f614,f552])).
% 6.63/6.25 fof(f4653,plain,(
% 6.63/6.25 rselect_head(q7)=rselect_head(queue_194)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4652,f317])).
% 6.63/6.25 fof(f4655,plain,(
% 6.63/6.25 rselect_tail(q7)=index_195),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4652,f314])).
% 6.63/6.25 fof(f4656,plain,(
% 6.63/6.25 rselect_head(q7)=index_189),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4645,f4653])).
% 6.63/6.25 fof(f4659,plain,(
% 6.63/6.25 index_198=index_195),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f474,f4655])).
% 6.63/6.25 fof(f4668,plain,(
% 6.63/6.25 index_198=s(index_192)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4659,f473])).
% 6.63/6.25 fof(f4671,plain,(
% 6.63/6.25 ![X0]: (index_57=X0|select(earray_58,X0)=select(earray_56,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f419,f311])).
% 6.63/6.25 fof(f4773,plain,(
% 6.63/6.25 rselect_head(queue_200)=rselect_head(q7)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f553,f318])).
% 6.63/6.25 fof(f4776,plain,(
% 6.63/6.25 rselect_head(queue_200)=index_189),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4656,f4773])).
% 6.63/6.25 fof(f4777,plain,(
% 6.63/6.25 ![X0]: (index_63=X0|select(earray_64,X0)=select(earray_62,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f421,f311])).
% 6.63/6.25 fof(f4779,plain,(
% 6.63/6.25 ![X0]: (index_72=X0|select(earray_73,X0)=select(earray_71,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f423,f311])).
% 6.63/6.25 fof(f4781,plain,(
% 6.63/6.25 q8=rstore_tail(queue_200,index_201)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f615,f554])).
% 6.63/6.25 fof(f4782,plain,(
% 6.63/6.25 rselect_head(q8)=rselect_head(queue_200)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4781,f317])).
% 6.63/6.25 fof(f4784,plain,(
% 6.63/6.25 rselect_tail(q8)=index_201),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4781,f314])).
% 6.63/6.25 fof(f4785,plain,(
% 6.63/6.25 rselect_head(q8)=index_189),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4776,f4782])).
% 6.63/6.25 fof(f4788,plain,(
% 6.63/6.25 index_204=index_201),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f476,f4784])).
% 6.63/6.25 fof(f4797,plain,(
% 6.63/6.25 index_204=s(index_198)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4788,f475])).
% 6.63/6.25 fof(f4900,plain,(
% 6.63/6.25 rselect_head(queue_206)=rselect_head(q8)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f555,f318])).
% 6.63/6.25 fof(f4903,plain,(
% 6.63/6.25 rselect_head(queue_206)=index_189),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4785,f4900])).
% 6.63/6.25 fof(f4904,plain,(
% 6.63/6.25 rselect_head(queue_208)=rselect_head(queue_206)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f556,f317])).
% 6.63/6.25 fof(f4906,plain,(
% 6.63/6.25 rselect_tail(queue_208)=index_207),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f556,f314])).
% 6.63/6.25 fof(f4907,plain,(
% 6.63/6.25 index_209=rselect_head(queue_206)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f478,f4904])).
% 6.63/6.25 fof(f4908,plain,(
% 6.63/6.25 index_209=index_189),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4903,f4907])).
% 6.63/6.25 fof(f4912,plain,(
% 6.63/6.25 ![X0]: (index_84=X0|select(earray_85,X0)=select(earray_83,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f428,f311])).
% 6.63/6.25 fof(f4914,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_91,X0)=select(earray_89,X0))),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f430,f311])).
% 6.63/6.25 fof(f4918,plain,(
% 6.63/6.25 index_210=s(index_189)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4908,f480])).
% 6.63/6.25 fof(f4971,plain,(
% 6.63/6.25 q9=rstore_head(queue_208,index_210)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f616,f557])).
% 6.63/6.25 fof(f4972,plain,(
% 6.63/6.25 rselect_tail(q9)=rselect_tail(queue_208)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4971,f320])).
% 6.63/6.25 fof(f4974,plain,(
% 6.63/6.25 rselect_head(q9)=index_210),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4971,f313])).
% 6.63/6.25 fof(f4975,plain,(
% 6.63/6.25 index_9=rselect_tail(queue_208)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f509,f4972])).
% 6.63/6.25 fof(f4977,plain,(
% 6.63/6.25 index_9=index_207),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4975,f4906])).
% 6.63/6.25 fof(f4984,plain,(
% 6.63/6.25 index_9=s(index_204)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f4977,f477])).
% 6.63/6.25 fof(f4991,plain,(
% 6.63/6.25 rselect_head(queue_23)=rselect_head(q11)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f558,f318])).
% 6.63/6.25 fof(f4992,plain,(
% 6.63/6.25 rselect_seq(queue_23)=earray_22),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f558,f312])).
% 6.63/6.25 fof(f4994,plain,(
% 6.63/6.25 rselect_head(queue_25)=rselect_head(queue_23)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f559,f317])).
% 6.63/6.25 fof(f4995,plain,(
% 6.63/6.25 rselect_seq(queue_25)=rselect_seq(queue_23)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f559,f316])).
% 6.63/6.25 fof(f4996,plain,(
% 6.63/6.25 rselect_tail(queue_25)=index_24),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f559,f314])).
% 6.63/6.25 fof(f4997,plain,(
% 6.63/6.25 index_26=rselect_head(queue_23)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f483,f4994])).
% 6.63/6.25 fof(f5192,plain,(
% 6.63/6.25 q12=rstore_head(queue_25,index_27)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f590,f560])).
% 6.63/6.25 fof(f5193,plain,(
% 6.63/6.25 rselect_tail(q12)=rselect_tail(queue_25)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5192,f320])).
% 6.63/6.25 fof(f5194,plain,(
% 6.63/6.25 rselect_seq(q12)=rselect_seq(queue_25)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5192,f315])).
% 6.63/6.25 fof(f5195,plain,(
% 6.63/6.25 rselect_head(q12)=index_27),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5192,f313])).
% 6.63/6.25 fof(f5196,plain,(
% 6.63/6.25 index_30=rselect_tail(queue_25)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f486,f5193])).
% 6.63/6.25 fof(f5197,plain,(
% 6.63/6.25 earray_29=rselect_seq(queue_25)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f409,f5194])).
% 6.63/6.25 fof(f5198,plain,(
% 6.63/6.25 index_30=index_24),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5196,f4996])).
% 6.63/6.25 fof(f5202,plain,(
% 6.63/6.25 ~s(index_30)=index_15),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5198,f4496])).
% 6.63/6.25 fof(f5203,plain,(
% 6.63/6.25 ~index_30=index_15),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5198,f4419])).
% 6.63/6.25 fof(f5209,plain,(
% 6.63/6.25 ~index_33=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f487,f5202])).
% 6.63/6.25 fof(f5212,plain,(
% 6.63/6.25 rselect_head(queue_32)=rselect_head(q12)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f561,f318])).
% 6.63/6.25 fof(f5213,plain,(
% 6.63/6.25 rselect_seq(queue_32)=earray_31),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f561,f312])).
% 6.63/6.25 fof(f5215,plain,(
% 6.63/6.25 q13=rstore_tail(queue_32,index_33)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f591,f562])).
% 6.63/6.25 fof(f5216,plain,(
% 6.63/6.25 rselect_head(q13)=rselect_head(queue_32)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5215,f317])).
% 6.63/6.25 fof(f5217,plain,(
% 6.63/6.25 rselect_seq(q13)=rselect_seq(queue_32)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5215,f316])).
% 6.63/6.25 fof(f5218,plain,(
% 6.63/6.25 rselect_tail(q13)=index_33),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5215,f314])).
% 6.63/6.25 fof(f5219,plain,(
% 6.63/6.25 earray_35=rselect_seq(queue_32)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f411,f5217])).
% 6.63/6.25 fof(f5220,plain,(
% 6.63/6.25 index_36=index_33),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f488,f5218])).
% 6.63/6.25 fof(f5222,plain,(
% 6.63/6.25 rselect_head(queue_38)=rselect_head(q13)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f563,f318])).
% 6.63/6.25 fof(f5223,plain,(
% 6.63/6.25 rselect_seq(queue_38)=earray_37),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f563,f312])).
% 6.63/6.25 fof(f5227,plain,(
% 6.63/6.25 ~index_36=index_15),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5220,f5209])).
% 6.63/6.25 fof(f5231,plain,(
% 6.63/6.25 index_36=s(index_30)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5220,f487])).
% 6.63/6.25 fof(f5233,plain,(
% 6.63/6.25 q14=rstore_tail(queue_38,index_39)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f592,f564])).
% 6.63/6.25 fof(f5234,plain,(
% 6.63/6.25 rselect_head(q14)=rselect_head(queue_38)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5233,f317])).
% 6.63/6.25 fof(f5235,plain,(
% 6.63/6.25 rselect_seq(q14)=rselect_seq(queue_38)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5233,f316])).
% 6.63/6.25 fof(f5236,plain,(
% 6.63/6.25 rselect_tail(q14)=index_39),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5233,f314])).
% 6.63/6.25 fof(f5237,plain,(
% 6.63/6.25 earray_41=rselect_seq(queue_38)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f414,f5235])).
% 6.63/6.25 fof(f5238,plain,(
% 6.63/6.25 index_42=index_39),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f490,f5236])).
% 6.63/6.25 fof(f5243,plain,(
% 6.63/6.25 index_42=s(index_36)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5238,f489])).
% 6.63/6.25 fof(f5297,plain,(
% 6.63/6.25 earray_35=earray_31),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5213,f5219])).
% 6.63/6.25 fof(f5299,plain,(
% 6.63/6.25 rselect_head(queue_44)=rselect_head(q14)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f565,f318])).
% 6.63/6.25 fof(f5300,plain,(
% 6.63/6.25 rselect_seq(queue_44)=earray_43),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f565,f312])).
% 6.63/6.25 fof(f5302,plain,(
% 6.63/6.25 rselect_head(queue_46)=rselect_head(queue_44)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f566,f317])).
% 6.63/6.25 fof(f5303,plain,(
% 6.63/6.25 rselect_seq(queue_46)=rselect_seq(queue_44)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f566,f316])).
% 6.63/6.25 fof(f5304,plain,(
% 6.63/6.25 rselect_tail(queue_46)=index_45),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f566,f314])).
% 6.63/6.25 fof(f5305,plain,(
% 6.63/6.25 index_47=rselect_head(queue_44)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f492,f5302])).
% 6.63/6.25 fof(f5358,plain,(
% 6.63/6.25 earray_41=earray_37),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5223,f5237])).
% 6.63/6.25 fof(f5460,plain,(
% 6.63/6.25 q15=rstore_head(queue_46,index_48)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f593,f567])).
% 6.63/6.25 fof(f5461,plain,(
% 6.63/6.25 rselect_tail(q15)=rselect_tail(queue_46)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5460,f320])).
% 6.63/6.25 fof(f5462,plain,(
% 6.63/6.25 rselect_seq(q15)=rselect_seq(queue_46)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5460,f315])).
% 6.63/6.25 fof(f5463,plain,(
% 6.63/6.25 rselect_head(q15)=index_48),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5460,f313])).
% 6.63/6.25 fof(f5464,plain,(
% 6.63/6.25 index_51=rselect_tail(queue_46)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f494,f5461])).
% 6.63/6.25 fof(f5465,plain,(
% 6.63/6.25 earray_50=rselect_seq(queue_46)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f416,f5462])).
% 6.63/6.25 fof(f5466,plain,(
% 6.63/6.25 index_51=index_45),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5464,f5304])).
% 6.63/6.25 fof(f5472,plain,(
% 6.63/6.25 index_51=s(index_42)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5466,f491])).
% 6.63/6.25 fof(f5476,plain,(
% 6.63/6.25 rselect_head(queue_5)=rselect_head(q0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f568,f318])).
% 6.63/6.25 fof(f5479,plain,(
% 6.63/6.25 rselect_head(queue_5)=index_3),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1832,f5476])).
% 6.63/6.25 fof(f5481,plain,(
% 6.63/6.25 rselect_head(queue_53)=rselect_head(q15)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f569,f318])).
% 6.63/6.25 fof(f5482,plain,(
% 6.63/6.25 rselect_seq(queue_53)=earray_52),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f569,f312])).
% 6.63/6.25 fof(f5484,plain,(
% 6.63/6.25 q16=rstore_tail(queue_53,index_54)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f594,f570])).
% 6.63/6.25 fof(f5485,plain,(
% 6.63/6.25 rselect_head(q16)=rselect_head(queue_53)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5484,f317])).
% 6.63/6.25 fof(f5486,plain,(
% 6.63/6.25 rselect_seq(q16)=rselect_seq(queue_53)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5484,f316])).
% 6.63/6.25 fof(f5487,plain,(
% 6.63/6.25 rselect_tail(q16)=index_54),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5484,f314])).
% 6.63/6.25 fof(f5488,plain,(
% 6.63/6.25 earray_56=rselect_seq(queue_53)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f418,f5486])).
% 6.63/6.25 fof(f5489,plain,(
% 6.63/6.25 index_57=index_54),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f496,f5487])).
% 6.63/6.25 fof(f5495,plain,(
% 6.63/6.25 index_57=s(index_51)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5489,f495])).
% 6.63/6.25 fof(f5498,plain,(
% 6.63/6.25 rselect_head(queue_59)=rselect_head(q16)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f571,f318])).
% 6.63/6.25 fof(f5499,plain,(
% 6.63/6.25 rselect_seq(queue_59)=earray_58),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f571,f312])).
% 6.63/6.25 fof(f5553,plain,(
% 6.63/6.25 earray_56=earray_52),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5482,f5488])).
% 6.63/6.25 fof(f5653,plain,(
% 6.63/6.25 q17=rstore_tail(queue_59,index_60)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f595,f572])).
% 6.63/6.25 fof(f5654,plain,(
% 6.63/6.25 rselect_head(q17)=rselect_head(queue_59)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5653,f317])).
% 6.63/6.25 fof(f5655,plain,(
% 6.63/6.25 rselect_seq(q17)=rselect_seq(queue_59)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5653,f316])).
% 6.63/6.25 fof(f5656,plain,(
% 6.63/6.25 rselect_tail(q17)=index_60),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5653,f314])).
% 6.63/6.25 fof(f5657,plain,(
% 6.63/6.25 earray_62=rselect_seq(queue_59)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f420,f5655])).
% 6.63/6.25 fof(f5658,plain,(
% 6.63/6.25 index_63=index_60),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f499,f5656])).
% 6.63/6.25 fof(f5660,plain,(
% 6.63/6.25 rselect_head(queue_65)=rselect_head(q17)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f573,f318])).
% 6.63/6.25 fof(f5661,plain,(
% 6.63/6.25 rselect_seq(queue_65)=earray_64),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f573,f312])).
% 6.63/6.25 fof(f5667,plain,(
% 6.63/6.25 index_63=s(index_57)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5658,f498])).
% 6.63/6.25 fof(f5674,plain,(
% 6.63/6.25 earray_62=earray_58),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5499,f5657])).
% 6.63/6.25 fof(f5774,plain,(
% 6.63/6.25 rselect_head(queue_67)=rselect_head(queue_65)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f574,f317])).
% 6.63/6.25 fof(f5775,plain,(
% 6.63/6.25 rselect_seq(queue_67)=rselect_seq(queue_65)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f574,f316])).
% 6.63/6.25 fof(f5776,plain,(
% 6.63/6.25 rselect_tail(queue_67)=index_66),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f574,f314])).
% 6.63/6.25 fof(f5777,plain,(
% 6.63/6.25 index_68=rselect_head(queue_65)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f501,f5774])).
% 6.63/6.25 fof(f5778,plain,(
% 6.63/6.25 rselect_seq(queue_67)=earray_64),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5661,f5775])).
% 6.63/6.25 fof(f5779,plain,(
% 6.63/6.25 q1=rstore_tail(queue_5,index_6)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f587,f575])).
% 6.63/6.25 fof(f5780,plain,(
% 6.63/6.25 rselect_head(q1)=rselect_head(queue_5)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5779,f317])).
% 6.63/6.25 fof(f5782,plain,(
% 6.63/6.25 rselect_tail(q1)=index_6),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5779,f314])).
% 6.63/6.25 fof(f5783,plain,(
% 6.63/6.25 rselect_head(q1)=index_3),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5479,f5780])).
% 6.63/6.25 fof(f5786,plain,(
% 6.63/6.25 index_78=index_6),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f505,f5782])).
% 6.63/6.25 fof(f5787,plain,(
% 6.63/6.25 q18=rstore_head(queue_67,index_69)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f596,f576])).
% 6.63/6.25 fof(f5788,plain,(
% 6.63/6.25 rselect_tail(q18)=rselect_tail(queue_67)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5787,f320])).
% 6.63/6.25 fof(f5789,plain,(
% 6.63/6.25 rselect_seq(q18)=rselect_seq(queue_67)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5787,f315])).
% 6.63/6.25 fof(f5790,plain,(
% 6.63/6.25 rselect_head(q18)=index_69),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5787,f313])).
% 6.63/6.25 fof(f5791,plain,(
% 6.63/6.25 index_72=rselect_tail(queue_67)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f503,f5788])).
% 6.63/6.25 fof(f5792,plain,(
% 6.63/6.25 earray_71=rselect_seq(queue_67)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f422,f5789])).
% 6.63/6.25 fof(f5793,plain,(
% 6.63/6.25 earray_71=earray_64),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5778,f5792])).
% 6.63/6.25 fof(f5795,plain,(
% 6.63/6.25 rselect_head(queue_74)=rselect_head(q18)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f577,f318])).
% 6.63/6.25 fof(f5796,plain,(
% 6.63/6.25 rselect_seq(queue_74)=earray_73),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f577,f312])).
% 6.63/6.25 fof(f5803,plain,(
% 6.63/6.25 index_78=s(index_3)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5786,f497])).
% 6.63/6.25 fof(f5807,plain,(
% 6.63/6.25 q19=rstore_tail(queue_74,index_75)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f597,f578])).
% 6.63/6.25 fof(f5808,plain,(
% 6.63/6.25 rselect_head(q19)=rselect_head(queue_74)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5807,f317])).
% 6.63/6.25 fof(f5809,plain,(
% 6.63/6.25 rselect_seq(q19)=rselect_seq(queue_74)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5807,f316])).
% 6.63/6.25 fof(f5810,plain,(
% 6.63/6.25 rselect_tail(q19)=index_75),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5807,f314])).
% 6.63/6.25 fof(f5811,plain,(
% 6.63/6.25 earray_83=rselect_seq(queue_74)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f427,f5809])).
% 6.63/6.25 fof(f5812,plain,(
% 6.63/6.25 index_84=index_75),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f507,f5810])).
% 6.63/6.25 fof(f5816,plain,(
% 6.63/6.25 index_84=s(index_72)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5812,f504])).
% 6.63/6.25 fof(f5818,plain,(
% 6.63/6.25 index_72=index_66),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5791,f5776])).
% 6.63/6.25 fof(f5825,plain,(
% 6.63/6.25 index_72=s(index_63)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5818,f500])).
% 6.63/6.25 fof(f5827,plain,(
% 6.63/6.25 rselect_head(queue_80)=rselect_head(q1)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f579,f318])).
% 6.63/6.25 fof(f5830,plain,(
% 6.63/6.25 rselect_head(queue_80)=index_3),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5783,f5827])).
% 6.63/6.25 fof(f5831,plain,(
% 6.63/6.25 q2=rstore_tail(queue_80,index_81)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f598,f580])).
% 6.63/6.25 fof(f5832,plain,(
% 6.63/6.25 rselect_head(q2)=rselect_head(queue_80)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5831,f317])).
% 6.63/6.25 fof(f5834,plain,(
% 6.63/6.25 rselect_tail(q2)=index_81),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f5831,f314])).
% 6.63/6.25 fof(f5836,plain,(
% 6.63/6.25 index_153=index_81),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f455,f5834])).
% 6.63/6.25 fof(f5841,plain,(
% 6.63/6.25 index_153=s(index_78)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f5836,f506])).
% 6.63/6.25 fof(f5895,plain,(
% 6.63/6.25 earray_83=earray_73),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5796,f5811])).
% 6.63/6.25 fof(f6926,plain,(
% 6.63/6.25 rselect_head(queue_86)=rselect_head(q19)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f581,f318])).
% 6.63/6.25 fof(f6927,plain,(
% 6.63/6.25 rselect_seq(queue_86)=earray_85),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f581,f312])).
% 6.63/6.25 fof(f6929,plain,(
% 6.63/6.25 q20=rstore_tail(queue_86,index_87)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f599,f582])).
% 6.63/6.25 fof(f6930,plain,(
% 6.63/6.25 rselect_head(q20)=rselect_head(queue_86)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f6929,f317])).
% 6.63/6.25 fof(f6931,plain,(
% 6.63/6.25 rselect_seq(q20)=rselect_seq(queue_86)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f6929,f316])).
% 6.63/6.25 fof(f6932,plain,(
% 6.63/6.25 rselect_tail(q20)=index_87),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f6929,f314])).
% 6.63/6.25 fof(f6933,plain,(
% 6.63/6.25 earray_89=rselect_seq(queue_86)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f429,f6931])).
% 6.63/6.25 fof(f6934,plain,(
% 6.63/6.25 index_90=index_87),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f510,f6932])).
% 6.63/6.25 fof(f6936,plain,(
% 6.63/6.25 rselect_head(queue_92)=rselect_head(q20)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f583,f318])).
% 6.63/6.25 fof(f6937,plain,(
% 6.63/6.25 rselect_seq(queue_92)=earray_91),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f583,f312])).
% 6.63/6.25 fof(f6939,plain,(
% 6.63/6.25 rselect_head(queue_94)=rselect_head(queue_92)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f584,f317])).
% 6.63/6.25 fof(f6941,plain,(
% 6.63/6.25 rselect_tail(queue_94)=index_93),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f584,f314])).
% 6.63/6.25 fof(f6942,plain,(
% 6.63/6.25 index_95=rselect_head(queue_92)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f512,f6939])).
% 6.63/6.25 fof(f6949,plain,(
% 6.63/6.25 index_90=s(index_84)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f6934,f508])).
% 6.63/6.25 fof(f6951,plain,(
% 6.63/6.25 q21=rstore_head(queue_94,index_96)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f600,f585])).
% 6.63/6.25 fof(f6952,plain,(
% 6.63/6.25 rselect_tail(q21)=rselect_tail(queue_94)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f6951,f320])).
% 6.63/6.25 fof(f6953,plain,(
% 6.63/6.25 rselect_seq(q21)=rselect_seq(queue_94)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f6951,f315])).
% 6.63/6.25 fof(f6954,plain,(
% 6.63/6.25 rselect_head(q21)=index_96),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f6951,f313])).
% 6.63/6.25 fof(f6955,plain,(
% 6.63/6.25 index_99=rselect_tail(queue_94)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f514,f6952])).
% 6.63/6.25 fof(f6956,plain,(
% 6.63/6.25 earray_98=rselect_seq(queue_94)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f431,f6953])).
% 6.63/6.25 fof(f6971,plain,(
% 6.63/6.25 earray_89=earray_85),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6927,f6933])).
% 6.63/6.25 fof(f7084,plain,(
% 6.63/6.25 index_99=index_93),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f6955,f6941])).
% 6.63/6.25 fof(f7089,plain,(
% 6.63/6.25 queue_94=rstore_tail(queue_92,index_99)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f7084,f584])).
% 6.63/6.25 fof(f7092,plain,(
% 6.63/6.25 index_99=s(index_90)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f7084,f511])).
% 6.63/6.25 fof(f7692,plain,(
% 6.63/6.25 rselect_head(queue_101)=index_96),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6954,f1834])).
% 6.63/6.25 fof(f7693,plain,(
% 6.63/6.25 rselect_head(q22)=index_96),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7692,f1838])).
% 6.63/6.25 fof(f7694,plain,(
% 6.63/6.25 rselect_head(queue_107)=index_96),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7693,f1910])).
% 6.63/6.25 fof(f7695,plain,(
% 6.63/6.25 rselect_head(q23)=index_96),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7694,f1914])).
% 6.63/6.25 fof(f7696,plain,(
% 6.63/6.25 rselect_head(queue_11)=index_210),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4974,f2159])).
% 6.63/6.25 fof(f7697,plain,(
% 6.63/6.25 index_116=index_96),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f7698,f7695])).
% 6.63/6.25 fof(f7698,plain,(
% 6.63/6.25 index_116=rselect_head(q23)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2169,f2163])).
% 6.63/6.25 fof(f7707,plain,(
% 6.63/6.25 index_116=s(index_95)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f7697,f513])).
% 6.63/6.25 fof(f7918,plain,(
% 6.63/6.25 rselect_head(q10)=index_210),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7696,f2634])).
% 6.63/6.25 fof(f7941,plain,(
% 6.63/6.25 index_158=rselect_head(q2)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3801,f3795])).
% 6.63/6.25 fof(f7946,plain,(
% 6.63/6.25 rselect_head(queue_17)=index_210),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7918,f4074])).
% 6.63/6.25 fof(f7970,plain,(
% 6.63/6.25 rselect_head(q11)=index_210),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7946,f4404])).
% 6.63/6.25 fof(f7971,plain,(
% 6.63/6.25 ~s(s(index_30))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4474])).
% 6.63/6.25 fof(f7972,plain,(
% 6.63/6.25 ~s(index_36)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f7971])).
% 6.63/6.25 fof(f7973,plain,(
% 6.63/6.25 ~index_42=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f7972])).
% 6.63/6.25 fof(f7994,plain,(
% 6.63/6.25 index_26=rselect_head(q11)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4997,f4991])).
% 6.63/6.25 fof(f7999,plain,(
% 6.63/6.25 index_27=s(index_210)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8001,f484])).
% 6.63/6.25 fof(f8001,plain,(
% 6.63/6.25 index_26=index_210),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7970,f7994])).
% 6.63/6.25 fof(f8055,plain,(
% 6.63/6.25 earray_29=rselect_seq(queue_23)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5197,f4995])).
% 6.63/6.25 fof(f8059,plain,(
% 6.63/6.25 earray_29=earray_22),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4992,f8055])).
% 6.63/6.25 fof(f8076,plain,(
% 6.63/6.25 rselect_head(queue_32)=index_27),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5195,f5212])).
% 6.63/6.25 fof(f8077,plain,(
% 6.63/6.25 rselect_head(q13)=index_27),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8076,f5216])).
% 6.63/6.25 fof(f8078,plain,(
% 6.63/6.25 rselect_head(queue_38)=index_27),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8077,f5222])).
% 6.63/6.25 fof(f8079,plain,(
% 6.63/6.25 rselect_head(q14)=index_27),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8078,f5234])).
% 6.63/6.25 fof(f8084,plain,(
% 6.63/6.25 index_47=rselect_head(q14)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5305,f5299])).
% 6.63/6.25 fof(f8089,plain,(
% 6.63/6.25 index_48=s(index_27)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8091,f493])).
% 6.63/6.25 fof(f8091,plain,(
% 6.63/6.25 index_47=index_27),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8079,f8084])).
% 6.63/6.25 fof(f8144,plain,(
% 6.63/6.25 earray_50=rselect_seq(queue_44)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5465,f5303])).
% 6.63/6.25 fof(f8148,plain,(
% 6.63/6.25 earray_50=earray_43),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5300,f8144])).
% 6.63/6.25 fof(f8161,plain,(
% 6.63/6.25 rselect_head(queue_53)=index_48),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5463,f5481])).
% 6.63/6.25 fof(f8162,plain,(
% 6.63/6.25 rselect_head(q16)=index_48),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8161,f5485])).
% 6.63/6.25 fof(f8168,plain,(
% 6.63/6.25 rselect_head(queue_59)=index_48),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8162,f5498])).
% 6.63/6.25 fof(f8174,plain,(
% 6.63/6.25 rselect_head(q17)=index_48),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8168,f5654])).
% 6.63/6.25 fof(f8175,plain,(
% 6.63/6.25 index_68=rselect_head(q17)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5777,f5660])).
% 6.63/6.25 fof(f8180,plain,(
% 6.63/6.25 index_69=s(index_48)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8182,f502])).
% 6.63/6.25 fof(f8182,plain,(
% 6.63/6.25 index_68=index_48),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8174,f8175])).
% 6.63/6.25 fof(f8242,plain,(
% 6.63/6.25 rselect_head(queue_74)=index_69),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5790,f5795])).
% 6.63/6.25 fof(f8255,plain,(
% 6.63/6.25 rselect_head(q19)=index_69),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8242,f5808])).
% 6.63/6.25 fof(f8266,plain,(
% 6.63/6.25 index_158=rselect_head(queue_80)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7941,f5832])).
% 6.63/6.25 fof(f8272,plain,(
% 6.63/6.25 index_159=s(index_3)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8274,f458])).
% 6.63/6.25 fof(f8274,plain,(
% 6.63/6.25 index_158=index_3),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5830,f8266])).
% 6.63/6.25 fof(f8275,plain,(
% 6.63/6.25 index_159=index_78),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5803,f8272])).
% 6.63/6.25 fof(f8282,plain,(
% 6.63/6.25 index_189=s(index_78)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8275,f4348])).
% 6.63/6.25 fof(f8292,plain,(
% 6.63/6.25 index_189=index_153),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5841,f8282])).
% 6.63/6.25 fof(f8297,plain,(
% 6.63/6.25 index_210=s(index_153)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8292,f4918])).
% 6.63/6.25 fof(f8307,plain,(
% 6.63/6.25 index_210=index_171),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3827,f8297])).
% 6.63/6.25 fof(f8313,plain,(
% 6.63/6.25 index_27=s(index_171)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8307,f7999])).
% 6.63/6.25 fof(f8323,plain,(
% 6.63/6.25 index_27=index_177),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4099,f8313])).
% 6.63/6.25 fof(f8336,plain,(
% 6.63/6.25 index_48=s(index_177)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8323,f8089])).
% 6.63/6.25 fof(f8346,plain,(
% 6.63/6.25 index_48=index_183),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4227,f8336])).
% 6.63/6.25 fof(f8351,plain,(
% 6.63/6.25 index_69=s(index_183)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8346,f8180])).
% 6.63/6.25 fof(f8362,plain,(
% 6.63/6.25 index_69=index_192),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4539,f8351])).
% 6.63/6.25 fof(f8365,plain,(
% 6.63/6.25 rselect_head(q19)=index_192),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8362,f8255])).
% 6.63/6.25 fof(f8382,plain,(
% 6.63/6.25 rselect_seq(queue_94)=rselect_seq(queue_92)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f7089,f316])).
% 6.63/6.25 fof(f8385,plain,(
% 6.63/6.25 earray_98=rselect_seq(queue_92)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6956,f8382])).
% 6.63/6.25 fof(f8407,plain,(
% 6.63/6.25 earray_98=earray_91),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8385,f6937])).
% 6.63/6.25 fof(f8427,plain,(
% 6.63/6.25 rselect_head(queue_86)=index_192),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8365,f6926])).
% 6.63/6.25 fof(f8428,plain,(
% 6.63/6.25 rselect_head(q20)=index_192),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8427,f6930])).
% 6.63/6.25 fof(f8429,plain,(
% 6.63/6.25 index_95=rselect_head(q20)),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6942,f6936])).
% 6.63/6.25 fof(f8432,plain,(
% 6.63/6.25 index_116=s(index_192)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8438,f7707])).
% 6.63/6.25 fof(f8438,plain,(
% 6.63/6.25 index_95=index_192),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8428,f8429])).
% 6.63/6.25 fof(f8439,plain,(
% 6.63/6.25 index_116=index_198),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4668,f8432])).
% 6.63/6.25 fof(f8452,plain,(
% 6.63/6.25 index_117=s(index_198)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8439,f440])).
% 6.63/6.25 fof(f8454,plain,(
% 6.63/6.25 index_117=index_204),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4797,f8452])).
% 6.63/6.25 fof(f8471,plain,(
% 6.63/6.25 index_138=s(index_204)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8454,f3009])).
% 6.63/6.25 fof(f8481,plain,(
% 6.63/6.25 index_138=index_9),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4984,f8471])).
% 6.63/6.25 fof(f8486,plain,(
% 6.63/6.25 index_213=s(index_9)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8481,f4012])).
% 6.63/6.25 fof(f8497,plain,(
% 6.63/6.25 index_213=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2650,f8486])).
% 6.63/6.25 fof(f8503,plain,(
% 6.63/6.25 elem_214=select(earray_163,index_15)),
% 6.63/6.25 inference(backward_demodulation,[status(thm)],[f8497,f4009])).
% 6.63/6.25 fof(f8868,plain,(
% 6.63/6.25 ~s(s(s(index_30)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4475])).
% 6.63/6.25 fof(f8869,plain,(
% 6.63/6.25 ~s(s(index_36))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f8868])).
% 6.63/6.25 fof(f8870,plain,(
% 6.63/6.25 ~s(index_42)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f8869])).
% 6.63/6.25 fof(f8871,plain,(
% 6.63/6.25 ~index_51=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f8870])).
% 6.63/6.25 fof(f9320,plain,(
% 6.63/6.25 ~s(s(s(s(index_30))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4476])).
% 6.63/6.25 fof(f9321,plain,(
% 6.63/6.25 ~s(s(s(index_36)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f9320])).
% 6.63/6.25 fof(f9322,plain,(
% 6.63/6.25 ~s(s(index_42))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f9321])).
% 6.63/6.25 fof(f9323,plain,(
% 6.63/6.25 ~s(index_51)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f9322])).
% 6.63/6.25 fof(f9324,plain,(
% 6.63/6.25 ~index_57=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f9323])).
% 6.63/6.25 fof(f9534,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_148,index_15)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f8503,f4071])).
% 6.63/6.25 fof(f9538,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_142,index_15)|index_147=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f4066,f9534])).
% 6.63/6.25 fof(f9565,plain,(
% 6.63/6.25 ![X0]: (index_21=X0|select(earray_22,X0)=select(earray_16,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f4408,f4350])).
% 6.63/6.25 fof(f9568,plain,(
% 6.63/6.25 ![X0]: (index_30=X0|select(earray_31,X0)=select(earray_22,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8059,f4420])).
% 6.63/6.25 fof(f9571,plain,(
% 6.63/6.25 ![X0]: (index_36=X0|select(earray_37,X0)=select(earray_31,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5297,f4422])).
% 6.63/6.25 fof(f9576,plain,(
% 6.63/6.25 ![X0]: (index_42=X0|select(earray_43,X0)=select(earray_37,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5358,f4648])).
% 6.63/6.25 fof(f9586,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_133,index_15)|index_147=index_15|index_141=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f3943,f9538])).
% 6.63/6.25 fof(f9588,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_127,index_15)|index_147=index_15|index_141=index_15|index_132=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f3940,f9586])).
% 6.63/6.25 fof(f9590,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_121,index_15)|index_147=index_15|index_141=index_15|index_132=index_15|index_126=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f3822,f9588])).
% 6.63/6.25 fof(f9592,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_112,index_15)|index_147=index_15|index_141=index_15|index_132=index_15|index_126=index_15|index_120=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f3810,f9590])).
% 6.63/6.25 fof(f9594,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_106,index_15)|index_147=index_15|index_141=index_15|index_132=index_15|index_126=index_15|index_120=index_15|index_111=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f3807,f9592])).
% 6.63/6.25 fof(f9596,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)|index_147=index_15|index_141=index_15|index_132=index_15|index_126=index_15|index_120=index_15|index_111=index_15|index_105=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f3804,f9594])).
% 6.63/6.25 fof(f9598,plain,(
% 6.63/6.25 ![X0]: (index_51=X0|select(earray_52,X0)=select(earray_43,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8148,f4650])).
% 6.63/6.25 fof(f9601,plain,(
% 6.63/6.25 ![X0]: (index_57=X0|select(earray_58,X0)=select(earray_52,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5553,f4671])).
% 6.63/6.25 fof(f9604,plain,(
% 6.63/6.25 ![X0]: (index_63=X0|select(earray_64,X0)=select(earray_58,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5674,f4777])).
% 6.63/6.25 fof(f9607,plain,(
% 6.63/6.25 ![X0]: (index_72=X0|select(earray_73,X0)=select(earray_64,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5793,f4779])).
% 6.63/6.25 fof(f9648,plain,(
% 6.63/6.25 ![X0]: (index_84=X0|select(earray_85,X0)=select(earray_73,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5895,f4912])).
% 6.63/6.25 fof(f9651,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_89,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f8407,f4914])).
% 6.63/6.25 fof(f9652,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_85,X0))),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6971,f9651])).
% 6.63/6.25 fof(f9654,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_73,X0)|index_84=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9648,f9652])).
% 6.63/6.25 fof(f10161,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_30)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4477])).
% 6.63/6.25 fof(f10162,plain,(
% 6.63/6.25 ~s(s(s(s(index_36))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f10161])).
% 6.63/6.25 fof(f10163,plain,(
% 6.63/6.25 ~s(s(s(index_42)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f10162])).
% 6.63/6.25 fof(f10164,plain,(
% 6.63/6.25 ~s(s(index_51))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f10163])).
% 6.63/6.25 fof(f10165,plain,(
% 6.63/6.25 ~s(index_57)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f10164])).
% 6.63/6.25 fof(f10166,plain,(
% 6.63/6.25 ~index_63=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f10165])).
% 6.63/6.25 fof(f10738,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_30))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4478])).
% 6.63/6.25 fof(f10739,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_36)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f10738])).
% 6.63/6.25 fof(f10740,plain,(
% 6.63/6.25 ~s(s(s(s(index_42))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f10739])).
% 6.63/6.25 fof(f10741,plain,(
% 6.63/6.25 ~s(s(s(index_51)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f10740])).
% 6.63/6.25 fof(f10742,plain,(
% 6.63/6.25 ~s(s(index_57))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f10741])).
% 6.63/6.25 fof(f10743,plain,(
% 6.63/6.25 ~s(index_63)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f10742])).
% 6.63/6.25 fof(f10744,plain,(
% 6.63/6.25 ~index_72=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f10743])).
% 6.63/6.25 fof(f10981,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_64,X0)|index_84=X0|index_72=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9607,f9654])).
% 6.63/6.25 fof(f11445,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_30)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4479])).
% 6.63/6.25 fof(f11446,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_36))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f11445])).
% 6.63/6.25 fof(f11447,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_42)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f11446])).
% 6.63/6.25 fof(f11448,plain,(
% 6.63/6.25 ~s(s(s(s(index_51))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f11447])).
% 6.63/6.25 fof(f11449,plain,(
% 6.63/6.25 ~s(s(s(index_57)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f11448])).
% 6.63/6.25 fof(f11450,plain,(
% 6.63/6.25 ~s(s(index_63))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f11449])).
% 6.63/6.25 fof(f11451,plain,(
% 6.63/6.25 ~s(index_72)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f11450])).
% 6.63/6.25 fof(f11452,plain,(
% 6.63/6.25 ~index_84=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f11451])).
% 6.63/6.25 fof(f11694,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_58,X0)|index_84=X0|index_72=X0|index_63=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9604,f10981])).
% 6.63/6.25 fof(f12110,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_30))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4480])).
% 6.63/6.25 fof(f12111,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_36)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f12110])).
% 6.63/6.25 fof(f12112,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_42))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f12111])).
% 6.63/6.25 fof(f12113,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_51)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f12112])).
% 6.63/6.25 fof(f12114,plain,(
% 6.63/6.25 ~s(s(s(s(index_57))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f12113])).
% 6.63/6.25 fof(f12115,plain,(
% 6.63/6.25 ~s(s(s(index_63)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f12114])).
% 6.63/6.25 fof(f12116,plain,(
% 6.63/6.25 ~s(s(index_72))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f12115])).
% 6.63/6.25 fof(f12117,plain,(
% 6.63/6.25 ~s(index_84)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f12116])).
% 6.63/6.25 fof(f12118,plain,(
% 6.63/6.25 ~index_90=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f12117])).
% 6.63/6.25 fof(f12900,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_30)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4481])).
% 6.63/6.25 fof(f12901,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_36))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f12900])).
% 6.63/6.25 fof(f12902,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_42)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f12901])).
% 6.63/6.25 fof(f12903,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_51))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f12902])).
% 6.63/6.25 fof(f12904,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_57)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f12903])).
% 6.63/6.25 fof(f12905,plain,(
% 6.63/6.25 ~s(s(s(s(index_63))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f12904])).
% 6.63/6.25 fof(f12906,plain,(
% 6.63/6.25 ~s(s(s(index_72)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f12905])).
% 6.63/6.25 fof(f12907,plain,(
% 6.63/6.25 ~s(s(index_84))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f12906])).
% 6.63/6.25 fof(f12908,plain,(
% 6.63/6.25 ~s(index_90)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f12907])).
% 6.63/6.25 fof(f12909,plain,(
% 6.63/6.25 ~index_99=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f12908])).
% 6.63/6.25 fof(f13170,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_52,X0)|index_84=X0|index_72=X0|index_63=X0|index_57=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9601,f11694])).
% 6.63/6.25 fof(f13841,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_30))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4482])).
% 6.63/6.25 fof(f13842,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_36)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f13841])).
% 6.63/6.25 fof(f13843,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_42))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f13842])).
% 6.63/6.25 fof(f13844,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_51)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f13843])).
% 6.63/6.25 fof(f13845,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_57))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f13844])).
% 6.63/6.25 fof(f13846,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_63)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f13845])).
% 6.63/6.25 fof(f13847,plain,(
% 6.63/6.25 ~s(s(s(s(index_72))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f13846])).
% 6.63/6.25 fof(f13848,plain,(
% 6.63/6.25 ~s(s(s(index_84)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f13847])).
% 6.63/6.25 fof(f13849,plain,(
% 6.63/6.25 ~s(s(index_90))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f13848])).
% 6.63/6.25 fof(f13850,plain,(
% 6.63/6.25 ~s(index_99)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f13849])).
% 6.63/6.25 fof(f13851,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)|index_147=index_15|index_141=index_15|index_132=index_15|index_126=index_15|index_120=index_15|index_111=index_15),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f9596,f13852])).
% 6.63/6.25 fof(f13852,plain,(
% 6.63/6.25 ~index_105=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f13850])).
% 6.63/6.25 fof(f14203,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_43,X0)|index_84=X0|index_72=X0|index_63=X0|index_57=X0|index_51=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9598,f13170])).
% 6.63/6.25 fof(f14924,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4483])).
% 6.63/6.25 fof(f14925,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_36))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f14924])).
% 6.63/6.25 fof(f14926,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_42)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f14925])).
% 6.63/6.25 fof(f14927,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_51))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f14926])).
% 6.63/6.25 fof(f14928,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_57)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f14927])).
% 6.63/6.25 fof(f14929,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_63))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f14928])).
% 6.63/6.25 fof(f14930,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_72)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f14929])).
% 6.63/6.25 fof(f14931,plain,(
% 6.63/6.25 ~s(s(s(s(index_84))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f14930])).
% 6.63/6.25 fof(f14932,plain,(
% 6.63/6.25 ~s(s(s(index_90)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f14931])).
% 6.63/6.25 fof(f14933,plain,(
% 6.63/6.25 ~s(s(index_99))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f14932])).
% 6.63/6.25 fof(f14934,plain,(
% 6.63/6.25 ~s(index_105)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f14933])).
% 6.63/6.25 fof(f14935,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)|index_147=index_15|index_141=index_15|index_132=index_15|index_126=index_15|index_120=index_15),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f13851,f14937])).
% 6.63/6.25 fof(f14937,plain,(
% 6.63/6.25 ~index_111=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2049,f14934])).
% 6.63/6.25 fof(f16036,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4484])).
% 6.63/6.25 fof(f16037,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f16036])).
% 6.63/6.25 fof(f16038,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_42))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f16037])).
% 6.63/6.25 fof(f16039,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_51)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f16038])).
% 6.63/6.25 fof(f16040,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_57))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f16039])).
% 6.63/6.25 fof(f16041,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_63)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f16040])).
% 6.63/6.25 fof(f16042,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_72))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f16041])).
% 6.63/6.25 fof(f16043,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_84)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f16042])).
% 6.63/6.25 fof(f16044,plain,(
% 6.63/6.25 ~s(s(s(s(index_90))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f16043])).
% 6.63/6.25 fof(f16045,plain,(
% 6.63/6.25 ~s(s(s(index_99)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f16044])).
% 6.63/6.25 fof(f16046,plain,(
% 6.63/6.25 ~s(s(index_105))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f16045])).
% 6.63/6.25 fof(f16047,plain,(
% 6.63/6.25 ~s(index_111)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2049,f16046])).
% 6.63/6.25 fof(f16049,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)|index_147=index_15|index_141=index_15|index_132=index_15|index_126=index_15),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f14935,f16051])).
% 6.63/6.25 fof(f16051,plain,(
% 6.63/6.25 ~index_120=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2272,f16047])).
% 6.63/6.25 fof(f16437,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_37,X0)|index_84=X0|index_72=X0|index_63=X0|index_57=X0|index_51=X0|index_42=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9576,f14203])).
% 6.63/6.25 fof(f17276,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4485])).
% 6.63/6.25 fof(f17277,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f17276])).
% 6.63/6.25 fof(f17278,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f17277])).
% 6.63/6.25 fof(f17279,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_51))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f17278])).
% 6.63/6.25 fof(f17280,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_57)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f17279])).
% 6.63/6.25 fof(f17281,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_63))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f17280])).
% 6.63/6.25 fof(f17282,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_72)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f17281])).
% 6.63/6.25 fof(f17283,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_84))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f17282])).
% 6.63/6.25 fof(f17284,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_90)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f17283])).
% 6.63/6.25 fof(f17285,plain,(
% 6.63/6.25 ~s(s(s(s(index_99))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f17284])).
% 6.63/6.25 fof(f17286,plain,(
% 6.63/6.25 ~s(s(s(index_105)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f17285])).
% 6.63/6.25 fof(f17287,plain,(
% 6.63/6.25 ~s(s(index_111))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2049,f17286])).
% 6.63/6.25 fof(f17288,plain,(
% 6.63/6.25 ~s(index_120)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2272,f17287])).
% 6.63/6.25 fof(f17290,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)|index_147=index_15|index_141=index_15|index_132=index_15),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f16049,f17293])).
% 6.63/6.25 fof(f17293,plain,(
% 6.63/6.25 ~index_126=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2504,f17288])).
% 6.63/6.25 fof(f17605,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_31,X0)|index_84=X0|index_72=X0|index_63=X0|index_57=X0|index_51=X0|index_42=X0|index_36=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9571,f16437])).
% 6.63/6.25 fof(f18401,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4486])).
% 6.63/6.25 fof(f18402,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f18401])).
% 6.63/6.25 fof(f18403,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f18402])).
% 6.63/6.25 fof(f18404,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f18403])).
% 6.63/6.25 fof(f18405,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_57))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f18404])).
% 6.63/6.25 fof(f18406,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_63)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f18405])).
% 6.63/6.25 fof(f18407,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_72))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f18406])).
% 6.63/6.25 fof(f18408,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_84)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f18407])).
% 6.63/6.25 fof(f18409,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_90))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f18408])).
% 6.63/6.25 fof(f18410,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_99)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f18409])).
% 6.63/6.25 fof(f18411,plain,(
% 6.63/6.25 ~s(s(s(s(index_105))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f18410])).
% 6.63/6.25 fof(f18412,plain,(
% 6.63/6.25 ~s(s(s(index_111)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2049,f18411])).
% 6.63/6.25 fof(f18413,plain,(
% 6.63/6.25 ~s(s(index_120))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2272,f18412])).
% 6.63/6.25 fof(f18414,plain,(
% 6.63/6.25 ~s(index_126)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2504,f18413])).
% 6.63/6.25 fof(f18416,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)|index_147=index_15|index_141=index_15),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f17290,f18420])).
% 6.63/6.25 fof(f18420,plain,(
% 6.63/6.25 ~index_132=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2746,f18414])).
% 6.63/6.25 fof(f19630,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4487])).
% 6.63/6.25 fof(f19631,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f19630])).
% 6.63/6.25 fof(f19632,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f19631])).
% 6.63/6.25 fof(f19633,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f19632])).
% 6.63/6.25 fof(f19634,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f19633])).
% 6.63/6.25 fof(f19635,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_63))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f19634])).
% 6.63/6.25 fof(f19636,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_72)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f19635])).
% 6.63/6.25 fof(f19637,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_84))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f19636])).
% 6.63/6.25 fof(f19638,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_90)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f19637])).
% 6.63/6.25 fof(f19639,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_99))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f19638])).
% 6.63/6.25 fof(f19640,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_105)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f19639])).
% 6.63/6.25 fof(f19641,plain,(
% 6.63/6.25 ~s(s(s(s(index_111))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2049,f19640])).
% 6.63/6.25 fof(f19642,plain,(
% 6.63/6.25 ~s(s(s(index_120)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2272,f19641])).
% 6.63/6.25 fof(f19643,plain,(
% 6.63/6.25 ~s(s(index_126))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2504,f19642])).
% 6.63/6.25 fof(f19644,plain,(
% 6.63/6.25 ~s(index_132)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2746,f19643])).
% 6.63/6.25 fof(f19648,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)|index_147=index_15),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f18416,f19651])).
% 6.63/6.25 fof(f19651,plain,(
% 6.63/6.25 ~index_141=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3126,f19644])).
% 6.63/6.25 fof(f19977,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_22,X0)|index_84=X0|index_72=X0|index_63=X0|index_57=X0|index_51=X0|index_42=X0|index_36=X0|index_30=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9568,f17605])).
% 6.63/6.25 fof(f20924,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4488])).
% 6.63/6.25 fof(f20925,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f20924])).
% 6.63/6.25 fof(f20926,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f20925])).
% 6.63/6.25 fof(f20927,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f20926])).
% 6.63/6.25 fof(f20928,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f20927])).
% 6.63/6.25 fof(f20929,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_63)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f20928])).
% 6.63/6.25 fof(f20930,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_72))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f20929])).
% 6.63/6.25 fof(f20931,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_84)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f20930])).
% 6.63/6.25 fof(f20932,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_90))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f20931])).
% 6.63/6.25 fof(f20933,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_99)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f20932])).
% 6.63/6.25 fof(f20934,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_105))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f20933])).
% 6.63/6.25 fof(f20935,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_111)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2049,f20934])).
% 6.63/6.25 fof(f20936,plain,(
% 6.63/6.25 ~s(s(s(s(index_120))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2272,f20935])).
% 6.63/6.25 fof(f20937,plain,(
% 6.63/6.25 ~s(s(s(index_126)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2504,f20936])).
% 6.63/6.25 fof(f20938,plain,(
% 6.63/6.25 ~s(s(index_132))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2746,f20937])).
% 6.63/6.25 fof(f20939,plain,(
% 6.63/6.25 ~s(index_141)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3126,f20938])).
% 6.63/6.25 fof(f20941,plain,(
% 6.63/6.25 index_162=index_15|elem_214=select(earray_100,index_15)),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f19648,f20947])).
% 6.63/6.25 fof(f20947,plain,(
% 6.63/6.25 ~index_147=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3342,f20939])).
% 6.63/6.25 fof(f21377,plain,(
% 6.63/6.25 ![X0]: (index_90=X0|select(earray_98,X0)=select(earray_16,X0)|index_84=X0|index_72=X0|index_63=X0|index_57=X0|index_51=X0|index_42=X0|index_36=X0|index_30=X0|index_21=X0)),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f9565,f19977])).
% 6.63/6.25 fof(f22362,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5198,f4489])).
% 6.63/6.25 fof(f22363,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5231,f22362])).
% 6.63/6.25 fof(f22364,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5243,f22363])).
% 6.63/6.25 fof(f22365,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5472,f22364])).
% 6.63/6.25 fof(f22366,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5495,f22365])).
% 6.63/6.25 fof(f22367,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(s(index_63))))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5667,f22366])).
% 6.63/6.25 fof(f22368,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(s(index_72)))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5825,f22367])).
% 6.63/6.25 fof(f22369,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(s(index_84))))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f5816,f22368])).
% 6.63/6.25 fof(f22370,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(s(index_90)))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f6949,f22369])).
% 6.63/6.25 fof(f22371,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(s(index_99))))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f7092,f22370])).
% 6.63/6.25 fof(f22372,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(s(index_105)))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f1848,f22371])).
% 6.63/6.25 fof(f22373,plain,(
% 6.63/6.25 ~s(s(s(s(s(s(index_111))))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2049,f22372])).
% 6.63/6.25 fof(f22374,plain,(
% 6.63/6.25 ~s(s(s(s(s(index_120)))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2272,f22373])).
% 6.63/6.25 fof(f22375,plain,(
% 6.63/6.25 ~s(s(s(s(index_126))))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2504,f22374])).
% 6.63/6.25 fof(f22376,plain,(
% 6.63/6.25 ~s(s(s(index_132)))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f2746,f22375])).
% 6.63/6.25 fof(f22377,plain,(
% 6.63/6.25 ~s(s(index_141))=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3126,f22376])).
% 6.63/6.25 fof(f22378,plain,(
% 6.63/6.25 ~s(index_147)=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3342,f22377])).
% 6.63/6.25 fof(f22384,plain,(
% 6.63/6.25 elem_214=select(earray_100,index_15)),
% 6.63/6.25 inference(backward_subsumption_resolution,[status(thm)],[f20941,f22387])).
% 6.63/6.25 fof(f22387,plain,(
% 6.63/6.25 ~index_162=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f3692,f22378])).
% 6.63/6.25 fof(f24266,plain,(
% 6.63/6.25 index_90=index_15|select(earray_98,index_15)=e10|index_84=index_15|index_72=index_15|index_63=index_15|index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f618,f21377])).
% 6.63/6.25 fof(f24270,plain,(
% 6.63/6.25 select(earray_98,index_15)=e10|index_84=index_15|index_72=index_15|index_63=index_15|index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15),
% 6.63/6.25 inference(forward_subsumption_resolution,[status(thm)],[f24266,f12118])).
% 6.63/6.25 fof(f24294,plain,(
% 6.63/6.25 select(earray_98,index_15)=e10|index_72=index_15|index_63=index_15|index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15),
% 6.63/6.25 inference(forward_subsumption_resolution,[status(thm)],[f24270,f11452])).
% 6.63/6.25 fof(f24296,plain,(
% 6.63/6.25 select(earray_100,index_15)=e10|index_72=index_15|index_63=index_15|index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.25 inference(paramodulation,[status(thm)],[f3675,f24294])).
% 6.63/6.25 fof(f24299,plain,(
% 6.63/6.25 elem_214=e10|index_72=index_15|index_63=index_15|index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.25 inference(forward_demodulation,[status(thm)],[f22384,f24296])).
% 6.63/6.25 fof(f24300,plain,(
% 6.63/6.25 index_72=index_15|index_63=index_15|index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.25 inference(forward_subsumption_resolution,[status(thm)],[f24299,f617])).
% 6.63/6.26 fof(f24303,plain,(
% 6.63/6.26 index_63=index_15|index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.26 inference(forward_subsumption_resolution,[status(thm)],[f24300,f10744])).
% 6.63/6.26 fof(f24304,plain,(
% 6.63/6.26 index_57=index_15|index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.26 inference(resolution,[status(thm)],[f24303,f10166])).
% 6.63/6.26 fof(f24336,plain,(
% 6.63/6.26 index_51=index_15|index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.26 inference(forward_subsumption_resolution,[status(thm)],[f24304,f9324])).
% 6.63/6.26 fof(f24347,plain,(
% 6.63/6.26 index_42=index_15|index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.26 inference(forward_subsumption_resolution,[status(thm)],[f24336,f8871])).
% 6.63/6.26 fof(f24348,plain,(
% 6.63/6.26 index_36=index_15|index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.26 inference(resolution,[status(thm)],[f24347,f7973])).
% 6.63/6.26 fof(f24378,plain,(
% 6.63/6.26 index_30=index_15|index_21=index_15|index_99=index_15),
% 6.63/6.26 inference(forward_subsumption_resolution,[status(thm)],[f24348,f5227])).
% 6.63/6.26 fof(f24391,plain,(
% 6.63/6.26 index_21=index_15|index_99=index_15),
% 6.63/6.26 inference(forward_subsumption_resolution,[status(thm)],[f24378,f5203])).
% 6.63/6.26 fof(f24392,plain,(
% 6.63/6.26 index_99=index_15),
% 6.63/6.26 inference(resolution,[status(thm)],[f24391,f4416])).
% 6.63/6.26 fof(f24418,plain,(
% 6.63/6.26 $false),
% 6.63/6.26 inference(forward_subsumption_resolution,[status(thm)],[f24392,f12909])).
% 6.63/6.26 % SZS output end CNFRefutation for theBenchmark.p
% 6.63/6.27 % Elapsed time: 0.929971 seconds
% 6.63/6.27 % CPU time: 7.143918 seconds
% 6.63/6.27 % Total memory used: 295.204 MB
% 6.63/6.27 % Net memory used: 293.021 MB
%------------------------------------------------------------------------------