%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV568-1.030 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 09:31:16 PM UTC 2025
% Result : Unsatisfiable 39.78s 21.65s
% Output : CNFRefutation 40.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 255
% Syntax : Number of formulae : 1097 (1054 unt; 0 typ; 0 def)
% Number of atoms : 1215 (1206 equ)
% Maximal formula atoms : 12 ( 1 avg)
% Number of connectives : 200 ( 82 ~; 118 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 1 avg)
% Maximal term depth : 49 ( 5 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 286 ( 286 usr; 277 con; 0-3 aty)
% Number of variables : 120 ( 120 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ store > select > rstore_tail > rstore_seq > rstore_head > #nlpp > s > rselect_tail > rselect_seq > rselect_head > queue_97 > queue_94 > queue_92 > queue_88 > queue_86 > queue_82 > queue_80 > queue_76 > queue_74 > queue_70 > queue_7 > queue_67 > queue_65 > queue_61 > queue_59 > queue_55 > queue_53 > queue_5 > queue_49 > queue_46 > queue_44 > queue_40 > queue_38 > queue_34 > queue_32 > queue_28 > queue_25 > queue_23 > queue_211 > queue_208 > queue_206 > queue_202 > queue_200 > queue_196 > queue_194 > queue_190 > queue_19 > queue_187 > queue_185 > queue_181 > queue_179 > queue_175 > queue_173 > queue_17 > queue_169 > queue_166 > queue_164 > queue_160 > queue_157 > queue_155 > queue_151 > queue_149 > queue_145 > queue_143 > queue_139 > queue_136 > queue_134 > queue_130 > queue_13 > queue_128 > queue_124 > queue_122 > queue_118 > queue_115 > queue_113 > queue_11 > queue_109 > queue_107 > queue_103 > queue_101 > queue_1 > q9 > q8 > q7 > q6 > q5 > q4 > q30 > q3 > q29 > q28 > q27 > q26 > q25 > q24 > q23 > q22 > q21 > q20 > q2 > q19 > q18 > q17 > q16 > q15 > q14 > q13 > q12 > q11 > q10 > q1 > q0 > q > index_99 > index_96 > index_95 > index_93 > index_90 > index_9 > index_87 > index_84 > index_81 > index_78 > index_75 > index_72 > index_69 > index_68 > index_66 > index_63 > index_60 > index_6 > index_57 > index_54 > index_51 > index_48 > index_47 > index_45 > index_42 > index_39 > index_36 > index_33 > index_30 > index_3 > index_27 > index_26 > index_24 > index_213 > index_210 > index_21 > index_209 > index_207 > index_204 > index_201 > index_198 > index_195 > index_192 > index_189 > index_188 > index_186 > index_183 > index_180 > index_18 > index_177 > index_174 > index_171 > index_168 > index_167 > index_165 > index_162 > index_159 > index_158 > index_156 > index_153 > index_150 > index_15 > index_147 > index_144 > index_141 > index_138 > index_137 > index_135 > index_132 > index_129 > index_126 > index_123 > index_120 > index_12 > index_117 > index_116 > index_114 > index_111 > index_108 > index_105 > index_102 > index_0 > elem_214 > earray_98 > earray_91 > earray_89 > earray_85 > earray_83 > earray_8 > earray_79 > earray_77 > earray_73 > earray_71 > earray_64 > earray_62 > earray_58 > earray_56 > earray_52 > earray_50 > earray_43 > earray_41 > earray_4 > earray_37 > earray_35 > earray_31 > earray_29 > earray_22 > earray_212 > earray_205 > earray_203 > earray_20 > earray_2 > earray_199 > earray_197 > earray_193 > earray_191 > earray_184 > earray_182 > earray_178 > earray_176 > earray_172 > earray_170 > earray_163 > earray_161 > earray_16 > earray_154 > earray_152 > earray_148 > earray_146 > earray_142 > earray_140 > earray_14 > earray_133 > earray_131 > earray_127 > earray_125 > earray_121 > earray_119 > earray_112 > earray_110 > earray_106 > earray_104 > earray_100 > earray_10 > e9 > e8 > e7 > e6 > e5 > e4 > e3 > e29 > e28 > e27 > e26 > e25 > e24 > e23 > e22 > e21 > e20 > e2 > e19 > e18 > e17 > e16 > e15 > e14 > e13 > e12 > e11 > e10 > e1 > e0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(e29,type,
e29: $i ).
tff(index_75,type,
index_75: $i ).
tff(earray_172,type,
earray_172: $i ).
tff(q4,type,
q4: $i ).
tff(q9,type,
q9: $i ).
tff(index_90,type,
index_90: $i ).
tff(earray_98,type,
earray_98: $i ).
tff(q16,type,
q16: $i ).
tff(earray_8,type,
earray_8: $i ).
tff(q3,type,
q3: $i ).
tff(index_6,type,
index_6: $i ).
tff(earray_163,type,
earray_163: $i ).
tff(q7,type,
q7: $i ).
tff(e1,type,
e1: $i ).
tff(earray_16,type,
earray_16: $i ).
tff(earray_52,type,
earray_52: $i ).
tff(index_30,type,
index_30: $i ).
tff(e8,type,
e8: $i ).
tff(queue_13,type,
queue_13: $i ).
tff(earray_142,type,
earray_142: $i ).
tff(elem_214,type,
elem_214: $i ).
tff(earray_20,type,
earray_20: $i ).
tff(earray_133,type,
earray_133: $i ).
tff(index_99,type,
index_99: $i ).
tff(queue_70,type,
queue_70: $i ).
tff(earray_125,type,
earray_125: $i ).
tff(e21,type,
e21: $i ).
tff(queue_101,type,
queue_101: $i ).
tff(index_48,type,
index_48: $i ).
tff(q20,type,
q20: $i ).
tff(queue_136,type,
queue_136: $i ).
tff(index_51,type,
index_51: $i ).
tff(queue_211,type,
queue_211: $i ).
tff(e15,type,
e15: $i ).
tff(earray_176,type,
earray_176: $i ).
tff(queue_65,type,
queue_65: $i ).
tff(queue_175,type,
queue_175: $i ).
tff(earray_50,type,
earray_50: $i ).
tff(queue_196,type,
queue_196: $i ).
tff(earray_197,type,
earray_197: $i ).
tff(q5,type,
q5: $i ).
tff(index_81,type,
index_81: $i ).
tff(queue_7,type,
queue_7: $i ).
tff(index_123,type,
index_123: $i ).
tff(queue_124,type,
queue_124: $i ).
tff(earray_4,type,
earray_4: $i ).
tff(queue_113,type,
queue_113: $i ).
tff(queue_32,type,
queue_32: $i ).
tff(index_102,type,
index_102: $i ).
tff(queue_149,type,
queue_149: $i ).
tff(e0,type,
e0: $i ).
tff(index_0,type,
index_0: $i ).
tff(s,type,
s: $i > $i ).
tff(q29,type,
q29: $i ).
tff(q25,type,
q25: $i ).
tff(index_135,type,
index_135: $i ).
tff(earray_106,type,
earray_106: $i ).
tff(e18,type,
e18: $i ).
tff(queue_166,type,
queue_166: $i ).
tff(queue_38,type,
queue_38: $i ).
tff(q23,type,
q23: $i ).
tff(index_96,type,
index_96: $i ).
tff(earray_14,type,
earray_14: $i ).
tff(e24,type,
e24: $i ).
tff(index_15,type,
index_15: $i ).
tff(index_27,type,
index_27: $i ).
tff(q2,type,
q2: $i ).
tff(index_195,type,
index_195: $i ).
tff(earray_112,type,
earray_112: $i ).
tff(index_138,type,
index_138: $i ).
tff(queue_128,type,
queue_128: $i ).
tff(queue_1,type,
queue_1: $i ).
tff(q10,type,
q10: $i ).
tff(q24,type,
q24: $i ).
tff(index_177,type,
index_177: $i ).
tff(store,type,
store: ( $i * $i * $i ) > $i ).
tff(index_108,type,
index_108: $i ).
tff(index_129,type,
index_129: $i ).
tff(queue_109,type,
queue_109: $i ).
tff(q1,type,
q1: $i ).
tff(index_213,type,
index_213: $i ).
tff(e20,type,
e20: $i ).
tff(earray_62,type,
earray_62: $i ).
tff(e19,type,
e19: $i ).
tff(e16,type,
e16: $i ).
tff(index_95,type,
index_95: $i ).
tff(queue_118,type,
queue_118: $i ).
tff(queue_76,type,
queue_76: $i ).
tff(earray_161,type,
earray_161: $i ).
tff(earray_203,type,
earray_203: $i ).
tff(q0,type,
q0: $i ).
tff(e2,type,
e2: $i ).
tff(index_63,type,
index_63: $i ).
tff(index_158,type,
index_158: $i ).
tff(index_42,type,
index_42: $i ).
tff(queue_169,type,
queue_169: $i ).
tff(earray_2,type,
earray_2: $i ).
tff(queue_82,type,
queue_82: $i ).
tff(q8,type,
q8: $i ).
tff(index_159,type,
index_159: $i ).
tff(queue_80,type,
queue_80: $i ).
tff(earray_85,type,
earray_85: $i ).
tff(index_54,type,
index_54: $i ).
tff(earray_191,type,
earray_191: $i ).
tff(queue_206,type,
queue_206: $i ).
tff(earray_205,type,
earray_205: $i ).
tff(e13,type,
e13: $i ).
tff(queue_179,type,
queue_179: $i ).
tff(earray_29,type,
earray_29: $i ).
tff(q26,type,
q26: $i ).
tff(queue_74,type,
queue_74: $i ).
tff(index_47,type,
index_47: $i ).
tff(earray_127,type,
earray_127: $i ).
tff(queue_194,type,
queue_194: $i ).
tff(queue_185,type,
queue_185: $i ).
tff(e22,type,
e22: $i ).
tff(index_144,type,
index_144: $i ).
tff(index_188,type,
index_188: $i ).
tff(index_3,type,
index_3: $i ).
tff(q18,type,
q18: $i ).
tff(q14,type,
q14: $i ).
tff(index_84,type,
index_84: $i ).
tff(index_186,type,
index_186: $i ).
tff(q22,type,
q22: $i ).
tff(earray_77,type,
earray_77: $i ).
tff(queue_208,type,
queue_208: $i ).
tff(e9,type,
e9: $i ).
tff(index_105,type,
index_105: $i ).
tff(rstore_seq,type,
rstore_seq: ( $i * $i ) > $i ).
tff(index_141,type,
index_141: $i ).
tff(q15,type,
q15: $i ).
tff(earray_56,type,
earray_56: $i ).
tff(index_24,type,
index_24: $i ).
tff(queue_155,type,
queue_155: $i ).
tff(earray_73,type,
earray_73: $i ).
tff(index_165,type,
index_165: $i ).
tff(index_201,type,
index_201: $i ).
tff(index_87,type,
index_87: $i ).
tff(rstore_head,type,
rstore_head: ( $i * $i ) > $i ).
tff(e25,type,
e25: $i ).
tff(queue_97,type,
queue_97: $i ).
tff(e26,type,
e26: $i ).
tff(queue_19,type,
queue_19: $i ).
tff(queue_173,type,
queue_173: $i ).
tff(q27,type,
q27: $i ).
tff(index_78,type,
index_78: $i ).
tff(queue_160,type,
queue_160: $i ).
tff(index_93,type,
index_93: $i ).
tff(earray_89,type,
earray_89: $i ).
tff(index_33,type,
index_33: $i ).
tff(earray_104,type,
earray_104: $i ).
tff(queue_11,type,
queue_11: $i ).
tff(e17,type,
e17: $i ).
tff(q17,type,
q17: $i ).
tff(index_192,type,
index_192: $i ).
tff(queue_103,type,
queue_103: $i ).
tff(index_68,type,
index_68: $i ).
tff(e27,type,
e27: $i ).
tff(earray_35,type,
earray_35: $i ).
tff(index_117,type,
index_117: $i ).
tff(e10,type,
e10: $i ).
tff(index_204,type,
index_204: $i ).
tff(index_120,type,
index_120: $i ).
tff(e7,type,
e7: $i ).
tff(queue_86,type,
queue_86: $i ).
tff(index_171,type,
index_171: $i ).
tff(earray_10,type,
earray_10: $i ).
tff(index_18,type,
index_18: $i ).
tff(queue_44,type,
queue_44: $i ).
tff(earray_131,type,
earray_131: $i ).
tff(q30,type,
q30: $i ).
tff(queue_107,type,
queue_107: $i ).
tff(index_150,type,
index_150: $i ).
tff(earray_31,type,
earray_31: $i ).
tff(index_189,type,
index_189: $i ).
tff(index_174,type,
index_174: $i ).
tff(index_207,type,
index_207: $i ).
tff(index_153,type,
index_153: $i ).
tff(earray_43,type,
earray_43: $i ).
tff(earray_193,type,
earray_193: $i ).
tff(q13,type,
q13: $i ).
tff(queue_67,type,
queue_67: $i ).
tff(index_116,type,
index_116: $i ).
tff(index_126,type,
index_126: $i ).
tff(queue_5,type,
queue_5: $i ).
tff(index_167,type,
index_167: $i ).
tff(queue_61,type,
queue_61: $i ).
tff(queue_25,type,
queue_25: $i ).
tff(index_72,type,
index_72: $i ).
tff(queue_190,type,
queue_190: $i ).
tff(queue_151,type,
queue_151: $i ).
tff(earray_22,type,
earray_22: $i ).
tff(index_183,type,
index_183: $i ).
tff(queue_92,type,
queue_92: $i ).
tff(earray_121,type,
earray_121: $i ).
tff(index_132,type,
index_132: $i ).
tff(earray_146,type,
earray_146: $i ).
tff(queue_157,type,
queue_157: $i ).
tff(earray_37,type,
earray_37: $i ).
tff(queue_40,type,
queue_40: $i ).
tff(index_21,type,
index_21: $i ).
tff(earray_184,type,
earray_184: $i ).
tff(earray_152,type,
earray_152: $i ).
tff(select,type,
select: ( $i * $i ) > $i ).
tff(queue_134,type,
queue_134: $i ).
tff(earray_110,type,
earray_110: $i ).
tff(index_209,type,
index_209: $i ).
tff(queue_88,type,
queue_88: $i ).
tff(index_66,type,
index_66: $i ).
tff(rselect_tail,type,
rselect_tail: $i > $i ).
tff(earray_148,type,
earray_148: $i ).
tff(rselect_seq,type,
rselect_seq: $i > $i ).
tff(index_12,type,
index_12: $i ).
tff(index_26,type,
index_26: $i ).
tff(earray_100,type,
earray_100: $i ).
tff(q,type,
q: $i ).
tff(queue_59,type,
queue_59: $i ).
tff(q19,type,
q19: $i ).
tff(queue_115,type,
queue_115: $i ).
tff(queue_94,type,
queue_94: $i ).
tff(index_198,type,
index_198: $i ).
tff(queue_49,type,
queue_49: $i ).
tff(queue_200,type,
queue_200: $i ).
tff(index_137,type,
index_137: $i ).
tff(index_57,type,
index_57: $i ).
tff(earray_140,type,
earray_140: $i ).
tff(e23,type,
e23: $i ).
tff(index_162,type,
index_162: $i ).
tff(earray_58,type,
earray_58: $i ).
tff(earray_170,type,
earray_170: $i ).
tff(index_114,type,
index_114: $i ).
tff(index_45,type,
index_45: $i ).
tff(e14,type,
e14: $i ).
tff(earray_212,type,
earray_212: $i ).
tff(earray_154,type,
earray_154: $i ).
tff(earray_199,type,
earray_199: $i ).
tff(queue_23,type,
queue_23: $i ).
tff(queue_28,type,
queue_28: $i ).
tff(q12,type,
q12: $i ).
tff(queue_139,type,
queue_139: $i ).
tff(earray_119,type,
earray_119: $i ).
tff(queue_145,type,
queue_145: $i ).
tff(earray_83,type,
earray_83: $i ).
tff(e12,type,
e12: $i ).
tff(e4,type,
e4: $i ).
tff(queue_130,type,
queue_130: $i ).
tff(index_111,type,
index_111: $i ).
tff(earray_41,type,
earray_41: $i ).
tff(earray_178,type,
earray_178: $i ).
tff(index_9,type,
index_9: $i ).
tff(q28,type,
q28: $i ).
tff(earray_182,type,
earray_182: $i ).
tff(index_180,type,
index_180: $i ).
tff(index_36,type,
index_36: $i ).
tff(index_156,type,
index_156: $i ).
tff(index_210,type,
index_210: $i ).
tff(index_60,type,
index_60: $i ).
tff(queue_53,type,
queue_53: $i ).
tff(q11,type,
q11: $i ).
tff(e6,type,
e6: $i ).
tff(queue_122,type,
queue_122: $i ).
tff(e11,type,
e11: $i ).
tff(e28,type,
e28: $i ).
tff(index_168,type,
index_168: $i ).
tff(e3,type,
e3: $i ).
tff(queue_181,type,
queue_181: $i ).
tff(rstore_tail,type,
rstore_tail: ( $i * $i ) > $i ).
tff(earray_79,type,
earray_79: $i ).
tff(queue_164,type,
queue_164: $i ).
tff(earray_71,type,
earray_71: $i ).
tff(rselect_head,type,
rselect_head: $i > $i ).
tff(earray_64,type,
earray_64: $i ).
tff(q21,type,
q21: $i ).
tff(queue_55,type,
queue_55: $i ).
tff(index_39,type,
index_39: $i ).
tff(index_147,type,
index_147: $i ).
tff(e5,type,
e5: $i ).
tff(earray_91,type,
earray_91: $i ).
tff(queue_143,type,
queue_143: $i ).
tff(queue_187,type,
queue_187: $i ).
tff(queue_202,type,
queue_202: $i ).
tff(queue_34,type,
queue_34: $i ).
tff(queue_46,type,
queue_46: $i ).
tff(index_69,type,
index_69: $i ).
tff(queue_17,type,
queue_17: $i ).
tff(q6,type,
q6: $i ).
tff(f_415,axiom,
q10 = queue_13,
file(unknown,unknown) ).
tff(f_354,axiom,
queue_13 = rstore_tail(queue_11,index_12),
file(unknown,unknown) ).
tff(f_35,axiom,
! [A,E] : ( rselect_tail(rstore_tail(A,E)) = E ),
file(unknown,unknown) ).
tff(f_280,axiom,
index_15 = rselect_tail(q10),
file(unknown,unknown) ).
tff(f_293,axiom,
index_18 = s(index_15),
file(unknown,unknown) ).
tff(f_197,axiom,
! [X] : ( s(X) != X ),
file(unknown,unknown) ).
tff(f_386,axiom,
queue_25 = rstore_tail(queue_23,index_24),
file(unknown,unknown) ).
tff(f_313,axiom,
index_30 = rselect_tail(q12),
file(unknown,unknown) ).
tff(f_417,axiom,
q12 = queue_28,
file(unknown,unknown) ).
tff(f_387,axiom,
queue_28 = rstore_head(queue_25,index_27),
file(unknown,unknown) ).
tff(f_47,axiom,
! [A,E] : ( rselect_tail(rstore_head(A,E)) = rselect_tail(A) ),
file(unknown,unknown) ).
tff(f_314,axiom,
index_33 = s(index_30),
file(unknown,unknown) ).
tff(f_416,axiom,
q11 = queue_19,
file(unknown,unknown) ).
tff(f_376,axiom,
queue_19 = rstore_tail(queue_17,index_18),
file(unknown,unknown) ).
tff(f_306,axiom,
index_21 = rselect_tail(q11),
file(unknown,unknown) ).
tff(f_309,axiom,
index_24 = s(index_21),
file(unknown,unknown) ).
tff(f_191,axiom,
! [X] : ( s(s(s(X))) != X ),
file(unknown,unknown) ).
tff(f_418,axiom,
q13 = queue_34,
file(unknown,unknown) ).
tff(f_389,axiom,
queue_34 = rstore_tail(queue_32,index_33),
file(unknown,unknown) ).
tff(f_315,axiom,
index_36 = rselect_tail(q13),
file(unknown,unknown) ).
tff(f_316,axiom,
index_39 = s(index_36),
file(unknown,unknown) ).
tff(f_188,axiom,
! [X] : ( s(s(s(s(X)))) != X ),
file(unknown,unknown) ).
tff(f_419,axiom,
q14 = queue_40,
file(unknown,unknown) ).
tff(f_391,axiom,
queue_40 = rstore_tail(queue_38,index_39),
file(unknown,unknown) ).
tff(f_317,axiom,
index_42 = rselect_tail(q14),
file(unknown,unknown) ).
tff(f_318,axiom,
index_45 = s(index_42),
file(unknown,unknown) ).
tff(f_185,axiom,
! [X] : ( s(s(s(s(s(X))))) != X ),
file(unknown,unknown) ).
tff(f_422,axiom,
q17 = queue_61,
file(unknown,unknown) ).
tff(f_399,axiom,
queue_61 = rstore_tail(queue_59,index_60),
file(unknown,unknown) ).
tff(f_326,axiom,
index_63 = rselect_tail(q17),
file(unknown,unknown) ).
tff(f_327,axiom,
index_66 = s(index_63),
file(unknown,unknown) ).
tff(f_421,axiom,
q16 = queue_55,
file(unknown,unknown) ).
tff(f_397,axiom,
queue_55 = rstore_tail(queue_53,index_54),
file(unknown,unknown) ).
tff(f_323,axiom,
index_57 = rselect_tail(q16),
file(unknown,unknown) ).
tff(f_325,axiom,
index_60 = s(index_57),
file(unknown,unknown) ).
tff(f_393,axiom,
queue_46 = rstore_tail(queue_44,index_45),
file(unknown,unknown) ).
tff(f_321,axiom,
index_51 = rselect_tail(q15),
file(unknown,unknown) ).
tff(f_420,axiom,
q15 = queue_49,
file(unknown,unknown) ).
tff(f_394,axiom,
queue_49 = rstore_head(queue_46,index_48),
file(unknown,unknown) ).
tff(f_322,axiom,
index_54 = s(index_51),
file(unknown,unknown) ).
tff(f_176,axiom,
! [X] : ( s(s(s(s(s(s(s(s(X)))))))) != X ),
file(unknown,unknown) ).
tff(f_401,axiom,
queue_67 = rstore_tail(queue_65,index_66),
file(unknown,unknown) ).
tff(f_330,axiom,
index_72 = rselect_tail(q18),
file(unknown,unknown) ).
tff(f_423,axiom,
q18 = queue_70,
file(unknown,unknown) ).
tff(f_403,axiom,
queue_70 = rstore_head(queue_67,index_69),
file(unknown,unknown) ).
tff(f_331,axiom,
index_75 = s(index_72),
file(unknown,unknown) ).
tff(f_173,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(X))))))))) != X ),
file(unknown,unknown) ).
tff(f_426,axiom,
q20 = queue_88,
file(unknown,unknown) ).
tff(f_409,axiom,
queue_88 = rstore_tail(queue_86,index_87),
file(unknown,unknown) ).
tff(f_337,axiom,
index_90 = rselect_tail(q20),
file(unknown,unknown) ).
tff(f_338,axiom,
index_93 = s(index_90),
file(unknown,unknown) ).
tff(f_424,axiom,
q19 = queue_76,
file(unknown,unknown) ).
tff(f_405,axiom,
queue_76 = rstore_tail(queue_74,index_75),
file(unknown,unknown) ).
tff(f_334,axiom,
index_84 = rselect_tail(q19),
file(unknown,unknown) ).
tff(f_335,axiom,
index_87 = s(index_84),
file(unknown,unknown) ).
tff(f_167,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X ),
file(unknown,unknown) ).
tff(f_170,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(X)))))))))) != X ),
file(unknown,unknown) ).
tff(f_179,axiom,
! [X] : ( s(s(s(s(s(s(s(X))))))) != X ),
file(unknown,unknown) ).
tff(f_182,axiom,
! [X] : ( s(s(s(s(s(s(X)))))) != X ),
file(unknown,unknown) ).
tff(f_194,axiom,
! [X] : ( s(s(X)) != X ),
file(unknown,unknown) ).
tff(f_445,axiom,
elem_214 != e10,
file(unknown,unknown) ).
tff(f_435,axiom,
q29 = queue_151,
file(unknown,unknown) ).
tff(f_362,axiom,
queue_151 = rstore_tail(queue_149,index_150),
file(unknown,unknown) ).
tff(f_286,axiom,
index_162 = rselect_tail(q29),
file(unknown,unknown) ).
tff(f_287,axiom,
index_165 = s(index_162),
file(unknown,unknown) ).
tff(f_434,axiom,
q28 = queue_145,
file(unknown,unknown) ).
tff(f_360,axiom,
queue_145 = rstore_tail(queue_143,index_144),
file(unknown,unknown) ).
tff(f_279,axiom,
index_147 = rselect_tail(q28),
file(unknown,unknown) ).
tff(f_281,axiom,
index_150 = s(index_147),
file(unknown,unknown) ).
tff(f_357,axiom,
queue_136 = rstore_tail(queue_134,index_135),
file(unknown,unknown) ).
tff(f_277,axiom,
index_141 = rselect_tail(q27),
file(unknown,unknown) ).
tff(f_433,axiom,
q27 = queue_139,
file(unknown,unknown) ).
tff(f_358,axiom,
queue_139 = rstore_head(queue_136,index_138),
file(unknown,unknown) ).
tff(f_278,axiom,
index_144 = s(index_141),
file(unknown,unknown) ).
tff(f_432,axiom,
q26 = queue_130,
file(unknown,unknown) ).
tff(f_355,axiom,
queue_130 = rstore_tail(queue_128,index_129),
file(unknown,unknown) ).
tff(f_273,axiom,
index_132 = rselect_tail(q26),
file(unknown,unknown) ).
tff(f_274,axiom,
index_135 = s(index_132),
file(unknown,unknown) ).
tff(f_431,axiom,
q25 = queue_124,
file(unknown,unknown) ).
tff(f_352,axiom,
queue_124 = rstore_tail(queue_122,index_123),
file(unknown,unknown) ).
tff(f_271,axiom,
index_126 = rselect_tail(q25),
file(unknown,unknown) ).
tff(f_272,axiom,
index_129 = s(index_126),
file(unknown,unknown) ).
tff(f_349,axiom,
queue_115 = rstore_tail(queue_113,index_114),
file(unknown,unknown) ).
tff(f_269,axiom,
index_120 = rselect_tail(q24),
file(unknown,unknown) ).
tff(f_430,axiom,
q24 = queue_118,
file(unknown,unknown) ).
tff(f_350,axiom,
queue_118 = rstore_head(queue_115,index_117),
file(unknown,unknown) ).
tff(f_270,axiom,
index_123 = s(index_120),
file(unknown,unknown) ).
tff(f_429,axiom,
q23 = queue_109,
file(unknown,unknown) ).
tff(f_346,axiom,
queue_109 = rstore_tail(queue_107,index_108),
file(unknown,unknown) ).
tff(f_264,axiom,
index_111 = rselect_tail(q23),
file(unknown,unknown) ).
tff(f_265,axiom,
index_114 = s(index_111),
file(unknown,unknown) ).
tff(f_428,axiom,
q22 = queue_103,
file(unknown,unknown) ).
tff(f_344,axiom,
queue_103 = rstore_tail(queue_101,index_102),
file(unknown,unknown) ).
tff(f_262,axiom,
index_105 = rselect_tail(q22),
file(unknown,unknown) ).
tff(f_263,axiom,
index_108 = s(index_105),
file(unknown,unknown) ).
tff(f_411,axiom,
queue_94 = rstore_tail(queue_92,index_93),
file(unknown,unknown) ).
tff(f_341,axiom,
index_99 = rselect_tail(q21),
file(unknown,unknown) ).
tff(f_427,axiom,
q21 = queue_97,
file(unknown,unknown) ).
tff(f_412,axiom,
queue_97 = rstore_head(queue_94,index_96),
file(unknown,unknown) ).
tff(f_261,axiom,
index_102 = s(index_99),
file(unknown,unknown) ).
tff(f_351,axiom,
queue_122 = rstore_seq(q24,earray_121),
file(unknown,unknown) ).
tff(f_31,axiom,
! [A,E] : ( rselect_seq(rstore_seq(A,E)) = E ),
file(unknown,unknown) ).
tff(f_206,axiom,
earray_125 = rselect_seq(q25),
file(unknown,unknown) ).
tff(f_39,axiom,
! [A,E] : ( rselect_seq(rstore_tail(A,E)) = rselect_seq(A) ),
file(unknown,unknown) ).
tff(f_207,axiom,
earray_127 = store(earray_125,index_126,e25),
file(unknown,unknown) ).
tff(f_29,axiom,
! [I,J,A,E] :
( ( I = J )
| ( select(store(A,I,E),J) = select(A,J) ) ),
file(unknown,unknown) ).
tff(f_359,axiom,
queue_143 = rstore_seq(q27,earray_142),
file(unknown,unknown) ).
tff(f_213,axiom,
earray_146 = rselect_seq(q28),
file(unknown,unknown) ).
tff(f_214,axiom,
earray_148 = store(earray_146,index_147,e28),
file(unknown,unknown) ).
tff(f_361,axiom,
queue_149 = rstore_seq(q28,earray_148),
file(unknown,unknown) ).
tff(f_218,axiom,
earray_161 = rselect_seq(q29),
file(unknown,unknown) ).
tff(f_219,axiom,
earray_163 = store(earray_161,index_162,e29),
file(unknown,unknown) ).
tff(f_33,axiom,
! [A,E] : ( rselect_head(rstore_head(A,E)) = E ),
file(unknown,unknown) ).
tff(f_43,axiom,
! [A,E] : ( rselect_head(rstore_seq(A,E)) = rselect_head(A) ),
file(unknown,unknown) ).
tff(f_41,axiom,
! [A,E] : ( rselect_head(rstore_tail(A,E)) = rselect_head(A) ),
file(unknown,unknown) ).
tff(f_353,axiom,
queue_128 = rstore_seq(q25,earray_127),
file(unknown,unknown) ).
tff(f_275,axiom,
index_137 = rselect_head(queue_136),
file(unknown,unknown) ).
tff(f_356,axiom,
queue_134 = rstore_seq(q26,earray_133),
file(unknown,unknown) ).
tff(f_276,axiom,
index_138 = s(index_137),
file(unknown,unknown) ).
tff(f_267,axiom,
index_117 = s(index_116),
file(unknown,unknown) ).
tff(f_439,axiom,
q5 = queue_181,
file(unknown,unknown) ).
tff(f_373,axiom,
queue_181 = rstore_tail(queue_179,index_180),
file(unknown,unknown) ).
tff(f_295,axiom,
index_183 = rselect_tail(q5),
file(unknown,unknown) ).
tff(f_296,axiom,
index_186 = s(index_183),
file(unknown,unknown) ).
tff(f_438,axiom,
q4 = queue_175,
file(unknown,unknown) ).
tff(f_371,axiom,
queue_175 = rstore_tail(queue_173,index_174),
file(unknown,unknown) ).
tff(f_292,axiom,
index_177 = rselect_tail(q4),
file(unknown,unknown) ).
tff(f_294,axiom,
index_180 = s(index_177),
file(unknown,unknown) ).
tff(f_364,axiom,
queue_157 = rstore_tail(queue_155,index_156),
file(unknown,unknown) ).
tff(f_290,axiom,
index_171 = rselect_tail(q3),
file(unknown,unknown) ).
tff(f_436,axiom,
q3 = queue_160,
file(unknown,unknown) ).
tff(f_365,axiom,
queue_160 = rstore_head(queue_157,index_159),
file(unknown,unknown) ).
tff(f_291,axiom,
index_174 = s(index_171),
file(unknown,unknown) ).
tff(f_283,axiom,
index_156 = s(index_153),
file(unknown,unknown) ).
tff(f_284,axiom,
index_158 = rselect_head(queue_157),
file(unknown,unknown) ).
tff(f_363,axiom,
queue_155 = rstore_seq(q2,earray_154),
file(unknown,unknown) ).
tff(f_282,axiom,
index_153 = rselect_tail(q2),
file(unknown,unknown) ).
tff(f_425,axiom,
q2 = queue_82,
file(unknown,unknown) ).
tff(f_407,axiom,
queue_82 = rstore_tail(queue_80,index_81),
file(unknown,unknown) ).
tff(f_406,axiom,
queue_80 = rstore_seq(q1,earray_79),
file(unknown,unknown) ).
tff(f_413,axiom,
q0 = queue_1,
file(unknown,unknown) ).
tff(f_342,axiom,
queue_1 = rstore_head(q,index_0),
file(unknown,unknown) ).
tff(f_395,axiom,
queue_5 = rstore_seq(q0,earray_4),
file(unknown,unknown) ).
tff(f_414,axiom,
q1 = queue_7,
file(unknown,unknown) ).
tff(f_402,axiom,
queue_7 = rstore_tail(queue_5,index_6),
file(unknown,unknown) ).
tff(f_285,axiom,
index_159 = s(index_158),
file(unknown,unknown) ).
tff(f_260,axiom,
index_0 = rselect_tail(q),
file(unknown,unknown) ).
tff(f_312,axiom,
index_3 = rselect_tail(q0),
file(unknown,unknown) ).
tff(f_324,axiom,
index_6 = s(index_3),
file(unknown,unknown) ).
tff(f_332,axiom,
index_78 = rselect_tail(q1),
file(unknown,unknown) ).
tff(f_333,axiom,
index_81 = s(index_78),
file(unknown,unknown) ).
tff(f_370,axiom,
queue_173 = rstore_seq(q3,earray_172),
file(unknown,unknown) ).
tff(f_372,axiom,
queue_179 = rstore_seq(q4,earray_178),
file(unknown,unknown) ).
tff(f_297,axiom,
index_188 = rselect_head(queue_187),
file(unknown,unknown) ).
tff(f_375,axiom,
queue_187 = rstore_tail(queue_185,index_186),
file(unknown,unknown) ).
tff(f_374,axiom,
queue_185 = rstore_seq(q5,earray_184),
file(unknown,unknown) ).
tff(f_298,axiom,
index_189 = s(index_188),
file(unknown,unknown) ).
tff(f_440,axiom,
q6 = queue_190,
file(unknown,unknown) ).
tff(f_377,axiom,
queue_190 = rstore_head(queue_187,index_189),
file(unknown,unknown) ).
tff(f_378,axiom,
queue_194 = rstore_seq(q6,earray_193),
file(unknown,unknown) ).
tff(f_441,axiom,
q7 = queue_196,
file(unknown,unknown) ).
tff(f_379,axiom,
queue_196 = rstore_tail(queue_194,index_195),
file(unknown,unknown) ).
tff(f_380,axiom,
queue_200 = rstore_seq(q7,earray_199),
file(unknown,unknown) ).
tff(f_305,axiom,
index_209 = rselect_head(queue_208),
file(unknown,unknown) ).
tff(f_383,axiom,
queue_208 = rstore_tail(queue_206,index_207),
file(unknown,unknown) ).
tff(f_382,axiom,
queue_206 = rstore_seq(q8,earray_205),
file(unknown,unknown) ).
tff(f_442,axiom,
q8 = queue_202,
file(unknown,unknown) ).
tff(f_381,axiom,
queue_202 = rstore_tail(queue_200,index_201),
file(unknown,unknown) ).
tff(f_307,axiom,
index_210 = s(index_209),
file(unknown,unknown) ).
tff(f_369,axiom,
queue_17 = rstore_seq(q10,earray_16),
file(unknown,unknown) ).
tff(f_310,axiom,
index_26 = rselect_head(queue_25),
file(unknown,unknown) ).
tff(f_385,axiom,
queue_23 = rstore_seq(q11,earray_22),
file(unknown,unknown) ).
tff(f_443,axiom,
q9 = queue_211,
file(unknown,unknown) ).
tff(f_384,axiom,
queue_211 = rstore_head(queue_208,index_210),
file(unknown,unknown) ).
tff(f_347,axiom,
queue_11 = rstore_seq(q9,earray_10),
file(unknown,unknown) ).
tff(f_311,axiom,
index_27 = s(index_26),
file(unknown,unknown) ).
tff(f_388,axiom,
queue_32 = rstore_seq(q12,earray_31),
file(unknown,unknown) ).
tff(f_319,axiom,
index_47 = rselect_head(queue_46),
file(unknown,unknown) ).
tff(f_392,axiom,
queue_44 = rstore_seq(q14,earray_43),
file(unknown,unknown) ).
tff(f_390,axiom,
queue_38 = rstore_seq(q13,earray_37),
file(unknown,unknown) ).
tff(f_320,axiom,
index_48 = s(index_47),
file(unknown,unknown) ).
tff(f_328,axiom,
index_68 = rselect_head(queue_67),
file(unknown,unknown) ).
tff(f_400,axiom,
queue_65 = rstore_seq(q17,earray_64),
file(unknown,unknown) ).
tff(f_396,axiom,
queue_53 = rstore_seq(q15,earray_52),
file(unknown,unknown) ).
tff(f_398,axiom,
queue_59 = rstore_seq(q16,earray_58),
file(unknown,unknown) ).
tff(f_329,axiom,
index_69 = s(index_68),
file(unknown,unknown) ).
tff(f_404,axiom,
queue_74 = rstore_seq(q18,earray_73),
file(unknown,unknown) ).
tff(f_408,axiom,
queue_86 = rstore_seq(q19,earray_85),
file(unknown,unknown) ).
tff(f_339,axiom,
index_95 = rselect_head(queue_94),
file(unknown,unknown) ).
tff(f_410,axiom,
queue_92 = rstore_seq(q20,earray_91),
file(unknown,unknown) ).
tff(f_266,axiom,
index_116 = rselect_head(queue_115),
file(unknown,unknown) ).
tff(f_348,axiom,
queue_113 = rstore_seq(q23,earray_112),
file(unknown,unknown) ).
tff(f_343,axiom,
queue_101 = rstore_seq(q21,earray_100),
file(unknown,unknown) ).
tff(f_345,axiom,
queue_107 = rstore_seq(q22,earray_106),
file(unknown,unknown) ).
tff(f_340,axiom,
index_96 = s(index_95),
file(unknown,unknown) ).
tff(f_299,axiom,
index_192 = rselect_tail(q6),
file(unknown,unknown) ).
tff(f_300,axiom,
index_195 = s(index_192),
file(unknown,unknown) ).
tff(f_301,axiom,
index_198 = rselect_tail(q7),
file(unknown,unknown) ).
tff(f_302,axiom,
index_201 = s(index_198),
file(unknown,unknown) ).
tff(f_303,axiom,
index_204 = rselect_tail(q8),
file(unknown,unknown) ).
tff(f_304,axiom,
index_207 = s(index_204),
file(unknown,unknown) ).
tff(f_336,axiom,
index_9 = rselect_tail(q9),
file(unknown,unknown) ).
tff(f_268,axiom,
index_12 = s(index_9),
file(unknown,unknown) ).
tff(f_288,axiom,
index_167 = rselect_head(queue_166),
file(unknown,unknown) ).
tff(f_367,axiom,
queue_166 = rstore_tail(queue_164,index_165),
file(unknown,unknown) ).
tff(f_366,axiom,
queue_164 = rstore_seq(q29,earray_163),
file(unknown,unknown) ).
tff(f_289,axiom,
index_168 = s(index_167),
file(unknown,unknown) ).
tff(f_234,axiom,
earray_212 = rselect_seq(q30),
file(unknown,unknown) ).
tff(f_437,axiom,
q30 = queue_169,
file(unknown,unknown) ).
tff(f_368,axiom,
queue_169 = rstore_head(queue_166,index_168),
file(unknown,unknown) ).
tff(f_37,axiom,
! [A,E] : ( rselect_seq(rstore_head(A,E)) = rselect_seq(A) ),
file(unknown,unknown) ).
tff(f_308,axiom,
index_213 = rselect_head(q30),
file(unknown,unknown) ).
tff(f_259,axiom,
elem_214 = select(earray_212,index_213),
file(unknown,unknown) ).
tff(f_86,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))) != X ),
file(unknown,unknown) ).
tff(f_92,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))) != X ),
file(unknown,unknown) ).
tff(f_211,axiom,
earray_140 = rselect_seq(q27),
file(unknown,unknown) ).
tff(f_212,axiom,
earray_142 = store(earray_140,index_141,e27),
file(unknown,unknown) ).
tff(f_98,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))) != X ),
file(unknown,unknown) ).
tff(f_208,axiom,
earray_131 = rselect_seq(q26),
file(unknown,unknown) ).
tff(f_209,axiom,
earray_133 = store(earray_131,index_132,e26),
file(unknown,unknown) ).
tff(f_56,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))))))))))) != X ),
file(unknown,unknown) ).
tff(f_65,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))))))))) != X ),
file(unknown,unknown) ).
tff(f_204,axiom,
earray_119 = rselect_seq(q24),
file(unknown,unknown) ).
tff(f_205,axiom,
earray_121 = store(earray_119,index_120,e24),
file(unknown,unknown) ).
tff(f_74,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))))))))))))))))))))))))))) != X ),
file(unknown,unknown) ).
tff(f_202,axiom,
earray_110 = rselect_seq(q23),
file(unknown,unknown) ).
tff(f_203,axiom,
earray_112 = store(earray_110,index_111,e23),
file(unknown,unknown) ).
tff(f_83,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))))))))))))))))))))))) != X ),
file(unknown,unknown) ).
tff(f_200,axiom,
earray_104 = rselect_seq(q22),
file(unknown,unknown) ).
tff(f_201,axiom,
earray_106 = store(earray_104,index_105,e22),
file(unknown,unknown) ).
tff(f_164,axiom,
! [X] : ( s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X ),
file(unknown,unknown) ).
tff(f_231,axiom,
earray_20 = rselect_seq(q11),
file(unknown,unknown) ).
tff(f_235,axiom,
earray_22 = store(earray_20,index_21,e11),
file(unknown,unknown) ).
tff(f_238,axiom,
earray_35 = rselect_seq(q13),
file(unknown,unknown) ).
tff(f_239,axiom,
earray_37 = store(earray_35,index_36,e13),
file(unknown,unknown) ).
tff(f_241,axiom,
earray_41 = rselect_seq(q14),
file(unknown,unknown) ).
tff(f_242,axiom,
earray_43 = store(earray_41,index_42,e14),
file(unknown,unknown) ).
tff(f_243,axiom,
earray_50 = rselect_seq(q15),
file(unknown,unknown) ).
tff(f_244,axiom,
earray_52 = store(earray_50,index_51,e15),
file(unknown,unknown) ).
tff(f_249,axiom,
earray_71 = rselect_seq(q18),
file(unknown,unknown) ).
tff(f_250,axiom,
earray_73 = store(earray_71,index_72,e18),
file(unknown,unknown) ).
tff(f_254,axiom,
earray_83 = rselect_seq(q19),
file(unknown,unknown) ).
tff(f_255,axiom,
earray_85 = store(earray_83,index_84,e19),
file(unknown,unknown) ).
tff(f_258,axiom,
earray_98 = rselect_seq(q21),
file(unknown,unknown) ).
tff(f_199,axiom,
earray_100 = store(earray_98,index_99,e21),
file(unknown,unknown) ).
tff(f_256,axiom,
earray_89 = rselect_seq(q20),
file(unknown,unknown) ).
tff(f_257,axiom,
earray_91 = store(earray_89,index_90,e20),
file(unknown,unknown) ).
tff(f_247,axiom,
earray_62 = rselect_seq(q17),
file(unknown,unknown) ).
tff(f_248,axiom,
earray_64 = store(earray_62,index_63,e17),
file(unknown,unknown) ).
tff(f_245,axiom,
earray_56 = rselect_seq(q16),
file(unknown,unknown) ).
tff(f_246,axiom,
earray_58 = store(earray_56,index_57,e16),
file(unknown,unknown) ).
tff(f_236,axiom,
earray_29 = rselect_seq(q12),
file(unknown,unknown) ).
tff(f_237,axiom,
earray_31 = store(earray_29,index_30,e12),
file(unknown,unknown) ).
tff(f_217,axiom,
earray_16 = store(earray_14,index_15,e10),
file(unknown,unknown) ).
tff(f_25,axiom,
! [A,I,E] : ( select(store(A,I,E),I) = E ),
file(unknown,unknown) ).
tff(c_558,plain,
queue_13 = q10,
inference(cnfTransformation,[status(thm)],[f_415]) ).
tff(c_436,plain,
rstore_tail(queue_11,index_12) = queue_13,
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_642,plain,
rstore_tail(queue_11,index_12) = q10,
inference(demodulation,[status(thm),theory(equality)],[c_558,c_436]) ).
tff(c_1953,plain,
! [A_80,E_81] : ( rselect_tail(rstore_tail(A_80,E_81)) = E_81 ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_1989,plain,
rselect_tail(q10) = index_12,
inference(superposition,[status(thm),theory(equality)],[c_642,c_1953]) ).
tff(c_288,plain,
rselect_tail(q10) = index_15,
inference(cnfTransformation,[status(thm)],[f_280]) ).
tff(c_2121,plain,
index_15 = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_1989,c_288]) ).
tff(c_314,plain,
s(index_15) = index_18,
inference(cnfTransformation,[status(thm)],[f_293]) ).
tff(c_122,plain,
! [X_75] : ( s(X_75) != X_75 ),
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_1050,plain,
index_18 != index_15,
inference(superposition,[status(thm),theory(equality)],[c_314,c_122]) ).
tff(c_2127,plain,
index_18 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2121,c_1050]) ).
tff(c_500,plain,
rstore_tail(queue_23,index_24) = queue_25,
inference(cnfTransformation,[status(thm)],[f_386]) ).
tff(c_2049,plain,
rselect_tail(queue_25) = index_24,
inference(superposition,[status(thm),theory(equality)],[c_500,c_1953]) ).
tff(c_354,plain,
rselect_tail(q12) = index_30,
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_562,plain,
queue_28 = q12,
inference(cnfTransformation,[status(thm)],[f_417]) ).
tff(c_502,plain,
rstore_head(queue_25,index_27) = queue_28,
inference(cnfTransformation,[status(thm)],[f_387]) ).
tff(c_628,plain,
rstore_head(queue_25,index_27) = q12,
inference(demodulation,[status(thm),theory(equality)],[c_562,c_502]) ).
tff(c_2943,plain,
! [A_89,E_90] : ( rselect_tail(rstore_head(A_89,E_90)) = rselect_tail(A_89) ),
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_2958,plain,
rselect_tail(queue_25) = rselect_tail(q12),
inference(superposition,[status(thm),theory(equality)],[c_628,c_2943]) ).
tff(c_2987,plain,
index_30 = index_24,
inference(demodulation,[status(thm),theory(equality)],[c_2049,c_354,c_2958]) ).
tff(c_356,plain,
s(index_30) = index_33,
inference(cnfTransformation,[status(thm)],[f_314]) ).
tff(c_3388,plain,
s(index_24) = index_33,
inference(demodulation,[status(thm),theory(equality)],[c_2987,c_356]) ).
tff(c_560,plain,
queue_19 = q11,
inference(cnfTransformation,[status(thm)],[f_416]) ).
tff(c_480,plain,
rstore_tail(queue_17,index_18) = queue_19,
inference(cnfTransformation,[status(thm)],[f_376]) ).
tff(c_633,plain,
rstore_tail(queue_17,index_18) = q11,
inference(demodulation,[status(thm),theory(equality)],[c_560,c_480]) ).
tff(c_2013,plain,
rselect_tail(q11) = index_18,
inference(superposition,[status(thm),theory(equality)],[c_633,c_1953]) ).
tff(c_340,plain,
rselect_tail(q11) = index_21,
inference(cnfTransformation,[status(thm)],[f_306]) ).
tff(c_2538,plain,
index_21 = index_18,
inference(demodulation,[status(thm),theory(equality)],[c_2013,c_340]) ).
tff(c_346,plain,
s(index_21) = index_24,
inference(cnfTransformation,[status(thm)],[f_309]) ).
tff(c_2550,plain,
s(index_18) = index_24,
inference(demodulation,[status(thm),theory(equality)],[c_2538,c_346]) ).
tff(c_2128,plain,
s(index_12) = index_18,
inference(demodulation,[status(thm),theory(equality)],[c_2121,c_314]) ).
tff(c_2357,plain,
! [X_84] : ( s(s(s(X_84))) != X_84 ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_2369,plain,
s(s(index_18)) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_2357]) ).
tff(c_15339,plain,
index_33 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_3388,c_2550,c_2369]) ).
tff(c_564,plain,
queue_34 = q13,
inference(cnfTransformation,[status(thm)],[f_418]) ).
tff(c_506,plain,
rstore_tail(queue_32,index_33) = queue_34,
inference(cnfTransformation,[status(thm)],[f_389]) ).
tff(c_627,plain,
rstore_tail(queue_32,index_33) = q13,
inference(demodulation,[status(thm),theory(equality)],[c_564,c_506]) ).
tff(c_2004,plain,
rselect_tail(q13) = index_33,
inference(superposition,[status(thm),theory(equality)],[c_627,c_1953]) ).
tff(c_358,plain,
rselect_tail(q13) = index_36,
inference(cnfTransformation,[status(thm)],[f_315]) ).
tff(c_5840,plain,
index_36 = index_33,
inference(demodulation,[status(thm),theory(equality)],[c_2004,c_358]) ).
tff(c_360,plain,
s(index_36) = index_39,
inference(cnfTransformation,[status(thm)],[f_316]) ).
tff(c_5847,plain,
s(index_33) = index_39,
inference(demodulation,[status(thm),theory(equality)],[c_5840,c_360]) ).
tff(c_3012,plain,
! [X_91] : ( s(s(s(s(X_91)))) != X_91 ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_3036,plain,
s(s(s(index_18))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_3012]) ).
tff(c_3131,plain,
s(s(index_24)) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_3036]) ).
tff(c_15427,plain,
index_39 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_5847,c_3388,c_3131]) ).
tff(c_566,plain,
queue_40 = q14,
inference(cnfTransformation,[status(thm)],[f_419]) ).
tff(c_510,plain,
rstore_tail(queue_38,index_39) = queue_40,
inference(cnfTransformation,[status(thm)],[f_391]) ).
tff(c_626,plain,
rstore_tail(queue_38,index_39) = q14,
inference(demodulation,[status(thm),theory(equality)],[c_566,c_510]) ).
tff(c_1974,plain,
rselect_tail(q14) = index_39,
inference(superposition,[status(thm),theory(equality)],[c_626,c_1953]) ).
tff(c_362,plain,
rselect_tail(q14) = index_42,
inference(cnfTransformation,[status(thm)],[f_317]) ).
tff(c_2337,plain,
index_42 = index_39,
inference(demodulation,[status(thm),theory(equality)],[c_1974,c_362]) ).
tff(c_364,plain,
s(index_42) = index_45,
inference(cnfTransformation,[status(thm)],[f_318]) ).
tff(c_2348,plain,
s(index_39) = index_45,
inference(demodulation,[status(thm),theory(equality)],[c_2337,c_364]) ).
tff(c_3576,plain,
! [X_101] : ( s(s(s(s(s(X_101))))) != X_101 ),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_3600,plain,
s(s(s(s(index_18)))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_3576]) ).
tff(c_3668,plain,
s(s(s(index_24))) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_3600]) ).
tff(c_15798,plain,
index_45 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2348,c_5847,c_3388,c_3668]) ).
tff(c_572,plain,
queue_61 = q17,
inference(cnfTransformation,[status(thm)],[f_422]) ).
tff(c_526,plain,
rstore_tail(queue_59,index_60) = queue_61,
inference(cnfTransformation,[status(thm)],[f_399]) ).
tff(c_623,plain,
rstore_tail(queue_59,index_60) = q17,
inference(demodulation,[status(thm),theory(equality)],[c_572,c_526]) ).
tff(c_2007,plain,
rselect_tail(q17) = index_60,
inference(superposition,[status(thm),theory(equality)],[c_623,c_1953]) ).
tff(c_380,plain,
rselect_tail(q17) = index_63,
inference(cnfTransformation,[status(thm)],[f_326]) ).
tff(c_4660,plain,
index_63 = index_60,
inference(demodulation,[status(thm),theory(equality)],[c_2007,c_380]) ).
tff(c_382,plain,
s(index_63) = index_66,
inference(cnfTransformation,[status(thm)],[f_327]) ).
tff(c_4762,plain,
s(index_60) = index_66,
inference(demodulation,[status(thm),theory(equality)],[c_4660,c_382]) ).
tff(c_570,plain,
queue_55 = q16,
inference(cnfTransformation,[status(thm)],[f_421]) ).
tff(c_522,plain,
rstore_tail(queue_53,index_54) = queue_55,
inference(cnfTransformation,[status(thm)],[f_397]) ).
tff(c_624,plain,
rstore_tail(queue_53,index_54) = q16,
inference(demodulation,[status(thm),theory(equality)],[c_570,c_522]) ).
tff(c_1980,plain,
rselect_tail(q16) = index_54,
inference(superposition,[status(thm),theory(equality)],[c_624,c_1953]) ).
tff(c_374,plain,
rselect_tail(q16) = index_57,
inference(cnfTransformation,[status(thm)],[f_323]) ).
tff(c_4173,plain,
index_57 = index_54,
inference(demodulation,[status(thm),theory(equality)],[c_1980,c_374]) ).
tff(c_378,plain,
s(index_57) = index_60,
inference(cnfTransformation,[status(thm)],[f_325]) ).
tff(c_4180,plain,
s(index_54) = index_60,
inference(demodulation,[status(thm),theory(equality)],[c_4173,c_378]) ).
tff(c_514,plain,
rstore_tail(queue_44,index_45) = queue_46,
inference(cnfTransformation,[status(thm)],[f_393]) ).
tff(c_2034,plain,
rselect_tail(queue_46) = index_45,
inference(superposition,[status(thm),theory(equality)],[c_514,c_1953]) ).
tff(c_370,plain,
rselect_tail(q15) = index_51,
inference(cnfTransformation,[status(thm)],[f_321]) ).
tff(c_568,plain,
queue_49 = q15,
inference(cnfTransformation,[status(thm)],[f_420]) ).
tff(c_516,plain,
rstore_head(queue_46,index_48) = queue_49,
inference(cnfTransformation,[status(thm)],[f_394]) ).
tff(c_625,plain,
rstore_head(queue_46,index_48) = q15,
inference(demodulation,[status(thm),theory(equality)],[c_568,c_516]) ).
tff(c_2952,plain,
rselect_tail(queue_46) = rselect_tail(q15),
inference(superposition,[status(thm),theory(equality)],[c_625,c_2943]) ).
tff(c_2985,plain,
index_51 = index_45,
inference(demodulation,[status(thm),theory(equality)],[c_2034,c_370,c_2952]) ).
tff(c_372,plain,
s(index_51) = index_54,
inference(cnfTransformation,[status(thm)],[f_322]) ).
tff(c_3406,plain,
s(index_45) = index_54,
inference(demodulation,[status(thm),theory(equality)],[c_2985,c_372]) ).
tff(c_3890,plain,
! [X_104] : ( s(s(s(s(s(s(s(s(X_104)))))))) != X_104 ),
inference(cnfTransformation,[status(thm)],[f_176]) ).
tff(c_3914,plain,
s(s(s(s(s(s(s(index_18))))))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_3890]) ).
tff(c_3982,plain,
s(s(s(s(s(s(index_24)))))) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_3914]) ).
tff(c_18642,plain,
index_66 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_3982]) ).
tff(c_530,plain,
rstore_tail(queue_65,index_66) = queue_67,
inference(cnfTransformation,[status(thm)],[f_401]) ).
tff(c_1968,plain,
rselect_tail(queue_67) = index_66,
inference(superposition,[status(thm),theory(equality)],[c_530,c_1953]) ).
tff(c_388,plain,
rselect_tail(q18) = index_72,
inference(cnfTransformation,[status(thm)],[f_330]) ).
tff(c_574,plain,
queue_70 = q18,
inference(cnfTransformation,[status(thm)],[f_423]) ).
tff(c_534,plain,
rstore_head(queue_67,index_69) = queue_70,
inference(cnfTransformation,[status(thm)],[f_403]) ).
tff(c_621,plain,
rstore_head(queue_67,index_69) = q18,
inference(demodulation,[status(thm),theory(equality)],[c_574,c_534]) ).
tff(c_2976,plain,
rselect_tail(queue_67) = rselect_tail(q18),
inference(superposition,[status(thm),theory(equality)],[c_621,c_2943]) ).
tff(c_2992,plain,
rselect_tail(queue_67) = index_72,
inference(demodulation,[status(thm),theory(equality)],[c_388,c_2976]) ).
tff(c_10624,plain,
index_72 = index_66,
inference(demodulation,[status(thm),theory(equality)],[c_1968,c_2992]) ).
tff(c_390,plain,
s(index_72) = index_75,
inference(cnfTransformation,[status(thm)],[f_331]) ).
tff(c_10630,plain,
s(index_66) = index_75,
inference(demodulation,[status(thm),theory(equality)],[c_10624,c_390]) ).
tff(c_4063,plain,
! [X_109] : ( s(s(s(s(s(s(s(s(s(X_109))))))))) != X_109 ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4090,plain,
s(s(s(s(s(s(s(s(index_18)))))))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_4063]) ).
tff(c_4159,plain,
s(s(s(s(s(s(s(index_24))))))) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_4090]) ).
tff(c_21211,plain,
index_75 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_4159]) ).
tff(c_580,plain,
queue_88 = q20,
inference(cnfTransformation,[status(thm)],[f_426]) ).
tff(c_546,plain,
rstore_tail(queue_86,index_87) = queue_88,
inference(cnfTransformation,[status(thm)],[f_409]) ).
tff(c_618,plain,
rstore_tail(queue_86,index_87) = q20,
inference(demodulation,[status(thm),theory(equality)],[c_580,c_546]) ).
tff(c_2025,plain,
rselect_tail(q20) = index_87,
inference(superposition,[status(thm),theory(equality)],[c_618,c_1953]) ).
tff(c_402,plain,
rselect_tail(q20) = index_90,
inference(cnfTransformation,[status(thm)],[f_337]) ).
tff(c_2664,plain,
index_90 = index_87,
inference(demodulation,[status(thm),theory(equality)],[c_2025,c_402]) ).
tff(c_404,plain,
s(index_90) = index_93,
inference(cnfTransformation,[status(thm)],[f_338]) ).
tff(c_2672,plain,
s(index_87) = index_93,
inference(demodulation,[status(thm),theory(equality)],[c_2664,c_404]) ).
tff(c_576,plain,
queue_76 = q19,
inference(cnfTransformation,[status(thm)],[f_424]) ).
tff(c_538,plain,
rstore_tail(queue_74,index_75) = queue_76,
inference(cnfTransformation,[status(thm)],[f_405]) ).
tff(c_620,plain,
rstore_tail(queue_74,index_75) = q19,
inference(demodulation,[status(thm),theory(equality)],[c_576,c_538]) ).
tff(c_2010,plain,
rselect_tail(q19) = index_75,
inference(superposition,[status(thm),theory(equality)],[c_620,c_1953]) ).
tff(c_396,plain,
rselect_tail(q19) = index_84,
inference(cnfTransformation,[status(thm)],[f_334]) ).
tff(c_2525,plain,
index_84 = index_75,
inference(demodulation,[status(thm),theory(equality)],[c_2010,c_396]) ).
tff(c_398,plain,
s(index_84) = index_87,
inference(cnfTransformation,[status(thm)],[f_335]) ).
tff(c_2533,plain,
s(index_75) = index_87,
inference(demodulation,[status(thm),theory(equality)],[c_2525,c_398]) ).
tff(c_4322,plain,
! [X_111] : ( s(s(s(s(s(s(s(s(s(s(s(X_111))))))))))) != X_111 ),
inference(cnfTransformation,[status(thm)],[f_167]) ).
tff(c_4352,plain,
s(s(s(s(s(s(s(s(s(s(index_18)))))))))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_4322]) ).
tff(c_4418,plain,
s(s(s(s(s(s(s(s(s(index_24))))))))) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_4352]) ).
tff(c_21406,plain,
index_93 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_4418]) ).
tff(c_4185,plain,
! [X_110] : ( s(s(s(s(s(s(s(s(s(s(X_110)))))))))) != X_110 ),
inference(cnfTransformation,[status(thm)],[f_170]) ).
tff(c_4212,plain,
s(s(s(s(s(s(s(s(s(index_18))))))))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_4185]) ).
tff(c_4278,plain,
s(s(s(s(s(s(s(s(index_24)))))))) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_4212]) ).
tff(c_21289,plain,
index_87 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_4278]) ).
tff(c_3784,plain,
! [X_103] : ( s(s(s(s(s(s(s(X_103))))))) != X_103 ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_3808,plain,
s(s(s(s(s(s(index_18)))))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_3784]) ).
tff(c_3876,plain,
s(s(s(s(s(index_24))))) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_3808]) ).
tff(c_15923,plain,
index_60 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_4180,c_3406,c_2348,c_5847,c_3388,c_3876]) ).
tff(c_3674,plain,
! [X_102] : ( s(s(s(s(s(s(X_102)))))) != X_102 ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_3698,plain,
s(s(s(s(s(index_18))))) != index_12,
inference(superposition,[status(thm),theory(equality)],[c_2128,c_3674]) ).
tff(c_3766,plain,
s(s(s(s(index_24)))) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_3698]) ).
tff(c_15864,plain,
index_54 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_3406,c_2348,c_5847,c_3388,c_3766]) ).
tff(c_1421,plain,
! [X_77] : ( s(s(X_77)) != X_77 ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_1475,plain,
s(index_18) != index_15,
inference(superposition,[status(thm),theory(equality)],[c_314,c_1421]) ).
tff(c_2126,plain,
s(index_18) != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2121,c_1475]) ).
tff(c_3988,plain,
index_24 != index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_2126]) ).
tff(c_616,plain,
elem_214 != e10,
inference(cnfTransformation,[status(thm)],[f_445]) ).
tff(c_598,plain,
queue_151 = q29,
inference(cnfTransformation,[status(thm)],[f_435]) ).
tff(c_452,plain,
rstore_tail(queue_149,index_150) = queue_151,
inference(cnfTransformation,[status(thm)],[f_362]) ).
tff(c_638,plain,
rstore_tail(queue_149,index_150) = q29,
inference(demodulation,[status(thm),theory(equality)],[c_598,c_452]) ).
tff(c_2001,plain,
rselect_tail(q29) = index_150,
inference(superposition,[status(thm),theory(equality)],[c_638,c_1953]) ).
tff(c_300,plain,
rselect_tail(q29) = index_162,
inference(cnfTransformation,[status(thm)],[f_286]) ).
tff(c_6606,plain,
index_162 = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_2001,c_300]) ).
tff(c_302,plain,
s(index_162) = index_165,
inference(cnfTransformation,[status(thm)],[f_287]) ).
tff(c_6613,plain,
s(index_150) = index_165,
inference(demodulation,[status(thm),theory(equality)],[c_6606,c_302]) ).
tff(c_596,plain,
queue_145 = q28,
inference(cnfTransformation,[status(thm)],[f_434]) ).
tff(c_448,plain,
rstore_tail(queue_143,index_144) = queue_145,
inference(cnfTransformation,[status(thm)],[f_360]) ).
tff(c_639,plain,
rstore_tail(queue_143,index_144) = q28,
inference(demodulation,[status(thm),theory(equality)],[c_596,c_448]) ).
tff(c_1971,plain,
rselect_tail(q28) = index_144,
inference(superposition,[status(thm),theory(equality)],[c_639,c_1953]) ).
tff(c_286,plain,
rselect_tail(q28) = index_147,
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_2081,plain,
index_147 = index_144,
inference(demodulation,[status(thm),theory(equality)],[c_1971,c_286]) ).
tff(c_290,plain,
s(index_147) = index_150,
inference(cnfTransformation,[status(thm)],[f_281]) ).
tff(c_2089,plain,
s(index_144) = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_2081,c_290]) ).
tff(c_442,plain,
rstore_tail(queue_134,index_135) = queue_136,
inference(cnfTransformation,[status(thm)],[f_357]) ).
tff(c_2046,plain,
rselect_tail(queue_136) = index_135,
inference(superposition,[status(thm),theory(equality)],[c_442,c_1953]) ).
tff(c_282,plain,
rselect_tail(q27) = index_141,
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_594,plain,
queue_139 = q27,
inference(cnfTransformation,[status(thm)],[f_433]) ).
tff(c_444,plain,
rstore_head(queue_136,index_138) = queue_139,
inference(cnfTransformation,[status(thm)],[f_358]) ).
tff(c_640,plain,
rstore_head(queue_136,index_138) = q27,
inference(demodulation,[status(thm),theory(equality)],[c_594,c_444]) ).
tff(c_2955,plain,
rselect_tail(queue_136) = rselect_tail(q27),
inference(superposition,[status(thm),theory(equality)],[c_640,c_2943]) ).
tff(c_2986,plain,
index_141 = index_135,
inference(demodulation,[status(thm),theory(equality)],[c_2046,c_282,c_2955]) ).
tff(c_284,plain,
s(index_141) = index_144,
inference(cnfTransformation,[status(thm)],[f_278]) ).
tff(c_3398,plain,
s(index_135) = index_144,
inference(demodulation,[status(thm),theory(equality)],[c_2986,c_284]) ).
tff(c_592,plain,
queue_130 = q26,
inference(cnfTransformation,[status(thm)],[f_432]) ).
tff(c_438,plain,
rstore_tail(queue_128,index_129) = queue_130,
inference(cnfTransformation,[status(thm)],[f_355]) ).
tff(c_641,plain,
rstore_tail(queue_128,index_129) = q26,
inference(demodulation,[status(thm),theory(equality)],[c_592,c_438]) ).
tff(c_1983,plain,
rselect_tail(q26) = index_129,
inference(superposition,[status(thm),theory(equality)],[c_641,c_1953]) ).
tff(c_274,plain,
rselect_tail(q26) = index_132,
inference(cnfTransformation,[status(thm)],[f_273]) ).
tff(c_4428,plain,
index_132 = index_129,
inference(demodulation,[status(thm),theory(equality)],[c_1983,c_274]) ).
tff(c_276,plain,
s(index_132) = index_135,
inference(cnfTransformation,[status(thm)],[f_274]) ).
tff(c_4435,plain,
s(index_129) = index_135,
inference(demodulation,[status(thm),theory(equality)],[c_4428,c_276]) ).
tff(c_590,plain,
queue_124 = q25,
inference(cnfTransformation,[status(thm)],[f_431]) ).
tff(c_432,plain,
rstore_tail(queue_122,index_123) = queue_124,
inference(cnfTransformation,[status(thm)],[f_352]) ).
tff(c_643,plain,
rstore_tail(queue_122,index_123) = q25,
inference(demodulation,[status(thm),theory(equality)],[c_590,c_432]) ).
tff(c_2043,plain,
rselect_tail(q25) = index_123,
inference(superposition,[status(thm),theory(equality)],[c_643,c_1953]) ).
tff(c_270,plain,
rselect_tail(q25) = index_126,
inference(cnfTransformation,[status(thm)],[f_271]) ).
tff(c_7953,plain,
index_126 = index_123,
inference(demodulation,[status(thm),theory(equality)],[c_2043,c_270]) ).
tff(c_272,plain,
s(index_126) = index_129,
inference(cnfTransformation,[status(thm)],[f_272]) ).
tff(c_7961,plain,
s(index_123) = index_129,
inference(demodulation,[status(thm),theory(equality)],[c_7953,c_272]) ).
tff(c_426,plain,
rstore_tail(queue_113,index_114) = queue_115,
inference(cnfTransformation,[status(thm)],[f_349]) ).
tff(c_2031,plain,
rselect_tail(queue_115) = index_114,
inference(superposition,[status(thm),theory(equality)],[c_426,c_1953]) ).
tff(c_266,plain,
rselect_tail(q24) = index_120,
inference(cnfTransformation,[status(thm)],[f_269]) ).
tff(c_588,plain,
queue_118 = q24,
inference(cnfTransformation,[status(thm)],[f_430]) ).
tff(c_428,plain,
rstore_head(queue_115,index_117) = queue_118,
inference(cnfTransformation,[status(thm)],[f_350]) ).
tff(c_644,plain,
rstore_head(queue_115,index_117) = q24,
inference(demodulation,[status(thm),theory(equality)],[c_588,c_428]) ).
tff(c_2979,plain,
rselect_tail(queue_115) = rselect_tail(q24),
inference(superposition,[status(thm),theory(equality)],[c_644,c_2943]) ).
tff(c_2993,plain,
index_120 = index_114,
inference(demodulation,[status(thm),theory(equality)],[c_2031,c_266,c_2979]) ).
tff(c_268,plain,
s(index_120) = index_123,
inference(cnfTransformation,[status(thm)],[f_270]) ).
tff(c_3162,plain,
s(index_114) = index_123,
inference(demodulation,[status(thm),theory(equality)],[c_2993,c_268]) ).
tff(c_586,plain,
queue_109 = q23,
inference(cnfTransformation,[status(thm)],[f_429]) ).
tff(c_420,plain,
rstore_tail(queue_107,index_108) = queue_109,
inference(cnfTransformation,[status(thm)],[f_346]) ).
tff(c_645,plain,
rstore_tail(queue_107,index_108) = q23,
inference(demodulation,[status(thm),theory(equality)],[c_586,c_420]) ).
tff(c_1986,plain,
rselect_tail(q23) = index_108,
inference(superposition,[status(thm),theory(equality)],[c_645,c_1953]) ).
tff(c_256,plain,
rselect_tail(q23) = index_111,
inference(cnfTransformation,[status(thm)],[f_264]) ).
tff(c_2306,plain,
index_111 = index_108,
inference(demodulation,[status(thm),theory(equality)],[c_1986,c_256]) ).
tff(c_258,plain,
s(index_111) = index_114,
inference(cnfTransformation,[status(thm)],[f_265]) ).
tff(c_2314,plain,
s(index_108) = index_114,
inference(demodulation,[status(thm),theory(equality)],[c_2306,c_258]) ).
tff(c_584,plain,
queue_103 = q22,
inference(cnfTransformation,[status(thm)],[f_428]) ).
tff(c_416,plain,
rstore_tail(queue_101,index_102) = queue_103,
inference(cnfTransformation,[status(thm)],[f_344]) ).
tff(c_646,plain,
rstore_tail(queue_101,index_102) = q22,
inference(demodulation,[status(thm),theory(equality)],[c_584,c_416]) ).
tff(c_2037,plain,
rselect_tail(q22) = index_102,
inference(superposition,[status(thm),theory(equality)],[c_646,c_1953]) ).
tff(c_252,plain,
rselect_tail(q22) = index_105,
inference(cnfTransformation,[status(thm)],[f_262]) ).
tff(c_2181,plain,
index_105 = index_102,
inference(demodulation,[status(thm),theory(equality)],[c_2037,c_252]) ).
tff(c_254,plain,
s(index_105) = index_108,
inference(cnfTransformation,[status(thm)],[f_263]) ).
tff(c_2189,plain,
s(index_102) = index_108,
inference(demodulation,[status(thm),theory(equality)],[c_2181,c_254]) ).
tff(c_550,plain,
rstore_tail(queue_92,index_93) = queue_94,
inference(cnfTransformation,[status(thm)],[f_411]) ).
tff(c_2040,plain,
rselect_tail(queue_94) = index_93,
inference(superposition,[status(thm),theory(equality)],[c_550,c_1953]) ).
tff(c_410,plain,
rselect_tail(q21) = index_99,
inference(cnfTransformation,[status(thm)],[f_341]) ).
tff(c_582,plain,
queue_97 = q21,
inference(cnfTransformation,[status(thm)],[f_427]) ).
tff(c_552,plain,
rstore_head(queue_94,index_96) = queue_97,
inference(cnfTransformation,[status(thm)],[f_412]) ).
tff(c_617,plain,
rstore_head(queue_94,index_96) = q21,
inference(demodulation,[status(thm),theory(equality)],[c_582,c_552]) ).
tff(c_2973,plain,
rselect_tail(queue_94) = rselect_tail(q21),
inference(superposition,[status(thm),theory(equality)],[c_617,c_2943]) ).
tff(c_2991,plain,
index_99 = index_93,
inference(demodulation,[status(thm),theory(equality)],[c_2040,c_410,c_2973]) ).
tff(c_250,plain,
s(index_99) = index_102,
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_3173,plain,
s(index_93) = index_102,
inference(demodulation,[status(thm),theory(equality)],[c_2991,c_250]) ).
tff(c_430,plain,
rstore_seq(q24,earray_121) = queue_122,
inference(cnfTransformation,[status(thm)],[f_351]) ).
tff(c_1786,plain,
! [A_78,E_79] : ( rselect_seq(rstore_seq(A_78,E_79)) = E_79 ),
inference(cnfTransformation,[status(thm)],[f_31]) ).
tff(c_1807,plain,
rselect_seq(queue_122) = earray_121,
inference(superposition,[status(thm),theory(equality)],[c_430,c_1786]) ).
tff(c_140,plain,
rselect_seq(q25) = earray_125,
inference(cnfTransformation,[status(thm)],[f_206]) ).
tff(c_2677,plain,
! [A_85,E_86] : ( rselect_seq(rstore_tail(A_85,E_86)) = rselect_seq(A_85) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_2764,plain,
rselect_seq(queue_122) = rselect_seq(q25),
inference(superposition,[status(thm),theory(equality)],[c_643,c_2677]) ).
tff(c_2796,plain,
earray_125 = earray_121,
inference(demodulation,[status(thm),theory(equality)],[c_1807,c_140,c_2764]) ).
tff(c_142,plain,
store(earray_125,index_126,e25) = earray_127,
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_2922,plain,
store(earray_121,index_126,e25) = earray_127,
inference(demodulation,[status(thm),theory(equality)],[c_2796,c_142]) ).
tff(c_15534,plain,
store(earray_121,index_123,e25) = earray_127,
inference(demodulation,[status(thm),theory(equality)],[c_7953,c_2922]) ).
tff(c_4,plain,
! [A_6,I_4,E_7,J_5] :
( ( select(store(A_6,I_4,E_7),J_5) = select(A_6,J_5) )
| ( J_5 = I_4 ) ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_18694,plain,
! [J_185] :
( ( select(earray_127,J_185) = select(earray_121,J_185) )
| ( index_123 = J_185 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15534,c_4]) ).
tff(c_446,plain,
rstore_seq(q27,earray_142) = queue_143,
inference(cnfTransformation,[status(thm)],[f_359]) ).
tff(c_1795,plain,
rselect_seq(queue_143) = earray_142,
inference(superposition,[status(thm),theory(equality)],[c_446,c_1786]) ).
tff(c_154,plain,
rselect_seq(q28) = earray_146,
inference(cnfTransformation,[status(thm)],[f_213]) ).
tff(c_2695,plain,
rselect_seq(queue_143) = rselect_seq(q28),
inference(superposition,[status(thm),theory(equality)],[c_639,c_2677]) ).
tff(c_2775,plain,
earray_146 = earray_142,
inference(demodulation,[status(thm),theory(equality)],[c_1795,c_154,c_2695]) ).
tff(c_156,plain,
store(earray_146,index_147,e28) = earray_148,
inference(cnfTransformation,[status(thm)],[f_214]) ).
tff(c_2086,plain,
store(earray_146,index_144,e28) = earray_148,
inference(demodulation,[status(thm),theory(equality)],[c_2081,c_156]) ).
tff(c_15655,plain,
store(earray_142,index_144,e28) = earray_148,
inference(demodulation,[status(thm),theory(equality)],[c_2775,c_2086]) ).
tff(c_16451,plain,
! [J_166] :
( ( select(earray_148,J_166) = select(earray_142,J_166) )
| ( index_144 = J_166 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15655,c_4]) ).
tff(c_450,plain,
rstore_seq(q28,earray_148) = queue_149,
inference(cnfTransformation,[status(thm)],[f_361]) ).
tff(c_1858,plain,
rselect_seq(queue_149) = earray_148,
inference(superposition,[status(thm),theory(equality)],[c_450,c_1786]) ).
tff(c_164,plain,
rselect_seq(q29) = earray_161,
inference(cnfTransformation,[status(thm)],[f_218]) ).
tff(c_2725,plain,
rselect_seq(queue_149) = rselect_seq(q29),
inference(superposition,[status(thm),theory(equality)],[c_638,c_2677]) ).
tff(c_2785,plain,
earray_161 = earray_148,
inference(demodulation,[status(thm),theory(equality)],[c_1858,c_164,c_2725]) ).
tff(c_166,plain,
store(earray_161,index_162,e29) = earray_163,
inference(cnfTransformation,[status(thm)],[f_219]) ).
tff(c_3564,plain,
store(earray_148,index_162,e29) = earray_163,
inference(demodulation,[status(thm),theory(equality)],[c_2785,c_166]) ).
tff(c_15703,plain,
store(earray_148,index_150,e29) = earray_163,
inference(demodulation,[status(thm),theory(equality)],[c_6606,c_3564]) ).
tff(c_16056,plain,
! [J_156] :
( ( select(earray_163,J_156) = select(earray_148,J_156) )
| ( index_150 = J_156 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15703,c_4]) ).
tff(c_2194,plain,
! [A_82,E_83] : ( rselect_head(rstore_head(A_82,E_83)) = E_83 ),
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_2230,plain,
rselect_head(q24) = index_117,
inference(superposition,[status(thm),theory(equality)],[c_644,c_2194]) ).
tff(c_3412,plain,
! [A_96,E_97] : ( rselect_head(rstore_seq(A_96,E_97)) = rselect_head(A_96) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_3433,plain,
rselect_head(queue_122) = rselect_head(q24),
inference(superposition,[status(thm),theory(equality)],[c_430,c_3412]) ).
tff(c_3513,plain,
rselect_head(queue_122) = index_117,
inference(demodulation,[status(thm),theory(equality)],[c_2230,c_3433]) ).
tff(c_2810,plain,
! [A_87,E_88] : ( rselect_head(rstore_tail(A_87,E_88)) = rselect_head(A_87) ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_2897,plain,
rselect_head(queue_122) = rselect_head(q25),
inference(superposition,[status(thm),theory(equality)],[c_643,c_2810]) ).
tff(c_11835,plain,
rselect_head(q25) = index_117,
inference(demodulation,[status(thm),theory(equality)],[c_3513,c_2897]) ).
tff(c_434,plain,
rstore_seq(q25,earray_127) = queue_128,
inference(cnfTransformation,[status(thm)],[f_353]) ).
tff(c_3505,plain,
rselect_head(queue_128) = rselect_head(q25),
inference(superposition,[status(thm),theory(equality)],[c_434,c_3412]) ).
tff(c_12052,plain,
rselect_head(queue_128) = index_117,
inference(demodulation,[status(thm),theory(equality)],[c_11835,c_3505]) ).
tff(c_278,plain,
rselect_head(queue_136) = index_137,
inference(cnfTransformation,[status(thm)],[f_275]) ).
tff(c_2900,plain,
rselect_head(queue_136) = rselect_head(queue_134),
inference(superposition,[status(thm),theory(equality)],[c_442,c_2810]) ).
tff(c_2914,plain,
rselect_head(queue_134) = index_137,
inference(demodulation,[status(thm),theory(equality)],[c_278,c_2900]) ).
tff(c_440,plain,
rstore_seq(q26,earray_133) = queue_134,
inference(cnfTransformation,[status(thm)],[f_356]) ).
tff(c_3448,plain,
rselect_head(queue_134) = rselect_head(q26),
inference(superposition,[status(thm),theory(equality)],[c_440,c_3412]) ).
tff(c_11938,plain,
rselect_head(q26) = index_137,
inference(demodulation,[status(thm),theory(equality)],[c_2914,c_3448]) ).
tff(c_2840,plain,
rselect_head(queue_128) = rselect_head(q26),
inference(superposition,[status(thm),theory(equality)],[c_641,c_2810]) ).
tff(c_12854,plain,
index_137 = index_117,
inference(demodulation,[status(thm),theory(equality)],[c_12052,c_11938,c_2840]) ).
tff(c_280,plain,
s(index_137) = index_138,
inference(cnfTransformation,[status(thm)],[f_276]) ).
tff(c_12861,plain,
s(index_117) = index_138,
inference(demodulation,[status(thm),theory(equality)],[c_12854,c_280]) ).
tff(c_262,plain,
s(index_116) = index_117,
inference(cnfTransformation,[status(thm)],[f_267]) ).
tff(c_606,plain,
queue_181 = q5,
inference(cnfTransformation,[status(thm)],[f_439]) ).
tff(c_474,plain,
rstore_tail(queue_179,index_180) = queue_181,
inference(cnfTransformation,[status(thm)],[f_373]) ).
tff(c_634,plain,
rstore_tail(queue_179,index_180) = q5,
inference(demodulation,[status(thm),theory(equality)],[c_606,c_474]) ).
tff(c_2019,plain,
rselect_tail(q5) = index_180,
inference(superposition,[status(thm),theory(equality)],[c_634,c_1953]) ).
tff(c_318,plain,
rselect_tail(q5) = index_183,
inference(cnfTransformation,[status(thm)],[f_295]) ).
tff(c_2160,plain,
index_183 = index_180,
inference(demodulation,[status(thm),theory(equality)],[c_2019,c_318]) ).
tff(c_320,plain,
s(index_183) = index_186,
inference(cnfTransformation,[status(thm)],[f_296]) ).
tff(c_2168,plain,
s(index_180) = index_186,
inference(demodulation,[status(thm),theory(equality)],[c_2160,c_320]) ).
tff(c_604,plain,
queue_175 = q4,
inference(cnfTransformation,[status(thm)],[f_438]) ).
tff(c_470,plain,
rstore_tail(queue_173,index_174) = queue_175,
inference(cnfTransformation,[status(thm)],[f_371]) ).
tff(c_635,plain,
rstore_tail(queue_173,index_174) = q4,
inference(demodulation,[status(thm),theory(equality)],[c_604,c_470]) ).
tff(c_1995,plain,
rselect_tail(q4) = index_174,
inference(superposition,[status(thm),theory(equality)],[c_635,c_1953]) ).
tff(c_312,plain,
rselect_tail(q4) = index_177,
inference(cnfTransformation,[status(thm)],[f_292]) ).
tff(c_8728,plain,
index_177 = index_174,
inference(demodulation,[status(thm),theory(equality)],[c_1995,c_312]) ).
tff(c_316,plain,
s(index_177) = index_180,
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_8737,plain,
s(index_174) = index_180,
inference(demodulation,[status(thm),theory(equality)],[c_8728,c_316]) ).
tff(c_456,plain,
rstore_tail(queue_155,index_156) = queue_157,
inference(cnfTransformation,[status(thm)],[f_364]) ).
tff(c_1998,plain,
rselect_tail(queue_157) = index_156,
inference(superposition,[status(thm),theory(equality)],[c_456,c_1953]) ).
tff(c_308,plain,
rselect_tail(q3) = index_171,
inference(cnfTransformation,[status(thm)],[f_290]) ).
tff(c_600,plain,
queue_160 = q3,
inference(cnfTransformation,[status(thm)],[f_436]) ).
tff(c_458,plain,
rstore_head(queue_157,index_159) = queue_160,
inference(cnfTransformation,[status(thm)],[f_365]) ).
tff(c_637,plain,
rstore_head(queue_157,index_159) = q3,
inference(demodulation,[status(thm),theory(equality)],[c_600,c_458]) ).
tff(c_2967,plain,
rselect_tail(queue_157) = rselect_tail(q3),
inference(superposition,[status(thm),theory(equality)],[c_637,c_2943]) ).
tff(c_2989,plain,
index_171 = index_156,
inference(demodulation,[status(thm),theory(equality)],[c_1998,c_308,c_2967]) ).
tff(c_310,plain,
s(index_171) = index_174,
inference(cnfTransformation,[status(thm)],[f_291]) ).
tff(c_3370,plain,
s(index_156) = index_174,
inference(demodulation,[status(thm),theory(equality)],[c_2989,c_310]) ).
tff(c_294,plain,
s(index_153) = index_156,
inference(cnfTransformation,[status(thm)],[f_283]) ).
tff(c_296,plain,
rselect_head(queue_157) = index_158,
inference(cnfTransformation,[status(thm)],[f_284]) ).
tff(c_2855,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(superposition,[status(thm),theory(equality)],[c_456,c_2810]) ).
tff(c_2908,plain,
rselect_head(queue_155) = index_158,
inference(demodulation,[status(thm),theory(equality)],[c_296,c_2855]) ).
tff(c_454,plain,
rstore_seq(q2,earray_154) = queue_155,
inference(cnfTransformation,[status(thm)],[f_363]) ).
tff(c_3469,plain,
rselect_head(queue_155) = rselect_head(q2),
inference(superposition,[status(thm),theory(equality)],[c_454,c_3412]) ).
tff(c_11995,plain,
rselect_head(q2) = index_158,
inference(demodulation,[status(thm),theory(equality)],[c_2908,c_3469]) ).
tff(c_292,plain,
rselect_tail(q2) = index_153,
inference(cnfTransformation,[status(thm)],[f_282]) ).
tff(c_578,plain,
queue_82 = q2,
inference(cnfTransformation,[status(thm)],[f_425]) ).
tff(c_542,plain,
rstore_tail(queue_80,index_81) = queue_82,
inference(cnfTransformation,[status(thm)],[f_407]) ).
tff(c_619,plain,
rstore_tail(queue_80,index_81) = q2,
inference(demodulation,[status(thm),theory(equality)],[c_578,c_542]) ).
tff(c_2028,plain,
rselect_tail(q2) = index_81,
inference(superposition,[status(thm),theory(equality)],[c_619,c_1953]) ).
tff(c_2052,plain,
index_81 = index_153,
inference(demodulation,[status(thm),theory(equality)],[c_292,c_2028]) ).
tff(c_2054,plain,
rstore_tail(queue_80,index_153) = q2,
inference(demodulation,[status(thm),theory(equality)],[c_2052,c_619]) ).
tff(c_16,plain,
! [A_18,E_19] : ( rselect_head(rstore_tail(A_18,E_19)) = rselect_head(A_18) ),
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_12024,plain,
rselect_head(queue_80) = rselect_head(q2),
inference(superposition,[status(thm),theory(equality)],[c_2054,c_16]) ).
tff(c_12033,plain,
rselect_head(queue_80) = index_158,
inference(demodulation,[status(thm),theory(equality)],[c_11995,c_12024]) ).
tff(c_540,plain,
rstore_seq(q1,earray_79) = queue_80,
inference(cnfTransformation,[status(thm)],[f_406]) ).
tff(c_3487,plain,
rselect_head(queue_80) = rselect_head(q1),
inference(superposition,[status(thm),theory(equality)],[c_540,c_3412]) ).
tff(c_12369,plain,
rselect_head(q1) = index_158,
inference(demodulation,[status(thm),theory(equality)],[c_12033,c_3487]) ).
tff(c_554,plain,
queue_1 = q0,
inference(cnfTransformation,[status(thm)],[f_413]) ).
tff(c_412,plain,
rstore_head(q,index_0) = queue_1,
inference(cnfTransformation,[status(thm)],[f_342]) ).
tff(c_647,plain,
rstore_head(q,index_0) = q0,
inference(demodulation,[status(thm),theory(equality)],[c_554,c_412]) ).
tff(c_2233,plain,
rselect_head(q0) = index_0,
inference(superposition,[status(thm),theory(equality)],[c_647,c_2194]) ).
tff(c_518,plain,
rstore_seq(q0,earray_4) = queue_5,
inference(cnfTransformation,[status(thm)],[f_395]) ).
tff(c_3499,plain,
rselect_head(queue_5) = rselect_head(q0),
inference(superposition,[status(thm),theory(equality)],[c_518,c_3412]) ).
tff(c_3518,plain,
rselect_head(queue_5) = index_0,
inference(demodulation,[status(thm),theory(equality)],[c_2233,c_3499]) ).
tff(c_556,plain,
queue_7 = q1,
inference(cnfTransformation,[status(thm)],[f_414]) ).
tff(c_532,plain,
rstore_tail(queue_5,index_6) = queue_7,
inference(cnfTransformation,[status(thm)],[f_402]) ).
tff(c_622,plain,
rstore_tail(queue_5,index_6) = q1,
inference(demodulation,[status(thm),theory(equality)],[c_556,c_532]) ).
tff(c_2849,plain,
rselect_head(queue_5) = rselect_head(q1),
inference(superposition,[status(thm),theory(equality)],[c_622,c_2810]) ).
tff(c_13225,plain,
index_158 = index_0,
inference(demodulation,[status(thm),theory(equality)],[c_12369,c_3518,c_2849]) ).
tff(c_298,plain,
s(index_158) = index_159,
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_13233,plain,
s(index_0) = index_159,
inference(demodulation,[status(thm),theory(equality)],[c_13225,c_298]) ).
tff(c_248,plain,
rselect_tail(q) = index_0,
inference(cnfTransformation,[status(thm)],[f_260]) ).
tff(c_352,plain,
rselect_tail(q0) = index_3,
inference(cnfTransformation,[status(thm)],[f_312]) ).
tff(c_2982,plain,
rselect_tail(q0) = rselect_tail(q),
inference(superposition,[status(thm),theory(equality)],[c_647,c_2943]) ).
tff(c_2994,plain,
index_3 = index_0,
inference(demodulation,[status(thm),theory(equality)],[c_248,c_352,c_2982]) ).
tff(c_376,plain,
s(index_3) = index_6,
inference(cnfTransformation,[status(thm)],[f_324]) ).
tff(c_3153,plain,
s(index_0) = index_6,
inference(demodulation,[status(thm),theory(equality)],[c_2994,c_376]) ).
tff(c_13239,plain,
index_6 = index_159,
inference(demodulation,[status(thm),theory(equality)],[c_13233,c_3153]) ).
tff(c_1992,plain,
rselect_tail(q1) = index_6,
inference(superposition,[status(thm),theory(equality)],[c_622,c_1953]) ).
tff(c_392,plain,
rselect_tail(q1) = index_78,
inference(cnfTransformation,[status(thm)],[f_332]) ).
tff(c_7304,plain,
index_78 = index_6,
inference(demodulation,[status(thm),theory(equality)],[c_1992,c_392]) ).
tff(c_394,plain,
s(index_78) = index_81,
inference(cnfTransformation,[status(thm)],[f_333]) ).
tff(c_2056,plain,
s(index_78) = index_153,
inference(demodulation,[status(thm),theory(equality)],[c_2052,c_394]) ).
tff(c_7310,plain,
s(index_6) = index_153,
inference(demodulation,[status(thm),theory(equality)],[c_7304,c_2056]) ).
tff(c_13396,plain,
s(index_159) = index_153,
inference(demodulation,[status(thm),theory(equality)],[c_13239,c_7310]) ).
tff(c_2218,plain,
rselect_head(q3) = index_159,
inference(superposition,[status(thm),theory(equality)],[c_637,c_2194]) ).
tff(c_468,plain,
rstore_seq(q3,earray_172) = queue_173,
inference(cnfTransformation,[status(thm)],[f_370]) ).
tff(c_3472,plain,
rselect_head(queue_173) = rselect_head(q3),
inference(superposition,[status(thm),theory(equality)],[c_468,c_3412]) ).
tff(c_11948,plain,
rselect_head(queue_173) = index_159,
inference(demodulation,[status(thm),theory(equality)],[c_2218,c_3472]) ).
tff(c_2852,plain,
rselect_head(queue_173) = rselect_head(q4),
inference(superposition,[status(thm),theory(equality)],[c_635,c_2810]) ).
tff(c_12316,plain,
rselect_head(q4) = index_159,
inference(demodulation,[status(thm),theory(equality)],[c_11948,c_2852]) ).
tff(c_472,plain,
rstore_seq(q4,earray_178) = queue_179,
inference(cnfTransformation,[status(thm)],[f_372]) ).
tff(c_3475,plain,
rselect_head(queue_179) = rselect_head(q4),
inference(superposition,[status(thm),theory(equality)],[c_472,c_3412]) ).
tff(c_2876,plain,
rselect_head(queue_179) = rselect_head(q5),
inference(superposition,[status(thm),theory(equality)],[c_634,c_2810]) ).
tff(c_12057,plain,
rselect_head(q5) = rselect_head(q4),
inference(demodulation,[status(thm),theory(equality)],[c_3475,c_2876]) ).
tff(c_12317,plain,
rselect_head(q5) = index_159,
inference(demodulation,[status(thm),theory(equality)],[c_12316,c_12057]) ).
tff(c_322,plain,
rselect_head(queue_187) = index_188,
inference(cnfTransformation,[status(thm)],[f_297]) ).
tff(c_478,plain,
rstore_tail(queue_185,index_186) = queue_187,
inference(cnfTransformation,[status(thm)],[f_375]) ).
tff(c_2879,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(superposition,[status(thm),theory(equality)],[c_478,c_2810]) ).
tff(c_2910,plain,
rselect_head(queue_185) = index_188,
inference(demodulation,[status(thm),theory(equality)],[c_322,c_2879]) ).
tff(c_476,plain,
rstore_seq(q5,earray_184) = queue_185,
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_3457,plain,
rselect_head(queue_185) = rselect_head(q5),
inference(superposition,[status(thm),theory(equality)],[c_476,c_3412]) ).
tff(c_14125,plain,
index_188 = index_159,
inference(demodulation,[status(thm),theory(equality)],[c_12317,c_2910,c_3457]) ).
tff(c_324,plain,
s(index_188) = index_189,
inference(cnfTransformation,[status(thm)],[f_298]) ).
tff(c_14130,plain,
s(index_159) = index_189,
inference(demodulation,[status(thm),theory(equality)],[c_14125,c_324]) ).
tff(c_14132,plain,
index_189 = index_153,
inference(demodulation,[status(thm),theory(equality)],[c_13396,c_14130]) ).
tff(c_608,plain,
queue_190 = q6,
inference(cnfTransformation,[status(thm)],[f_440]) ).
tff(c_482,plain,
rstore_head(queue_187,index_189) = queue_190,
inference(cnfTransformation,[status(thm)],[f_377]) ).
tff(c_632,plain,
rstore_head(queue_187,index_189) = q6,
inference(demodulation,[status(thm),theory(equality)],[c_608,c_482]) ).
tff(c_2215,plain,
rselect_head(q6) = index_189,
inference(superposition,[status(thm),theory(equality)],[c_632,c_2194]) ).
tff(c_484,plain,
rstore_seq(q6,earray_193) = queue_194,
inference(cnfTransformation,[status(thm)],[f_378]) ).
tff(c_3496,plain,
rselect_head(queue_194) = rselect_head(q6),
inference(superposition,[status(thm),theory(equality)],[c_484,c_3412]) ).
tff(c_3517,plain,
rselect_head(queue_194) = index_189,
inference(demodulation,[status(thm),theory(equality)],[c_2215,c_3496]) ).
tff(c_610,plain,
queue_196 = q7,
inference(cnfTransformation,[status(thm)],[f_441]) ).
tff(c_486,plain,
rstore_tail(queue_194,index_195) = queue_196,
inference(cnfTransformation,[status(thm)],[f_379]) ).
tff(c_631,plain,
rstore_tail(queue_194,index_195) = q7,
inference(demodulation,[status(thm),theory(equality)],[c_610,c_486]) ).
tff(c_2822,plain,
rselect_head(queue_194) = rselect_head(q7),
inference(superposition,[status(thm),theory(equality)],[c_631,c_2810]) ).
tff(c_11943,plain,
rselect_head(q7) = index_189,
inference(demodulation,[status(thm),theory(equality)],[c_3517,c_2822]) ).
tff(c_488,plain,
rstore_seq(q7,earray_199) = queue_200,
inference(cnfTransformation,[status(thm)],[f_380]) ).
tff(c_3430,plain,
rselect_head(queue_200) = rselect_head(q7),
inference(superposition,[status(thm),theory(equality)],[c_488,c_3412]) ).
tff(c_12849,plain,
rselect_head(queue_200) = index_189,
inference(demodulation,[status(thm),theory(equality)],[c_11943,c_3430]) ).
tff(c_338,plain,
rselect_head(queue_208) = index_209,
inference(cnfTransformation,[status(thm)],[f_305]) ).
tff(c_494,plain,
rstore_tail(queue_206,index_207) = queue_208,
inference(cnfTransformation,[status(thm)],[f_383]) ).
tff(c_2819,plain,
rselect_head(queue_208) = rselect_head(queue_206),
inference(superposition,[status(thm),theory(equality)],[c_494,c_2810]) ).
tff(c_2906,plain,
rselect_head(queue_206) = index_209,
inference(demodulation,[status(thm),theory(equality)],[c_338,c_2819]) ).
tff(c_492,plain,
rstore_seq(q8,earray_205) = queue_206,
inference(cnfTransformation,[status(thm)],[f_382]) ).
tff(c_3454,plain,
rselect_head(queue_206) = rselect_head(q8),
inference(superposition,[status(thm),theory(equality)],[c_492,c_3412]) ).
tff(c_12267,plain,
rselect_head(q8) = index_209,
inference(demodulation,[status(thm),theory(equality)],[c_2906,c_3454]) ).
tff(c_612,plain,
queue_202 = q8,
inference(cnfTransformation,[status(thm)],[f_442]) ).
tff(c_490,plain,
rstore_tail(queue_200,index_201) = queue_202,
inference(cnfTransformation,[status(thm)],[f_381]) ).
tff(c_630,plain,
rstore_tail(queue_200,index_201) = q8,
inference(demodulation,[status(thm),theory(equality)],[c_612,c_490]) ).
tff(c_2834,plain,
rselect_head(queue_200) = rselect_head(q8),
inference(superposition,[status(thm),theory(equality)],[c_630,c_2810]) ).
tff(c_13895,plain,
index_209 = index_189,
inference(demodulation,[status(thm),theory(equality)],[c_12849,c_12267,c_2834]) ).
tff(c_342,plain,
s(index_209) = index_210,
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_13902,plain,
s(index_189) = index_210,
inference(demodulation,[status(thm),theory(equality)],[c_13895,c_342]) ).
tff(c_14149,plain,
s(index_153) = index_210,
inference(demodulation,[status(thm),theory(equality)],[c_14132,c_13902]) ).
tff(c_14160,plain,
index_210 = index_156,
inference(demodulation,[status(thm),theory(equality)],[c_294,c_14149]) ).
tff(c_466,plain,
rstore_seq(q10,earray_16) = queue_17,
inference(cnfTransformation,[status(thm)],[f_369]) ).
tff(c_3478,plain,
rselect_head(queue_17) = rselect_head(q10),
inference(superposition,[status(thm),theory(equality)],[c_466,c_3412]) ).
tff(c_2870,plain,
rselect_head(queue_17) = rselect_head(q11),
inference(superposition,[status(thm),theory(equality)],[c_633,c_2810]) ).
tff(c_11926,plain,
rselect_head(q11) = rselect_head(q10),
inference(demodulation,[status(thm),theory(equality)],[c_3478,c_2870]) ).
tff(c_348,plain,
rselect_head(queue_25) = index_26,
inference(cnfTransformation,[status(thm)],[f_310]) ).
tff(c_2903,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(superposition,[status(thm),theory(equality)],[c_500,c_2810]) ).
tff(c_2915,plain,
rselect_head(queue_23) = index_26,
inference(demodulation,[status(thm),theory(equality)],[c_348,c_2903]) ).
tff(c_498,plain,
rstore_seq(q11,earray_22) = queue_23,
inference(cnfTransformation,[status(thm)],[f_385]) ).
tff(c_3508,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(superposition,[status(thm),theory(equality)],[c_498,c_3412]) ).
tff(c_12005,plain,
rselect_head(q10) = index_26,
inference(demodulation,[status(thm),theory(equality)],[c_11926,c_2915,c_3508]) ).
tff(c_614,plain,
queue_211 = q9,
inference(cnfTransformation,[status(thm)],[f_443]) ).
tff(c_496,plain,
rstore_head(queue_208,index_210) = queue_211,
inference(cnfTransformation,[status(thm)],[f_384]) ).
tff(c_629,plain,
rstore_head(queue_208,index_210) = q9,
inference(demodulation,[status(thm),theory(equality)],[c_614,c_496]) ).
tff(c_2221,plain,
rselect_head(q9) = index_210,
inference(superposition,[status(thm),theory(equality)],[c_629,c_2194]) ).
tff(c_422,plain,
rstore_seq(q9,earray_10) = queue_11,
inference(cnfTransformation,[status(thm)],[f_347]) ).
tff(c_3427,plain,
rselect_head(queue_11) = rselect_head(q9),
inference(superposition,[status(thm),theory(equality)],[c_422,c_3412]) ).
tff(c_3512,plain,
rselect_head(queue_11) = index_210,
inference(demodulation,[status(thm),theory(equality)],[c_2221,c_3427]) ).
tff(c_2846,plain,
rselect_head(queue_11) = rselect_head(q10),
inference(superposition,[status(thm),theory(equality)],[c_642,c_2810]) ).
tff(c_12072,plain,
index_26 = index_210,
inference(demodulation,[status(thm),theory(equality)],[c_12005,c_3512,c_2846]) ).
tff(c_350,plain,
s(index_26) = index_27,
inference(cnfTransformation,[status(thm)],[f_311]) ).
tff(c_12081,plain,
s(index_210) = index_27,
inference(demodulation,[status(thm),theory(equality)],[c_12072,c_350]) ).
tff(c_14172,plain,
s(index_156) = index_27,
inference(demodulation,[status(thm),theory(equality)],[c_14160,c_12081]) ).
tff(c_14182,plain,
index_27 = index_174,
inference(demodulation,[status(thm),theory(equality)],[c_3370,c_14172]) ).
tff(c_2209,plain,
rselect_head(q12) = index_27,
inference(superposition,[status(thm),theory(equality)],[c_628,c_2194]) ).
tff(c_504,plain,
rstore_seq(q12,earray_31) = queue_32,
inference(cnfTransformation,[status(thm)],[f_388]) ).
tff(c_3466,plain,
rselect_head(queue_32) = rselect_head(q12),
inference(superposition,[status(thm),theory(equality)],[c_504,c_3412]) ).
tff(c_12067,plain,
rselect_head(queue_32) = index_27,
inference(demodulation,[status(thm),theory(equality)],[c_2209,c_3466]) ).
tff(c_366,plain,
rselect_head(queue_46) = index_47,
inference(cnfTransformation,[status(thm)],[f_319]) ).
tff(c_2888,plain,
rselect_head(queue_46) = rselect_head(queue_44),
inference(superposition,[status(thm),theory(equality)],[c_514,c_2810]) ).
tff(c_2912,plain,
rselect_head(queue_44) = index_47,
inference(demodulation,[status(thm),theory(equality)],[c_366,c_2888]) ).
tff(c_512,plain,
rstore_seq(q14,earray_43) = queue_44,
inference(cnfTransformation,[status(thm)],[f_392]) ).
tff(c_3436,plain,
rselect_head(queue_44) = rselect_head(q14),
inference(superposition,[status(thm),theory(equality)],[c_512,c_3412]) ).
tff(c_11968,plain,
rselect_head(q14) = index_47,
inference(demodulation,[status(thm),theory(equality)],[c_2912,c_3436]) ).
tff(c_2831,plain,
rselect_head(queue_38) = rselect_head(q14),
inference(superposition,[status(thm),theory(equality)],[c_626,c_2810]) ).
tff(c_11969,plain,
rselect_head(queue_38) = index_47,
inference(demodulation,[status(thm),theory(equality)],[c_11968,c_2831]) ).
tff(c_508,plain,
rstore_seq(q13,earray_37) = queue_38,
inference(cnfTransformation,[status(thm)],[f_390]) ).
tff(c_3463,plain,
rselect_head(queue_38) = rselect_head(q13),
inference(superposition,[status(thm),theory(equality)],[c_508,c_3412]) ).
tff(c_12000,plain,
rselect_head(q13) = index_47,
inference(demodulation,[status(thm),theory(equality)],[c_11969,c_3463]) ).
tff(c_2861,plain,
rselect_head(queue_32) = rselect_head(q13),
inference(superposition,[status(thm),theory(equality)],[c_627,c_2810]) ).
tff(c_13035,plain,
index_47 = index_27,
inference(demodulation,[status(thm),theory(equality)],[c_12067,c_12000,c_2861]) ).
tff(c_368,plain,
s(index_47) = index_48,
inference(cnfTransformation,[status(thm)],[f_320]) ).
tff(c_13043,plain,
s(index_27) = index_48,
inference(demodulation,[status(thm),theory(equality)],[c_13035,c_368]) ).
tff(c_14214,plain,
s(index_174) = index_48,
inference(demodulation,[status(thm),theory(equality)],[c_14182,c_13043]) ).
tff(c_14222,plain,
index_48 = index_180,
inference(demodulation,[status(thm),theory(equality)],[c_8737,c_14214]) ).
tff(c_384,plain,
rselect_head(queue_67) = index_68,
inference(cnfTransformation,[status(thm)],[f_328]) ).
tff(c_2825,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(superposition,[status(thm),theory(equality)],[c_530,c_2810]) ).
tff(c_2907,plain,
rselect_head(queue_65) = index_68,
inference(demodulation,[status(thm),theory(equality)],[c_384,c_2825]) ).
tff(c_528,plain,
rstore_seq(q17,earray_64) = queue_65,
inference(cnfTransformation,[status(thm)],[f_400]) ).
tff(c_3502,plain,
rselect_head(queue_65) = rselect_head(q17),
inference(superposition,[status(thm),theory(equality)],[c_528,c_3412]) ).
tff(c_11978,plain,
rselect_head(q17) = index_68,
inference(demodulation,[status(thm),theory(equality)],[c_2907,c_3502]) ).
tff(c_2864,plain,
rselect_head(queue_59) = rselect_head(q17),
inference(superposition,[status(thm),theory(equality)],[c_623,c_2810]) ).
tff(c_11979,plain,
rselect_head(queue_59) = index_68,
inference(demodulation,[status(thm),theory(equality)],[c_11978,c_2864]) ).
tff(c_2203,plain,
rselect_head(q15) = index_48,
inference(superposition,[status(thm),theory(equality)],[c_625,c_2194]) ).
tff(c_520,plain,
rstore_seq(q15,earray_52) = queue_53,
inference(cnfTransformation,[status(thm)],[f_396]) ).
tff(c_3442,plain,
rselect_head(queue_53) = rselect_head(q15),
inference(superposition,[status(thm),theory(equality)],[c_520,c_3412]) ).
tff(c_3515,plain,
rselect_head(queue_53) = index_48,
inference(demodulation,[status(thm),theory(equality)],[c_2203,c_3442]) ).
tff(c_2837,plain,
rselect_head(queue_53) = rselect_head(q16),
inference(superposition,[status(thm),theory(equality)],[c_624,c_2810]) ).
tff(c_11906,plain,
rselect_head(q16) = index_48,
inference(demodulation,[status(thm),theory(equality)],[c_3515,c_2837]) ).
tff(c_524,plain,
rstore_seq(q16,earray_58) = queue_59,
inference(cnfTransformation,[status(thm)],[f_398]) ).
tff(c_3493,plain,
rselect_head(queue_59) = rselect_head(q16),
inference(superposition,[status(thm),theory(equality)],[c_524,c_3412]) ).
tff(c_13407,plain,
index_68 = index_48,
inference(demodulation,[status(thm),theory(equality)],[c_11979,c_11906,c_3493]) ).
tff(c_386,plain,
s(index_68) = index_69,
inference(cnfTransformation,[status(thm)],[f_329]) ).
tff(c_13414,plain,
s(index_48) = index_69,
inference(demodulation,[status(thm),theory(equality)],[c_13407,c_386]) ).
tff(c_14401,plain,
s(index_180) = index_69,
inference(demodulation,[status(thm),theory(equality)],[c_14222,c_13414]) ).
tff(c_14409,plain,
index_69 = index_186,
inference(demodulation,[status(thm),theory(equality)],[c_2168,c_14401]) ).
tff(c_2227,plain,
rselect_head(q18) = index_69,
inference(superposition,[status(thm),theory(equality)],[c_621,c_2194]) ).
tff(c_536,plain,
rstore_seq(q18,earray_73) = queue_74,
inference(cnfTransformation,[status(thm)],[f_404]) ).
tff(c_3439,plain,
rselect_head(queue_74) = rselect_head(q18),
inference(superposition,[status(thm),theory(equality)],[c_536,c_3412]) ).
tff(c_3514,plain,
rselect_head(queue_74) = index_69,
inference(demodulation,[status(thm),theory(equality)],[c_2227,c_3439]) ).
tff(c_2867,plain,
rselect_head(queue_74) = rselect_head(q19),
inference(superposition,[status(thm),theory(equality)],[c_620,c_2810]) ).
tff(c_12331,plain,
rselect_head(q19) = index_69,
inference(demodulation,[status(thm),theory(equality)],[c_3514,c_2867]) ).
tff(c_544,plain,
rstore_seq(q19,earray_85) = queue_86,
inference(cnfTransformation,[status(thm)],[f_408]) ).
tff(c_3490,plain,
rselect_head(queue_86) = rselect_head(q19),
inference(superposition,[status(thm),theory(equality)],[c_544,c_3412]) ).
tff(c_12332,plain,
rselect_head(queue_86) = index_69,
inference(demodulation,[status(thm),theory(equality)],[c_12331,c_3490]) ).
tff(c_406,plain,
rselect_head(queue_94) = index_95,
inference(cnfTransformation,[status(thm)],[f_339]) ).
tff(c_2894,plain,
rselect_head(queue_94) = rselect_head(queue_92),
inference(superposition,[status(thm),theory(equality)],[c_550,c_2810]) ).
tff(c_2913,plain,
rselect_head(queue_92) = index_95,
inference(demodulation,[status(thm),theory(equality)],[c_406,c_2894]) ).
tff(c_548,plain,
rstore_seq(q20,earray_91) = queue_92,
inference(cnfTransformation,[status(thm)],[f_410]) ).
tff(c_3445,plain,
rselect_head(queue_92) = rselect_head(q20),
inference(superposition,[status(thm),theory(equality)],[c_548,c_3412]) ).
tff(c_12062,plain,
rselect_head(q20) = index_95,
inference(demodulation,[status(thm),theory(equality)],[c_2913,c_3445]) ).
tff(c_2882,plain,
rselect_head(queue_86) = rselect_head(q20),
inference(superposition,[status(thm),theory(equality)],[c_618,c_2810]) ).
tff(c_12612,plain,
index_95 = index_69,
inference(demodulation,[status(thm),theory(equality)],[c_12332,c_12062,c_2882]) ).
tff(c_260,plain,
rselect_head(queue_115) = index_116,
inference(cnfTransformation,[status(thm)],[f_266]) ).
tff(c_2885,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(superposition,[status(thm),theory(equality)],[c_426,c_2810]) ).
tff(c_2911,plain,
rselect_head(queue_113) = index_116,
inference(demodulation,[status(thm),theory(equality)],[c_260,c_2885]) ).
tff(c_424,plain,
rstore_seq(q23,earray_112) = queue_113,
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_3424,plain,
rselect_head(queue_113) = rselect_head(q23),
inference(superposition,[status(thm),theory(equality)],[c_424,c_3412]) ).
tff(c_12310,plain,
rselect_head(q23) = index_116,
inference(demodulation,[status(thm),theory(equality)],[c_2911,c_3424]) ).
tff(c_2224,plain,
rselect_head(q21) = index_96,
inference(superposition,[status(thm),theory(equality)],[c_617,c_2194]) ).
tff(c_414,plain,
rstore_seq(q21,earray_100) = queue_101,
inference(cnfTransformation,[status(thm)],[f_343]) ).
tff(c_3460,plain,
rselect_head(queue_101) = rselect_head(q21),
inference(superposition,[status(thm),theory(equality)],[c_414,c_3412]) ).
tff(c_3516,plain,
rselect_head(queue_101) = index_96,
inference(demodulation,[status(thm),theory(equality)],[c_2224,c_3460]) ).
tff(c_2891,plain,
rselect_head(queue_101) = rselect_head(q22),
inference(superposition,[status(thm),theory(equality)],[c_646,c_2810]) ).
tff(c_11912,plain,
rselect_head(q22) = index_96,
inference(demodulation,[status(thm),theory(equality)],[c_3516,c_2891]) ).
tff(c_418,plain,
rstore_seq(q22,earray_106) = queue_107,
inference(cnfTransformation,[status(thm)],[f_345]) ).
tff(c_3451,plain,
rselect_head(queue_107) = rselect_head(q22),
inference(superposition,[status(thm),theory(equality)],[c_418,c_3412]) ).
tff(c_11913,plain,
rselect_head(queue_107) = index_96,
inference(demodulation,[status(thm),theory(equality)],[c_11912,c_3451]) ).
tff(c_2843,plain,
rselect_head(queue_107) = rselect_head(q23),
inference(superposition,[status(thm),theory(equality)],[c_645,c_2810]) ).
tff(c_12374,plain,
index_96 = index_116,
inference(demodulation,[status(thm),theory(equality)],[c_12310,c_11913,c_2843]) ).
tff(c_408,plain,
s(index_95) = index_96,
inference(cnfTransformation,[status(thm)],[f_340]) ).
tff(c_12382,plain,
s(index_95) = index_116,
inference(demodulation,[status(thm),theory(equality)],[c_12374,c_408]) ).
tff(c_12614,plain,
s(index_69) = index_116,
inference(demodulation,[status(thm),theory(equality)],[c_12612,c_12382]) ).
tff(c_14431,plain,
s(index_186) = index_116,
inference(demodulation,[status(thm),theory(equality)],[c_14409,c_12614]) ).
tff(c_2022,plain,
rselect_tail(queue_187) = index_186,
inference(superposition,[status(thm),theory(equality)],[c_478,c_1953]) ).
tff(c_326,plain,
rselect_tail(q6) = index_192,
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_2964,plain,
rselect_tail(queue_187) = rselect_tail(q6),
inference(superposition,[status(thm),theory(equality)],[c_632,c_2943]) ).
tff(c_2988,plain,
index_192 = index_186,
inference(demodulation,[status(thm),theory(equality)],[c_2022,c_326,c_2964]) ).
tff(c_328,plain,
s(index_192) = index_195,
inference(cnfTransformation,[status(thm)],[f_300]) ).
tff(c_3378,plain,
s(index_186) = index_195,
inference(demodulation,[status(thm),theory(equality)],[c_2988,c_328]) ).
tff(c_14490,plain,
index_195 = index_116,
inference(demodulation,[status(thm),theory(equality)],[c_14431,c_3378]) ).
tff(c_1965,plain,
rselect_tail(q7) = index_195,
inference(superposition,[status(thm),theory(equality)],[c_631,c_1953]) ).
tff(c_330,plain,
rselect_tail(q7) = index_198,
inference(cnfTransformation,[status(thm)],[f_301]) ).
tff(c_4543,plain,
index_198 = index_195,
inference(demodulation,[status(thm),theory(equality)],[c_1965,c_330]) ).
tff(c_332,plain,
s(index_198) = index_201,
inference(cnfTransformation,[status(thm)],[f_302]) ).
tff(c_4550,plain,
s(index_195) = index_201,
inference(demodulation,[status(thm),theory(equality)],[c_4543,c_332]) ).
tff(c_14698,plain,
s(index_116) = index_201,
inference(demodulation,[status(thm),theory(equality)],[c_14490,c_4550]) ).
tff(c_14707,plain,
index_201 = index_117,
inference(demodulation,[status(thm),theory(equality)],[c_262,c_14698]) ).
tff(c_1977,plain,
rselect_tail(q8) = index_201,
inference(superposition,[status(thm),theory(equality)],[c_630,c_1953]) ).
tff(c_334,plain,
rselect_tail(q8) = index_204,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_2627,plain,
index_204 = index_201,
inference(demodulation,[status(thm),theory(equality)],[c_1977,c_334]) ).
tff(c_336,plain,
s(index_204) = index_207,
inference(cnfTransformation,[status(thm)],[f_304]) ).
tff(c_2639,plain,
s(index_201) = index_207,
inference(demodulation,[status(thm),theory(equality)],[c_2627,c_336]) ).
tff(c_14725,plain,
s(index_117) = index_207,
inference(demodulation,[status(thm),theory(equality)],[c_14707,c_2639]) ).
tff(c_14730,plain,
index_207 = index_138,
inference(demodulation,[status(thm),theory(equality)],[c_12861,c_14725]) ).
tff(c_1962,plain,
rselect_tail(queue_208) = index_207,
inference(superposition,[status(thm),theory(equality)],[c_494,c_1953]) ).
tff(c_400,plain,
rselect_tail(q9) = index_9,
inference(cnfTransformation,[status(thm)],[f_336]) ).
tff(c_2970,plain,
rselect_tail(queue_208) = rselect_tail(q9),
inference(superposition,[status(thm),theory(equality)],[c_629,c_2943]) ).
tff(c_2990,plain,
index_9 = index_207,
inference(demodulation,[status(thm),theory(equality)],[c_1962,c_400,c_2970]) ).
tff(c_264,plain,
s(index_9) = index_12,
inference(cnfTransformation,[status(thm)],[f_268]) ).
tff(c_3308,plain,
s(index_207) = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_2990,c_264]) ).
tff(c_14765,plain,
s(index_138) = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_14730,c_3308]) ).
tff(c_2206,plain,
rselect_head(q27) = index_138,
inference(superposition,[status(thm),theory(equality)],[c_640,c_2194]) ).
tff(c_3421,plain,
rselect_head(queue_143) = rselect_head(q27),
inference(superposition,[status(thm),theory(equality)],[c_446,c_3412]) ).
tff(c_3511,plain,
rselect_head(queue_143) = index_138,
inference(demodulation,[status(thm),theory(equality)],[c_2206,c_3421]) ).
tff(c_2828,plain,
rselect_head(queue_143) = rselect_head(q28),
inference(superposition,[status(thm),theory(equality)],[c_639,c_2810]) ).
tff(c_12353,plain,
rselect_head(q28) = index_138,
inference(demodulation,[status(thm),theory(equality)],[c_3511,c_2828]) ).
tff(c_3484,plain,
rselect_head(queue_149) = rselect_head(q28),
inference(superposition,[status(thm),theory(equality)],[c_450,c_3412]) ).
tff(c_12354,plain,
rselect_head(queue_149) = index_138,
inference(demodulation,[status(thm),theory(equality)],[c_12353,c_3484]) ).
tff(c_304,plain,
rselect_head(queue_166) = index_167,
inference(cnfTransformation,[status(thm)],[f_288]) ).
tff(c_462,plain,
rstore_tail(queue_164,index_165) = queue_166,
inference(cnfTransformation,[status(thm)],[f_367]) ).
tff(c_2873,plain,
rselect_head(queue_166) = rselect_head(queue_164),
inference(superposition,[status(thm),theory(equality)],[c_462,c_2810]) ).
tff(c_2909,plain,
rselect_head(queue_164) = index_167,
inference(demodulation,[status(thm),theory(equality)],[c_304,c_2873]) ).
tff(c_460,plain,
rstore_seq(q29,earray_163) = queue_164,
inference(cnfTransformation,[status(thm)],[f_366]) ).
tff(c_3481,plain,
rselect_head(queue_164) = rselect_head(q29),
inference(superposition,[status(thm),theory(equality)],[c_460,c_3412]) ).
tff(c_11875,plain,
rselect_head(q29) = index_167,
inference(demodulation,[status(thm),theory(equality)],[c_2909,c_3481]) ).
tff(c_2858,plain,
rselect_head(queue_149) = rselect_head(q29),
inference(superposition,[status(thm),theory(equality)],[c_638,c_2810]) ).
tff(c_14191,plain,
index_167 = index_138,
inference(demodulation,[status(thm),theory(equality)],[c_12354,c_11875,c_2858]) ).
tff(c_306,plain,
s(index_167) = index_168,
inference(cnfTransformation,[status(thm)],[f_289]) ).
tff(c_14197,plain,
s(index_138) = index_168,
inference(demodulation,[status(thm),theory(equality)],[c_14191,c_306]) ).
tff(c_14850,plain,
index_168 = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_14765,c_14197]) ).
tff(c_196,plain,
rselect_seq(q30) = earray_212,
inference(cnfTransformation,[status(thm)],[f_234]) ).
tff(c_602,plain,
queue_169 = q30,
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_464,plain,
rstore_head(queue_166,index_168) = queue_169,
inference(cnfTransformation,[status(thm)],[f_368]) ).
tff(c_636,plain,
rstore_head(queue_166,index_168) = q30,
inference(demodulation,[status(thm),theory(equality)],[c_602,c_464]) ).
tff(c_3313,plain,
! [A_94,E_95] : ( rselect_seq(rstore_head(A_94,E_95)) = rselect_seq(A_94) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_3331,plain,
rselect_seq(queue_166) = rselect_seq(q30),
inference(superposition,[status(thm),theory(equality)],[c_636,c_3313]) ).
tff(c_3358,plain,
rselect_seq(queue_166) = earray_212,
inference(demodulation,[status(thm),theory(equality)],[c_196,c_3331]) ).
tff(c_1855,plain,
rselect_seq(queue_164) = earray_163,
inference(superposition,[status(thm),theory(equality)],[c_460,c_1786]) ).
tff(c_2740,plain,
rselect_seq(queue_166) = rselect_seq(queue_164),
inference(superposition,[status(thm),theory(equality)],[c_462,c_2677]) ).
tff(c_11860,plain,
earray_212 = earray_163,
inference(demodulation,[status(thm),theory(equality)],[c_3358,c_1855,c_2740]) ).
tff(c_2212,plain,
rselect_head(q30) = index_168,
inference(superposition,[status(thm),theory(equality)],[c_636,c_2194]) ).
tff(c_344,plain,
rselect_head(q30) = index_213,
inference(cnfTransformation,[status(thm)],[f_308]) ).
tff(c_2511,plain,
index_213 = index_168,
inference(demodulation,[status(thm),theory(equality)],[c_2212,c_344]) ).
tff(c_246,plain,
select(earray_212,index_213) = elem_214,
inference(cnfTransformation,[status(thm)],[f_259]) ).
tff(c_2520,plain,
select(earray_212,index_168) = elem_214,
inference(demodulation,[status(thm),theory(equality)],[c_2511,c_246]) ).
tff(c_12342,plain,
select(earray_163,index_168) = elem_214,
inference(demodulation,[status(thm),theory(equality)],[c_11860,c_2520]) ).
tff(c_15066,plain,
select(earray_163,index_12) = elem_214,
inference(demodulation,[status(thm),theory(equality)],[c_14850,c_12342]) ).
tff(c_16062,plain,
( ( select(earray_148,index_12) = elem_214 )
| ( index_150 = index_12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16056,c_15066]) ).
tff(c_16079,plain,
index_150 = index_12,
inference(splitLeft,[status(thm)],[c_16062]) ).
tff(c_16104,plain,
s(index_144) = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_16079,c_2089]) ).
tff(c_48,plain,
! [X_38] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X_38)))))))))))))))))))))))))))))))))))))) != X_38 ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_16175,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_12))))))))))))))))))))))))))))))))))))) != index_144,
inference(superposition,[status(thm),theory(equality)],[c_16104,c_48]) ).
tff(c_16303,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_2550,c_2128,c_16104,c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_2550,c_2128,c_16175]) ).
tff(c_16304,plain,
select(earray_148,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_16062]) ).
tff(c_16457,plain,
( ( select(earray_142,index_12) = elem_214 )
| ( index_144 = index_12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16451,c_16304]) ).
tff(c_16474,plain,
index_144 = index_12,
inference(splitLeft,[status(thm)],[c_16457]) ).
tff(c_16495,plain,
s(index_12) = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_16474,c_2089]) ).
tff(c_16493,plain,
s(index_135) = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_16474,c_3398]) ).
tff(c_16527,plain,
index_18 = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_16495,c_2128]) ).
tff(c_16766,plain,
s(index_150) = index_24,
inference(demodulation,[status(thm),theory(equality)],[c_16527,c_2550]) ).
tff(c_16772,plain,
index_24 = index_165,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_16766]) ).
tff(c_16819,plain,
s(index_165) = index_33,
inference(demodulation,[status(thm),theory(equality)],[c_16772,c_3388]) ).
tff(c_52,plain,
! [X_40] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X_40)))))))))))))))))))))))))))))))))))) != X_40 ),
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_17187,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_33))))))))))))))))))))))))))))))))))) != index_165,
inference(superposition,[status(thm),theory(equality)],[c_16819,c_52]) ).
tff(c_17311,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_16495,c_16493,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_16819,c_6613,c_16495,c_16493,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_17187]) ).
tff(c_17312,plain,
select(earray_142,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_16457]) ).
tff(c_1822,plain,
rselect_seq(queue_134) = earray_133,
inference(superposition,[status(thm),theory(equality)],[c_440,c_1786]) ).
tff(c_2767,plain,
rselect_seq(queue_136) = rselect_seq(queue_134),
inference(superposition,[status(thm),theory(equality)],[c_442,c_2677]) ).
tff(c_2797,plain,
rselect_seq(queue_136) = earray_133,
inference(demodulation,[status(thm),theory(equality)],[c_1822,c_2767]) ).
tff(c_150,plain,
rselect_seq(q27) = earray_140,
inference(cnfTransformation,[status(thm)],[f_211]) ).
tff(c_3325,plain,
rselect_seq(queue_136) = rselect_seq(q27),
inference(superposition,[status(thm),theory(equality)],[c_640,c_3313]) ).
tff(c_3356,plain,
rselect_seq(queue_136) = earray_140,
inference(demodulation,[status(thm),theory(equality)],[c_150,c_3325]) ).
tff(c_11743,plain,
earray_140 = earray_133,
inference(demodulation,[status(thm),theory(equality)],[c_2797,c_3356]) ).
tff(c_152,plain,
store(earray_140,index_141,e27) = earray_142,
inference(cnfTransformation,[status(thm)],[f_212]) ).
tff(c_3393,plain,
store(earray_140,index_135,e27) = earray_142,
inference(demodulation,[status(thm),theory(equality)],[c_2986,c_152]) ).
tff(c_15762,plain,
store(earray_133,index_135,e27) = earray_142,
inference(demodulation,[status(thm),theory(equality)],[c_11743,c_3393]) ).
tff(c_15766,plain,
! [J_5] :
( ( select(earray_142,J_5) = select(earray_133,J_5) )
| ( index_135 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15762,c_4]) ).
tff(c_17317,plain,
( ( select(earray_133,index_12) = elem_214 )
| ( index_135 = index_12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17312,c_15766]) ).
tff(c_17327,plain,
index_135 = index_12,
inference(splitLeft,[status(thm)],[c_17317]) ).
tff(c_17344,plain,
s(index_129) = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_17327,c_4435]) ).
tff(c_56,plain,
! [X_42] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X_42)))))))))))))))))))))))))))))))))) != X_42 ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_17437,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_12))))))))))))))))))))))))))))))))) != index_129,
inference(superposition,[status(thm),theory(equality)],[c_17344,c_56]) ).
tff(c_17557,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_2550,c_2128,c_17344,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_2550,c_2128,c_17437]) ).
tff(c_17558,plain,
select(earray_133,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_17317]) ).
tff(c_1879,plain,
rselect_seq(queue_128) = earray_127,
inference(superposition,[status(thm),theory(equality)],[c_434,c_1786]) ).
tff(c_144,plain,
rselect_seq(q26) = earray_131,
inference(cnfTransformation,[status(thm)],[f_208]) ).
tff(c_2707,plain,
rselect_seq(queue_128) = rselect_seq(q26),
inference(superposition,[status(thm),theory(equality)],[c_641,c_2677]) ).
tff(c_2779,plain,
earray_131 = earray_127,
inference(demodulation,[status(thm),theory(equality)],[c_1879,c_144,c_2707]) ).
tff(c_146,plain,
store(earray_131,index_132,e26) = earray_133,
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_3006,plain,
store(earray_127,index_132,e26) = earray_133,
inference(demodulation,[status(thm),theory(equality)],[c_2779,c_146]) ).
tff(c_15730,plain,
store(earray_127,index_129,e26) = earray_133,
inference(demodulation,[status(thm),theory(equality)],[c_4428,c_3006]) ).
tff(c_15734,plain,
! [J_5] :
( ( select(earray_133,J_5) = select(earray_127,J_5) )
| ( index_129 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15730,c_4]) ).
tff(c_17563,plain,
( ( select(earray_127,index_12) = elem_214 )
| ( index_129 = index_12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17558,c_15734]) ).
tff(c_17573,plain,
index_129 = index_12,
inference(splitLeft,[status(thm)],[c_17563]) ).
tff(c_17592,plain,
s(index_12) = index_135,
inference(demodulation,[status(thm),theory(equality)],[c_17573,c_4435]) ).
tff(c_17627,plain,
index_18 = index_135,
inference(demodulation,[status(thm),theory(equality)],[c_17592,c_2128]) ).
tff(c_17848,plain,
s(index_135) = index_24,
inference(demodulation,[status(thm),theory(equality)],[c_17627,c_2550]) ).
tff(c_17854,plain,
index_24 = index_144,
inference(demodulation,[status(thm),theory(equality)],[c_3398,c_17848]) ).
tff(c_17902,plain,
s(index_144) = index_33,
inference(demodulation,[status(thm),theory(equality)],[c_17854,c_3388]) ).
tff(c_17909,plain,
index_33 = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_2089,c_17902]) ).
tff(c_17951,plain,
s(index_150) = index_39,
inference(demodulation,[status(thm),theory(equality)],[c_17909,c_5847]) ).
tff(c_17957,plain,
index_39 = index_165,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_17951]) ).
tff(c_17992,plain,
s(index_165) = index_45,
inference(demodulation,[status(thm),theory(equality)],[c_17957,c_2348]) ).
tff(c_17594,plain,
s(index_123) = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_17573,c_7961]) ).
tff(c_28,plain,
! [X_28] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X_28)))))))))))))))))))))))))))))))))))))))))))))))) != X_28 ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_18320,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_12))))))))))))))))))))))))))))))))))))))))))))))) != index_123,
inference(superposition,[status(thm),theory(equality)],[c_17594,c_28]) ).
tff(c_18468,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_17992,c_6613,c_2089,c_3398,c_17592,c_17594,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_17992,c_6613,c_2089,c_3398,c_17592,c_17594,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_17992,c_6613,c_2089,c_3398,c_17592,c_18320]) ).
tff(c_18469,plain,
select(earray_127,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_17563]) ).
tff(c_18700,plain,
( ( select(earray_121,index_12) = elem_214 )
| ( index_123 = index_12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18694,c_18469]) ).
tff(c_18717,plain,
index_123 = index_12,
inference(splitLeft,[status(thm)],[c_18700]) ).
tff(c_18741,plain,
s(index_114) = index_12,
inference(demodulation,[status(thm),theory(equality)],[c_18717,c_3162]) ).
tff(c_34,plain,
! [X_31] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X_31))))))))))))))))))))))))))))))))))))))))))))) != X_31 ),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_18777,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_12)))))))))))))))))))))))))))))))))))))))))))) != index_114,
inference(superposition,[status(thm),theory(equality)],[c_18741,c_34]) ).
tff(c_18919,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_2550,c_2128,c_18741,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_2550,c_2128,c_18741,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_4180,c_3406,c_2348,c_5847,c_3388,c_2550,c_2128,c_18777]) ).
tff(c_18920,plain,
select(earray_121,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_18700]) ).
tff(c_1798,plain,
rselect_seq(queue_113) = earray_112,
inference(superposition,[status(thm),theory(equality)],[c_424,c_1786]) ).
tff(c_2752,plain,
rselect_seq(queue_115) = rselect_seq(queue_113),
inference(superposition,[status(thm),theory(equality)],[c_426,c_2677]) ).
tff(c_2792,plain,
rselect_seq(queue_115) = earray_112,
inference(demodulation,[status(thm),theory(equality)],[c_1798,c_2752]) ).
tff(c_136,plain,
rselect_seq(q24) = earray_119,
inference(cnfTransformation,[status(thm)],[f_204]) ).
tff(c_3349,plain,
rselect_seq(queue_115) = rselect_seq(q24),
inference(superposition,[status(thm),theory(equality)],[c_644,c_3313]) ).
tff(c_3364,plain,
rselect_seq(queue_115) = earray_119,
inference(demodulation,[status(thm),theory(equality)],[c_136,c_3349]) ).
tff(c_11808,plain,
earray_119 = earray_112,
inference(demodulation,[status(thm),theory(equality)],[c_2792,c_3364]) ).
tff(c_138,plain,
store(earray_119,index_120,e24) = earray_121,
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_3159,plain,
store(earray_119,index_114,e24) = earray_121,
inference(demodulation,[status(thm),theory(equality)],[c_2993,c_138]) ).
tff(c_15591,plain,
store(earray_112,index_114,e24) = earray_121,
inference(demodulation,[status(thm),theory(equality)],[c_11808,c_3159]) ).
tff(c_15595,plain,
! [J_5] :
( ( select(earray_121,J_5) = select(earray_112,J_5) )
| ( index_114 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15591,c_4]) ).
tff(c_18926,plain,
( ( select(earray_112,index_12) = elem_214 )
| ( index_12 = index_114 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18920,c_15595]) ).
tff(c_18935,plain,
index_12 = index_114,
inference(splitLeft,[status(thm)],[c_18926]) ).
tff(c_18972,plain,
s(index_114) = index_18,
inference(demodulation,[status(thm),theory(equality)],[c_18935,c_2128]) ).
tff(c_18978,plain,
index_18 = index_123,
inference(demodulation,[status(thm),theory(equality)],[c_3162,c_18972]) ).
tff(c_19019,plain,
s(index_123) = index_24,
inference(demodulation,[status(thm),theory(equality)],[c_18978,c_2550]) ).
tff(c_19024,plain,
index_24 = index_129,
inference(demodulation,[status(thm),theory(equality)],[c_7961,c_19019]) ).
tff(c_19100,plain,
s(index_129) = index_33,
inference(demodulation,[status(thm),theory(equality)],[c_19024,c_3388]) ).
tff(c_19106,plain,
index_33 = index_135,
inference(demodulation,[status(thm),theory(equality)],[c_4435,c_19100]) ).
tff(c_19153,plain,
s(index_135) = index_39,
inference(demodulation,[status(thm),theory(equality)],[c_19106,c_5847]) ).
tff(c_19159,plain,
index_39 = index_144,
inference(demodulation,[status(thm),theory(equality)],[c_3398,c_19153]) ).
tff(c_19194,plain,
s(index_144) = index_45,
inference(demodulation,[status(thm),theory(equality)],[c_19159,c_2348]) ).
tff(c_19199,plain,
index_45 = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_2089,c_19194]) ).
tff(c_19233,plain,
s(index_150) = index_54,
inference(demodulation,[status(thm),theory(equality)],[c_19199,c_3406]) ).
tff(c_19240,plain,
index_54 = index_165,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_19233]) ).
tff(c_19285,plain,
s(index_165) = index_60,
inference(demodulation,[status(thm),theory(equality)],[c_19240,c_4180]) ).
tff(c_40,plain,
! [X_34] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X_34)))))))))))))))))))))))))))))))))))))))))) != X_34 ),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_19449,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_60))))))))))))))))))))))))))))))))))))))))) != index_165,
inference(superposition,[status(thm),theory(equality)],[c_19285,c_40]) ).
tff(c_19585,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_2089,c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_19285,c_6613,c_2089,c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_19285,c_6613,c_2089,c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_4762,c_19449]) ).
tff(c_19586,plain,
select(earray_112,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_18926]) ).
tff(c_1825,plain,
rselect_seq(queue_107) = earray_106,
inference(superposition,[status(thm),theory(equality)],[c_418,c_1786]) ).
tff(c_132,plain,
rselect_seq(q23) = earray_110,
inference(cnfTransformation,[status(thm)],[f_202]) ).
tff(c_2710,plain,
rselect_seq(queue_107) = rselect_seq(q23),
inference(superposition,[status(thm),theory(equality)],[c_645,c_2677]) ).
tff(c_2780,plain,
earray_110 = earray_106,
inference(demodulation,[status(thm),theory(equality)],[c_1825,c_132,c_2710]) ).
tff(c_134,plain,
store(earray_110,index_111,e23) = earray_112,
inference(cnfTransformation,[status(thm)],[f_203]) ).
tff(c_2311,plain,
store(earray_110,index_108,e23) = earray_112,
inference(demodulation,[status(thm),theory(equality)],[c_2306,c_134]) ).
tff(c_15549,plain,
store(earray_106,index_108,e23) = earray_112,
inference(demodulation,[status(thm),theory(equality)],[c_2780,c_2311]) ).
tff(c_15553,plain,
! [J_5] :
( ( select(earray_112,J_5) = select(earray_106,J_5) )
| ( index_108 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15549,c_4]) ).
tff(c_19592,plain,
( ( select(earray_106,index_12) = elem_214 )
| ( index_12 = index_108 ) ),
inference(superposition,[status(thm),theory(equality)],[c_19586,c_15553]) ).
tff(c_19602,plain,
index_12 = index_108,
inference(splitLeft,[status(thm)],[c_19592]) ).
tff(c_19641,plain,
s(index_108) = index_18,
inference(demodulation,[status(thm),theory(equality)],[c_19602,c_2128]) ).
tff(c_19647,plain,
index_18 = index_114,
inference(demodulation,[status(thm),theory(equality)],[c_2314,c_19641]) ).
tff(c_19708,plain,
s(index_114) = index_24,
inference(demodulation,[status(thm),theory(equality)],[c_19647,c_2550]) ).
tff(c_19713,plain,
index_24 = index_123,
inference(demodulation,[status(thm),theory(equality)],[c_3162,c_19708]) ).
tff(c_19761,plain,
s(index_123) = index_33,
inference(demodulation,[status(thm),theory(equality)],[c_19713,c_3388]) ).
tff(c_19767,plain,
index_33 = index_129,
inference(demodulation,[status(thm),theory(equality)],[c_7961,c_19761]) ).
tff(c_19814,plain,
s(index_129) = index_39,
inference(demodulation,[status(thm),theory(equality)],[c_19767,c_5847]) ).
tff(c_19820,plain,
index_39 = index_135,
inference(demodulation,[status(thm),theory(equality)],[c_4435,c_19814]) ).
tff(c_19879,plain,
s(index_135) = index_45,
inference(demodulation,[status(thm),theory(equality)],[c_19820,c_2348]) ).
tff(c_19884,plain,
index_45 = index_144,
inference(demodulation,[status(thm),theory(equality)],[c_3398,c_19879]) ).
tff(c_19917,plain,
s(index_144) = index_54,
inference(demodulation,[status(thm),theory(equality)],[c_19884,c_3406]) ).
tff(c_19924,plain,
index_54 = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_2089,c_19917]) ).
tff(c_19969,plain,
s(index_150) = index_60,
inference(demodulation,[status(thm),theory(equality)],[c_19924,c_4180]) ).
tff(c_19974,plain,
index_60 = index_165,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_19969]) ).
tff(c_20005,plain,
s(index_165) = index_66,
inference(demodulation,[status(thm),theory(equality)],[c_19974,c_4762]) ).
tff(c_46,plain,
! [X_37] : ( s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X_37))))))))))))))))))))))))))))))))))))))) != X_37 ),
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_20412,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_66)))))))))))))))))))))))))))))))))))))) != index_165,
inference(superposition,[status(thm),theory(equality)],[c_20005,c_46]) ).
tff(c_20542,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_2089,c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_20005,c_6613,c_2089,c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_20005,c_6613,c_2089,c_3398,c_4435,c_7961,c_3162,c_2314,c_2189,c_3173,c_2672,c_2533,c_10630,c_20412]) ).
tff(c_20543,plain,
select(earray_106,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_19592]) ).
tff(c_1834,plain,
rselect_seq(queue_101) = earray_100,
inference(superposition,[status(thm),theory(equality)],[c_414,c_1786]) ).
tff(c_128,plain,
rselect_seq(q22) = earray_104,
inference(cnfTransformation,[status(thm)],[f_200]) ).
tff(c_2758,plain,
rselect_seq(queue_101) = rselect_seq(q22),
inference(superposition,[status(thm),theory(equality)],[c_646,c_2677]) ).
tff(c_2794,plain,
rselect_seq(queue_101) = earray_104,
inference(demodulation,[status(thm),theory(equality)],[c_128,c_2758]) ).
tff(c_11790,plain,
earray_104 = earray_100,
inference(demodulation,[status(thm),theory(equality)],[c_1834,c_2794]) ).
tff(c_130,plain,
store(earray_104,index_105,e22) = earray_106,
inference(cnfTransformation,[status(thm)],[f_201]) ).
tff(c_2186,plain,
store(earray_104,index_102,e22) = earray_106,
inference(demodulation,[status(thm),theory(equality)],[c_2181,c_130]) ).
tff(c_15491,plain,
store(earray_100,index_102,e22) = earray_106,
inference(demodulation,[status(thm),theory(equality)],[c_11790,c_2186]) ).
tff(c_15495,plain,
! [J_5] :
( ( select(earray_106,J_5) = select(earray_100,J_5) )
| ( index_102 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15491,c_4]) ).
tff(c_20549,plain,
( ( select(earray_100,index_12) = elem_214 )
| ( index_12 = index_102 ) ),
inference(superposition,[status(thm),theory(equality)],[c_20543,c_15495]) ).
tff(c_20586,plain,
index_12 = index_102,
inference(splitLeft,[status(thm)],[c_20549]) ).
tff(c_20627,plain,
s(index_102) = index_18,
inference(demodulation,[status(thm),theory(equality)],[c_20586,c_2128]) ).
tff(c_20633,plain,
index_18 = index_108,
inference(demodulation,[status(thm),theory(equality)],[c_2189,c_20627]) ).
tff(c_20690,plain,
s(index_108) = index_24,
inference(demodulation,[status(thm),theory(equality)],[c_20633,c_2550]) ).
tff(c_20695,plain,
index_24 = index_114,
inference(demodulation,[status(thm),theory(equality)],[c_2314,c_20690]) ).
tff(c_20753,plain,
s(index_114) = index_33,
inference(demodulation,[status(thm),theory(equality)],[c_20695,c_3388]) ).
tff(c_20759,plain,
index_33 = index_123,
inference(demodulation,[status(thm),theory(equality)],[c_3162,c_20753]) ).
tff(c_20805,plain,
s(index_123) = index_39,
inference(demodulation,[status(thm),theory(equality)],[c_20759,c_5847]) ).
tff(c_20811,plain,
index_39 = index_129,
inference(demodulation,[status(thm),theory(equality)],[c_7961,c_20805]) ).
tff(c_20846,plain,
s(index_129) = index_45,
inference(demodulation,[status(thm),theory(equality)],[c_20811,c_2348]) ).
tff(c_20851,plain,
index_45 = index_135,
inference(demodulation,[status(thm),theory(equality)],[c_4435,c_20846]) ).
tff(c_20883,plain,
s(index_135) = index_54,
inference(demodulation,[status(thm),theory(equality)],[c_20851,c_3406]) ).
tff(c_20890,plain,
index_54 = index_144,
inference(demodulation,[status(thm),theory(equality)],[c_3398,c_20883]) ).
tff(c_20931,plain,
s(index_144) = index_60,
inference(demodulation,[status(thm),theory(equality)],[c_20890,c_4180]) ).
tff(c_20936,plain,
index_60 = index_150,
inference(demodulation,[status(thm),theory(equality)],[c_2089,c_20931]) ).
tff(c_20965,plain,
s(index_150) = index_66,
inference(demodulation,[status(thm),theory(equality)],[c_20936,c_4762]) ).
tff(c_20970,plain,
index_66 = index_165,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_20965]) ).
tff(c_21015,plain,
s(index_165) = index_75,
inference(demodulation,[status(thm),theory(equality)],[c_20970,c_10630]) ).
tff(c_100,plain,
! [X_64] : ( s(s(s(s(s(s(s(s(s(s(s(s(X_64)))))))))))) != X_64 ),
inference(cnfTransformation,[status(thm)],[f_164]) ).
tff(c_11424,plain,
s(s(s(s(s(s(s(s(s(s(s(index_93))))))))))) != index_87,
inference(superposition,[status(thm),theory(equality)],[c_2672,c_100]) ).
tff(c_11498,plain,
s(s(s(s(s(s(index_129)))))) != index_87,
inference(demodulation,[status(thm),theory(equality)],[c_7961,c_3162,c_2314,c_2189,c_3173,c_11424]) ).
tff(c_18573,plain,
s(s(index_165)) != index_87,
inference(demodulation,[status(thm),theory(equality)],[c_6613,c_2089,c_3398,c_4435,c_11498]) ).
tff(c_21082,plain,
s(index_75) != index_87,
inference(demodulation,[status(thm),theory(equality)],[c_21015,c_18573]) ).
tff(c_21124,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2533,c_21082]) ).
tff(c_21125,plain,
select(earray_100,index_12) = elem_214,
inference(splitRight,[status(thm)],[c_20549]) ).
tff(c_1852,plain,
rselect_seq(queue_17) = earray_16,
inference(superposition,[status(thm),theory(equality)],[c_466,c_1786]) ).
tff(c_190,plain,
rselect_seq(q11) = earray_20,
inference(cnfTransformation,[status(thm)],[f_231]) ).
tff(c_2737,plain,
rselect_seq(queue_17) = rselect_seq(q11),
inference(superposition,[status(thm),theory(equality)],[c_633,c_2677]) ).
tff(c_2789,plain,
earray_20 = earray_16,
inference(demodulation,[status(thm),theory(equality)],[c_1852,c_190,c_2737]) ).
tff(c_198,plain,
store(earray_20,index_21,e11) = earray_22,
inference(cnfTransformation,[status(thm)],[f_235]) ).
tff(c_2547,plain,
store(earray_20,index_18,e11) = earray_22,
inference(demodulation,[status(thm),theory(equality)],[c_2538,c_198]) ).
tff(c_15448,plain,
store(earray_16,index_18,e11) = earray_22,
inference(demodulation,[status(thm),theory(equality)],[c_2789,c_2547]) ).
tff(c_15452,plain,
! [J_5] :
( ( select(earray_22,J_5) = select(earray_16,J_5) )
| ( index_18 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15448,c_4]) ).
tff(c_1840,plain,
rselect_seq(queue_32) = earray_31,
inference(superposition,[status(thm),theory(equality)],[c_504,c_1786]) ).
tff(c_204,plain,
rselect_seq(q13) = earray_35,
inference(cnfTransformation,[status(thm)],[f_238]) ).
tff(c_2728,plain,
rselect_seq(queue_32) = rselect_seq(q13),
inference(superposition,[status(thm),theory(equality)],[c_627,c_2677]) ).
tff(c_2786,plain,
earray_35 = earray_31,
inference(demodulation,[status(thm),theory(equality)],[c_1840,c_204,c_2728]) ).
tff(c_206,plain,
store(earray_35,index_36,e13) = earray_37,
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_3558,plain,
store(earray_31,index_36,e13) = earray_37,
inference(demodulation,[status(thm),theory(equality)],[c_2786,c_206]) ).
tff(c_15564,plain,
store(earray_31,index_33,e13) = earray_37,
inference(demodulation,[status(thm),theory(equality)],[c_5840,c_3558]) ).
tff(c_15568,plain,
! [J_5] :
( ( select(earray_37,J_5) = select(earray_31,J_5) )
| ( index_33 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15564,c_4]) ).
tff(c_1837,plain,
rselect_seq(queue_38) = earray_37,
inference(superposition,[status(thm),theory(equality)],[c_508,c_1786]) ).
tff(c_210,plain,
rselect_seq(q14) = earray_41,
inference(cnfTransformation,[status(thm)],[f_241]) ).
tff(c_2698,plain,
rselect_seq(queue_38) = rselect_seq(q14),
inference(superposition,[status(thm),theory(equality)],[c_626,c_2677]) ).
tff(c_2776,plain,
earray_41 = earray_37,
inference(demodulation,[status(thm),theory(equality)],[c_1837,c_210,c_2698]) ).
tff(c_212,plain,
store(earray_41,index_42,e14) = earray_43,
inference(cnfTransformation,[status(thm)],[f_242]) ).
tff(c_2645,plain,
store(earray_41,index_39,e14) = earray_43,
inference(demodulation,[status(thm),theory(equality)],[c_2337,c_212]) ).
tff(c_2916,plain,
store(earray_37,index_39,e14) = earray_43,
inference(demodulation,[status(thm),theory(equality)],[c_2776,c_2645]) ).
tff(c_14799,plain,
! [J_5] :
( ( select(earray_43,J_5) = select(earray_37,J_5) )
| ( index_39 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_2916,c_4]) ).
tff(c_1810,plain,
rselect_seq(queue_44) = earray_43,
inference(superposition,[status(thm),theory(equality)],[c_512,c_1786]) ).
tff(c_2755,plain,
rselect_seq(queue_46) = rselect_seq(queue_44),
inference(superposition,[status(thm),theory(equality)],[c_514,c_2677]) ).
tff(c_2793,plain,
rselect_seq(queue_46) = earray_43,
inference(demodulation,[status(thm),theory(equality)],[c_1810,c_2755]) ).
tff(c_214,plain,
rselect_seq(q15) = earray_50,
inference(cnfTransformation,[status(thm)],[f_243]) ).
tff(c_3322,plain,
rselect_seq(queue_46) = rselect_seq(q15),
inference(superposition,[status(thm),theory(equality)],[c_625,c_3313]) ).
tff(c_3355,plain,
rselect_seq(queue_46) = earray_50,
inference(demodulation,[status(thm),theory(equality)],[c_214,c_3322]) ).
tff(c_11117,plain,
earray_50 = earray_43,
inference(demodulation,[status(thm),theory(equality)],[c_2793,c_3355]) ).
tff(c_216,plain,
store(earray_50,index_51,e15) = earray_52,
inference(cnfTransformation,[status(thm)],[f_244]) ).
tff(c_3403,plain,
store(earray_50,index_45,e15) = earray_52,
inference(demodulation,[status(thm),theory(equality)],[c_2985,c_216]) ).
tff(c_15670,plain,
store(earray_43,index_45,e15) = earray_52,
inference(demodulation,[status(thm),theory(equality)],[c_11117,c_3403]) ).
tff(c_15674,plain,
! [J_5] :
( ( select(earray_52,J_5) = select(earray_43,J_5) )
| ( index_45 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15670,c_4]) ).
tff(c_1876,plain,
rselect_seq(queue_65) = earray_64,
inference(superposition,[status(thm),theory(equality)],[c_528,c_1786]) ).
tff(c_2692,plain,
rselect_seq(queue_67) = rselect_seq(queue_65),
inference(superposition,[status(thm),theory(equality)],[c_530,c_2677]) ).
tff(c_2774,plain,
rselect_seq(queue_67) = earray_64,
inference(demodulation,[status(thm),theory(equality)],[c_1876,c_2692]) ).
tff(c_226,plain,
rselect_seq(q18) = earray_71,
inference(cnfTransformation,[status(thm)],[f_249]) ).
tff(c_3346,plain,
rselect_seq(queue_67) = rselect_seq(q18),
inference(superposition,[status(thm),theory(equality)],[c_621,c_3313]) ).
tff(c_3363,plain,
rselect_seq(queue_67) = earray_71,
inference(demodulation,[status(thm),theory(equality)],[c_226,c_3346]) ).
tff(c_11127,plain,
earray_71 = earray_64,
inference(demodulation,[status(thm),theory(equality)],[c_2774,c_3363]) ).
tff(c_228,plain,
store(earray_71,index_72,e18) = earray_73,
inference(cnfTransformation,[status(thm)],[f_250]) ).
tff(c_4006,plain,
! [A_105,I_106,E_107,J_108] :
( ( select(store(A_105,I_106,E_107),J_108) = select(A_105,J_108) )
| ( J_108 = I_106 ) ),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_4022,plain,
! [J_108] :
( ( select(earray_73,J_108) = select(earray_71,J_108) )
| ( index_72 = J_108 ) ),
inference(superposition,[status(thm),theory(equality)],[c_228,c_4006]) ).
tff(c_15954,plain,
! [J_108] :
( ( select(earray_73,J_108) = select(earray_64,J_108) )
| ( index_66 = J_108 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_10624,c_11127,c_4022]) ).
tff(c_1813,plain,
rselect_seq(queue_74) = earray_73,
inference(superposition,[status(thm),theory(equality)],[c_536,c_1786]) ).
tff(c_236,plain,
rselect_seq(q19) = earray_83,
inference(cnfTransformation,[status(thm)],[f_254]) ).
tff(c_2734,plain,
rselect_seq(queue_74) = rselect_seq(q19),
inference(superposition,[status(thm),theory(equality)],[c_620,c_2677]) ).
tff(c_2788,plain,
earray_83 = earray_73,
inference(demodulation,[status(thm),theory(equality)],[c_1813,c_236,c_2734]) ).
tff(c_238,plain,
store(earray_83,index_84,e19) = earray_85,
inference(cnfTransformation,[status(thm)],[f_255]) ).
tff(c_2530,plain,
store(earray_83,index_75,e19) = earray_85,
inference(demodulation,[status(thm),theory(equality)],[c_2525,c_238]) ).
tff(c_15741,plain,
store(earray_73,index_75,e19) = earray_85,
inference(demodulation,[status(thm),theory(equality)],[c_2788,c_2530]) ).
tff(c_15745,plain,
! [J_5] :
( ( select(earray_85,J_5) = select(earray_73,J_5) )
| ( index_75 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15741,c_4]) ).
tff(c_1819,plain,
rselect_seq(queue_92) = earray_91,
inference(superposition,[status(thm),theory(equality)],[c_548,c_1786]) ).
tff(c_2761,plain,
rselect_seq(queue_94) = rselect_seq(queue_92),
inference(superposition,[status(thm),theory(equality)],[c_550,c_2677]) ).
tff(c_2795,plain,
rselect_seq(queue_94) = earray_91,
inference(demodulation,[status(thm),theory(equality)],[c_1819,c_2761]) ).
tff(c_244,plain,
rselect_seq(q21) = earray_98,
inference(cnfTransformation,[status(thm)],[f_258]) ).
tff(c_3343,plain,
rselect_seq(queue_94) = rselect_seq(q21),
inference(superposition,[status(thm),theory(equality)],[c_617,c_3313]) ).
tff(c_3362,plain,
rselect_seq(queue_94) = earray_98,
inference(demodulation,[status(thm),theory(equality)],[c_244,c_3343]) ).
tff(c_10467,plain,
earray_98 = earray_91,
inference(demodulation,[status(thm),theory(equality)],[c_2795,c_3362]) ).
tff(c_126,plain,
store(earray_98,index_99,e21) = earray_100,
inference(cnfTransformation,[status(thm)],[f_199]) ).
tff(c_3169,plain,
store(earray_98,index_93,e21) = earray_100,
inference(demodulation,[status(thm),theory(equality)],[c_2991,c_126]) ).
tff(c_15414,plain,
store(earray_91,index_93,e21) = earray_100,
inference(demodulation,[status(thm),theory(equality)],[c_10467,c_3169]) ).
tff(c_18574,plain,
! [J_180] :
( ( select(earray_91,J_180) = select(earray_100,J_180) )
| ( index_93 = J_180 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15414,c_4]) ).
tff(c_1864,plain,
rselect_seq(queue_86) = earray_85,
inference(superposition,[status(thm),theory(equality)],[c_544,c_1786]) ).
tff(c_240,plain,
rselect_seq(q20) = earray_89,
inference(cnfTransformation,[status(thm)],[f_256]) ).
tff(c_2749,plain,
rselect_seq(queue_86) = rselect_seq(q20),
inference(superposition,[status(thm),theory(equality)],[c_618,c_2677]) ).
tff(c_2791,plain,
earray_89 = earray_85,
inference(demodulation,[status(thm),theory(equality)],[c_1864,c_240,c_2749]) ).
tff(c_242,plain,
store(earray_89,index_90,e20) = earray_91,
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_2669,plain,
store(earray_89,index_87,e20) = earray_91,
inference(demodulation,[status(thm),theory(equality)],[c_2664,c_242]) ).
tff(c_15609,plain,
store(earray_85,index_87,e20) = earray_91,
inference(demodulation,[status(thm),theory(equality)],[c_2791,c_2669]) ).
tff(c_15613,plain,
! [J_5] :
( ( select(earray_91,J_5) = select(earray_85,J_5) )
| ( index_87 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15609,c_4]) ).
tff(c_21308,plain,
! [J_201] :
( ( select(earray_85,J_201) = select(earray_100,J_201) )
| ( index_87 = J_201 )
| ( index_93 = J_201 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18574,c_15613]) ).
tff(c_21489,plain,
! [J_204] :
( ( select(earray_73,J_204) = select(earray_100,J_204) )
| ( index_87 = J_204 )
| ( index_93 = J_204 )
| ( index_75 = J_204 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15745,c_21308]) ).
tff(c_21655,plain,
! [J_206] :
( ( select(earray_64,J_206) = select(earray_100,J_206) )
| ( index_87 = J_206 )
| ( index_93 = J_206 )
| ( index_75 = J_206 )
| ( index_66 = J_206 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15954,c_21489]) ).
tff(c_1867,plain,
rselect_seq(queue_59) = earray_58,
inference(superposition,[status(thm),theory(equality)],[c_524,c_1786]) ).
tff(c_222,plain,
rselect_seq(q17) = earray_62,
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_2731,plain,
rselect_seq(queue_59) = rselect_seq(q17),
inference(superposition,[status(thm),theory(equality)],[c_623,c_2677]) ).
tff(c_2787,plain,
earray_62 = earray_58,
inference(demodulation,[status(thm),theory(equality)],[c_1867,c_222,c_2731]) ).
tff(c_224,plain,
store(earray_62,index_63,e17) = earray_64,
inference(cnfTransformation,[status(thm)],[f_248]) ).
tff(c_3552,plain,
store(earray_58,index_63,e17) = earray_64,
inference(demodulation,[status(thm),theory(equality)],[c_2787,c_224]) ).
tff(c_15520,plain,
store(earray_58,index_60,e17) = earray_64,
inference(demodulation,[status(thm),theory(equality)],[c_4660,c_3552]) ).
tff(c_15524,plain,
! [J_5] :
( ( select(earray_64,J_5) = select(earray_58,J_5) )
| ( index_60 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15520,c_4]) ).
tff(c_21819,plain,
! [J_208] :
( ( select(earray_58,J_208) = select(earray_100,J_208) )
| ( index_60 = J_208 )
| ( index_87 = J_208 )
| ( index_93 = J_208 )
| ( index_75 = J_208 )
| ( index_66 = J_208 ) ),
inference(superposition,[status(thm),theory(equality)],[c_21655,c_15524]) ).
tff(c_1816,plain,
rselect_seq(queue_53) = earray_52,
inference(superposition,[status(thm),theory(equality)],[c_520,c_1786]) ).
tff(c_218,plain,
rselect_seq(q16) = earray_56,
inference(cnfTransformation,[status(thm)],[f_245]) ).
tff(c_2704,plain,
rselect_seq(queue_53) = rselect_seq(q16),
inference(superposition,[status(thm),theory(equality)],[c_624,c_2677]) ).
tff(c_2778,plain,
earray_56 = earray_52,
inference(demodulation,[status(thm),theory(equality)],[c_1816,c_218,c_2704]) ).
tff(c_220,plain,
store(earray_56,index_57,e16) = earray_58,
inference(cnfTransformation,[status(thm)],[f_246]) ).
tff(c_3000,plain,
store(earray_52,index_57,e16) = earray_58,
inference(demodulation,[status(thm),theory(equality)],[c_2778,c_220]) ).
tff(c_15687,plain,
store(earray_52,index_54,e16) = earray_58,
inference(demodulation,[status(thm),theory(equality)],[c_4173,c_3000]) ).
tff(c_15691,plain,
! [J_5] :
( ( select(earray_58,J_5) = select(earray_52,J_5) )
| ( index_54 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15687,c_4]) ).
tff(c_21984,plain,
! [J_210] :
( ( select(earray_52,J_210) = select(earray_100,J_210) )
| ( index_54 = J_210 )
| ( index_60 = J_210 )
| ( index_87 = J_210 )
| ( index_93 = J_210 )
| ( index_75 = J_210 )
| ( index_66 = J_210 ) ),
inference(superposition,[status(thm),theory(equality)],[c_21819,c_15691]) ).
tff(c_22151,plain,
! [J_212] :
( ( select(earray_43,J_212) = select(earray_100,J_212) )
| ( index_54 = J_212 )
| ( index_60 = J_212 )
| ( index_87 = J_212 )
| ( index_93 = J_212 )
| ( index_75 = J_212 )
| ( index_66 = J_212 )
| ( index_45 = J_212 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15674,c_21984]) ).
tff(c_22331,plain,
! [J_214] :
( ( select(earray_37,J_214) = select(earray_100,J_214) )
| ( index_54 = J_214 )
| ( index_60 = J_214 )
| ( index_87 = J_214 )
| ( index_93 = J_214 )
| ( index_75 = J_214 )
| ( index_66 = J_214 )
| ( index_45 = J_214 )
| ( index_39 = J_214 ) ),
inference(superposition,[status(thm),theory(equality)],[c_14799,c_22151]) ).
tff(c_22525,plain,
! [J_216] :
( ( select(earray_31,J_216) = select(earray_100,J_216) )
| ( index_54 = J_216 )
| ( index_60 = J_216 )
| ( index_87 = J_216 )
| ( index_93 = J_216 )
| ( index_75 = J_216 )
| ( index_66 = J_216 )
| ( index_45 = J_216 )
| ( index_39 = J_216 )
| ( index_33 = J_216 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15568,c_22331]) ).
tff(c_1882,plain,
rselect_seq(queue_23) = earray_22,
inference(superposition,[status(thm),theory(equality)],[c_498,c_1786]) ).
tff(c_2770,plain,
rselect_seq(queue_25) = rselect_seq(queue_23),
inference(superposition,[status(thm),theory(equality)],[c_500,c_2677]) ).
tff(c_2798,plain,
rselect_seq(queue_25) = earray_22,
inference(demodulation,[status(thm),theory(equality)],[c_1882,c_2770]) ).
tff(c_200,plain,
rselect_seq(q12) = earray_29,
inference(cnfTransformation,[status(thm)],[f_236]) ).
tff(c_3328,plain,
rselect_seq(queue_25) = rselect_seq(q12),
inference(superposition,[status(thm),theory(equality)],[c_628,c_3313]) ).
tff(c_3357,plain,
rselect_seq(queue_25) = earray_29,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_3328]) ).
tff(c_11756,plain,
earray_29 = earray_22,
inference(demodulation,[status(thm),theory(equality)],[c_2798,c_3357]) ).
tff(c_202,plain,
store(earray_29,index_30,e12) = earray_31,
inference(cnfTransformation,[status(thm)],[f_237]) ).
tff(c_3384,plain,
store(earray_29,index_24,e12) = earray_31,
inference(demodulation,[status(thm),theory(equality)],[c_2987,c_202]) ).
tff(c_15624,plain,
store(earray_22,index_24,e12) = earray_31,
inference(demodulation,[status(thm),theory(equality)],[c_11756,c_3384]) ).
tff(c_15628,plain,
! [J_5] :
( ( select(earray_31,J_5) = select(earray_22,J_5) )
| ( index_24 = J_5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15624,c_4]) ).
tff(c_22679,plain,
! [J_217] :
( ( select(earray_22,J_217) = select(earray_100,J_217) )
| ( index_24 = J_217 )
| ( index_54 = J_217 )
| ( index_60 = J_217 )
| ( index_87 = J_217 )
| ( index_93 = J_217 )
| ( index_75 = J_217 )
| ( index_66 = J_217 )
| ( index_45 = J_217 )
| ( index_39 = J_217 )
| ( index_33 = J_217 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22525,c_15628]) ).
tff(c_22826,plain,
! [J_218] :
( ( select(earray_16,J_218) = select(earray_100,J_218) )
| ( index_24 = J_218 )
| ( index_54 = J_218 )
| ( index_60 = J_218 )
| ( index_87 = J_218 )
| ( index_93 = J_218 )
| ( index_75 = J_218 )
| ( index_66 = J_218 )
| ( index_45 = J_218 )
| ( index_39 = J_218 )
| ( index_33 = J_218 )
| ( index_18 = J_218 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15452,c_22679]) ).
tff(c_162,plain,
store(earray_14,index_15,e10) = earray_16,
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_2594,plain,
store(earray_14,index_12,e10) = earray_16,
inference(demodulation,[status(thm),theory(equality)],[c_2121,c_162]) ).
tff(c_3519,plain,
! [A_98,I_99,E_100] : ( select(store(A_98,I_99,E_100),I_99) = E_100 ),
inference(cnfTransformation,[status(thm)],[f_25]) ).
tff(c_3528,plain,
select(earray_16,index_12) = e10,
inference(superposition,[status(thm),theory(equality)],[c_2594,c_3519]) ).
tff(c_22835,plain,
( ( select(earray_100,index_12) = e10 )
| ( index_24 = index_12 )
| ( index_54 = index_12 )
| ( index_60 = index_12 )
| ( index_87 = index_12 )
| ( index_93 = index_12 )
| ( index_75 = index_12 )
| ( index_66 = index_12 )
| ( index_45 = index_12 )
| ( index_39 = index_12 )
| ( index_33 = index_12 )
| ( index_18 = index_12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22826,c_3528]) ).
tff(c_22846,plain,
( ( elem_214 = e10 )
| ( index_24 = index_12 )
| ( index_54 = index_12 )
| ( index_60 = index_12 )
| ( index_87 = index_12 )
| ( index_93 = index_12 )
| ( index_75 = index_12 )
| ( index_66 = index_12 )
| ( index_45 = index_12 )
| ( index_39 = index_12 )
| ( index_33 = index_12 )
| ( index_18 = index_12 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21125,c_22835]) ).
tff(c_22848,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2127,c_15339,c_15427,c_15798,c_18642,c_21211,c_21406,c_21289,c_15923,c_15864,c_3988,c_616,c_22846]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWV568-1.030 : TPTP v9.0.0. Released v4.0.0.
% 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.34 % Computer : n017.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Apr 9 04:06:10 EDT 2025
% 0.14/0.34 % CPUTime :
% 39.78/21.65 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 39.95/21.74
% 39.95/21.74 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------