%------------------------------------------------------------------------------
% File : SNARK---20120808r022
% Problem : SWV569-1.030 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run-snark %s %d
% 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 : 600s
% DateTime : Wed Jul 20 21:35:15 EDT 2022
% Result : Unsatisfiable 7.08s 7.31s
% Output : Refutation 7.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 249
% Syntax : Number of clauses : 619 ( 574 unt; 45 nHn; 568 RR)
% Number of literals : 664 ( 663 equ; 64 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 263 ( 263 usr; 260 con; 0-3 aty)
% Number of variables : 80 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(a1,axiom,
select(store(X,Y,Z),Y) = Z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
cnf(a2,axiom,
( X = Y
| select(store(Z,X,U),Y) = select(Z,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
cnf(head_distinct_from_tail,axiom,
head != tail,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_tail) ).
cnf(head_distinct_from_seq,axiom,
head != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_seq) ).
cnf(tail_distinct_from_seq,axiom,
tail != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tail_distinct_from_seq) ).
cnf(as19,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as19) ).
cnf(as18,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as18) ).
cnf(as17,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as17) ).
cnf(as16,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as16) ).
cnf(as15,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as15) ).
cnf(as14,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as14) ).
cnf(as13,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(X))))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as13) ).
cnf(as12,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(X)))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as12) ).
cnf(as11,axiom,
s(s(s(s(s(s(s(s(s(s(s(X))))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as11) ).
cnf(as10,axiom,
s(s(s(s(s(s(s(s(s(s(X)))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as10) ).
cnf(as9,axiom,
s(s(s(s(s(s(s(s(s(X))))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as9) ).
cnf(as8,axiom,
s(s(s(s(s(s(s(s(X)))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as8) ).
cnf(as7,axiom,
s(s(s(s(s(s(s(X))))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as7) ).
cnf(as6,axiom,
s(s(s(s(s(s(X)))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as6) ).
cnf(as5,axiom,
s(s(s(s(s(X))))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as5) ).
cnf(as4,axiom,
s(s(s(s(X)))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as4) ).
cnf(as3,axiom,
s(s(s(X))) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as3) ).
cnf(as2,axiom,
s(s(X)) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as2) ).
cnf(as1,axiom,
s(X) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as1) ).
cnf(hyp1,hypothesis,
earray_100 = store(earray_98,index_99,e21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
cnf(hyp2,hypothesis,
earray_104 = select(q22,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
cnf(hyp3,hypothesis,
earray_106 = store(earray_104,index_105,e22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
cnf(hyp4,hypothesis,
earray_110 = select(q23,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
cnf(hyp5,hypothesis,
earray_112 = store(earray_110,index_111,e23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
cnf(hyp6,hypothesis,
earray_119 = select(q24,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
cnf(hyp7,hypothesis,
earray_121 = store(earray_119,index_120,e24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
cnf(hyp8,hypothesis,
earray_125 = select(q25,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
cnf(hyp9,hypothesis,
earray_127 = store(earray_125,index_126,e25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
cnf(hyp10,hypothesis,
earray_131 = select(q26,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
cnf(hyp11,hypothesis,
earray_133 = store(earray_131,index_132,e26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
cnf(hyp13,hypothesis,
earray_140 = select(q27,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
cnf(hyp14,hypothesis,
earray_142 = store(earray_140,index_141,e27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
cnf(hyp15,hypothesis,
earray_146 = select(q28,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
cnf(hyp16,hypothesis,
earray_148 = store(earray_146,index_147,e28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
cnf(hyp19,hypothesis,
earray_16 = store(earray_14,index_15,e10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
cnf(hyp20,hypothesis,
earray_161 = select(q29,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp20) ).
cnf(hyp21,hypothesis,
earray_163 = store(earray_161,index_162,e29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp21) ).
cnf(hyp33,hypothesis,
earray_20 = select(q11,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp33) ).
cnf(hyp36,hypothesis,
earray_212 = select(q30,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp36) ).
cnf(hyp37,hypothesis,
earray_22 = store(earray_20,index_21,e11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp37) ).
cnf(hyp38,hypothesis,
earray_29 = select(q12,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp38) ).
cnf(hyp39,hypothesis,
earray_31 = store(earray_29,index_30,e12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp39) ).
cnf(hyp40,hypothesis,
earray_35 = select(q13,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp40) ).
cnf(hyp41,hypothesis,
earray_37 = store(earray_35,index_36,e13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp41) ).
cnf(hyp43,hypothesis,
earray_41 = select(q14,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp43) ).
cnf(hyp44,hypothesis,
earray_43 = store(earray_41,index_42,e14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp44) ).
cnf(hyp45,hypothesis,
earray_50 = select(q15,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp45) ).
cnf(hyp46,hypothesis,
earray_52 = store(earray_50,index_51,e15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp46) ).
cnf(hyp47,hypothesis,
earray_56 = select(q16,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp47) ).
cnf(hyp48,hypothesis,
earray_58 = store(earray_56,index_57,e16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp48) ).
cnf(hyp49,hypothesis,
earray_62 = select(q17,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp49) ).
cnf(hyp50,hypothesis,
earray_64 = store(earray_62,index_63,e17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp50) ).
cnf(hyp51,hypothesis,
earray_71 = select(q18,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp51) ).
cnf(hyp52,hypothesis,
earray_73 = store(earray_71,index_72,e18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp52) ).
cnf(hyp56,hypothesis,
earray_83 = select(q19,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp56) ).
cnf(hyp57,hypothesis,
earray_85 = store(earray_83,index_84,e19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp57) ).
cnf(hyp58,hypothesis,
earray_89 = select(q20,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp58) ).
cnf(hyp59,hypothesis,
earray_91 = store(earray_89,index_90,e20),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp59) ).
cnf(hyp60,hypothesis,
earray_98 = select(q21,seq),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp60) ).
cnf(hyp61,hypothesis,
elem_214 = select(earray_212,index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp61) ).
cnf(hyp62,hypothesis,
index_0 = select(q,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp62) ).
cnf(hyp63,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp63) ).
cnf(hyp64,hypothesis,
index_105 = select(q22,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp64) ).
cnf(hyp65,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp65) ).
cnf(hyp66,hypothesis,
index_111 = select(q23,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp66) ).
cnf(hyp67,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp67) ).
cnf(hyp68,hypothesis,
index_116 = select(queue_115,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp68) ).
cnf(hyp69,hypothesis,
index_117 = s(index_116),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp69) ).
cnf(hyp70,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp70) ).
cnf(hyp71,hypothesis,
index_120 = select(q24,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp71) ).
cnf(hyp72,hypothesis,
index_123 = s(index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp72) ).
cnf(hyp73,hypothesis,
index_126 = select(q25,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp73) ).
cnf(hyp74,hypothesis,
index_129 = s(index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp74) ).
cnf(hyp75,hypothesis,
index_132 = select(q26,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp75) ).
cnf(hyp76,hypothesis,
index_135 = s(index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp76) ).
cnf(hyp77,hypothesis,
index_137 = select(queue_136,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp77) ).
cnf(hyp78,hypothesis,
index_138 = s(index_137),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp78) ).
cnf(hyp79,hypothesis,
index_141 = select(q27,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp79) ).
cnf(hyp80,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp80) ).
cnf(hyp81,hypothesis,
index_147 = select(q28,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp81) ).
cnf(hyp82,hypothesis,
index_15 = select(q10,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp82) ).
cnf(hyp83,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp83) ).
cnf(hyp84,hypothesis,
index_153 = select(q2,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp84) ).
cnf(hyp85,hypothesis,
index_156 = s(index_153),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp85) ).
cnf(hyp86,hypothesis,
index_158 = select(queue_157,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp86) ).
cnf(hyp87,hypothesis,
index_159 = s(index_158),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp87) ).
cnf(hyp88,hypothesis,
index_162 = select(q29,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp88) ).
cnf(hyp90,hypothesis,
index_167 = select(queue_166,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp90) ).
cnf(hyp91,hypothesis,
index_168 = s(index_167),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp91) ).
cnf(hyp92,hypothesis,
index_171 = select(q3,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp92) ).
cnf(hyp93,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
cnf(hyp94,hypothesis,
index_177 = select(q4,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
cnf(hyp95,hypothesis,
index_18 = s(index_15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
cnf(hyp96,hypothesis,
index_180 = s(index_177),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
cnf(hyp97,hypothesis,
index_183 = select(q5,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp97) ).
cnf(hyp98,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp98) ).
cnf(hyp99,hypothesis,
index_188 = select(queue_187,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
cnf(hyp100,hypothesis,
index_189 = s(index_188),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
cnf(hyp101,hypothesis,
index_192 = select(q6,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
cnf(hyp102,hypothesis,
index_195 = s(index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
cnf(hyp103,hypothesis,
index_198 = select(q7,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
cnf(hyp104,hypothesis,
index_201 = s(index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
cnf(hyp105,hypothesis,
index_204 = select(q8,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp105) ).
cnf(hyp106,hypothesis,
index_207 = s(index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
cnf(hyp107,hypothesis,
index_209 = select(queue_208,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
cnf(hyp108,hypothesis,
index_21 = select(q11,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
cnf(hyp109,hypothesis,
index_210 = s(index_209),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
cnf(hyp110,hypothesis,
index_213 = select(q30,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
cnf(hyp111,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
cnf(hyp112,hypothesis,
index_26 = select(queue_25,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
cnf(hyp113,hypothesis,
index_27 = s(index_26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
cnf(hyp114,hypothesis,
index_3 = select(q0,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
cnf(hyp115,hypothesis,
index_30 = select(q12,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
cnf(hyp116,hypothesis,
index_33 = s(index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp116) ).
cnf(hyp117,hypothesis,
index_36 = select(q13,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
cnf(hyp118,hypothesis,
index_39 = s(index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
cnf(hyp119,hypothesis,
index_42 = select(q14,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
cnf(hyp120,hypothesis,
index_45 = s(index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
cnf(hyp121,hypothesis,
index_47 = select(queue_46,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp121) ).
cnf(hyp122,hypothesis,
index_48 = s(index_47),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp122) ).
cnf(hyp123,hypothesis,
index_51 = select(q15,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp123) ).
cnf(hyp124,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp124) ).
cnf(hyp125,hypothesis,
index_57 = select(q16,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp125) ).
cnf(hyp126,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp126) ).
cnf(hyp127,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp127) ).
cnf(hyp128,hypothesis,
index_63 = select(q17,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp128) ).
cnf(hyp129,hypothesis,
index_66 = s(index_63),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp129) ).
cnf(hyp130,hypothesis,
index_68 = select(queue_67,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp130) ).
cnf(hyp131,hypothesis,
index_69 = s(index_68),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp131) ).
cnf(hyp132,hypothesis,
index_72 = select(q18,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp132) ).
cnf(hyp133,hypothesis,
index_75 = s(index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
cnf(hyp134,hypothesis,
index_78 = select(q1,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
cnf(hyp135,hypothesis,
index_81 = s(index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp135) ).
cnf(hyp136,hypothesis,
index_84 = select(q19,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp136) ).
cnf(hyp137,hypothesis,
index_87 = s(index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp137) ).
cnf(hyp138,hypothesis,
index_9 = select(q9,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
cnf(hyp139,hypothesis,
index_90 = select(q20,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
cnf(hyp140,hypothesis,
index_93 = s(index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
cnf(hyp141,hypothesis,
index_95 = select(queue_94,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
cnf(hyp142,hypothesis,
index_96 = s(index_95),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
cnf(hyp143,hypothesis,
index_99 = select(q21,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp143) ).
cnf(hyp144,hypothesis,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp144) ).
cnf(hyp145,hypothesis,
queue_101 = store(q21,seq,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp145) ).
cnf(hyp146,hypothesis,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp146) ).
cnf(hyp147,hypothesis,
queue_107 = store(q22,seq,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
cnf(hyp148,hypothesis,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp148) ).
cnf(hyp149,hypothesis,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
cnf(hyp150,hypothesis,
queue_113 = store(q23,seq,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp150) ).
cnf(hyp151,hypothesis,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
cnf(hyp152,hypothesis,
queue_118 = store(queue_115,head,index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
cnf(hyp153,hypothesis,
queue_122 = store(q24,seq,earray_121),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
cnf(hyp154,hypothesis,
queue_124 = store(queue_122,tail,index_123),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp154) ).
cnf(hyp155,hypothesis,
queue_128 = store(q25,seq,earray_127),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
cnf(hyp156,hypothesis,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp156) ).
cnf(hyp157,hypothesis,
queue_130 = store(queue_128,tail,index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
cnf(hyp158,hypothesis,
queue_134 = store(q26,seq,earray_133),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp158) ).
cnf(hyp159,hypothesis,
queue_136 = store(queue_134,tail,index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
cnf(hyp160,hypothesis,
queue_139 = store(queue_136,head,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
cnf(hyp161,hypothesis,
queue_143 = store(q27,seq,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
cnf(hyp162,hypothesis,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp162) ).
cnf(hyp163,hypothesis,
queue_149 = store(q28,seq,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
cnf(hyp164,hypothesis,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
cnf(hyp165,hypothesis,
queue_155 = store(q2,seq,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
cnf(hyp166,hypothesis,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
cnf(hyp167,hypothesis,
queue_160 = store(queue_157,head,index_159),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp167) ).
cnf(hyp168,hypothesis,
queue_164 = store(q29,seq,earray_163),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
cnf(hyp169,hypothesis,
queue_166 = store(queue_164,tail,index_165),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
cnf(hyp170,hypothesis,
queue_169 = store(queue_166,head,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
cnf(hyp171,hypothesis,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
cnf(hyp172,hypothesis,
queue_173 = store(q3,seq,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
cnf(hyp173,hypothesis,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
cnf(hyp174,hypothesis,
queue_179 = store(q4,seq,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp174) ).
cnf(hyp175,hypothesis,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
cnf(hyp176,hypothesis,
queue_185 = store(q5,seq,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp176) ).
cnf(hyp177,hypothesis,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
cnf(hyp178,hypothesis,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp178) ).
cnf(hyp179,hypothesis,
queue_190 = store(queue_187,head,index_189),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp179) ).
cnf(hyp180,hypothesis,
queue_194 = store(q6,seq,earray_193),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
cnf(hyp181,hypothesis,
queue_196 = store(queue_194,tail,index_195),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp181) ).
cnf(hyp182,hypothesis,
queue_200 = store(q7,seq,earray_199),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp182) ).
cnf(hyp183,hypothesis,
queue_202 = store(queue_200,tail,index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp183) ).
cnf(hyp184,hypothesis,
queue_206 = store(q8,seq,earray_205),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp184) ).
cnf(hyp185,hypothesis,
queue_208 = store(queue_206,tail,index_207),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
cnf(hyp186,hypothesis,
queue_211 = store(queue_208,head,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
cnf(hyp187,hypothesis,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
cnf(hyp188,hypothesis,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
cnf(hyp189,hypothesis,
queue_28 = store(queue_25,head,index_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp189) ).
cnf(hyp190,hypothesis,
queue_32 = store(q12,seq,earray_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp190) ).
cnf(hyp191,hypothesis,
queue_34 = store(queue_32,tail,index_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
cnf(hyp192,hypothesis,
queue_38 = store(q13,seq,earray_37),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
cnf(hyp193,hypothesis,
queue_40 = store(queue_38,tail,index_39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
cnf(hyp194,hypothesis,
queue_44 = store(q14,seq,earray_43),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
cnf(hyp195,hypothesis,
queue_46 = store(queue_44,tail,index_45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
cnf(hyp196,hypothesis,
queue_49 = store(queue_46,head,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
cnf(hyp197,hypothesis,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
cnf(hyp198,hypothesis,
queue_53 = store(q15,seq,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
cnf(hyp199,hypothesis,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
cnf(hyp200,hypothesis,
queue_59 = store(q16,seq,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
cnf(hyp201,hypothesis,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
cnf(hyp202,hypothesis,
queue_65 = store(q17,seq,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
cnf(hyp203,hypothesis,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
cnf(hyp204,hypothesis,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
cnf(hyp205,hypothesis,
queue_70 = store(queue_67,head,index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
cnf(hyp206,hypothesis,
queue_74 = store(q18,seq,earray_73),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
cnf(hyp207,hypothesis,
queue_76 = store(queue_74,tail,index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
cnf(hyp208,hypothesis,
queue_80 = store(q1,seq,earray_79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
cnf(hyp209,hypothesis,
queue_82 = store(queue_80,tail,index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
cnf(hyp210,hypothesis,
queue_86 = store(q19,seq,earray_85),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
cnf(hyp211,hypothesis,
queue_88 = store(queue_86,tail,index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
cnf(hyp212,hypothesis,
queue_92 = store(q20,seq,earray_91),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
cnf(hyp213,hypothesis,
queue_94 = store(queue_92,tail,index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
cnf(hyp214,hypothesis,
queue_97 = store(queue_94,head,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
cnf(hyp215,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
cnf(hyp216,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
cnf(hyp217,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
cnf(hyp218,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
cnf(hyp219,hypothesis,
q12 = queue_28,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
cnf(hyp220,hypothesis,
q13 = queue_34,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
cnf(hyp221,hypothesis,
q14 = queue_40,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
cnf(hyp222,hypothesis,
q15 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
cnf(hyp223,hypothesis,
q16 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
cnf(hyp224,hypothesis,
q17 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
cnf(hyp225,hypothesis,
q18 = queue_70,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
cnf(hyp226,hypothesis,
q19 = queue_76,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
cnf(hyp227,hypothesis,
q2 = queue_82,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
cnf(hyp228,hypothesis,
q20 = queue_88,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
cnf(hyp229,hypothesis,
q21 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
cnf(hyp230,hypothesis,
q22 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
cnf(hyp231,hypothesis,
q23 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
cnf(hyp232,hypothesis,
q24 = queue_118,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
cnf(hyp233,hypothesis,
q25 = queue_124,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
cnf(hyp234,hypothesis,
q26 = queue_130,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
cnf(hyp235,hypothesis,
q27 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
cnf(hyp236,hypothesis,
q28 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
cnf(hyp237,hypothesis,
q29 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
cnf(hyp238,hypothesis,
q3 = queue_160,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
cnf(hyp239,hypothesis,
q30 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
cnf(hyp240,hypothesis,
q4 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
cnf(hyp241,hypothesis,
q5 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
cnf(hyp242,hypothesis,
q6 = queue_190,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
cnf(hyp243,hypothesis,
q7 = queue_196,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
cnf(hyp244,hypothesis,
q8 = queue_202,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
cnf(hyp245,hypothesis,
q9 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
cnf(goal,negated_conjecture,
elem_214 != e10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
cnf(303,plain,
q9 = store(queue_208,head,index_210),
inference('REWRITE',[status(thm)],[hyp186,hyp245,theory(equality)]) ).
cnf(304,plain,
q8 = store(queue_200,tail,index_201),
inference('REWRITE',[status(thm)],[hyp183,hyp244,theory(equality)]) ).
cnf(305,plain,
q7 = store(queue_194,tail,index_195),
inference('REWRITE',[status(thm)],[hyp181,hyp243,theory(equality)]) ).
cnf(306,plain,
q6 = store(queue_187,head,index_189),
inference('REWRITE',[status(thm)],[hyp179,hyp242,theory(equality)]) ).
cnf(307,plain,
q5 = store(queue_179,tail,index_180),
inference('REWRITE',[status(thm)],[hyp175,hyp241,theory(equality)]) ).
cnf(308,plain,
q4 = store(queue_173,tail,index_174),
inference('REWRITE',[status(thm)],[hyp173,hyp240,theory(equality)]) ).
cnf(309,plain,
q30 = store(queue_166,head,index_168),
inference('REWRITE',[status(thm)],[hyp170,hyp239,theory(equality)]) ).
cnf(310,plain,
q3 = store(queue_157,head,index_159),
inference('REWRITE',[status(thm)],[hyp167,hyp238,theory(equality)]) ).
cnf(311,plain,
q29 = store(queue_149,tail,index_150),
inference('REWRITE',[status(thm)],[hyp164,hyp237,theory(equality)]) ).
cnf(312,plain,
q28 = store(queue_143,tail,index_144),
inference('REWRITE',[status(thm)],[hyp162,hyp236,theory(equality)]) ).
cnf(313,plain,
q27 = store(queue_136,head,index_138),
inference('REWRITE',[status(thm)],[hyp160,hyp235,theory(equality)]) ).
cnf(314,plain,
q26 = store(queue_128,tail,index_129),
inference('REWRITE',[status(thm)],[hyp157,hyp234,theory(equality)]) ).
cnf(315,plain,
q25 = store(queue_122,tail,index_123),
inference('REWRITE',[status(thm)],[hyp154,hyp233,theory(equality)]) ).
cnf(316,plain,
q24 = store(queue_115,head,index_117),
inference('REWRITE',[status(thm)],[hyp152,hyp232,theory(equality)]) ).
cnf(317,plain,
q23 = store(queue_107,tail,index_108),
inference('REWRITE',[status(thm)],[hyp148,hyp231,theory(equality)]) ).
cnf(318,plain,
q22 = store(queue_101,tail,index_102),
inference('REWRITE',[status(thm)],[hyp146,hyp230,theory(equality)]) ).
cnf(319,plain,
q21 = store(queue_94,head,index_96),
inference('REWRITE',[status(thm)],[hyp214,hyp229,theory(equality)]) ).
cnf(320,plain,
q20 = store(queue_86,tail,index_87),
inference('REWRITE',[status(thm)],[hyp211,hyp228,theory(equality)]) ).
cnf(321,plain,
q2 = store(queue_80,tail,index_81),
inference('REWRITE',[status(thm)],[hyp209,hyp227,theory(equality)]) ).
cnf(322,plain,
q19 = store(queue_74,tail,index_75),
inference('REWRITE',[status(thm)],[hyp207,hyp226,theory(equality)]) ).
cnf(323,plain,
q18 = store(queue_67,head,index_69),
inference('REWRITE',[status(thm)],[hyp205,hyp225,theory(equality)]) ).
cnf(324,plain,
q17 = store(queue_59,tail,index_60),
inference('REWRITE',[status(thm)],[hyp201,hyp224,theory(equality)]) ).
cnf(325,plain,
q16 = store(queue_53,tail,index_54),
inference('REWRITE',[status(thm)],[hyp199,hyp223,theory(equality)]) ).
cnf(326,plain,
q15 = store(queue_46,head,index_48),
inference('REWRITE',[status(thm)],[hyp196,hyp222,theory(equality)]) ).
cnf(327,plain,
q14 = store(queue_38,tail,index_39),
inference('REWRITE',[status(thm)],[hyp193,hyp221,theory(equality)]) ).
cnf(328,plain,
q13 = store(queue_32,tail,index_33),
inference('REWRITE',[status(thm)],[hyp191,hyp220,theory(equality)]) ).
cnf(329,plain,
q12 = store(queue_25,head,index_27),
inference('REWRITE',[status(thm)],[hyp189,hyp219,theory(equality)]) ).
cnf(330,plain,
q11 = store(queue_17,tail,index_18),
inference('REWRITE',[status(thm)],[hyp178,hyp218,theory(equality)]) ).
cnf(331,plain,
q10 = store(queue_11,tail,index_12),
inference('REWRITE',[status(thm)],[hyp156,hyp217,theory(equality)]) ).
cnf(332,plain,
q1 = store(queue_5,tail,index_6),
inference('REWRITE',[status(thm)],[hyp204,hyp216,theory(equality)]) ).
cnf(333,plain,
q0 = store(q,head,index_0),
inference('REWRITE',[status(thm)],[hyp144,hyp215,theory(equality)]) ).
cnf(350,plain,
index_18 != index_15,
inference('PARAMODULATE',[status(thm)],[as1,hyp95,theory(equality)]) ).
cnf(403,plain,
s(index_18) != index_15,
inference('PARAMODULATE',[status(thm)],[as2,hyp95,theory(equality)]) ).
cnf(443,plain,
s(s(index_18)) != index_15,
inference('PARAMODULATE',[status(thm)],[as3,hyp95,theory(equality)]) ).
cnf(454,plain,
select(q21,head) = index_96,
inference('PARAMODULATE',[status(thm)],[a1,319,theory(equality)]) ).
cnf(455,plain,
select(queue_94,tail) = index_93,
inference('PARAMODULATE',[status(thm)],[a1,hyp213,theory(equality)]) ).
cnf(456,plain,
index_90 = index_87,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,320,theory(equality)]),hyp139,theory(equality)]) ).
cnf(457,plain,
earray_91 = store(earray_89,index_87,e20),
inference('REWRITE',[status(thm)],[hyp59,456,theory(equality)]) ).
cnf(459,plain,
index_93 = s(index_87),
inference('REWRITE',[status(thm)],[hyp140,456,theory(equality)]) ).
cnf(465,plain,
index_153 = index_81,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,321,theory(equality)]),hyp84,theory(equality)]) ).
cnf(466,plain,
index_153 = s(index_78),
inference('REWRITE',[status(thm)],[hyp135,465,theory(equality)]) ).
cnf(467,plain,
q2 = store(queue_80,tail,index_153),
inference('REWRITE',[status(thm)],[321,465,theory(equality)]) ).
cnf(471,plain,
index_84 = index_75,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,322,theory(equality)]),hyp136,theory(equality)]) ).
cnf(472,plain,
earray_85 = store(earray_83,index_75,e19),
inference('REWRITE',[status(thm)],[hyp57,471,theory(equality)]) ).
cnf(474,plain,
index_87 = s(index_75),
inference('REWRITE',[status(thm)],[hyp137,471,theory(equality)]) ).
cnf(480,plain,
select(q18,head) = index_69,
inference('PARAMODULATE',[status(thm)],[a1,323,theory(equality)]) ).
cnf(481,plain,
select(queue_67,tail) = index_66,
inference('PARAMODULATE',[status(thm)],[a1,hyp203,theory(equality)]) ).
cnf(482,plain,
index_63 = index_60,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,324,theory(equality)]),hyp128,theory(equality)]) ).
cnf(483,plain,
earray_64 = store(earray_62,index_60,e17),
inference('REWRITE',[status(thm)],[hyp50,482,theory(equality)]) ).
cnf(485,plain,
index_66 = s(index_60),
inference('REWRITE',[status(thm)],[hyp129,482,theory(equality)]) ).
cnf(491,plain,
index_78 = index_6,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,332,theory(equality)]),hyp134,theory(equality)]) ).
cnf(494,plain,
index_153 = s(index_6),
inference('REWRITE',[status(thm)],[466,491,theory(equality)]) ).
cnf(500,plain,
index_57 = index_54,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,325,theory(equality)]),hyp125,theory(equality)]) ).
cnf(501,plain,
earray_58 = store(earray_56,index_54,e16),
inference('REWRITE',[status(thm)],[hyp48,500,theory(equality)]) ).
cnf(503,plain,
index_60 = s(index_54),
inference('REWRITE',[status(thm)],[hyp127,500,theory(equality)]) ).
cnf(509,plain,
select(q15,head) = index_48,
inference('PARAMODULATE',[status(thm)],[a1,326,theory(equality)]) ).
cnf(510,plain,
select(queue_46,tail) = index_45,
inference('PARAMODULATE',[status(thm)],[a1,hyp195,theory(equality)]) ).
cnf(511,plain,
index_42 = index_39,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,327,theory(equality)]),hyp119,theory(equality)]) ).
cnf(512,plain,
earray_43 = store(earray_41,index_39,e14),
inference('REWRITE',[status(thm)],[hyp44,511,theory(equality)]) ).
cnf(514,plain,
index_45 = s(index_39),
inference('REWRITE',[status(thm)],[hyp120,511,theory(equality)]) ).
cnf(520,plain,
index_36 = index_33,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,328,theory(equality)]),hyp117,theory(equality)]) ).
cnf(521,plain,
earray_37 = store(earray_35,index_33,e13),
inference('REWRITE',[status(thm)],[hyp41,520,theory(equality)]) ).
cnf(523,plain,
index_39 = s(index_33),
inference('REWRITE',[status(thm)],[hyp118,520,theory(equality)]) ).
cnf(529,plain,
select(q12,head) = index_27,
inference('PARAMODULATE',[status(thm)],[a1,329,theory(equality)]) ).
cnf(530,plain,
select(queue_25,tail) = index_24,
inference('PARAMODULATE',[status(thm)],[a1,hyp188,theory(equality)]) ).
cnf(531,plain,
select(q9,head) = index_210,
inference('PARAMODULATE',[status(thm)],[a1,303,theory(equality)]) ).
cnf(532,plain,
select(queue_208,tail) = index_207,
inference('PARAMODULATE',[status(thm)],[a1,hyp185,theory(equality)]) ).
cnf(533,plain,
index_204 = index_201,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,304,theory(equality)]),hyp105,theory(equality)]) ).
cnf(536,plain,
index_207 = s(index_201),
inference('REWRITE',[status(thm)],[hyp106,533,theory(equality)]) ).
cnf(542,plain,
index_198 = index_195,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,305,theory(equality)]),hyp103,theory(equality)]) ).
cnf(545,plain,
index_201 = s(index_195),
inference('REWRITE',[status(thm)],[hyp104,542,theory(equality)]) ).
cnf(551,plain,
select(q6,head) = index_189,
inference('PARAMODULATE',[status(thm)],[a1,306,theory(equality)]) ).
cnf(552,plain,
select(queue_187,tail) = index_186,
inference('PARAMODULATE',[status(thm)],[a1,hyp177,theory(equality)]) ).
cnf(553,plain,
index_183 = index_180,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,307,theory(equality)]),hyp97,theory(equality)]) ).
cnf(556,plain,
index_186 = s(index_180),
inference('REWRITE',[status(thm)],[hyp98,553,theory(equality)]) ).
cnf(562,plain,
index_21 = index_18,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,330,theory(equality)]),hyp108,theory(equality)]) ).
cnf(563,plain,
earray_22 = store(earray_20,index_18,e11),
inference('REWRITE',[status(thm)],[hyp37,562,theory(equality)]) ).
cnf(565,plain,
index_24 = s(index_18),
inference('REWRITE',[status(thm)],[hyp111,562,theory(equality)]) ).
cnf(566,plain,
index_24 != index_15,
inference('REWRITE',[status(thm)],[403,565,theory(equality)]) ).
cnf(567,plain,
s(index_24) != index_15,
inference('REWRITE',[status(thm)],[443,565,theory(equality)]) ).
cnf(571,plain,
index_177 = index_174,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,308,theory(equality)]),hyp94,theory(equality)]) ).
cnf(574,plain,
index_180 = s(index_174),
inference('REWRITE',[status(thm)],[hyp96,571,theory(equality)]) ).
cnf(580,plain,
index_213 = index_168,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,309,theory(equality)]),hyp110,theory(equality)]) ).
cnf(581,plain,
elem_214 = select(earray_212,index_168),
inference('REWRITE',[status(thm)],[hyp61,580,theory(equality)]) ).
cnf(584,plain,
select(q3,head) = index_159,
inference('PARAMODULATE',[status(thm)],[a1,310,theory(equality)]) ).
cnf(585,plain,
select(queue_157,tail) = index_156,
inference('PARAMODULATE',[status(thm)],[a1,hyp166,theory(equality)]) ).
cnf(586,plain,
index_162 = index_150,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,311,theory(equality)]),hyp88,theory(equality)]) ).
cnf(587,plain,
earray_163 = store(earray_161,index_150,e29),
inference('REWRITE',[status(thm)],[hyp21,586,theory(equality)]) ).
cnf(595,plain,
index_147 = index_144,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,312,theory(equality)]),hyp81,theory(equality)]) ).
cnf(596,plain,
earray_148 = store(earray_146,index_144,e28),
inference('REWRITE',[status(thm)],[hyp16,595,theory(equality)]) ).
cnf(598,plain,
index_150 = s(index_144),
inference('REWRITE',[status(thm)],[hyp83,595,theory(equality)]) ).
cnf(604,plain,
select(q27,head) = index_138,
inference('PARAMODULATE',[status(thm)],[a1,313,theory(equality)]) ).
cnf(605,plain,
select(queue_136,tail) = index_135,
inference('PARAMODULATE',[status(thm)],[a1,hyp159,theory(equality)]) ).
cnf(606,plain,
index_132 = index_129,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,314,theory(equality)]),hyp75,theory(equality)]) ).
cnf(607,plain,
earray_133 = store(earray_131,index_129,e26),
inference('REWRITE',[status(thm)],[hyp11,606,theory(equality)]) ).
cnf(609,plain,
index_135 = s(index_129),
inference('REWRITE',[status(thm)],[hyp76,606,theory(equality)]) ).
cnf(615,plain,
index_126 = index_123,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,315,theory(equality)]),hyp73,theory(equality)]) ).
cnf(616,plain,
earray_127 = store(earray_125,index_123,e25),
inference('REWRITE',[status(thm)],[hyp9,615,theory(equality)]) ).
cnf(618,plain,
index_129 = s(index_123),
inference('REWRITE',[status(thm)],[hyp74,615,theory(equality)]) ).
cnf(624,plain,
index_15 = index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,331,theory(equality)]),hyp82,theory(equality)]) ).
cnf(625,plain,
earray_16 = store(earray_14,index_12,e10),
inference('REWRITE',[status(thm)],[hyp19,624,theory(equality)]) ).
cnf(627,plain,
index_18 = s(index_12),
inference('REWRITE',[status(thm)],[hyp95,624,theory(equality)]) ).
cnf(630,plain,
index_18 != index_12,
inference('REWRITE',[status(thm)],[350,624,theory(equality)]) ).
cnf(631,plain,
index_24 != index_12,
inference('REWRITE',[status(thm)],[566,624,theory(equality)]) ).
cnf(632,plain,
s(index_24) != index_12,
inference('REWRITE',[status(thm)],[567,624,theory(equality)]) ).
cnf(633,plain,
select(q24,head) = index_117,
inference('PARAMODULATE',[status(thm)],[a1,316,theory(equality)]) ).
cnf(634,plain,
select(queue_115,tail) = index_114,
inference('PARAMODULATE',[status(thm)],[a1,hyp151,theory(equality)]) ).
cnf(635,plain,
index_111 = index_108,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,317,theory(equality)]),hyp66,theory(equality)]) ).
cnf(636,plain,
earray_112 = store(earray_110,index_108,e23),
inference('REWRITE',[status(thm)],[hyp5,635,theory(equality)]) ).
cnf(638,plain,
index_114 = s(index_108),
inference('REWRITE',[status(thm)],[hyp67,635,theory(equality)]) ).
cnf(644,plain,
index_105 = index_102,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[a1,318,theory(equality)]),hyp64,theory(equality)]) ).
cnf(645,plain,
earray_106 = store(earray_104,index_102,e22),
inference('REWRITE',[status(thm)],[hyp3,644,theory(equality)]) ).
cnf(647,plain,
index_108 = s(index_102),
inference('REWRITE',[status(thm)],[hyp65,644,theory(equality)]) ).
cnf(653,plain,
select(q0,head) = index_0,
inference('PARAMODULATE',[status(thm)],[a1,333,theory(equality)]) ).
cnf(654,plain,
select(queue_92,seq) = earray_91,
inference('PARAMODULATE',[status(thm)],[a1,hyp212,theory(equality)]) ).
cnf(655,plain,
select(queue_86,seq) = earray_85,
inference('PARAMODULATE',[status(thm)],[a1,hyp210,theory(equality)]) ).
cnf(658,plain,
select(queue_74,seq) = earray_73,
inference('PARAMODULATE',[status(thm)],[a1,hyp206,theory(equality)]) ).
cnf(659,plain,
select(queue_65,seq) = earray_64,
inference('PARAMODULATE',[status(thm)],[a1,hyp202,theory(equality)]) ).
cnf(660,plain,
select(queue_59,seq) = earray_58,
inference('PARAMODULATE',[status(thm)],[a1,hyp200,theory(equality)]) ).
cnf(662,plain,
select(queue_53,seq) = earray_52,
inference('PARAMODULATE',[status(thm)],[a1,hyp198,theory(equality)]) ).
cnf(663,plain,
select(queue_44,seq) = earray_43,
inference('PARAMODULATE',[status(thm)],[a1,hyp194,theory(equality)]) ).
cnf(666,plain,
select(queue_38,seq) = earray_37,
inference('PARAMODULATE',[status(thm)],[a1,hyp192,theory(equality)]) ).
cnf(668,plain,
select(queue_32,seq) = earray_31,
inference('PARAMODULATE',[status(thm)],[a1,hyp190,theory(equality)]) ).
cnf(669,plain,
select(queue_23,seq) = earray_22,
inference('PARAMODULATE',[status(thm)],[a1,hyp187,theory(equality)]) ).
cnf(678,plain,
select(queue_164,seq) = earray_163,
inference('PARAMODULATE',[status(thm)],[a1,hyp168,theory(equality)]) ).
cnf(679,plain,
select(queue_17,seq) = earray_16,
inference('PARAMODULATE',[status(thm)],[a1,hyp171,theory(equality)]) ).
cnf(682,plain,
select(queue_149,seq) = earray_148,
inference('PARAMODULATE',[status(thm)],[a1,hyp163,theory(equality)]) ).
cnf(684,plain,
select(queue_143,seq) = earray_142,
inference('PARAMODULATE',[status(thm)],[a1,hyp161,theory(equality)]) ).
cnf(685,plain,
select(queue_134,seq) = earray_133,
inference('PARAMODULATE',[status(thm)],[a1,hyp158,theory(equality)]) ).
cnf(686,plain,
select(queue_128,seq) = earray_127,
inference('PARAMODULATE',[status(thm)],[a1,hyp155,theory(equality)]) ).
cnf(688,plain,
select(queue_122,seq) = earray_121,
inference('PARAMODULATE',[status(thm)],[a1,hyp153,theory(equality)]) ).
cnf(689,plain,
select(queue_113,seq) = earray_112,
inference('PARAMODULATE',[status(thm)],[a1,hyp150,theory(equality)]) ).
cnf(690,plain,
select(queue_107,seq) = earray_106,
inference('PARAMODULATE',[status(thm)],[a1,hyp147,theory(equality)]) ).
cnf(692,plain,
select(queue_101,seq) = earray_100,
inference('PARAMODULATE',[status(thm)],[a1,hyp145,theory(equality)]) ).
cnf(711,plain,
select(earray_16,index_12) = e10,
inference('PARAMODULATE',[status(thm)],[a1,625,theory(equality)]) ).
cnf(739,plain,
s(s(index_24)) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as4,627,theory(equality)]),565,theory(equality)]) ).
cnf(779,plain,
s(s(s(index_24))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as5,627,theory(equality)]),565,theory(equality)]) ).
cnf(819,plain,
s(s(s(s(index_24)))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as6,627,theory(equality)]),565,theory(equality)]) ).
cnf(836,plain,
select(store(X,head,Y),seq) = select(X,seq),
inference('UR-RESOLVE',[status(thm)],[a2,head_distinct_from_seq]) ).
cnf(837,plain,
select(store(X,seq,Y),head) = select(X,head),
inference('UR-RESOLVE',[status(thm)],[a2,head_distinct_from_seq]) ).
cnf(838,plain,
select(store(X,tail,Y),seq) = select(X,seq),
inference('UR-RESOLVE',[status(thm)],[a2,tail_distinct_from_seq]) ).
cnf(840,plain,
select(store(X,head,Y),tail) = select(X,tail),
inference('UR-RESOLVE',[status(thm)],[a2,head_distinct_from_tail]) ).
cnf(841,plain,
select(store(X,tail,Y),head) = select(X,head),
inference('UR-RESOLVE',[status(thm)],[a2,head_distinct_from_tail]) ).
cnf(882,plain,
( index_87 = X
| select(earray_91,X) = select(earray_89,X) ),
inference('PARAMODULATE',[status(thm)],[a2,457,theory(equality)]) ).
cnf(884,plain,
( index_75 = X
| select(earray_85,X) = select(earray_83,X) ),
inference('PARAMODULATE',[status(thm)],[a2,472,theory(equality)]) ).
cnf(888,plain,
( index_72 = X
| select(earray_73,X) = select(earray_71,X) ),
inference('PARAMODULATE',[status(thm)],[a2,hyp52,theory(equality)]) ).
cnf(890,plain,
( index_60 = X
| select(earray_64,X) = select(earray_62,X) ),
inference('PARAMODULATE',[status(thm)],[a2,483,theory(equality)]) ).
cnf(892,plain,
( index_54 = X
| select(earray_58,X) = select(earray_56,X) ),
inference('PARAMODULATE',[status(thm)],[a2,501,theory(equality)]) ).
cnf(894,plain,
( index_51 = X
| select(earray_52,X) = select(earray_50,X) ),
inference('PARAMODULATE',[status(thm)],[a2,hyp46,theory(equality)]) ).
cnf(896,plain,
( index_39 = X
| select(earray_43,X) = select(earray_41,X) ),
inference('PARAMODULATE',[status(thm)],[a2,512,theory(equality)]) ).
cnf(900,plain,
( index_33 = X
| select(earray_37,X) = select(earray_35,X) ),
inference('PARAMODULATE',[status(thm)],[a2,521,theory(equality)]) ).
cnf(902,plain,
( index_30 = X
| select(earray_31,X) = select(earray_29,X) ),
inference('PARAMODULATE',[status(thm)],[a2,hyp39,theory(equality)]) ).
cnf(904,plain,
( index_18 = X
| select(earray_22,X) = select(earray_20,X) ),
inference('PARAMODULATE',[status(thm)],[a2,563,theory(equality)]) ).
cnf(918,plain,
( index_150 = X
| select(earray_163,X) = select(earray_161,X) ),
inference('PARAMODULATE',[status(thm)],[a2,587,theory(equality)]) ).
cnf(925,plain,
( index_144 = X
| select(earray_148,X) = select(earray_146,X) ),
inference('PARAMODULATE',[status(thm)],[a2,596,theory(equality)]) ).
cnf(927,plain,
( index_141 = X
| select(earray_142,X) = select(earray_140,X) ),
inference('PARAMODULATE',[status(thm)],[a2,hyp14,theory(equality)]) ).
cnf(929,plain,
( index_129 = X
| select(earray_133,X) = select(earray_131,X) ),
inference('PARAMODULATE',[status(thm)],[a2,607,theory(equality)]) ).
cnf(931,plain,
( index_123 = X
| select(earray_127,X) = select(earray_125,X) ),
inference('PARAMODULATE',[status(thm)],[a2,616,theory(equality)]) ).
cnf(933,plain,
( index_120 = X
| select(earray_121,X) = select(earray_119,X) ),
inference('PARAMODULATE',[status(thm)],[a2,hyp7,theory(equality)]) ).
cnf(935,plain,
( index_108 = X
| select(earray_112,X) = select(earray_110,X) ),
inference('PARAMODULATE',[status(thm)],[a2,636,theory(equality)]) ).
cnf(937,plain,
( index_102 = X
| select(earray_106,X) = select(earray_104,X) ),
inference('PARAMODULATE',[status(thm)],[a2,645,theory(equality)]) ).
cnf(939,plain,
( index_99 = X
| select(earray_100,X) = select(earray_98,X) ),
inference('PARAMODULATE',[status(thm)],[a2,hyp1,theory(equality)]) ).
cnf(980,plain,
s(s(s(s(s(index_24))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as7,627,theory(equality)]),565,theory(equality)]) ).
cnf(1022,plain,
s(s(s(s(s(s(index_24)))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as8,627,theory(equality)]),565,theory(equality)]) ).
cnf(1064,plain,
s(s(s(s(s(s(s(index_24))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as9,627,theory(equality)]),565,theory(equality)]) ).
cnf(1106,plain,
s(s(s(s(s(s(s(s(index_24)))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as10,627,theory(equality)]),565,theory(equality)]) ).
cnf(1148,plain,
s(s(s(s(s(s(s(s(s(index_24))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as11,627,theory(equality)]),565,theory(equality)]) ).
cnf(1190,plain,
s(s(s(s(s(s(s(s(s(s(index_24)))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as12,627,theory(equality)]),565,theory(equality)]) ).
cnf(1232,plain,
s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as13,627,theory(equality)]),565,theory(equality)]) ).
cnf(1274,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as14,627,theory(equality)]),565,theory(equality)]) ).
cnf(1316,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as15,627,theory(equality)]),565,theory(equality)]) ).
cnf(1358,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as16,627,theory(equality)]),565,theory(equality)]) ).
cnf(1400,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as17,627,theory(equality)]),565,theory(equality)]) ).
cnf(1442,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as18,627,theory(equality)]),565,theory(equality)]) ).
cnf(1484,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))) != index_12,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[as19,627,theory(equality)]),565,theory(equality)]) ).
cnf(3265,plain,
earray_212 = select(queue_166,seq),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[836,309,theory(equality)]),hyp36,theory(equality)]) ).
cnf(3267,plain,
earray_140 = select(queue_136,seq),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[836,313,theory(equality)]),hyp13,theory(equality)]) ).
cnf(3268,plain,
earray_119 = select(queue_115,seq),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[836,316,theory(equality)]),hyp6,theory(equality)]) ).
cnf(3269,plain,
earray_98 = select(queue_94,seq),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[836,319,theory(equality)]),hyp60,theory(equality)]) ).
cnf(3270,plain,
earray_71 = select(queue_67,seq),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[836,323,theory(equality)]),hyp51,theory(equality)]) ).
cnf(3271,plain,
earray_50 = select(queue_46,seq),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[836,326,theory(equality)]),hyp45,theory(equality)]) ).
cnf(3272,plain,
earray_29 = select(queue_25,seq),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[836,329,theory(equality)]),hyp38,theory(equality)]) ).
cnf(3274,plain,
select(queue_101,head) = index_96,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp145,theory(equality)]),454,theory(equality)]) ).
cnf(3275,plain,
select(queue_107,head) = select(q22,head),
inference('PARAMODULATE',[status(thm)],[837,hyp147,theory(equality)]) ).
cnf(3276,plain,
select(queue_11,head) = index_210,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp149,theory(equality)]),531,theory(equality)]) ).
cnf(3277,plain,
select(queue_113,head) = select(q23,head),
inference('PARAMODULATE',[status(thm)],[837,hyp150,theory(equality)]) ).
cnf(3278,plain,
select(queue_122,head) = index_117,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp153,theory(equality)]),633,theory(equality)]) ).
cnf(3279,plain,
select(queue_128,head) = select(q25,head),
inference('PARAMODULATE',[status(thm)],[837,hyp155,theory(equality)]) ).
cnf(3280,plain,
select(queue_134,head) = select(q26,head),
inference('PARAMODULATE',[status(thm)],[837,hyp158,theory(equality)]) ).
cnf(3281,plain,
select(queue_143,head) = index_138,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp161,theory(equality)]),604,theory(equality)]) ).
cnf(3282,plain,
select(queue_149,head) = select(q28,head),
inference('PARAMODULATE',[status(thm)],[837,hyp163,theory(equality)]) ).
cnf(3283,plain,
select(queue_155,head) = select(q2,head),
inference('PARAMODULATE',[status(thm)],[837,hyp165,theory(equality)]) ).
cnf(3284,plain,
select(queue_164,head) = select(q29,head),
inference('PARAMODULATE',[status(thm)],[837,hyp168,theory(equality)]) ).
cnf(3285,plain,
select(queue_17,head) = select(q10,head),
inference('PARAMODULATE',[status(thm)],[837,hyp171,theory(equality)]) ).
cnf(3286,plain,
select(queue_173,head) = index_159,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp172,theory(equality)]),584,theory(equality)]) ).
cnf(3287,plain,
select(queue_179,head) = select(q4,head),
inference('PARAMODULATE',[status(thm)],[837,hyp174,theory(equality)]) ).
cnf(3288,plain,
select(queue_185,head) = select(q5,head),
inference('PARAMODULATE',[status(thm)],[837,hyp176,theory(equality)]) ).
cnf(3289,plain,
select(queue_194,head) = index_189,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp180,theory(equality)]),551,theory(equality)]) ).
cnf(3290,plain,
select(queue_200,head) = select(q7,head),
inference('PARAMODULATE',[status(thm)],[837,hyp182,theory(equality)]) ).
cnf(3291,plain,
select(queue_206,head) = select(q8,head),
inference('PARAMODULATE',[status(thm)],[837,hyp184,theory(equality)]) ).
cnf(3292,plain,
select(queue_23,head) = select(q11,head),
inference('PARAMODULATE',[status(thm)],[837,hyp187,theory(equality)]) ).
cnf(3293,plain,
select(queue_32,head) = index_27,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp190,theory(equality)]),529,theory(equality)]) ).
cnf(3294,plain,
select(queue_38,head) = select(q13,head),
inference('PARAMODULATE',[status(thm)],[837,hyp192,theory(equality)]) ).
cnf(3295,plain,
select(queue_44,head) = select(q14,head),
inference('PARAMODULATE',[status(thm)],[837,hyp194,theory(equality)]) ).
cnf(3296,plain,
select(queue_5,head) = index_0,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp197,theory(equality)]),653,theory(equality)]) ).
cnf(3297,plain,
select(queue_53,head) = index_48,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp198,theory(equality)]),509,theory(equality)]) ).
cnf(3298,plain,
select(queue_59,head) = select(q16,head),
inference('PARAMODULATE',[status(thm)],[837,hyp200,theory(equality)]) ).
cnf(3299,plain,
select(queue_65,head) = select(q17,head),
inference('PARAMODULATE',[status(thm)],[837,hyp202,theory(equality)]) ).
cnf(3300,plain,
select(queue_74,head) = index_69,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[837,hyp206,theory(equality)]),480,theory(equality)]) ).
cnf(3301,plain,
select(queue_80,head) = select(q1,head),
inference('PARAMODULATE',[status(thm)],[837,hyp208,theory(equality)]) ).
cnf(3302,plain,
select(queue_86,head) = select(q19,head),
inference('PARAMODULATE',[status(thm)],[837,hyp210,theory(equality)]) ).
cnf(3303,plain,
select(queue_92,head) = select(q20,head),
inference('PARAMODULATE',[status(thm)],[837,hyp212,theory(equality)]) ).
cnf(3304,plain,
earray_119 = earray_112,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,hyp151,theory(equality)]),689,3268,theory(equality)]) ).
cnf(3307,plain,
( index_120 = X
| select(earray_121,X) = select(earray_112,X) ),
inference('REWRITE',[status(thm)],[933,3304,theory(equality)]) ).
cnf(3309,plain,
earray_140 = earray_133,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,hyp159,theory(equality)]),685,3267,theory(equality)]) ).
cnf(3312,plain,
( index_141 = X
| select(earray_142,X) = select(earray_133,X) ),
inference('REWRITE',[status(thm)],[927,3309,theory(equality)]) ).
cnf(3319,plain,
earray_212 = earray_163,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,hyp169,theory(equality)]),678,3265,theory(equality)]) ).
cnf(3321,plain,
elem_214 = select(earray_163,index_168),
inference('REWRITE',[status(thm)],[581,3319,theory(equality)]) ).
cnf(3333,plain,
earray_29 = earray_22,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,hyp188,theory(equality)]),669,3272,theory(equality)]) ).
cnf(3336,plain,
( index_30 = X
| select(earray_31,X) = select(earray_22,X) ),
inference('REWRITE',[status(thm)],[902,3333,theory(equality)]) ).
cnf(3338,plain,
earray_50 = earray_43,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,hyp195,theory(equality)]),663,3271,theory(equality)]) ).
cnf(3341,plain,
( index_51 = X
| select(earray_52,X) = select(earray_43,X) ),
inference('REWRITE',[status(thm)],[894,3338,theory(equality)]) ).
cnf(3343,plain,
earray_71 = earray_64,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,hyp203,theory(equality)]),659,3270,theory(equality)]) ).
cnf(3346,plain,
( index_72 = X
| select(earray_73,X) = select(earray_64,X) ),
inference('REWRITE',[status(thm)],[888,3343,theory(equality)]) ).
cnf(3348,plain,
earray_98 = earray_91,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,hyp213,theory(equality)]),654,3269,theory(equality)]) ).
cnf(3351,plain,
( index_99 = X
| select(earray_100,X) = select(earray_91,X) ),
inference('REWRITE',[status(thm)],[939,3348,theory(equality)]) ).
cnf(3369,plain,
earray_161 = earray_148,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,311,theory(equality)]),682,hyp20,theory(equality)]) ).
cnf(3372,plain,
( index_150 = X
| select(earray_163,X) = select(earray_148,X) ),
inference('REWRITE',[status(thm)],[918,3369,theory(equality)]) ).
cnf(3373,plain,
earray_146 = earray_142,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,312,theory(equality)]),684,hyp15,theory(equality)]) ).
cnf(3376,plain,
( index_144 = X
| select(earray_148,X) = select(earray_142,X) ),
inference('REWRITE',[status(thm)],[925,3373,theory(equality)]) ).
cnf(3377,plain,
earray_131 = earray_127,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,314,theory(equality)]),686,hyp10,theory(equality)]) ).
cnf(3380,plain,
( index_129 = X
| select(earray_133,X) = select(earray_127,X) ),
inference('REWRITE',[status(thm)],[929,3377,theory(equality)]) ).
cnf(3381,plain,
earray_125 = earray_121,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,315,theory(equality)]),688,hyp8,theory(equality)]) ).
cnf(3384,plain,
( index_123 = X
| select(earray_127,X) = select(earray_121,X) ),
inference('REWRITE',[status(thm)],[931,3381,theory(equality)]) ).
cnf(3385,plain,
earray_110 = earray_106,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,317,theory(equality)]),690,hyp4,theory(equality)]) ).
cnf(3388,plain,
( index_108 = X
| select(earray_112,X) = select(earray_106,X) ),
inference('REWRITE',[status(thm)],[935,3385,theory(equality)]) ).
cnf(3389,plain,
earray_104 = earray_100,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,318,theory(equality)]),692,hyp2,theory(equality)]) ).
cnf(3392,plain,
( index_102 = X
| select(earray_106,X) = select(earray_100,X) ),
inference('REWRITE',[status(thm)],[937,3389,theory(equality)]) ).
cnf(3393,plain,
earray_89 = earray_85,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,320,theory(equality)]),655,hyp58,theory(equality)]) ).
cnf(3396,plain,
( index_87 = X
| select(earray_91,X) = select(earray_85,X) ),
inference('REWRITE',[status(thm)],[882,3393,theory(equality)]) ).
cnf(3397,plain,
earray_83 = earray_73,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,322,theory(equality)]),658,hyp56,theory(equality)]) ).
cnf(3400,plain,
( index_75 = X
| select(earray_85,X) = select(earray_73,X) ),
inference('REWRITE',[status(thm)],[884,3397,theory(equality)]) ).
cnf(3401,plain,
earray_62 = earray_58,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,324,theory(equality)]),660,hyp49,theory(equality)]) ).
cnf(3404,plain,
( index_60 = X
| select(earray_64,X) = select(earray_58,X) ),
inference('REWRITE',[status(thm)],[890,3401,theory(equality)]) ).
cnf(3405,plain,
earray_56 = earray_52,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,325,theory(equality)]),662,hyp47,theory(equality)]) ).
cnf(3408,plain,
( index_54 = X
| select(earray_58,X) = select(earray_52,X) ),
inference('REWRITE',[status(thm)],[892,3405,theory(equality)]) ).
cnf(3409,plain,
earray_41 = earray_37,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,327,theory(equality)]),666,hyp43,theory(equality)]) ).
cnf(3412,plain,
( index_39 = X
| select(earray_43,X) = select(earray_37,X) ),
inference('REWRITE',[status(thm)],[896,3409,theory(equality)]) ).
cnf(3413,plain,
earray_35 = earray_31,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,328,theory(equality)]),668,hyp40,theory(equality)]) ).
cnf(3416,plain,
( index_33 = X
| select(earray_37,X) = select(earray_31,X) ),
inference('REWRITE',[status(thm)],[900,3413,theory(equality)]) ).
cnf(3417,plain,
earray_20 = earray_16,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[838,330,theory(equality)]),679,hyp33,theory(equality)]) ).
cnf(3420,plain,
( index_18 = X
| select(earray_22,X) = select(earray_16,X) ),
inference('REWRITE',[status(thm)],[904,3417,theory(equality)]) ).
cnf(3465,plain,
index_9 = index_207,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,303,theory(equality)]),532,hyp138,theory(equality)]) ).
cnf(3466,plain,
index_12 = s(index_207),
inference('REWRITE',[status(thm)],[hyp70,3465,theory(equality)]) ).
cnf(3704,plain,
index_192 = index_186,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,306,theory(equality)]),552,hyp101,theory(equality)]) ).
cnf(3706,plain,
index_195 = s(index_186),
inference('REWRITE',[status(thm)],[hyp102,3704,theory(equality)]) ).
cnf(3944,plain,
index_171 = index_156,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,310,theory(equality)]),585,hyp92,theory(equality)]) ).
cnf(3946,plain,
index_174 = s(index_156),
inference('REWRITE',[status(thm)],[hyp93,3944,theory(equality)]) ).
cnf(4183,plain,
index_141 = index_135,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,313,theory(equality)]),605,hyp79,theory(equality)]) ).
cnf(4185,plain,
index_144 = s(index_135),
inference('REWRITE',[status(thm)],[hyp80,4183,theory(equality)]) ).
cnf(4420,plain,
( index_135 = X
| select(earray_142,X) = select(earray_133,X) ),
inference('REWRITE',[status(thm)],[3312,4183,theory(equality)]) ).
cnf(4422,plain,
index_120 = index_114,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,316,theory(equality)]),634,hyp71,theory(equality)]) ).
cnf(4424,plain,
index_123 = s(index_114),
inference('REWRITE',[status(thm)],[hyp72,4422,theory(equality)]) ).
cnf(4604,plain,
( index_114 = X
| select(earray_121,X) = select(earray_112,X) ),
inference('REWRITE',[status(thm)],[3307,4422,theory(equality)]) ).
cnf(4661,plain,
index_99 = index_93,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,319,theory(equality)]),455,hyp143,theory(equality)]) ).
cnf(4662,plain,
index_102 = s(index_93),
inference('REWRITE',[status(thm)],[hyp63,4661,theory(equality)]) ).
cnf(4843,plain,
( index_93 = X
| select(earray_100,X) = select(earray_91,X) ),
inference('REWRITE',[status(thm)],[3351,4661,theory(equality)]) ).
cnf(4900,plain,
index_72 = index_66,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,323,theory(equality)]),481,hyp132,theory(equality)]) ).
cnf(4902,plain,
index_75 = s(index_66),
inference('REWRITE',[status(thm)],[hyp133,4900,theory(equality)]) ).
cnf(5082,plain,
( index_66 = X
| select(earray_73,X) = select(earray_64,X) ),
inference('REWRITE',[status(thm)],[3346,4900,theory(equality)]) ).
cnf(5139,plain,
index_51 = index_45,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,326,theory(equality)]),510,hyp123,theory(equality)]) ).
cnf(5141,plain,
index_54 = s(index_45),
inference('REWRITE',[status(thm)],[hyp124,5139,theory(equality)]) ).
cnf(5321,plain,
( index_45 = X
| select(earray_52,X) = select(earray_43,X) ),
inference('REWRITE',[status(thm)],[3341,5139,theory(equality)]) ).
cnf(5378,plain,
index_30 = index_24,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,329,theory(equality)]),530,hyp115,theory(equality)]) ).
cnf(5380,plain,
index_33 = s(index_24),
inference('REWRITE',[status(thm)],[hyp116,5378,theory(equality)]) ).
cnf(5383,plain,
index_33 != index_12,
inference('REWRITE',[status(thm)],[632,5380,theory(equality)]) ).
cnf(5385,plain,
index_39 != index_12,
inference('REWRITE',[status(thm)],[739,523,5380,theory(equality)]) ).
cnf(5387,plain,
index_45 != index_12,
inference('REWRITE',[status(thm)],[779,514,523,5380,theory(equality)]) ).
cnf(5389,plain,
index_54 != index_12,
inference('REWRITE',[status(thm)],[819,5141,514,523,5380,theory(equality)]) ).
cnf(5391,plain,
index_60 != index_12,
inference('REWRITE',[status(thm)],[980,503,5141,514,523,5380,theory(equality)]) ).
cnf(5393,plain,
index_66 != index_12,
inference('REWRITE',[status(thm)],[1022,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5395,plain,
index_75 != index_12,
inference('REWRITE',[status(thm)],[1064,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5397,plain,
index_87 != index_12,
inference('REWRITE',[status(thm)],[1106,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5399,plain,
index_93 != index_12,
inference('REWRITE',[status(thm)],[1148,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5401,plain,
index_102 != index_12,
inference('REWRITE',[status(thm)],[1190,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5403,plain,
index_108 != index_12,
inference('REWRITE',[status(thm)],[1232,647,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5405,plain,
index_114 != index_12,
inference('REWRITE',[status(thm)],[1274,638,647,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5407,plain,
index_123 != index_12,
inference('REWRITE',[status(thm)],[1316,4424,638,647,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5409,plain,
index_129 != index_12,
inference('REWRITE',[status(thm)],[1358,618,4424,638,647,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5411,plain,
index_135 != index_12,
inference('REWRITE',[status(thm)],[1400,609,618,4424,638,647,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5413,plain,
index_144 != index_12,
inference('REWRITE',[status(thm)],[1442,4185,609,618,4424,638,647,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5415,plain,
index_150 != index_12,
inference('REWRITE',[status(thm)],[1484,598,4185,609,618,4424,638,647,4662,459,474,4902,485,503,5141,514,523,5380,theory(equality)]) ).
cnf(5944,plain,
( index_24 = X
| select(earray_31,X) = select(earray_22,X) ),
inference('REWRITE',[status(thm)],[3336,5378,theory(equality)]) ).
cnf(6001,plain,
index_3 = index_0,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[840,333,theory(equality)]),hyp62,hyp114,theory(equality)]) ).
cnf(6004,plain,
index_6 = s(index_0),
inference('REWRITE',[status(thm)],[hyp126,6001,theory(equality)]) ).
cnf(6882,plain,
index_116 = select(q23,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp151,theory(equality)]),3277,hyp68,theory(equality)]) ).
cnf(6884,plain,
index_137 = select(q26,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp159,theory(equality)]),3280,hyp77,theory(equality)]) ).
cnf(6886,plain,
index_158 = select(q2,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp166,theory(equality)]),3283,hyp86,theory(equality)]) ).
cnf(6888,plain,
index_167 = select(q29,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp169,theory(equality)]),3284,hyp90,theory(equality)]) ).
cnf(6890,plain,
index_188 = select(q5,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp177,theory(equality)]),3288,hyp99,theory(equality)]) ).
cnf(6892,plain,
index_209 = select(q8,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp185,theory(equality)]),3291,hyp107,theory(equality)]) ).
cnf(6894,plain,
index_26 = select(q11,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp188,theory(equality)]),3292,hyp112,theory(equality)]) ).
cnf(6896,plain,
index_47 = select(q14,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp195,theory(equality)]),3295,hyp121,theory(equality)]) ).
cnf(6898,plain,
index_68 = select(q17,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp203,theory(equality)]),3299,hyp130,theory(equality)]) ).
cnf(6900,plain,
index_95 = select(q20,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,hyp213,theory(equality)]),3303,hyp141,theory(equality)]) ).
cnf(6902,plain,
index_209 = select(q7,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,304,theory(equality)]),3290,6892,theory(equality)]) ).
cnf(6904,plain,
index_209 = index_189,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,305,theory(equality)]),3289,6902,theory(equality)]) ).
cnf(6906,plain,
index_210 = s(index_189),
inference('REWRITE',[status(thm)],[hyp109,6904,theory(equality)]) ).
cnf(7028,plain,
index_188 = select(q4,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,307,theory(equality)]),3287,6890,theory(equality)]) ).
cnf(7030,plain,
index_188 = index_159,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,308,theory(equality)]),3286,7028,theory(equality)]) ).
cnf(7032,plain,
index_189 = s(index_159),
inference('REWRITE',[status(thm)],[hyp100,7030,theory(equality)]) ).
cnf(7154,plain,
index_167 = select(q28,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,311,theory(equality)]),3282,6888,theory(equality)]) ).
cnf(7156,plain,
index_167 = index_138,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,312,theory(equality)]),3281,7154,theory(equality)]) ).
cnf(7158,plain,
index_168 = s(index_138),
inference('REWRITE',[status(thm)],[hyp91,7156,theory(equality)]) ).
cnf(7280,plain,
index_137 = select(q25,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,314,theory(equality)]),3279,6884,theory(equality)]) ).
cnf(7282,plain,
index_137 = index_117,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,315,theory(equality)]),3278,7280,theory(equality)]) ).
cnf(7284,plain,
index_138 = s(index_117),
inference('REWRITE',[status(thm)],[hyp78,7282,theory(equality)]) ).
cnf(7406,plain,
index_116 = select(q22,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,317,theory(equality)]),3275,6882,theory(equality)]) ).
cnf(7408,plain,
index_116 = index_96,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,318,theory(equality)]),3274,7406,theory(equality)]) ).
cnf(7409,plain,
index_116 = s(index_95),
inference('REWRITE',[status(thm)],[hyp142,7408,theory(equality)]) ).
cnf(7473,plain,
index_95 = select(q19,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,320,theory(equality)]),3302,6900,theory(equality)]) ).
cnf(7475,plain,
index_95 = index_69,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,322,theory(equality)]),3300,7473,theory(equality)]) ).
cnf(7479,plain,
index_116 = s(index_69),
inference('REWRITE',[status(thm)],[7409,7475,theory(equality)]) ).
cnf(7599,plain,
index_68 = select(q16,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,324,theory(equality)]),3298,6898,theory(equality)]) ).
cnf(7601,plain,
index_68 = index_48,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,325,theory(equality)]),3297,7599,theory(equality)]) ).
cnf(7603,plain,
index_69 = s(index_48),
inference('REWRITE',[status(thm)],[hyp131,7601,theory(equality)]) ).
cnf(7725,plain,
index_47 = select(q13,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,327,theory(equality)]),3294,6896,theory(equality)]) ).
cnf(7727,plain,
index_47 = index_27,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,328,theory(equality)]),3293,7725,theory(equality)]) ).
cnf(7729,plain,
index_48 = s(index_27),
inference('REWRITE',[status(thm)],[hyp122,7727,theory(equality)]) ).
cnf(7851,plain,
index_26 = select(q10,head),
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,330,theory(equality)]),3285,6894,theory(equality)]) ).
cnf(7853,plain,
index_26 = index_210,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,331,theory(equality)]),3276,7851,theory(equality)]) ).
cnf(7855,plain,
index_27 = s(index_210),
inference('REWRITE',[status(thm)],[hyp113,7853,theory(equality)]) ).
cnf(8082,plain,
select(q1,head) = index_0,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,332,theory(equality)]),3296,theory(equality)]) ).
cnf(8083,plain,
select(queue_80,head) = index_0,
inference('REWRITE',[status(thm)],[3301,8082,theory(equality)]) ).
cnf(8084,plain,
index_158 = index_0,
inference('REWRITE',[status(thm)],[inference('PARAMODULATE',[status(thm)],[841,467,theory(equality)]),8083,6886,theory(equality)]) ).
cnf(8086,plain,
index_159 = index_6,
inference('REWRITE',[status(thm)],[hyp87,6004,8084,theory(equality)]) ).
cnf(8090,plain,
index_153 = index_189,
inference('REWRITE',[status(thm)],[494,7032,8086,theory(equality)]) ).
cnf(8096,plain,
index_210 = index_156,
inference('REWRITE',[status(thm)],[6906,hyp85,8090,theory(equality)]) ).
cnf(8105,plain,
index_27 = index_174,
inference('REWRITE',[status(thm)],[7855,3946,8096,theory(equality)]) ).
cnf(8111,plain,
index_48 = index_180,
inference('REWRITE',[status(thm)],[7729,574,8105,theory(equality)]) ).
cnf(8117,plain,
index_69 = index_186,
inference('REWRITE',[status(thm)],[7603,556,8111,theory(equality)]) ).
cnf(8125,plain,
index_116 = index_195,
inference('REWRITE',[status(thm)],[7479,3706,8117,theory(equality)]) ).
cnf(8129,plain,
index_201 = index_117,
inference('REWRITE',[status(thm)],[545,hyp69,8125,theory(equality)]) ).
cnf(8133,plain,
index_207 = index_138,
inference('REWRITE',[status(thm)],[536,7284,8129,theory(equality)]) ).
cnf(8137,plain,
index_12 = index_168,
inference('REWRITE',[status(thm)],[3466,7158,8133,theory(equality)]) ).
cnf(8141,plain,
elem_214 = select(earray_163,index_12),
inference('REWRITE',[status(thm)],[3321,8137,theory(equality)]) ).
cnf(12459,plain,
elem_214 = select(earray_148,index_12),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[3372,5415]),8141,theory(equality)]) ).
cnf(12555,plain,
elem_214 = select(earray_142,index_12),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[3376,5413]),12459,theory(equality)]) ).
cnf(12692,plain,
select(earray_133,index_12) = select(earray_127,index_12),
inference('UR-RESOLVE',[status(thm)],[3380,5409]) ).
cnf(12785,plain,
select(earray_127,index_12) = select(earray_121,index_12),
inference('UR-RESOLVE',[status(thm)],[3384,5407]) ).
cnf(12786,plain,
select(earray_133,index_12) = select(earray_121,index_12),
inference('REWRITE',[status(thm)],[12692,12785,theory(equality)]) ).
cnf(12917,plain,
select(earray_112,index_12) = select(earray_106,index_12),
inference('UR-RESOLVE',[status(thm)],[3388,5403]) ).
cnf(13007,plain,
select(earray_106,index_12) = select(earray_100,index_12),
inference('UR-RESOLVE',[status(thm)],[3392,5401]) ).
cnf(13008,plain,
select(earray_112,index_12) = select(earray_100,index_12),
inference('REWRITE',[status(thm)],[12917,13007,theory(equality)]) ).
cnf(13133,plain,
select(earray_91,index_12) = select(earray_85,index_12),
inference('UR-RESOLVE',[status(thm)],[3396,5397]) ).
cnf(13220,plain,
select(earray_85,index_12) = select(earray_73,index_12),
inference('UR-RESOLVE',[status(thm)],[3400,5395]) ).
cnf(13221,plain,
select(earray_91,index_12) = select(earray_73,index_12),
inference('REWRITE',[status(thm)],[13133,13220,theory(equality)]) ).
cnf(13340,plain,
select(earray_64,index_12) = select(earray_58,index_12),
inference('UR-RESOLVE',[status(thm)],[3404,5391]) ).
cnf(13424,plain,
select(earray_58,index_12) = select(earray_52,index_12),
inference('UR-RESOLVE',[status(thm)],[3408,5389]) ).
cnf(13425,plain,
select(earray_64,index_12) = select(earray_52,index_12),
inference('REWRITE',[status(thm)],[13340,13424,theory(equality)]) ).
cnf(13538,plain,
select(earray_43,index_12) = select(earray_37,index_12),
inference('UR-RESOLVE',[status(thm)],[3412,5385]) ).
cnf(13619,plain,
select(earray_37,index_12) = select(earray_31,index_12),
inference('UR-RESOLVE',[status(thm)],[3416,5383]) ).
cnf(13620,plain,
select(earray_43,index_12) = select(earray_31,index_12),
inference('REWRITE',[status(thm)],[13538,13619,theory(equality)]) ).
cnf(13710,plain,
select(earray_22,index_12) = e10,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[3420,630]),711,theory(equality)]) ).
cnf(14202,plain,
elem_214 = select(earray_121,index_12),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[4420,5411]),12786,12555,theory(equality)]) ).
cnf(14472,plain,
elem_214 = select(earray_100,index_12),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[4604,5405]),13008,14202,theory(equality)]) ).
cnf(14877,plain,
elem_214 = select(earray_73,index_12),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[4843,5399]),13221,14472,theory(equality)]) ).
cnf(15112,plain,
elem_214 = select(earray_52,index_12),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[5082,5393]),13425,14877,theory(equality)]) ).
cnf(15340,plain,
elem_214 = select(earray_31,index_12),
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[5321,5387]),13620,15112,theory(equality)]) ).
cnf(15508,plain,
$false,
inference('REWRITE',[status(thm)],[inference('UR-RESOLVE',[status(thm)],[5944,631]),goal,13710,15340,theory(equality)]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SWV569-1.030 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.13 % Command : run-snark %s %d
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Thu Jun 16 00:23:25 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.46 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.47 *
% 0.19/0.47 *
% 0.19/0.47 #<PACKAGE "SNARK-USER">
% 0.19/0.47 *
% 0.19/0.47 SNARK-TPTP-OPTIONS
% 0.19/0.47 *
% 0.19/0.48 ((AGENDA-LENGTH-LIMIT NIL) (AGENDA-LENGTH-BEFORE-SIMPLIFICATION-LIMIT NIL)
% 0.19/0.48 (USE-HYPERRESOLUTION T) (USE-UR-RESOLUTION T) (USE-PARAMODULATION T)
% 0.19/0.48 (USE-FACTORING :POS)
% 0.19/0.48 (USE-LITERAL-ORDERING-WITH-HYPERRESOLUTION 'LITERAL-ORDERING-P)
% 0.19/0.48 (USE-LITERAL-ORDERING-WITH-PARAMODULATION 'LITERAL-ORDERING-P)
% 0.19/0.48 (ORDERING-FUNCTIONS>CONSTANTS T) (ASSERT-CONTEXT :CURRENT)
% 0.19/0.48 (RUN-TIME-LIMIT 300) (LISTEN-FOR-COMMANDS NIL)
% 0.19/0.48 (USE-CLOSURE-WHEN-SATISFIABLE T) (PRINT-ROWS-WHEN-GIVEN NIL)
% 0.19/0.48 (PRINT-ROWS-WHEN-DERIVED NIL) (PRINT-UNORIENTABLE-ROWS NIL)
% 0.19/0.48 (PRINT-ROW-WFFS-PRETTILY NIL) (PRINT-FINAL-ROWS :TPTP)
% 0.19/0.48 (PRINT-OPTIONS-WHEN-STARTING NIL) (USE-VARIABLE-NAME-SORTS NIL)
% 0.19/0.48 (USE-PURITY-TEST T) (USE-RELEVANCE-TEST T) (DECLARE-TPTP-SYMBOLS1)
% 0.19/0.48 (DECLARE-TPTP-SYMBOLS2))
% 0.19/0.48 *
% 0.19/0.48 "."
% 0.19/0.48 *
% 0.19/0.48 ; Begin refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-16T00:23:25
% 0.19/0.48 ; Running SNARK from /davis/home/graph/tptp/Systems/SNARK---20120808r022/Source/snark-system.lisp in SBCL 1.0.12 on n017.cluster.edu at 2022-06-16T00:23:25
% 7.08/7.31
% 7.08/7.31
% 7.08/7.31 #||
% 7.08/7.31 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.08/7.31 % SZS output start Refutation
% See solution above
% 7.18/7.38 ||#
% 7.18/7.38
% 7.18/7.38 ; Summary of computation:
% 7.18/7.38 ; 22400 formulas have been input or derived (from 3313 formulas).
% 7.18/7.38 ; 15508 (69%) were retained. Of these,
% 7.18/7.38 ; 6903 (45%) were simplified or subsumed later,
% 7.18/7.38 ; 8605 (55%) are still being kept.
% 7.18/7.38 ;
% 7.18/7.38 ; Run time in seconds excluding printing time:
% 7.18/7.38 ; 0.041 1% Read assertion file (1 call)
% 7.18/7.38 ; 0.006 0% Assert (302 calls)
% 7.18/7.38 ; 1.894 28% Process new row (22,286 calls)
% 7.18/7.38 ; 2.181 32% Resolution (6,624 calls)
% 7.18/7.38 ; 0.195 3% Paramodulation (3,312 calls)
% 7.18/7.38 ; 0.000 0% Factoring (97 calls)
% 7.18/7.38 ; 0.004 0% Condensing (230 calls)
% 7.18/7.38 ; 0.005 0% Forward subsumption (230 calls)
% 7.18/7.38 ; 0.003 0% Backward subsumption (176 calls)
% 7.18/7.38 ; 0.000 0% Clause clause subsumption (54 calls)
% 7.18/7.38 ; 1.750 26% Forward simplification (22,234 calls)
% 7.18/7.38 ; 0.546 8% Backward simplification (15,508 calls)
% 7.18/7.38 ; 0.068 1% Ordering (35,918 calls)
% 7.18/7.38 ; 0.000 0% Sortal reasoning (32 calls)
% 7.18/7.38 ; 0.000 0% Purity testing (1 call)
% 7.18/7.38 ; 0.138 2% Other
% 7.18/7.38 ; 6.831 Total
% 7.18/7.38 ; 6.906 Real time
% 7.18/7.38 ;
% 7.18/7.38 ; Term-hash-array has 28,869 terms in all.
% 7.18/7.38 ; Feature-vector-row-index has 133 entries (133 at peak, 176 added, 43 deleted).
% 7.18/7.38 ; Feature-vector-row-index has 570 nodes (570 at peak, 729 added, 159 deleted).
% 7.18/7.38 ; Retrieved 203 possibly forward subsuming rows in 230 calls.
% 7.18/7.38 ; Retrieved 58 possibly backward subsumed rows in 176 calls.
% 7.18/7.38 ; Path-index has 20,051 entries (20,051 at peak, 31,296 added, 11,245 deleted).
% 7.18/7.38 ; Path-index has 2,818 nodes (4,765 at peak, 6,275 added, 3,457 deleted).
% 7.18/7.38 ; Trie-index has 20,051 entries (20,051 at peak, 31,296 added, 11,245 deleted).
% 7.18/7.38 ; Trie-index has 159,806 nodes (159,833 at peak, 200,515 added, 40,709 deleted).
% 7.18/7.38 ; Retrieved 176,204 generalization terms in 468,005 calls.
% 7.18/7.38 ; Retrieved 16,556 instance terms in 15,331 calls.
% 7.18/7.38 ; Retrieved 866,667 unifiable terms in 28,306 calls.
% 7.18/7.38 ;
% 7.18/7.38 ; The agenda of rows to process has 105 entries:
% 7.18/7.38 ; 28 with value 11 1 with value 56 1 with value 110
% 7.18/7.38 ; 1 with value 13 1 with value 59 1 with value 113
% 7.18/7.38 ; 3 with value 14 1 with value 62 1 with value 116
% 7.18/7.38 ; 1 with value 15 1 with value 65 1 with value 119
% 7.18/7.38 ; 20 with value 16 1 with value 68 1 with value 122
% 7.18/7.38 ; 2 with value 17 1 with value 71 1 with value 125
% 7.18/7.38 ; 2 with value 20 1 with value 74 1 with value 128
% 7.18/7.38 ; 2 with value 23 1 with value 77 1 with value 131
% 7.18/7.38 ; 1 with value 26 1 with value 80 1 with value 134
% 7.18/7.38 ; 1 with value 29 1 with value 83 1 with value 137
% 7.18/7.38 ; 1 with value 32 1 with value 86 1 with value 140
% 7.18/7.38 ; 1 with value 35 1 with value 89 1 with value 143
% 7.18/7.38 ; 1 with value 38 1 with value 92 1 with value 146
% 7.18/7.38 ; 1 with value 41 1 with value 95 1 with value 149
% 7.18/7.38 ; 1 with value 44 1 with value 98 1 with value 152
% 7.18/7.38 ; 1 with value 47 1 with value 101 1 with value 155
% 7.18/7.38 ; 1 with value 50 1 with value 104 1 with value 158
% 7.18/7.38 ; 1 with value 53 1 with value 107 1 with value 161
% 7.18/7.38 ; The agenda of rows to give has 6667 entries:
% 7.18/7.38 ; 18 with value (4 9) 2 with value (4 58) 1 with value (4 102)
% 7.18/7.38 ; 100 with value (4 14) 118 with value (4 59) 2 with value (4 103)
% 7.18/7.38 ; 960 with value (4 15) 1 with value (4 60) 90 with value (4 104)
% 7.18/7.38 ; 2 with value (4 16) 23 with value (4 61) 2 with value (4 106)
% 7.18/7.38 ; 185 with value (4 17) 96 with value (4 62) 88 with value (4 107)
% 7.18/7.38 ; 1 with value (4 18) 21 with value (4 63) 1 with value (4 108)
% 7.18/7.38 ; 92 with value (4 19) 2 with value (4 64) 1 with value (4 109)
% 7.18/7.38 ; 126 with value (4 20) 115 with value (4 65) 89 with value (4 110)
% 7.18/7.38 ; 60 with value (4 21) 1 with value (4 66) 2 with value (4 112)
% 7.18/7.38 ; 2 with value (4 22) 20 with value (4 67) 87 with value (4 113)
% 7.18/7.38 ; 185 with value (4 23) 96 with value (4 68) 1 with value (4 114)
% 7.18/7.38 ; 1 with value (4 24) 18 with value (4 69) 1 with value (4 115)
% 7.18/7.38 ; 31 with value (4 25) 2 with value (4 70) 86 with value (4 116)
% 7.18/7.38 ; 126 with value (4 26) 112 with value (4 71) 1 with value (4 118)
% 7.18/7.38 ; 30 with value (4 27) 1 with value (4 72) 85 with value (4 119)
% 7.18/7.38 ; 2 with value (4 28) 17 with value (4 73) 1 with value (4 121)
% 7.18/7.38 ; 125 with value (4 29) 96 with value (4 74) 84 with value (4 122)
% 7.18/7.38 ; 1 with value (4 30) 15 with value (4 75) 1 with value (4 124)
% 7.18/7.38 ; 31 with value (4 31) 2 with value (4 76) 83 with value (4 125)
% 7.18/7.38 ; 96 with value (4 32) 109 with value (4 77) 1 with value (4 127)
% 7.18/7.38 ; 30 with value (4 33) 1 with value (4 78) 82 with value (4 128)
% 7.18/7.38 ; 2 with value (4 34) 14 with value (4 79) 1 with value (4 130)
% 7.18/7.38 ; 125 with value (4 35) 95 with value (4 80) 81 with value (4 131)
% 7.18/7.38 ; 1 with value (4 36) 12 with value (4 81) 1 with value (4 133)
% 7.18/7.38 ; 31 with value (4 37) 2 with value (4 82) 80 with value (4 134)
% 7.18/7.38 ; 96 with value (4 38) 104 with value (4 83) 1 with value (4 136)
% 7.18/7.38 ; 30 with value (4 39) 1 with value (4 84) 79 with value (4 137)
% 7.18/7.38 ; 2 with value (4 40) 11 with value (4 85) 1 with value (4 139)
% 7.18/7.38 ; 125 with value (4 41) 93 with value (4 86) 78 with value (4 140)
% 7.18/7.38 ; 1 with value (4 42) 9 with value (4 87) 1 with value (4 142)
% 7.18/7.38 ; 31 with value (4 43) 2 with value (4 88) 77 with value (4 143)
% 7.18/7.38 ; 96 with value (4 44) 99 with value (4 89) 1 with value (4 145)
% 7.18/7.38 ; 30 with value (4 45) 1 with value (4 90) 76 with value (4 146)
% 7.18/7.38 ; 2 with value (4 46) 8 with value (4 91) 1 with value (4 148)
% 7.18/7.38 ; 124 with value (4 47) 91 with value (4 92) 75 with value (4 149)
% 7.18/7.38 ; 1 with value (4 48) 6 with value (4 93) 1 with value (4 151)
% 7.18/7.38 ; 29 with value (4 49) 2 with value (4 94) 74 with value (4 152)
% 7.18/7.38 ; 96 with value (4 50) 95 with value (4 95) 1 with value (4 154)
% 7.18/7.38 ; 27 with value (4 51) 1 with value (4 96) 73 with value (4 155)
% 7.18/7.38 ; 2 with value (4 52) 5 with value (4 97) 1 with value (4 157)
% 7.18/7.38 ; 121 with value (4 53) 91 with value (4 98) 72 with value (4 158)
% 7.18/7.38 ; 1 with value (4 54) 3 with value (4 99) 1 with value (4 160)
% 7.18/7.38 ; 26 with value (4 55) 2 with value (4 100) 71 with value (4 161)
% 7.18/7.38 ; 96 with value (4 56) 92 with value (4 101) 1 with value (4 163)
% 7.18/7.38 ; 24 with value (4 57)
% 7.18/7.38 Evaluation took:
% 7.18/7.38 6.908 seconds of real time
% 7.18/7.38 6.566855 seconds of user run time
% 7.18/7.38 0.341051 seconds of system run time
% 7.18/7.38 [Run times include 1.048 seconds GC run time.]
% 7.18/7.38 0 calls to %EVAL
% 7.18/7.38 0 page faults and
% 7.18/7.38 775,004,520 bytes consed.
% 7.18/7.38 :PROOF-FOUND
% 7.18/7.38 ; End refute-file /export/starexec/sandbox2/benchmark/theBenchmark.p 2022-06-16T00:23:32
% 7.18/7.38 :PROOF-FOUND
% 7.18/7.38 *
%------------------------------------------------------------------------------