%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV569-1.040 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:04:22 AM UTC 2026
% Result : Unsatisfiable 138.89s 24.08s
% Output : CNFRefutation 138.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 329
% Syntax : Number of clauses : 1702 (1267 unt; 434 nHn;1505 RR)
% Number of literals : 2551 (2550 equ; 429 neg)
% Maximal clause size : 8 ( 1 avg)
% Maximal term depth : 27 ( 4 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 346 ( 346 usr; 343 con; 0-3 aty)
% Number of variables : 259 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(a1,axiom,
select(store(X0,X1,X2),X1) = X2 ).
cnf(a2,axiom,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ) ).
cnf(head_distinct_from_tail,axiom,
head != tail ).
cnf(head_distinct_from_seq,axiom,
head != seq ).
cnf(tail_distinct_from_seq,axiom,
tail != seq ).
cnf(as26,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))))) != X0 ).
cnf(as25,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))))) != X0 ).
cnf(as24,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))) != X0 ).
cnf(as23,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))) != X0 ).
cnf(as22,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))) != X0 ).
cnf(as21,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))) != X0 ).
cnf(as20,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))) != X0 ).
cnf(as19,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))) != X0 ).
cnf(as18,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))) != X0 ).
cnf(as17,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))) != X0 ).
cnf(as16,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0 ).
cnf(as15,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0 ).
cnf(as14,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0 ).
cnf(as13,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0 ).
cnf(as12,axiom,
s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0 ).
cnf(as11,axiom,
s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0 ).
cnf(as10,axiom,
s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0 ).
cnf(as9,axiom,
s(s(s(s(s(s(s(s(s(X0))))))))) != X0 ).
cnf(as8,axiom,
s(s(s(s(s(s(s(s(X0)))))))) != X0 ).
cnf(as7,axiom,
s(s(s(s(s(s(s(X0))))))) != X0 ).
cnf(as6,axiom,
s(s(s(s(s(s(X0)))))) != X0 ).
cnf(as5,axiom,
s(s(s(s(s(X0))))) != X0 ).
cnf(as4,axiom,
s(s(s(s(X0)))) != X0 ).
cnf(as3,axiom,
s(s(s(X0))) != X0 ).
cnf(as2,axiom,
s(s(X0)) != X0 ).
cnf(as1,axiom,
s(X0) != X0 ).
cnf(hyp1,hypothesis,
'earray$u100' = store('earray$u98','index$u99',e21) ).
cnf(hyp2,hypothesis,
'earray$u104' = select(q22,seq) ).
cnf(hyp3,hypothesis,
'earray$u106' = store('earray$u104','index$u105',e22) ).
cnf(hyp4,hypothesis,
'earray$u110' = select(q23,seq) ).
cnf(hyp5,hypothesis,
'earray$u112' = store('earray$u110','index$u111',e23) ).
cnf(hyp6,hypothesis,
'earray$u119' = select(q24,seq) ).
cnf(hyp7,hypothesis,
'earray$u121' = store('earray$u119','index$u120',e24) ).
cnf(hyp8,hypothesis,
'earray$u125' = select(q25,seq) ).
cnf(hyp9,hypothesis,
'earray$u127' = store('earray$u125','index$u126',e25) ).
cnf(hyp10,hypothesis,
'earray$u131' = select(q26,seq) ).
cnf(hyp11,hypothesis,
'earray$u133' = store('earray$u131','index$u132',e26) ).
cnf(hyp13,hypothesis,
'earray$u140' = select(q27,seq) ).
cnf(hyp14,hypothesis,
'earray$u142' = store('earray$u140','index$u141',e27) ).
cnf(hyp15,hypothesis,
'earray$u146' = select(q28,seq) ).
cnf(hyp16,hypothesis,
'earray$u148' = store('earray$u146','index$u147',e28) ).
cnf(hyp20,hypothesis,
'earray$u161' = select(q29,seq) ).
cnf(hyp21,hypothesis,
'earray$u163' = store('earray$u161','index$u162',e29) ).
cnf(hyp22,hypothesis,
'earray$u170' = select(q30,seq) ).
cnf(hyp23,hypothesis,
'earray$u172' = store('earray$u170','index$u171',e30) ).
cnf(hyp24,hypothesis,
'earray$u176' = select(q31,seq) ).
cnf(hyp25,hypothesis,
'earray$u178' = store('earray$u176','index$u177',e31) ).
cnf(hyp26,hypothesis,
'earray$u182' = select(q32,seq) ).
cnf(hyp27,hypothesis,
'earray$u184' = store('earray$u182','index$u183',e32) ).
cnf(hyp28,hypothesis,
'earray$u191' = select(q33,seq) ).
cnf(hyp29,hypothesis,
'earray$u193' = store('earray$u191','index$u192',e33) ).
cnf(hyp30,hypothesis,
'earray$u197' = select(q34,seq) ).
cnf(hyp31,hypothesis,
'earray$u199' = store('earray$u197','index$u198',e34) ).
cnf(hyp34,hypothesis,
'earray$u203' = select(q35,seq) ).
cnf(hyp35,hypothesis,
'earray$u205' = store('earray$u203','index$u204',e35) ).
cnf(hyp36,hypothesis,
'earray$u212' = select(q36,seq) ).
cnf(hyp37,hypothesis,
'earray$u214' = store('earray$u212','index$u213',e36) ).
cnf(hyp38,hypothesis,
'earray$u218' = select(q37,seq) ).
cnf(hyp40,hypothesis,
'earray$u220' = store('earray$u218','index$u219',e37) ).
cnf(hyp41,hypothesis,
'earray$u224' = select(q38,seq) ).
cnf(hyp42,hypothesis,
'earray$u226' = store('earray$u224','index$u225',e38) ).
cnf(hyp45,hypothesis,
'earray$u239' = select(q39,seq) ).
cnf(hyp46,hypothesis,
'earray$u241' = store('earray$u239','index$u240',e39) ).
cnf(hyp57,hypothesis,
'earray$u281' = select(q40,seq) ).
cnf(hyp61,hypothesis,
'earray$u37' = store('earray$u35','index$u36',e13) ).
cnf(hyp63,hypothesis,
'earray$u41' = select(q14,seq) ).
cnf(hyp64,hypothesis,
'earray$u43' = store('earray$u41','index$u42',e14) ).
cnf(hyp65,hypothesis,
'earray$u50' = select(q15,seq) ).
cnf(hyp66,hypothesis,
'earray$u52' = store('earray$u50','index$u51',e15) ).
cnf(hyp67,hypothesis,
'earray$u56' = select(q16,seq) ).
cnf(hyp68,hypothesis,
'earray$u58' = store('earray$u56','index$u57',e16) ).
cnf(hyp69,hypothesis,
'earray$u62' = select(q17,seq) ).
cnf(hyp70,hypothesis,
'earray$u64' = store('earray$u62','index$u63',e17) ).
cnf(hyp71,hypothesis,
'earray$u71' = select(q18,seq) ).
cnf(hyp72,hypothesis,
'earray$u73' = store('earray$u71','index$u72',e18) ).
cnf(hyp76,hypothesis,
'earray$u83' = select(q19,seq) ).
cnf(hyp77,hypothesis,
'earray$u85' = store('earray$u83','index$u84',e19) ).
cnf(hyp78,hypothesis,
'earray$u89' = select(q20,seq) ).
cnf(hyp79,hypothesis,
'earray$u91' = store('earray$u89','index$u90',e20) ).
cnf(hyp80,hypothesis,
'earray$u98' = select(q21,seq) ).
cnf(hyp81,hypothesis,
'elem$u283' = select('earray$u281','index$u282') ).
cnf(hyp82,hypothesis,
'index$u0' = select(q,tail) ).
cnf(hyp83,hypothesis,
'index$u102' = s('index$u99') ).
cnf(hyp84,hypothesis,
'index$u105' = select(q22,tail) ).
cnf(hyp85,hypothesis,
'index$u108' = s('index$u105') ).
cnf(hyp86,hypothesis,
'index$u111' = select(q23,tail) ).
cnf(hyp87,hypothesis,
'index$u114' = s('index$u111') ).
cnf(hyp88,hypothesis,
'index$u116' = select('queue$u115',head) ).
cnf(hyp89,hypothesis,
'index$u117' = s('index$u116') ).
cnf(hyp90,hypothesis,
'index$u12' = s('index$u9') ).
cnf(hyp91,hypothesis,
'index$u120' = select(q24,tail) ).
cnf(hyp92,hypothesis,
'index$u123' = s('index$u120') ).
cnf(hyp93,hypothesis,
'index$u126' = select(q25,tail) ).
cnf(hyp94,hypothesis,
'index$u129' = s('index$u126') ).
cnf(hyp95,hypothesis,
'index$u132' = select(q26,tail) ).
cnf(hyp96,hypothesis,
'index$u135' = s('index$u132') ).
cnf(hyp97,hypothesis,
'index$u137' = select('queue$u136',head) ).
cnf(hyp98,hypothesis,
'index$u138' = s('index$u137') ).
cnf(hyp99,hypothesis,
'index$u141' = select(q27,tail) ).
cnf(hyp100,hypothesis,
'index$u144' = s('index$u141') ).
cnf(hyp101,hypothesis,
'index$u147' = select(q28,tail) ).
cnf(hyp102,hypothesis,
'index$u15' = select(q10,tail) ).
cnf(hyp103,hypothesis,
'index$u150' = s('index$u147') ).
cnf(hyp104,hypothesis,
'index$u153' = select(q2,tail) ).
cnf(hyp105,hypothesis,
'index$u156' = s('index$u153') ).
cnf(hyp106,hypothesis,
'index$u158' = select('queue$u157',head) ).
cnf(hyp107,hypothesis,
'index$u159' = s('index$u158') ).
cnf(hyp108,hypothesis,
'index$u162' = select(q29,tail) ).
cnf(hyp109,hypothesis,
'index$u165' = s('index$u162') ).
cnf(hyp110,hypothesis,
'index$u167' = select('queue$u166',head) ).
cnf(hyp111,hypothesis,
'index$u168' = s('index$u167') ).
cnf(hyp112,hypothesis,
'index$u171' = select(q30,tail) ).
cnf(hyp113,hypothesis,
'index$u174' = s('index$u171') ).
cnf(hyp114,hypothesis,
'index$u177' = select(q31,tail) ).
cnf(hyp115,hypothesis,
'index$u18' = s('index$u15') ).
cnf(hyp116,hypothesis,
'index$u180' = s('index$u177') ).
cnf(hyp117,hypothesis,
'index$u183' = select(q32,tail) ).
cnf(hyp118,hypothesis,
'index$u186' = s('index$u183') ).
cnf(hyp119,hypothesis,
'index$u188' = select('queue$u187',head) ).
cnf(hyp120,hypothesis,
'index$u189' = s('index$u188') ).
cnf(hyp121,hypothesis,
'index$u192' = select(q33,tail) ).
cnf(hyp122,hypothesis,
'index$u195' = s('index$u192') ).
cnf(hyp123,hypothesis,
'index$u198' = select(q34,tail) ).
cnf(hyp124,hypothesis,
'index$u201' = s('index$u198') ).
cnf(hyp125,hypothesis,
'index$u204' = select(q35,tail) ).
cnf(hyp126,hypothesis,
'index$u207' = s('index$u204') ).
cnf(hyp127,hypothesis,
'index$u209' = select('queue$u208',head) ).
cnf(hyp128,hypothesis,
'index$u21' = select(q11,tail) ).
cnf(hyp129,hypothesis,
'index$u210' = s('index$u209') ).
cnf(hyp130,hypothesis,
'index$u213' = select(q36,tail) ).
cnf(hyp131,hypothesis,
'index$u216' = s('index$u213') ).
cnf(hyp132,hypothesis,
'index$u219' = select(q37,tail) ).
cnf(hyp133,hypothesis,
'index$u222' = s('index$u219') ).
cnf(hyp134,hypothesis,
'index$u225' = select(q38,tail) ).
cnf(hyp135,hypothesis,
'index$u228' = s('index$u225') ).
cnf(hyp136,hypothesis,
'index$u230' = select('queue$u229',head) ).
cnf(hyp137,hypothesis,
'index$u231' = s('index$u230') ).
cnf(hyp138,hypothesis,
'index$u234' = select(q3,tail) ).
cnf(hyp139,hypothesis,
'index$u237' = s('index$u234') ).
cnf(hyp140,hypothesis,
'index$u24' = s('index$u21') ).
cnf(hyp141,hypothesis,
'index$u240' = select(q39,tail) ).
cnf(hyp143,hypothesis,
'index$u246' = select(q4,tail) ).
cnf(hyp144,hypothesis,
'index$u249' = s('index$u246') ).
cnf(hyp145,hypothesis,
'index$u252' = select(q5,tail) ).
cnf(hyp146,hypothesis,
'index$u255' = s('index$u252') ).
cnf(hyp147,hypothesis,
'index$u257' = select('queue$u256',head) ).
cnf(hyp148,hypothesis,
'index$u258' = s('index$u257') ).
cnf(hyp149,hypothesis,
'index$u26' = select('queue$u25',head) ).
cnf(hyp150,hypothesis,
'index$u261' = select(q6,tail) ).
cnf(hyp151,hypothesis,
'index$u264' = s('index$u261') ).
cnf(hyp152,hypothesis,
'index$u267' = select(q7,tail) ).
cnf(hyp153,hypothesis,
'index$u27' = s('index$u26') ).
cnf(hyp154,hypothesis,
'index$u270' = s('index$u267') ).
cnf(hyp155,hypothesis,
'index$u273' = select(q8,tail) ).
cnf(hyp156,hypothesis,
'index$u276' = s('index$u273') ).
cnf(hyp157,hypothesis,
'index$u278' = select('queue$u277',head) ).
cnf(hyp158,hypothesis,
'index$u279' = s('index$u278') ).
cnf(hyp159,hypothesis,
'index$u282' = select(q40,head) ).
cnf(hyp160,hypothesis,
'index$u3' = select(q0,tail) ).
cnf(hyp161,hypothesis,
'index$u30' = select(q12,tail) ).
cnf(hyp162,hypothesis,
'index$u33' = s('index$u30') ).
cnf(hyp163,hypothesis,
'index$u36' = select(q13,tail) ).
cnf(hyp164,hypothesis,
'index$u39' = s('index$u36') ).
cnf(hyp165,hypothesis,
'index$u42' = select(q14,tail) ).
cnf(hyp166,hypothesis,
'index$u45' = s('index$u42') ).
cnf(hyp167,hypothesis,
'index$u47' = select('queue$u46',head) ).
cnf(hyp168,hypothesis,
'index$u48' = s('index$u47') ).
cnf(hyp169,hypothesis,
'index$u51' = select(q15,tail) ).
cnf(hyp170,hypothesis,
'index$u54' = s('index$u51') ).
cnf(hyp171,hypothesis,
'index$u57' = select(q16,tail) ).
cnf(hyp172,hypothesis,
'index$u6' = s('index$u3') ).
cnf(hyp173,hypothesis,
'index$u60' = s('index$u57') ).
cnf(hyp174,hypothesis,
'index$u63' = select(q17,tail) ).
cnf(hyp175,hypothesis,
'index$u66' = s('index$u63') ).
cnf(hyp176,hypothesis,
'index$u68' = select('queue$u67',head) ).
cnf(hyp177,hypothesis,
'index$u69' = s('index$u68') ).
cnf(hyp178,hypothesis,
'index$u72' = select(q18,tail) ).
cnf(hyp179,hypothesis,
'index$u75' = s('index$u72') ).
cnf(hyp180,hypothesis,
'index$u78' = select(q1,tail) ).
cnf(hyp181,hypothesis,
'index$u81' = s('index$u78') ).
cnf(hyp182,hypothesis,
'index$u84' = select(q19,tail) ).
cnf(hyp183,hypothesis,
'index$u87' = s('index$u84') ).
cnf(hyp184,hypothesis,
'index$u9' = select(q9,tail) ).
cnf(hyp185,hypothesis,
'index$u90' = select(q20,tail) ).
cnf(hyp186,hypothesis,
'index$u93' = s('index$u90') ).
cnf(hyp187,hypothesis,
'index$u95' = select('queue$u94',head) ).
cnf(hyp188,hypothesis,
'index$u96' = s('index$u95') ).
cnf(hyp189,hypothesis,
'index$u99' = select(q21,tail) ).
cnf(hyp190,hypothesis,
'queue$u1' = store(q,head,'index$u0') ).
cnf(hyp191,hypothesis,
'queue$u101' = store(q21,seq,'earray$u100') ).
cnf(hyp192,hypothesis,
'queue$u103' = store('queue$u101',tail,'index$u102') ).
cnf(hyp193,hypothesis,
'queue$u107' = store(q22,seq,'earray$u106') ).
cnf(hyp194,hypothesis,
'queue$u109' = store('queue$u107',tail,'index$u108') ).
cnf(hyp195,hypothesis,
'queue$u11' = store(q9,seq,'earray$u10') ).
cnf(hyp196,hypothesis,
'queue$u113' = store(q23,seq,'earray$u112') ).
cnf(hyp197,hypothesis,
'queue$u115' = store('queue$u113',tail,'index$u114') ).
cnf(hyp198,hypothesis,
'queue$u118' = store('queue$u115',head,'index$u117') ).
cnf(hyp199,hypothesis,
'queue$u122' = store(q24,seq,'earray$u121') ).
cnf(hyp200,hypothesis,
'queue$u124' = store('queue$u122',tail,'index$u123') ).
cnf(hyp201,hypothesis,
'queue$u128' = store(q25,seq,'earray$u127') ).
cnf(hyp202,hypothesis,
'queue$u13' = store('queue$u11',tail,'index$u12') ).
cnf(hyp203,hypothesis,
'queue$u130' = store('queue$u128',tail,'index$u129') ).
cnf(hyp204,hypothesis,
'queue$u134' = store(q26,seq,'earray$u133') ).
cnf(hyp205,hypothesis,
'queue$u136' = store('queue$u134',tail,'index$u135') ).
cnf(hyp206,hypothesis,
'queue$u139' = store('queue$u136',head,'index$u138') ).
cnf(hyp207,hypothesis,
'queue$u143' = store(q27,seq,'earray$u142') ).
cnf(hyp208,hypothesis,
'queue$u145' = store('queue$u143',tail,'index$u144') ).
cnf(hyp209,hypothesis,
'queue$u149' = store(q28,seq,'earray$u148') ).
cnf(hyp210,hypothesis,
'queue$u151' = store('queue$u149',tail,'index$u150') ).
cnf(hyp211,hypothesis,
'queue$u155' = store(q2,seq,'earray$u154') ).
cnf(hyp212,hypothesis,
'queue$u157' = store('queue$u155',tail,'index$u156') ).
cnf(hyp213,hypothesis,
'queue$u160' = store('queue$u157',head,'index$u159') ).
cnf(hyp214,hypothesis,
'queue$u164' = store(q29,seq,'earray$u163') ).
cnf(hyp215,hypothesis,
'queue$u166' = store('queue$u164',tail,'index$u165') ).
cnf(hyp216,hypothesis,
'queue$u169' = store('queue$u166',head,'index$u168') ).
cnf(hyp217,hypothesis,
'queue$u17' = store(q10,seq,'earray$u16') ).
cnf(hyp218,hypothesis,
'queue$u173' = store(q30,seq,'earray$u172') ).
cnf(hyp219,hypothesis,
'queue$u175' = store('queue$u173',tail,'index$u174') ).
cnf(hyp220,hypothesis,
'queue$u179' = store(q31,seq,'earray$u178') ).
cnf(hyp221,hypothesis,
'queue$u181' = store('queue$u179',tail,'index$u180') ).
cnf(hyp222,hypothesis,
'queue$u185' = store(q32,seq,'earray$u184') ).
cnf(hyp223,hypothesis,
'queue$u187' = store('queue$u185',tail,'index$u186') ).
cnf(hyp224,hypothesis,
'queue$u19' = store('queue$u17',tail,'index$u18') ).
cnf(hyp225,hypothesis,
'queue$u190' = store('queue$u187',head,'index$u189') ).
cnf(hyp226,hypothesis,
'queue$u194' = store(q33,seq,'earray$u193') ).
cnf(hyp227,hypothesis,
'queue$u196' = store('queue$u194',tail,'index$u195') ).
cnf(hyp228,hypothesis,
'queue$u200' = store(q34,seq,'earray$u199') ).
cnf(hyp229,hypothesis,
'queue$u202' = store('queue$u200',tail,'index$u201') ).
cnf(hyp230,hypothesis,
'queue$u206' = store(q35,seq,'earray$u205') ).
cnf(hyp231,hypothesis,
'queue$u208' = store('queue$u206',tail,'index$u207') ).
cnf(hyp232,hypothesis,
'queue$u211' = store('queue$u208',head,'index$u210') ).
cnf(hyp233,hypothesis,
'queue$u215' = store(q36,seq,'earray$u214') ).
cnf(hyp234,hypothesis,
'queue$u217' = store('queue$u215',tail,'index$u216') ).
cnf(hyp235,hypothesis,
'queue$u221' = store(q37,seq,'earray$u220') ).
cnf(hyp236,hypothesis,
'queue$u223' = store('queue$u221',tail,'index$u222') ).
cnf(hyp237,hypothesis,
'queue$u227' = store(q38,seq,'earray$u226') ).
cnf(hyp238,hypothesis,
'queue$u229' = store('queue$u227',tail,'index$u228') ).
cnf(hyp239,hypothesis,
'queue$u23' = store(q11,seq,'earray$u22') ).
cnf(hyp240,hypothesis,
'queue$u232' = store('queue$u229',head,'index$u231') ).
cnf(hyp241,hypothesis,
'queue$u236' = store(q3,seq,'earray$u235') ).
cnf(hyp242,hypothesis,
'queue$u238' = store('queue$u236',tail,'index$u237') ).
cnf(hyp243,hypothesis,
'queue$u242' = store(q39,seq,'earray$u241') ).
cnf(hyp244,hypothesis,
'queue$u244' = store('queue$u242',tail,'index$u243') ).
cnf(hyp245,hypothesis,
'queue$u248' = store(q4,seq,'earray$u247') ).
cnf(hyp246,hypothesis,
'queue$u25' = store('queue$u23',tail,'index$u24') ).
cnf(hyp247,hypothesis,
'queue$u250' = store('queue$u248',tail,'index$u249') ).
cnf(hyp248,hypothesis,
'queue$u254' = store(q5,seq,'earray$u253') ).
cnf(hyp249,hypothesis,
'queue$u256' = store('queue$u254',tail,'index$u255') ).
cnf(hyp250,hypothesis,
'queue$u259' = store('queue$u256',head,'index$u258') ).
cnf(hyp251,hypothesis,
'queue$u263' = store(q6,seq,'earray$u262') ).
cnf(hyp252,hypothesis,
'queue$u265' = store('queue$u263',tail,'index$u264') ).
cnf(hyp253,hypothesis,
'queue$u269' = store(q7,seq,'earray$u268') ).
cnf(hyp254,hypothesis,
'queue$u271' = store('queue$u269',tail,'index$u270') ).
cnf(hyp255,hypothesis,
'queue$u275' = store(q8,seq,'earray$u274') ).
cnf(hyp256,hypothesis,
'queue$u277' = store('queue$u275',tail,'index$u276') ).
cnf(hyp257,hypothesis,
'queue$u28' = store('queue$u25',head,'index$u27') ).
cnf(hyp258,hypothesis,
'queue$u280' = store('queue$u277',head,'index$u279') ).
cnf(hyp259,hypothesis,
'queue$u32' = store(q12,seq,'earray$u31') ).
cnf(hyp260,hypothesis,
'queue$u34' = store('queue$u32',tail,'index$u33') ).
cnf(hyp261,hypothesis,
'queue$u38' = store(q13,seq,'earray$u37') ).
cnf(hyp262,hypothesis,
'queue$u40' = store('queue$u38',tail,'index$u39') ).
cnf(hyp263,hypothesis,
'queue$u44' = store(q14,seq,'earray$u43') ).
cnf(hyp264,hypothesis,
'queue$u46' = store('queue$u44',tail,'index$u45') ).
cnf(hyp265,hypothesis,
'queue$u49' = store('queue$u46',head,'index$u48') ).
cnf(hyp266,hypothesis,
'queue$u5' = store(q0,seq,'earray$u4') ).
cnf(hyp267,hypothesis,
'queue$u53' = store(q15,seq,'earray$u52') ).
cnf(hyp268,hypothesis,
'queue$u55' = store('queue$u53',tail,'index$u54') ).
cnf(hyp269,hypothesis,
'queue$u59' = store(q16,seq,'earray$u58') ).
cnf(hyp270,hypothesis,
'queue$u61' = store('queue$u59',tail,'index$u60') ).
cnf(hyp271,hypothesis,
'queue$u65' = store(q17,seq,'earray$u64') ).
cnf(hyp272,hypothesis,
'queue$u67' = store('queue$u65',tail,'index$u66') ).
cnf(hyp273,hypothesis,
'queue$u7' = store('queue$u5',tail,'index$u6') ).
cnf(hyp274,hypothesis,
'queue$u70' = store('queue$u67',head,'index$u69') ).
cnf(hyp275,hypothesis,
'queue$u74' = store(q18,seq,'earray$u73') ).
cnf(hyp276,hypothesis,
'queue$u76' = store('queue$u74',tail,'index$u75') ).
cnf(hyp277,hypothesis,
'queue$u80' = store(q1,seq,'earray$u79') ).
cnf(hyp278,hypothesis,
'queue$u82' = store('queue$u80',tail,'index$u81') ).
cnf(hyp279,hypothesis,
'queue$u86' = store(q19,seq,'earray$u85') ).
cnf(hyp280,hypothesis,
'queue$u88' = store('queue$u86',tail,'index$u87') ).
cnf(hyp281,hypothesis,
'queue$u92' = store(q20,seq,'earray$u91') ).
cnf(hyp282,hypothesis,
'queue$u94' = store('queue$u92',tail,'index$u93') ).
cnf(hyp283,hypothesis,
'queue$u97' = store('queue$u94',head,'index$u96') ).
cnf(hyp284,hypothesis,
q0 = 'queue$u1' ).
cnf(hyp285,hypothesis,
q1 = 'queue$u7' ).
cnf(hyp286,hypothesis,
q10 = 'queue$u13' ).
cnf(hyp287,hypothesis,
q11 = 'queue$u19' ).
cnf(hyp288,hypothesis,
q12 = 'queue$u28' ).
cnf(hyp289,hypothesis,
q13 = 'queue$u34' ).
cnf(hyp290,hypothesis,
q14 = 'queue$u40' ).
cnf(hyp291,hypothesis,
q15 = 'queue$u49' ).
cnf(hyp292,hypothesis,
q16 = 'queue$u55' ).
cnf(hyp293,hypothesis,
q17 = 'queue$u61' ).
cnf(hyp294,hypothesis,
q18 = 'queue$u70' ).
cnf(hyp295,hypothesis,
q19 = 'queue$u76' ).
cnf(hyp296,hypothesis,
q2 = 'queue$u82' ).
cnf(hyp297,hypothesis,
q20 = 'queue$u88' ).
cnf(hyp298,hypothesis,
q21 = 'queue$u97' ).
cnf(hyp299,hypothesis,
q22 = 'queue$u103' ).
cnf(hyp300,hypothesis,
q23 = 'queue$u109' ).
cnf(hyp301,hypothesis,
q24 = 'queue$u118' ).
cnf(hyp302,hypothesis,
q25 = 'queue$u124' ).
cnf(hyp303,hypothesis,
q26 = 'queue$u130' ).
cnf(hyp304,hypothesis,
q27 = 'queue$u139' ).
cnf(hyp305,hypothesis,
q28 = 'queue$u145' ).
cnf(hyp306,hypothesis,
q29 = 'queue$u151' ).
cnf(hyp307,hypothesis,
q3 = 'queue$u160' ).
cnf(hyp308,hypothesis,
q30 = 'queue$u169' ).
cnf(hyp309,hypothesis,
q31 = 'queue$u175' ).
cnf(hyp310,hypothesis,
q32 = 'queue$u181' ).
cnf(hyp311,hypothesis,
q33 = 'queue$u190' ).
cnf(hyp312,hypothesis,
q34 = 'queue$u196' ).
cnf(hyp313,hypothesis,
q35 = 'queue$u202' ).
cnf(hyp314,hypothesis,
q36 = 'queue$u211' ).
cnf(hyp315,hypothesis,
q37 = 'queue$u217' ).
cnf(hyp316,hypothesis,
q38 = 'queue$u223' ).
cnf(hyp317,hypothesis,
q39 = 'queue$u232' ).
cnf(hyp318,hypothesis,
q4 = 'queue$u238' ).
cnf(hyp319,hypothesis,
q40 = 'queue$u244' ).
cnf(hyp320,hypothesis,
q5 = 'queue$u250' ).
cnf(hyp321,hypothesis,
q6 = 'queue$u259' ).
cnf(hyp322,hypothesis,
q7 = 'queue$u265' ).
cnf(hyp323,hypothesis,
q8 = 'queue$u271' ).
cnf(hyp324,hypothesis,
q9 = 'queue$u280' ).
cnf(goal,negated_conjecture,
'elem$u283' != e13 ).
cnf(c0,plain,
select(store(X0,X1,X2),X1) = X2,
inference(clausification,[status(esa)],[a1]) ).
cnf(c1,plain,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(clausification,[status(esa)],[a2]) ).
cnf(c2,plain,
head != tail,
inference(clausification,[status(esa)],[head_distinct_from_tail]) ).
cnf(c3,plain,
head != seq,
inference(clausification,[status(esa)],[head_distinct_from_seq]) ).
cnf(c4,plain,
tail != seq,
inference(clausification,[status(esa)],[tail_distinct_from_seq]) ).
cnf(c45,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as26]) ).
cnf(c46,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as25]) ).
cnf(c47,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as24]) ).
cnf(c48,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as23]) ).
cnf(c49,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as22]) ).
cnf(c50,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as21]) ).
cnf(c51,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as20]) ).
cnf(c52,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as19]) ).
cnf(c53,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as18]) ).
cnf(c54,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))))) != X0,
inference(clausification,[status(esa)],[as17]) ).
cnf(c55,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))))) != X0,
inference(clausification,[status(esa)],[as16]) ).
cnf(c56,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))))) != X0,
inference(clausification,[status(esa)],[as15]) ).
cnf(c57,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))))) != X0,
inference(clausification,[status(esa)],[as14]) ).
cnf(c58,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(X0))))))))))))) != X0,
inference(clausification,[status(esa)],[as13]) ).
cnf(c59,plain,
s(s(s(s(s(s(s(s(s(s(s(s(X0)))))))))))) != X0,
inference(clausification,[status(esa)],[as12]) ).
cnf(c60,plain,
s(s(s(s(s(s(s(s(s(s(s(X0))))))))))) != X0,
inference(clausification,[status(esa)],[as11]) ).
cnf(c61,plain,
s(s(s(s(s(s(s(s(s(s(X0)))))))))) != X0,
inference(clausification,[status(esa)],[as10]) ).
cnf(c62,plain,
s(s(s(s(s(s(s(s(s(X0))))))))) != X0,
inference(clausification,[status(esa)],[as9]) ).
cnf(c63,plain,
s(s(s(s(s(s(s(s(X0)))))))) != X0,
inference(clausification,[status(esa)],[as8]) ).
cnf(c64,plain,
s(s(s(s(s(s(s(X0))))))) != X0,
inference(clausification,[status(esa)],[as7]) ).
cnf(c65,plain,
s(s(s(s(s(s(X0)))))) != X0,
inference(clausification,[status(esa)],[as6]) ).
cnf(c66,plain,
s(s(s(s(s(X0))))) != X0,
inference(clausification,[status(esa)],[as5]) ).
cnf(c67,plain,
s(s(s(s(X0)))) != X0,
inference(clausification,[status(esa)],[as4]) ).
cnf(c68,plain,
s(s(s(X0))) != X0,
inference(clausification,[status(esa)],[as3]) ).
cnf(c69,plain,
s(s(X0)) != X0,
inference(clausification,[status(esa)],[as2]) ).
cnf(c70,plain,
s(X0) != X0,
inference(clausification,[status(esa)],[as1]) ).
cnf(c72,plain,
'earray$u100' = store('earray$u98','index$u99',e21),
inference(clausification,[status(esa)],[hyp1]) ).
cnf(c73,plain,
'earray$u104' = select(q22,seq),
inference(clausification,[status(esa)],[hyp2]) ).
cnf(c74,plain,
'earray$u106' = store('earray$u104','index$u105',e22),
inference(clausification,[status(esa)],[hyp3]) ).
cnf(c75,plain,
'earray$u110' = select(q23,seq),
inference(clausification,[status(esa)],[hyp4]) ).
cnf(c76,plain,
'earray$u112' = store('earray$u110','index$u111',e23),
inference(clausification,[status(esa)],[hyp5]) ).
cnf(c77,plain,
'earray$u119' = select(q24,seq),
inference(clausification,[status(esa)],[hyp6]) ).
cnf(c78,plain,
'earray$u121' = store('earray$u119','index$u120',e24),
inference(clausification,[status(esa)],[hyp7]) ).
cnf(c79,plain,
'earray$u125' = select(q25,seq),
inference(clausification,[status(esa)],[hyp8]) ).
cnf(c80,plain,
'earray$u127' = store('earray$u125','index$u126',e25),
inference(clausification,[status(esa)],[hyp9]) ).
cnf(c81,plain,
'earray$u131' = select(q26,seq),
inference(clausification,[status(esa)],[hyp10]) ).
cnf(c82,plain,
'earray$u133' = store('earray$u131','index$u132',e26),
inference(clausification,[status(esa)],[hyp11]) ).
cnf(c84,plain,
'earray$u140' = select(q27,seq),
inference(clausification,[status(esa)],[hyp13]) ).
cnf(c85,plain,
'earray$u142' = store('earray$u140','index$u141',e27),
inference(clausification,[status(esa)],[hyp14]) ).
cnf(c86,plain,
'earray$u146' = select(q28,seq),
inference(clausification,[status(esa)],[hyp15]) ).
cnf(c87,plain,
'earray$u148' = store('earray$u146','index$u147',e28),
inference(clausification,[status(esa)],[hyp16]) ).
cnf(c91,plain,
'earray$u161' = select(q29,seq),
inference(clausification,[status(esa)],[hyp20]) ).
cnf(c92,plain,
'earray$u163' = store('earray$u161','index$u162',e29),
inference(clausification,[status(esa)],[hyp21]) ).
cnf(c93,plain,
'earray$u170' = select(q30,seq),
inference(clausification,[status(esa)],[hyp22]) ).
cnf(c94,plain,
'earray$u172' = store('earray$u170','index$u171',e30),
inference(clausification,[status(esa)],[hyp23]) ).
cnf(c95,plain,
'earray$u176' = select(q31,seq),
inference(clausification,[status(esa)],[hyp24]) ).
cnf(c96,plain,
'earray$u178' = store('earray$u176','index$u177',e31),
inference(clausification,[status(esa)],[hyp25]) ).
cnf(c97,plain,
'earray$u182' = select(q32,seq),
inference(clausification,[status(esa)],[hyp26]) ).
cnf(c98,plain,
'earray$u184' = store('earray$u182','index$u183',e32),
inference(clausification,[status(esa)],[hyp27]) ).
cnf(c99,plain,
'earray$u191' = select(q33,seq),
inference(clausification,[status(esa)],[hyp28]) ).
cnf(c100,plain,
'earray$u193' = store('earray$u191','index$u192',e33),
inference(clausification,[status(esa)],[hyp29]) ).
cnf(c101,plain,
'earray$u197' = select(q34,seq),
inference(clausification,[status(esa)],[hyp30]) ).
cnf(c102,plain,
'earray$u199' = store('earray$u197','index$u198',e34),
inference(clausification,[status(esa)],[hyp31]) ).
cnf(c105,plain,
'earray$u203' = select(q35,seq),
inference(clausification,[status(esa)],[hyp34]) ).
cnf(c106,plain,
'earray$u205' = store('earray$u203','index$u204',e35),
inference(clausification,[status(esa)],[hyp35]) ).
cnf(c107,plain,
'earray$u212' = select(q36,seq),
inference(clausification,[status(esa)],[hyp36]) ).
cnf(c108,plain,
'earray$u214' = store('earray$u212','index$u213',e36),
inference(clausification,[status(esa)],[hyp37]) ).
cnf(c109,plain,
'earray$u218' = select(q37,seq),
inference(clausification,[status(esa)],[hyp38]) ).
cnf(c111,plain,
'earray$u220' = store('earray$u218','index$u219',e37),
inference(clausification,[status(esa)],[hyp40]) ).
cnf(c112,plain,
'earray$u224' = select(q38,seq),
inference(clausification,[status(esa)],[hyp41]) ).
cnf(c113,plain,
'earray$u226' = store('earray$u224','index$u225',e38),
inference(clausification,[status(esa)],[hyp42]) ).
cnf(c116,plain,
'earray$u239' = select(q39,seq),
inference(clausification,[status(esa)],[hyp45]) ).
cnf(c117,plain,
'earray$u241' = store('earray$u239','index$u240',e39),
inference(clausification,[status(esa)],[hyp46]) ).
cnf(c128,plain,
'earray$u281' = select(q40,seq),
inference(clausification,[status(esa)],[hyp57]) ).
cnf(c132,plain,
'earray$u37' = store('earray$u35','index$u36',e13),
inference(clausification,[status(esa)],[hyp61]) ).
cnf(c134,plain,
'earray$u41' = select(q14,seq),
inference(clausification,[status(esa)],[hyp63]) ).
cnf(c135,plain,
'earray$u43' = store('earray$u41','index$u42',e14),
inference(clausification,[status(esa)],[hyp64]) ).
cnf(c136,plain,
'earray$u50' = select(q15,seq),
inference(clausification,[status(esa)],[hyp65]) ).
cnf(c137,plain,
'earray$u52' = store('earray$u50','index$u51',e15),
inference(clausification,[status(esa)],[hyp66]) ).
cnf(c138,plain,
'earray$u56' = select(q16,seq),
inference(clausification,[status(esa)],[hyp67]) ).
cnf(c139,plain,
'earray$u58' = store('earray$u56','index$u57',e16),
inference(clausification,[status(esa)],[hyp68]) ).
cnf(c140,plain,
'earray$u62' = select(q17,seq),
inference(clausification,[status(esa)],[hyp69]) ).
cnf(c141,plain,
'earray$u64' = store('earray$u62','index$u63',e17),
inference(clausification,[status(esa)],[hyp70]) ).
cnf(c142,plain,
'earray$u71' = select(q18,seq),
inference(clausification,[status(esa)],[hyp71]) ).
cnf(c143,plain,
'earray$u73' = store('earray$u71','index$u72',e18),
inference(clausification,[status(esa)],[hyp72]) ).
cnf(c147,plain,
'earray$u83' = select(q19,seq),
inference(clausification,[status(esa)],[hyp76]) ).
cnf(c148,plain,
'earray$u85' = store('earray$u83','index$u84',e19),
inference(clausification,[status(esa)],[hyp77]) ).
cnf(c149,plain,
'earray$u89' = select(q20,seq),
inference(clausification,[status(esa)],[hyp78]) ).
cnf(c150,plain,
'earray$u91' = store('earray$u89','index$u90',e20),
inference(clausification,[status(esa)],[hyp79]) ).
cnf(c151,plain,
'earray$u98' = select(q21,seq),
inference(clausification,[status(esa)],[hyp80]) ).
cnf(c152,plain,
'elem$u283' = select('earray$u281','index$u282'),
inference(clausification,[status(esa)],[hyp81]) ).
cnf(c153,plain,
'index$u0' = select(q,tail),
inference(clausification,[status(esa)],[hyp82]) ).
cnf(c154,plain,
'index$u102' = s('index$u99'),
inference(clausification,[status(esa)],[hyp83]) ).
cnf(c155,plain,
'index$u105' = select(q22,tail),
inference(clausification,[status(esa)],[hyp84]) ).
cnf(c156,plain,
'index$u108' = s('index$u105'),
inference(clausification,[status(esa)],[hyp85]) ).
cnf(c157,plain,
'index$u111' = select(q23,tail),
inference(clausification,[status(esa)],[hyp86]) ).
cnf(c158,plain,
'index$u114' = s('index$u111'),
inference(clausification,[status(esa)],[hyp87]) ).
cnf(c159,plain,
'index$u116' = select('queue$u115',head),
inference(clausification,[status(esa)],[hyp88]) ).
cnf(c160,plain,
'index$u117' = s('index$u116'),
inference(clausification,[status(esa)],[hyp89]) ).
cnf(c161,plain,
'index$u12' = s('index$u9'),
inference(clausification,[status(esa)],[hyp90]) ).
cnf(c162,plain,
'index$u120' = select(q24,tail),
inference(clausification,[status(esa)],[hyp91]) ).
cnf(c163,plain,
'index$u123' = s('index$u120'),
inference(clausification,[status(esa)],[hyp92]) ).
cnf(c164,plain,
'index$u126' = select(q25,tail),
inference(clausification,[status(esa)],[hyp93]) ).
cnf(c165,plain,
'index$u129' = s('index$u126'),
inference(clausification,[status(esa)],[hyp94]) ).
cnf(c166,plain,
'index$u132' = select(q26,tail),
inference(clausification,[status(esa)],[hyp95]) ).
cnf(c167,plain,
'index$u135' = s('index$u132'),
inference(clausification,[status(esa)],[hyp96]) ).
cnf(c168,plain,
'index$u137' = select('queue$u136',head),
inference(clausification,[status(esa)],[hyp97]) ).
cnf(c169,plain,
'index$u138' = s('index$u137'),
inference(clausification,[status(esa)],[hyp98]) ).
cnf(c170,plain,
'index$u141' = select(q27,tail),
inference(clausification,[status(esa)],[hyp99]) ).
cnf(c171,plain,
'index$u144' = s('index$u141'),
inference(clausification,[status(esa)],[hyp100]) ).
cnf(c172,plain,
'index$u147' = select(q28,tail),
inference(clausification,[status(esa)],[hyp101]) ).
cnf(c173,plain,
'index$u15' = select(q10,tail),
inference(clausification,[status(esa)],[hyp102]) ).
cnf(c174,plain,
'index$u150' = s('index$u147'),
inference(clausification,[status(esa)],[hyp103]) ).
cnf(c175,plain,
'index$u153' = select(q2,tail),
inference(clausification,[status(esa)],[hyp104]) ).
cnf(c176,plain,
'index$u156' = s('index$u153'),
inference(clausification,[status(esa)],[hyp105]) ).
cnf(c177,plain,
'index$u158' = select('queue$u157',head),
inference(clausification,[status(esa)],[hyp106]) ).
cnf(c178,plain,
'index$u159' = s('index$u158'),
inference(clausification,[status(esa)],[hyp107]) ).
cnf(c179,plain,
'index$u162' = select(q29,tail),
inference(clausification,[status(esa)],[hyp108]) ).
cnf(c180,plain,
'index$u165' = s('index$u162'),
inference(clausification,[status(esa)],[hyp109]) ).
cnf(c181,plain,
'index$u167' = select('queue$u166',head),
inference(clausification,[status(esa)],[hyp110]) ).
cnf(c182,plain,
'index$u168' = s('index$u167'),
inference(clausification,[status(esa)],[hyp111]) ).
cnf(c183,plain,
'index$u171' = select(q30,tail),
inference(clausification,[status(esa)],[hyp112]) ).
cnf(c184,plain,
'index$u174' = s('index$u171'),
inference(clausification,[status(esa)],[hyp113]) ).
cnf(c185,plain,
'index$u177' = select(q31,tail),
inference(clausification,[status(esa)],[hyp114]) ).
cnf(c186,plain,
'index$u18' = s('index$u15'),
inference(clausification,[status(esa)],[hyp115]) ).
cnf(c187,plain,
'index$u180' = s('index$u177'),
inference(clausification,[status(esa)],[hyp116]) ).
cnf(c188,plain,
'index$u183' = select(q32,tail),
inference(clausification,[status(esa)],[hyp117]) ).
cnf(c189,plain,
'index$u186' = s('index$u183'),
inference(clausification,[status(esa)],[hyp118]) ).
cnf(c190,plain,
'index$u188' = select('queue$u187',head),
inference(clausification,[status(esa)],[hyp119]) ).
cnf(c191,plain,
'index$u189' = s('index$u188'),
inference(clausification,[status(esa)],[hyp120]) ).
cnf(c192,plain,
'index$u192' = select(q33,tail),
inference(clausification,[status(esa)],[hyp121]) ).
cnf(c193,plain,
'index$u195' = s('index$u192'),
inference(clausification,[status(esa)],[hyp122]) ).
cnf(c194,plain,
'index$u198' = select(q34,tail),
inference(clausification,[status(esa)],[hyp123]) ).
cnf(c195,plain,
'index$u201' = s('index$u198'),
inference(clausification,[status(esa)],[hyp124]) ).
cnf(c196,plain,
'index$u204' = select(q35,tail),
inference(clausification,[status(esa)],[hyp125]) ).
cnf(c197,plain,
'index$u207' = s('index$u204'),
inference(clausification,[status(esa)],[hyp126]) ).
cnf(c198,plain,
'index$u209' = select('queue$u208',head),
inference(clausification,[status(esa)],[hyp127]) ).
cnf(c199,plain,
'index$u21' = select(q11,tail),
inference(clausification,[status(esa)],[hyp128]) ).
cnf(c200,plain,
'index$u210' = s('index$u209'),
inference(clausification,[status(esa)],[hyp129]) ).
cnf(c201,plain,
'index$u213' = select(q36,tail),
inference(clausification,[status(esa)],[hyp130]) ).
cnf(c202,plain,
'index$u216' = s('index$u213'),
inference(clausification,[status(esa)],[hyp131]) ).
cnf(c203,plain,
'index$u219' = select(q37,tail),
inference(clausification,[status(esa)],[hyp132]) ).
cnf(c204,plain,
'index$u222' = s('index$u219'),
inference(clausification,[status(esa)],[hyp133]) ).
cnf(c205,plain,
'index$u225' = select(q38,tail),
inference(clausification,[status(esa)],[hyp134]) ).
cnf(c206,plain,
'index$u228' = s('index$u225'),
inference(clausification,[status(esa)],[hyp135]) ).
cnf(c207,plain,
'index$u230' = select('queue$u229',head),
inference(clausification,[status(esa)],[hyp136]) ).
cnf(c208,plain,
'index$u231' = s('index$u230'),
inference(clausification,[status(esa)],[hyp137]) ).
cnf(c209,plain,
'index$u234' = select(q3,tail),
inference(clausification,[status(esa)],[hyp138]) ).
cnf(c210,plain,
'index$u237' = s('index$u234'),
inference(clausification,[status(esa)],[hyp139]) ).
cnf(c211,plain,
'index$u24' = s('index$u21'),
inference(clausification,[status(esa)],[hyp140]) ).
cnf(c212,plain,
'index$u240' = select(q39,tail),
inference(clausification,[status(esa)],[hyp141]) ).
cnf(c214,plain,
'index$u246' = select(q4,tail),
inference(clausification,[status(esa)],[hyp143]) ).
cnf(c215,plain,
'index$u249' = s('index$u246'),
inference(clausification,[status(esa)],[hyp144]) ).
cnf(c216,plain,
'index$u252' = select(q5,tail),
inference(clausification,[status(esa)],[hyp145]) ).
cnf(c217,plain,
'index$u255' = s('index$u252'),
inference(clausification,[status(esa)],[hyp146]) ).
cnf(c218,plain,
'index$u257' = select('queue$u256',head),
inference(clausification,[status(esa)],[hyp147]) ).
cnf(c219,plain,
'index$u258' = s('index$u257'),
inference(clausification,[status(esa)],[hyp148]) ).
cnf(c220,plain,
'index$u26' = select('queue$u25',head),
inference(clausification,[status(esa)],[hyp149]) ).
cnf(c221,plain,
'index$u261' = select(q6,tail),
inference(clausification,[status(esa)],[hyp150]) ).
cnf(c222,plain,
'index$u264' = s('index$u261'),
inference(clausification,[status(esa)],[hyp151]) ).
cnf(c223,plain,
'index$u267' = select(q7,tail),
inference(clausification,[status(esa)],[hyp152]) ).
cnf(c224,plain,
'index$u27' = s('index$u26'),
inference(clausification,[status(esa)],[hyp153]) ).
cnf(c225,plain,
'index$u270' = s('index$u267'),
inference(clausification,[status(esa)],[hyp154]) ).
cnf(c226,plain,
'index$u273' = select(q8,tail),
inference(clausification,[status(esa)],[hyp155]) ).
cnf(c227,plain,
'index$u276' = s('index$u273'),
inference(clausification,[status(esa)],[hyp156]) ).
cnf(c228,plain,
'index$u278' = select('queue$u277',head),
inference(clausification,[status(esa)],[hyp157]) ).
cnf(c229,plain,
'index$u279' = s('index$u278'),
inference(clausification,[status(esa)],[hyp158]) ).
cnf(c230,plain,
'index$u282' = select(q40,head),
inference(clausification,[status(esa)],[hyp159]) ).
cnf(c231,plain,
'index$u3' = select(q0,tail),
inference(clausification,[status(esa)],[hyp160]) ).
cnf(c232,plain,
'index$u30' = select(q12,tail),
inference(clausification,[status(esa)],[hyp161]) ).
cnf(c233,plain,
'index$u33' = s('index$u30'),
inference(clausification,[status(esa)],[hyp162]) ).
cnf(c234,plain,
'index$u36' = select(q13,tail),
inference(clausification,[status(esa)],[hyp163]) ).
cnf(c235,plain,
'index$u39' = s('index$u36'),
inference(clausification,[status(esa)],[hyp164]) ).
cnf(c236,plain,
'index$u42' = select(q14,tail),
inference(clausification,[status(esa)],[hyp165]) ).
cnf(c237,plain,
'index$u45' = s('index$u42'),
inference(clausification,[status(esa)],[hyp166]) ).
cnf(c238,plain,
'index$u47' = select('queue$u46',head),
inference(clausification,[status(esa)],[hyp167]) ).
cnf(c239,plain,
'index$u48' = s('index$u47'),
inference(clausification,[status(esa)],[hyp168]) ).
cnf(c240,plain,
'index$u51' = select(q15,tail),
inference(clausification,[status(esa)],[hyp169]) ).
cnf(c241,plain,
'index$u54' = s('index$u51'),
inference(clausification,[status(esa)],[hyp170]) ).
cnf(c242,plain,
'index$u57' = select(q16,tail),
inference(clausification,[status(esa)],[hyp171]) ).
cnf(c243,plain,
'index$u6' = s('index$u3'),
inference(clausification,[status(esa)],[hyp172]) ).
cnf(c244,plain,
'index$u60' = s('index$u57'),
inference(clausification,[status(esa)],[hyp173]) ).
cnf(c245,plain,
'index$u63' = select(q17,tail),
inference(clausification,[status(esa)],[hyp174]) ).
cnf(c246,plain,
'index$u66' = s('index$u63'),
inference(clausification,[status(esa)],[hyp175]) ).
cnf(c247,plain,
'index$u68' = select('queue$u67',head),
inference(clausification,[status(esa)],[hyp176]) ).
cnf(c248,plain,
'index$u69' = s('index$u68'),
inference(clausification,[status(esa)],[hyp177]) ).
cnf(c249,plain,
'index$u72' = select(q18,tail),
inference(clausification,[status(esa)],[hyp178]) ).
cnf(c250,plain,
'index$u75' = s('index$u72'),
inference(clausification,[status(esa)],[hyp179]) ).
cnf(c251,plain,
'index$u78' = select(q1,tail),
inference(clausification,[status(esa)],[hyp180]) ).
cnf(c252,plain,
'index$u81' = s('index$u78'),
inference(clausification,[status(esa)],[hyp181]) ).
cnf(c253,plain,
'index$u84' = select(q19,tail),
inference(clausification,[status(esa)],[hyp182]) ).
cnf(c254,plain,
'index$u87' = s('index$u84'),
inference(clausification,[status(esa)],[hyp183]) ).
cnf(c255,plain,
'index$u9' = select(q9,tail),
inference(clausification,[status(esa)],[hyp184]) ).
cnf(c256,plain,
'index$u90' = select(q20,tail),
inference(clausification,[status(esa)],[hyp185]) ).
cnf(c257,plain,
'index$u93' = s('index$u90'),
inference(clausification,[status(esa)],[hyp186]) ).
cnf(c258,plain,
'index$u95' = select('queue$u94',head),
inference(clausification,[status(esa)],[hyp187]) ).
cnf(c259,plain,
'index$u96' = s('index$u95'),
inference(clausification,[status(esa)],[hyp188]) ).
cnf(c260,plain,
'index$u99' = select(q21,tail),
inference(clausification,[status(esa)],[hyp189]) ).
cnf(c261,plain,
'queue$u1' = store(q,head,'index$u0'),
inference(clausification,[status(esa)],[hyp190]) ).
cnf(c262,plain,
'queue$u101' = store(q21,seq,'earray$u100'),
inference(clausification,[status(esa)],[hyp191]) ).
cnf(c263,plain,
'queue$u103' = store('queue$u101',tail,'index$u102'),
inference(clausification,[status(esa)],[hyp192]) ).
cnf(c264,plain,
'queue$u107' = store(q22,seq,'earray$u106'),
inference(clausification,[status(esa)],[hyp193]) ).
cnf(c265,plain,
'queue$u109' = store('queue$u107',tail,'index$u108'),
inference(clausification,[status(esa)],[hyp194]) ).
cnf(c266,plain,
'queue$u11' = store(q9,seq,'earray$u10'),
inference(clausification,[status(esa)],[hyp195]) ).
cnf(c267,plain,
'queue$u113' = store(q23,seq,'earray$u112'),
inference(clausification,[status(esa)],[hyp196]) ).
cnf(c268,plain,
'queue$u115' = store('queue$u113',tail,'index$u114'),
inference(clausification,[status(esa)],[hyp197]) ).
cnf(c269,plain,
'queue$u118' = store('queue$u115',head,'index$u117'),
inference(clausification,[status(esa)],[hyp198]) ).
cnf(c270,plain,
'queue$u122' = store(q24,seq,'earray$u121'),
inference(clausification,[status(esa)],[hyp199]) ).
cnf(c271,plain,
'queue$u124' = store('queue$u122',tail,'index$u123'),
inference(clausification,[status(esa)],[hyp200]) ).
cnf(c272,plain,
'queue$u128' = store(q25,seq,'earray$u127'),
inference(clausification,[status(esa)],[hyp201]) ).
cnf(c273,plain,
'queue$u13' = store('queue$u11',tail,'index$u12'),
inference(clausification,[status(esa)],[hyp202]) ).
cnf(c274,plain,
'queue$u130' = store('queue$u128',tail,'index$u129'),
inference(clausification,[status(esa)],[hyp203]) ).
cnf(c275,plain,
'queue$u134' = store(q26,seq,'earray$u133'),
inference(clausification,[status(esa)],[hyp204]) ).
cnf(c276,plain,
'queue$u136' = store('queue$u134',tail,'index$u135'),
inference(clausification,[status(esa)],[hyp205]) ).
cnf(c277,plain,
'queue$u139' = store('queue$u136',head,'index$u138'),
inference(clausification,[status(esa)],[hyp206]) ).
cnf(c278,plain,
'queue$u143' = store(q27,seq,'earray$u142'),
inference(clausification,[status(esa)],[hyp207]) ).
cnf(c279,plain,
'queue$u145' = store('queue$u143',tail,'index$u144'),
inference(clausification,[status(esa)],[hyp208]) ).
cnf(c280,plain,
'queue$u149' = store(q28,seq,'earray$u148'),
inference(clausification,[status(esa)],[hyp209]) ).
cnf(c281,plain,
'queue$u151' = store('queue$u149',tail,'index$u150'),
inference(clausification,[status(esa)],[hyp210]) ).
cnf(c282,plain,
'queue$u155' = store(q2,seq,'earray$u154'),
inference(clausification,[status(esa)],[hyp211]) ).
cnf(c283,plain,
'queue$u157' = store('queue$u155',tail,'index$u156'),
inference(clausification,[status(esa)],[hyp212]) ).
cnf(c284,plain,
'queue$u160' = store('queue$u157',head,'index$u159'),
inference(clausification,[status(esa)],[hyp213]) ).
cnf(c285,plain,
'queue$u164' = store(q29,seq,'earray$u163'),
inference(clausification,[status(esa)],[hyp214]) ).
cnf(c286,plain,
'queue$u166' = store('queue$u164',tail,'index$u165'),
inference(clausification,[status(esa)],[hyp215]) ).
cnf(c287,plain,
'queue$u169' = store('queue$u166',head,'index$u168'),
inference(clausification,[status(esa)],[hyp216]) ).
cnf(c288,plain,
'queue$u17' = store(q10,seq,'earray$u16'),
inference(clausification,[status(esa)],[hyp217]) ).
cnf(c289,plain,
'queue$u173' = store(q30,seq,'earray$u172'),
inference(clausification,[status(esa)],[hyp218]) ).
cnf(c290,plain,
'queue$u175' = store('queue$u173',tail,'index$u174'),
inference(clausification,[status(esa)],[hyp219]) ).
cnf(c291,plain,
'queue$u179' = store(q31,seq,'earray$u178'),
inference(clausification,[status(esa)],[hyp220]) ).
cnf(c292,plain,
'queue$u181' = store('queue$u179',tail,'index$u180'),
inference(clausification,[status(esa)],[hyp221]) ).
cnf(c293,plain,
'queue$u185' = store(q32,seq,'earray$u184'),
inference(clausification,[status(esa)],[hyp222]) ).
cnf(c294,plain,
'queue$u187' = store('queue$u185',tail,'index$u186'),
inference(clausification,[status(esa)],[hyp223]) ).
cnf(c295,plain,
'queue$u19' = store('queue$u17',tail,'index$u18'),
inference(clausification,[status(esa)],[hyp224]) ).
cnf(c296,plain,
'queue$u190' = store('queue$u187',head,'index$u189'),
inference(clausification,[status(esa)],[hyp225]) ).
cnf(c297,plain,
'queue$u194' = store(q33,seq,'earray$u193'),
inference(clausification,[status(esa)],[hyp226]) ).
cnf(c298,plain,
'queue$u196' = store('queue$u194',tail,'index$u195'),
inference(clausification,[status(esa)],[hyp227]) ).
cnf(c299,plain,
'queue$u200' = store(q34,seq,'earray$u199'),
inference(clausification,[status(esa)],[hyp228]) ).
cnf(c300,plain,
'queue$u202' = store('queue$u200',tail,'index$u201'),
inference(clausification,[status(esa)],[hyp229]) ).
cnf(c301,plain,
'queue$u206' = store(q35,seq,'earray$u205'),
inference(clausification,[status(esa)],[hyp230]) ).
cnf(c302,plain,
'queue$u208' = store('queue$u206',tail,'index$u207'),
inference(clausification,[status(esa)],[hyp231]) ).
cnf(c303,plain,
'queue$u211' = store('queue$u208',head,'index$u210'),
inference(clausification,[status(esa)],[hyp232]) ).
cnf(c304,plain,
'queue$u215' = store(q36,seq,'earray$u214'),
inference(clausification,[status(esa)],[hyp233]) ).
cnf(c305,plain,
'queue$u217' = store('queue$u215',tail,'index$u216'),
inference(clausification,[status(esa)],[hyp234]) ).
cnf(c306,plain,
'queue$u221' = store(q37,seq,'earray$u220'),
inference(clausification,[status(esa)],[hyp235]) ).
cnf(c307,plain,
'queue$u223' = store('queue$u221',tail,'index$u222'),
inference(clausification,[status(esa)],[hyp236]) ).
cnf(c308,plain,
'queue$u227' = store(q38,seq,'earray$u226'),
inference(clausification,[status(esa)],[hyp237]) ).
cnf(c309,plain,
'queue$u229' = store('queue$u227',tail,'index$u228'),
inference(clausification,[status(esa)],[hyp238]) ).
cnf(c310,plain,
'queue$u23' = store(q11,seq,'earray$u22'),
inference(clausification,[status(esa)],[hyp239]) ).
cnf(c311,plain,
'queue$u232' = store('queue$u229',head,'index$u231'),
inference(clausification,[status(esa)],[hyp240]) ).
cnf(c312,plain,
'queue$u236' = store(q3,seq,'earray$u235'),
inference(clausification,[status(esa)],[hyp241]) ).
cnf(c313,plain,
'queue$u238' = store('queue$u236',tail,'index$u237'),
inference(clausification,[status(esa)],[hyp242]) ).
cnf(c314,plain,
'queue$u242' = store(q39,seq,'earray$u241'),
inference(clausification,[status(esa)],[hyp243]) ).
cnf(c315,plain,
'queue$u244' = store('queue$u242',tail,'index$u243'),
inference(clausification,[status(esa)],[hyp244]) ).
cnf(c316,plain,
'queue$u248' = store(q4,seq,'earray$u247'),
inference(clausification,[status(esa)],[hyp245]) ).
cnf(c317,plain,
'queue$u25' = store('queue$u23',tail,'index$u24'),
inference(clausification,[status(esa)],[hyp246]) ).
cnf(c318,plain,
'queue$u250' = store('queue$u248',tail,'index$u249'),
inference(clausification,[status(esa)],[hyp247]) ).
cnf(c319,plain,
'queue$u254' = store(q5,seq,'earray$u253'),
inference(clausification,[status(esa)],[hyp248]) ).
cnf(c320,plain,
'queue$u256' = store('queue$u254',tail,'index$u255'),
inference(clausification,[status(esa)],[hyp249]) ).
cnf(c321,plain,
'queue$u259' = store('queue$u256',head,'index$u258'),
inference(clausification,[status(esa)],[hyp250]) ).
cnf(c322,plain,
'queue$u263' = store(q6,seq,'earray$u262'),
inference(clausification,[status(esa)],[hyp251]) ).
cnf(c323,plain,
'queue$u265' = store('queue$u263',tail,'index$u264'),
inference(clausification,[status(esa)],[hyp252]) ).
cnf(c324,plain,
'queue$u269' = store(q7,seq,'earray$u268'),
inference(clausification,[status(esa)],[hyp253]) ).
cnf(c325,plain,
'queue$u271' = store('queue$u269',tail,'index$u270'),
inference(clausification,[status(esa)],[hyp254]) ).
cnf(c326,plain,
'queue$u275' = store(q8,seq,'earray$u274'),
inference(clausification,[status(esa)],[hyp255]) ).
cnf(c327,plain,
'queue$u277' = store('queue$u275',tail,'index$u276'),
inference(clausification,[status(esa)],[hyp256]) ).
cnf(c328,plain,
'queue$u28' = store('queue$u25',head,'index$u27'),
inference(clausification,[status(esa)],[hyp257]) ).
cnf(c329,plain,
'queue$u280' = store('queue$u277',head,'index$u279'),
inference(clausification,[status(esa)],[hyp258]) ).
cnf(c330,plain,
'queue$u32' = store(q12,seq,'earray$u31'),
inference(clausification,[status(esa)],[hyp259]) ).
cnf(c331,plain,
'queue$u34' = store('queue$u32',tail,'index$u33'),
inference(clausification,[status(esa)],[hyp260]) ).
cnf(c332,plain,
'queue$u38' = store(q13,seq,'earray$u37'),
inference(clausification,[status(esa)],[hyp261]) ).
cnf(c333,plain,
'queue$u40' = store('queue$u38',tail,'index$u39'),
inference(clausification,[status(esa)],[hyp262]) ).
cnf(c334,plain,
'queue$u44' = store(q14,seq,'earray$u43'),
inference(clausification,[status(esa)],[hyp263]) ).
cnf(c335,plain,
'queue$u46' = store('queue$u44',tail,'index$u45'),
inference(clausification,[status(esa)],[hyp264]) ).
cnf(c336,plain,
'queue$u49' = store('queue$u46',head,'index$u48'),
inference(clausification,[status(esa)],[hyp265]) ).
cnf(c337,plain,
'queue$u5' = store(q0,seq,'earray$u4'),
inference(clausification,[status(esa)],[hyp266]) ).
cnf(c338,plain,
'queue$u53' = store(q15,seq,'earray$u52'),
inference(clausification,[status(esa)],[hyp267]) ).
cnf(c339,plain,
'queue$u55' = store('queue$u53',tail,'index$u54'),
inference(clausification,[status(esa)],[hyp268]) ).
cnf(c340,plain,
'queue$u59' = store(q16,seq,'earray$u58'),
inference(clausification,[status(esa)],[hyp269]) ).
cnf(c341,plain,
'queue$u61' = store('queue$u59',tail,'index$u60'),
inference(clausification,[status(esa)],[hyp270]) ).
cnf(c342,plain,
'queue$u65' = store(q17,seq,'earray$u64'),
inference(clausification,[status(esa)],[hyp271]) ).
cnf(c343,plain,
'queue$u67' = store('queue$u65',tail,'index$u66'),
inference(clausification,[status(esa)],[hyp272]) ).
cnf(c344,plain,
'queue$u7' = store('queue$u5',tail,'index$u6'),
inference(clausification,[status(esa)],[hyp273]) ).
cnf(c345,plain,
'queue$u70' = store('queue$u67',head,'index$u69'),
inference(clausification,[status(esa)],[hyp274]) ).
cnf(c346,plain,
'queue$u74' = store(q18,seq,'earray$u73'),
inference(clausification,[status(esa)],[hyp275]) ).
cnf(c347,plain,
'queue$u76' = store('queue$u74',tail,'index$u75'),
inference(clausification,[status(esa)],[hyp276]) ).
cnf(c348,plain,
'queue$u80' = store(q1,seq,'earray$u79'),
inference(clausification,[status(esa)],[hyp277]) ).
cnf(c349,plain,
'queue$u82' = store('queue$u80',tail,'index$u81'),
inference(clausification,[status(esa)],[hyp278]) ).
cnf(c350,plain,
'queue$u86' = store(q19,seq,'earray$u85'),
inference(clausification,[status(esa)],[hyp279]) ).
cnf(c351,plain,
'queue$u88' = store('queue$u86',tail,'index$u87'),
inference(clausification,[status(esa)],[hyp280]) ).
cnf(c352,plain,
'queue$u92' = store(q20,seq,'earray$u91'),
inference(clausification,[status(esa)],[hyp281]) ).
cnf(c353,plain,
'queue$u94' = store('queue$u92',tail,'index$u93'),
inference(clausification,[status(esa)],[hyp282]) ).
cnf(c354,plain,
'queue$u97' = store('queue$u94',head,'index$u96'),
inference(clausification,[status(esa)],[hyp283]) ).
cnf(c355,plain,
q0 = 'queue$u1',
inference(clausification,[status(esa)],[hyp284]) ).
cnf(c356,plain,
q1 = 'queue$u7',
inference(clausification,[status(esa)],[hyp285]) ).
cnf(c357,plain,
q10 = 'queue$u13',
inference(clausification,[status(esa)],[hyp286]) ).
cnf(c358,plain,
q11 = 'queue$u19',
inference(clausification,[status(esa)],[hyp287]) ).
cnf(c359,plain,
q12 = 'queue$u28',
inference(clausification,[status(esa)],[hyp288]) ).
cnf(c360,plain,
q13 = 'queue$u34',
inference(clausification,[status(esa)],[hyp289]) ).
cnf(c361,plain,
q14 = 'queue$u40',
inference(clausification,[status(esa)],[hyp290]) ).
cnf(c362,plain,
q15 = 'queue$u49',
inference(clausification,[status(esa)],[hyp291]) ).
cnf(c363,plain,
q16 = 'queue$u55',
inference(clausification,[status(esa)],[hyp292]) ).
cnf(c364,plain,
q17 = 'queue$u61',
inference(clausification,[status(esa)],[hyp293]) ).
cnf(c365,plain,
q18 = 'queue$u70',
inference(clausification,[status(esa)],[hyp294]) ).
cnf(c366,plain,
q19 = 'queue$u76',
inference(clausification,[status(esa)],[hyp295]) ).
cnf(c367,plain,
q2 = 'queue$u82',
inference(clausification,[status(esa)],[hyp296]) ).
cnf(c368,plain,
q20 = 'queue$u88',
inference(clausification,[status(esa)],[hyp297]) ).
cnf(c369,plain,
q21 = 'queue$u97',
inference(clausification,[status(esa)],[hyp298]) ).
cnf(c370,plain,
q22 = 'queue$u103',
inference(clausification,[status(esa)],[hyp299]) ).
cnf(c371,plain,
q23 = 'queue$u109',
inference(clausification,[status(esa)],[hyp300]) ).
cnf(c372,plain,
q24 = 'queue$u118',
inference(clausification,[status(esa)],[hyp301]) ).
cnf(c373,plain,
q25 = 'queue$u124',
inference(clausification,[status(esa)],[hyp302]) ).
cnf(c374,plain,
q26 = 'queue$u130',
inference(clausification,[status(esa)],[hyp303]) ).
cnf(c375,plain,
q27 = 'queue$u139',
inference(clausification,[status(esa)],[hyp304]) ).
cnf(c376,plain,
q28 = 'queue$u145',
inference(clausification,[status(esa)],[hyp305]) ).
cnf(c377,plain,
q29 = 'queue$u151',
inference(clausification,[status(esa)],[hyp306]) ).
cnf(c378,plain,
q3 = 'queue$u160',
inference(clausification,[status(esa)],[hyp307]) ).
cnf(c379,plain,
q30 = 'queue$u169',
inference(clausification,[status(esa)],[hyp308]) ).
cnf(c380,plain,
q31 = 'queue$u175',
inference(clausification,[status(esa)],[hyp309]) ).
cnf(c381,plain,
q32 = 'queue$u181',
inference(clausification,[status(esa)],[hyp310]) ).
cnf(c382,plain,
q33 = 'queue$u190',
inference(clausification,[status(esa)],[hyp311]) ).
cnf(c383,plain,
q34 = 'queue$u196',
inference(clausification,[status(esa)],[hyp312]) ).
cnf(c384,plain,
q35 = 'queue$u202',
inference(clausification,[status(esa)],[hyp313]) ).
cnf(c385,plain,
q36 = 'queue$u211',
inference(clausification,[status(esa)],[hyp314]) ).
cnf(c386,plain,
q37 = 'queue$u217',
inference(clausification,[status(esa)],[hyp315]) ).
cnf(c387,plain,
q38 = 'queue$u223',
inference(clausification,[status(esa)],[hyp316]) ).
cnf(c388,plain,
q39 = 'queue$u232',
inference(clausification,[status(esa)],[hyp317]) ).
cnf(c389,plain,
q4 = 'queue$u238',
inference(clausification,[status(esa)],[hyp318]) ).
cnf(c390,plain,
q40 = 'queue$u244',
inference(clausification,[status(esa)],[hyp319]) ).
cnf(c391,plain,
q5 = 'queue$u250',
inference(clausification,[status(esa)],[hyp320]) ).
cnf(c392,plain,
q6 = 'queue$u259',
inference(clausification,[status(esa)],[hyp321]) ).
cnf(c393,plain,
q7 = 'queue$u265',
inference(clausification,[status(esa)],[hyp322]) ).
cnf(c394,plain,
q8 = 'queue$u271',
inference(clausification,[status(esa)],[hyp323]) ).
cnf(c395,plain,
q9 = 'queue$u280',
inference(clausification,[status(esa)],[hyp324]) ).
cnf(c396,plain,
'elem$u283' != e13,
inference(clausification,[status(esa)],[goal]) ).
cnf(d0,plain,
( 'index$u99' = X0
| select('earray$u100',X0) = select('earray$u98',X0) ),
inference(superposition,[status(thm)],[c72,c1]) ).
cnf(d1,plain,
select('earray$u37','index$u36') = e13,
inference(superposition,[status(thm)],[c132,c0]) ).
cnf(d2,plain,
select('queue$u38',seq) = 'earray$u37',
inference(superposition,[status(thm)],[c332,c0]) ).
cnf(d3,plain,
q14 = store('queue$u38',tail,'index$u39'),
inference(demodulation,[status(thm)],[c333,c361]) ).
cnf(d4,plain,
( tail = X0
| select(q14,X0) = select('queue$u38',X0) ),
inference(superposition,[status(thm)],[d3,c1]) ).
cnf(d5,plain,
( tail = seq
| select(q14,seq) = 'earray$u37' ),
inference(superposition,[status(thm)],[d4,d2]) ).
cnf(d6,plain,
( tail = seq
| 'earray$u41' = 'earray$u37' ),
inference(demodulation,[status(thm)],[d5,c134]) ).
cnf(d7,plain,
'earray$u41' = 'earray$u37',
inference(resolution,[status(thm)],[c4,d6]) ).
cnf(d8,plain,
( 'index$u42' = X0
| select('earray$u43',X0) = select('earray$u41',X0) ),
inference(superposition,[status(thm)],[c135,c1]) ).
cnf(d9,plain,
( 'index$u42' = X0
| select('earray$u43',X0) = select('earray$u37',X0) ),
inference(demodulation,[status(thm)],[d8,d7]) ).
cnf(d10,plain,
select('queue$u44',seq) = 'earray$u43',
inference(superposition,[status(thm)],[c334,c0]) ).
cnf(d11,plain,
( tail = X0
| select('queue$u46',X0) = select('queue$u44',X0) ),
inference(superposition,[status(thm)],[c335,c1]) ).
cnf(d12,plain,
( tail = seq
| select('queue$u46',seq) = 'earray$u43' ),
inference(superposition,[status(thm)],[d11,d10]) ).
cnf(d13,plain,
select('queue$u46',seq) = 'earray$u43',
inference(resolution,[status(thm)],[c4,d12]) ).
cnf(d14,plain,
q15 = store('queue$u46',head,'index$u48'),
inference(demodulation,[status(thm)],[c336,c362]) ).
cnf(d15,plain,
( head = X0
| select(q15,X0) = select('queue$u46',X0) ),
inference(superposition,[status(thm)],[d14,c1]) ).
cnf(d16,plain,
( head = seq
| select(q15,seq) = 'earray$u43' ),
inference(superposition,[status(thm)],[d15,d13]) ).
cnf(d17,plain,
( head = seq
| 'earray$u50' = 'earray$u43' ),
inference(demodulation,[status(thm)],[d16,c136]) ).
cnf(d18,plain,
'earray$u50' = 'earray$u43',
inference(resolution,[status(thm)],[c3,d17]) ).
cnf(d19,plain,
( 'index$u51' = X0
| select('earray$u52',X0) = select('earray$u50',X0) ),
inference(superposition,[status(thm)],[c137,c1]) ).
cnf(d20,plain,
( 'index$u51' = X0
| select('earray$u52',X0) = select('earray$u43',X0) ),
inference(demodulation,[status(thm)],[d19,d18]) ).
cnf(d21,plain,
select('queue$u53',seq) = 'earray$u52',
inference(superposition,[status(thm)],[c338,c0]) ).
cnf(d22,plain,
q16 = store('queue$u53',tail,'index$u54'),
inference(demodulation,[status(thm)],[c339,c363]) ).
cnf(d23,plain,
( tail = X0
| select(q16,X0) = select('queue$u53',X0) ),
inference(superposition,[status(thm)],[d22,c1]) ).
cnf(d24,plain,
( tail = seq
| select(q16,seq) = 'earray$u52' ),
inference(superposition,[status(thm)],[d23,d21]) ).
cnf(d25,plain,
( tail = seq
| 'earray$u56' = 'earray$u52' ),
inference(demodulation,[status(thm)],[d24,c138]) ).
cnf(d26,plain,
'earray$u56' = 'earray$u52',
inference(resolution,[status(thm)],[c4,d25]) ).
cnf(d27,plain,
( 'index$u57' = X0
| select('earray$u58',X0) = select('earray$u56',X0) ),
inference(superposition,[status(thm)],[c139,c1]) ).
cnf(d28,plain,
( 'index$u57' = X0
| select('earray$u58',X0) = select('earray$u52',X0) ),
inference(demodulation,[status(thm)],[d27,d26]) ).
cnf(d29,plain,
select('queue$u59',seq) = 'earray$u58',
inference(superposition,[status(thm)],[c340,c0]) ).
cnf(d30,plain,
q17 = store('queue$u59',tail,'index$u60'),
inference(demodulation,[status(thm)],[c341,c364]) ).
cnf(d31,plain,
( tail = X0
| select(q17,X0) = select('queue$u59',X0) ),
inference(superposition,[status(thm)],[d30,c1]) ).
cnf(d32,plain,
( tail = seq
| select(q17,seq) = 'earray$u58' ),
inference(superposition,[status(thm)],[d31,d29]) ).
cnf(d33,plain,
( tail = seq
| 'earray$u62' = 'earray$u58' ),
inference(demodulation,[status(thm)],[d32,c140]) ).
cnf(d34,plain,
'earray$u62' = 'earray$u58',
inference(resolution,[status(thm)],[c4,d33]) ).
cnf(d35,plain,
( 'index$u63' = X0
| select('earray$u64',X0) = select('earray$u62',X0) ),
inference(superposition,[status(thm)],[c141,c1]) ).
cnf(d36,plain,
( 'index$u63' = X0
| select('earray$u64',X0) = select('earray$u58',X0) ),
inference(demodulation,[status(thm)],[d35,d34]) ).
cnf(d37,plain,
select('queue$u65',seq) = 'earray$u64',
inference(superposition,[status(thm)],[c342,c0]) ).
cnf(d38,plain,
( tail = X0
| select('queue$u67',X0) = select('queue$u65',X0) ),
inference(superposition,[status(thm)],[c343,c1]) ).
cnf(d39,plain,
( tail = seq
| select('queue$u67',seq) = 'earray$u64' ),
inference(superposition,[status(thm)],[d38,d37]) ).
cnf(d40,plain,
select('queue$u67',seq) = 'earray$u64',
inference(resolution,[status(thm)],[c4,d39]) ).
cnf(d41,plain,
q18 = store('queue$u67',head,'index$u69'),
inference(demodulation,[status(thm)],[c345,c365]) ).
cnf(d42,plain,
( head = X0
| select(q18,X0) = select('queue$u67',X0) ),
inference(superposition,[status(thm)],[d41,c1]) ).
cnf(d43,plain,
( head = seq
| select(q18,seq) = 'earray$u64' ),
inference(superposition,[status(thm)],[d42,d40]) ).
cnf(d44,plain,
( head = seq
| 'earray$u71' = 'earray$u64' ),
inference(demodulation,[status(thm)],[d43,c142]) ).
cnf(d45,plain,
'earray$u71' = 'earray$u64',
inference(resolution,[status(thm)],[c3,d44]) ).
cnf(d46,plain,
( 'index$u72' = X0
| select('earray$u73',X0) = select('earray$u71',X0) ),
inference(superposition,[status(thm)],[c143,c1]) ).
cnf(d47,plain,
( 'index$u72' = X0
| select('earray$u73',X0) = select('earray$u64',X0) ),
inference(demodulation,[status(thm)],[d46,d45]) ).
cnf(d48,plain,
select('queue$u74',seq) = 'earray$u73',
inference(superposition,[status(thm)],[c346,c0]) ).
cnf(d49,plain,
q19 = store('queue$u74',tail,'index$u75'),
inference(demodulation,[status(thm)],[c347,c366]) ).
cnf(d50,plain,
( tail = X0
| select(q19,X0) = select('queue$u74',X0) ),
inference(superposition,[status(thm)],[d49,c1]) ).
cnf(d51,plain,
( tail = seq
| select(q19,seq) = 'earray$u73' ),
inference(superposition,[status(thm)],[d50,d48]) ).
cnf(d52,plain,
( tail = seq
| 'earray$u83' = 'earray$u73' ),
inference(demodulation,[status(thm)],[d51,c147]) ).
cnf(d53,plain,
'earray$u83' = 'earray$u73',
inference(resolution,[status(thm)],[c4,d52]) ).
cnf(d54,plain,
( 'index$u84' = X0
| select('earray$u85',X0) = select('earray$u83',X0) ),
inference(superposition,[status(thm)],[c148,c1]) ).
cnf(d55,plain,
( 'index$u84' = X0
| select('earray$u85',X0) = select('earray$u73',X0) ),
inference(demodulation,[status(thm)],[d54,d53]) ).
cnf(d56,plain,
select('queue$u92',seq) = 'earray$u91',
inference(superposition,[status(thm)],[c352,c0]) ).
cnf(d57,plain,
( tail = X0
| select('queue$u94',X0) = select('queue$u92',X0) ),
inference(superposition,[status(thm)],[c353,c1]) ).
cnf(d58,plain,
( tail = seq
| select('queue$u94',seq) = 'earray$u91' ),
inference(superposition,[status(thm)],[d57,d56]) ).
cnf(d59,plain,
select('queue$u94',seq) = 'earray$u91',
inference(resolution,[status(thm)],[c4,d58]) ).
cnf(d60,plain,
q21 = store('queue$u94',head,'index$u96'),
inference(demodulation,[status(thm)],[c354,c369]) ).
cnf(d61,plain,
( head = X0
| select(q21,X0) = select('queue$u94',X0) ),
inference(superposition,[status(thm)],[d60,c1]) ).
cnf(d62,plain,
( head = seq
| select(q21,seq) = 'earray$u91' ),
inference(superposition,[status(thm)],[d61,d59]) ).
cnf(d63,plain,
( head = seq
| 'earray$u98' = 'earray$u91' ),
inference(demodulation,[status(thm)],[d62,c151]) ).
cnf(d64,plain,
'earray$u98' = 'earray$u91',
inference(resolution,[status(thm)],[c3,d63]) ).
cnf(d65,plain,
select('queue$u86',seq) = 'earray$u85',
inference(superposition,[status(thm)],[c350,c0]) ).
cnf(d66,plain,
q20 = store('queue$u86',tail,'index$u87'),
inference(demodulation,[status(thm)],[c351,c368]) ).
cnf(d67,plain,
( tail = X0
| select(q20,X0) = select('queue$u86',X0) ),
inference(superposition,[status(thm)],[d66,c1]) ).
cnf(d68,plain,
( tail = seq
| select(q20,seq) = 'earray$u85' ),
inference(superposition,[status(thm)],[d67,d65]) ).
cnf(d69,plain,
( tail = seq
| 'earray$u89' = 'earray$u85' ),
inference(demodulation,[status(thm)],[d68,c149]) ).
cnf(d70,plain,
'earray$u89' = 'earray$u85',
inference(resolution,[status(thm)],[c4,d69]) ).
cnf(d71,plain,
( 'index$u90' = X0
| select('earray$u91',X0) = select('earray$u89',X0) ),
inference(superposition,[status(thm)],[c150,c1]) ).
cnf(d72,plain,
( 'index$u90' = X0
| select('earray$u91',X0) = select('earray$u85',X0) ),
inference(demodulation,[status(thm)],[d71,d70]) ).
cnf(d73,plain,
( 'index$u90' = X0
| select('earray$u98',X0) = select('earray$u85',X0) ),
inference(demodulation,[status(thm)],[d72,d64]) ).
cnf(d74,plain,
( 'index$u90' = X0
| 'index$u84' = X0
| select('earray$u98',X0) = select('earray$u73',X0) ),
inference(superposition,[status(thm)],[d73,d55]) ).
cnf(d75,plain,
( 'index$u90' = X0
| 'index$u84' = X0
| 'index$u72' = X0
| select('earray$u98',X0) = select('earray$u64',X0) ),
inference(superposition,[status(thm)],[d74,d47]) ).
cnf(d76,plain,
( 'index$u90' = X0
| 'index$u84' = X0
| 'index$u72' = X0
| 'index$u63' = X0
| select('earray$u98',X0) = select('earray$u58',X0) ),
inference(superposition,[status(thm)],[d75,d36]) ).
cnf(d77,plain,
( 'index$u90' = X0
| 'index$u84' = X0
| 'index$u72' = X0
| 'index$u63' = X0
| 'index$u57' = X0
| select('earray$u98',X0) = select('earray$u52',X0) ),
inference(superposition,[status(thm)],[d76,d28]) ).
cnf(d78,plain,
( 'index$u90' = X0
| 'index$u84' = X0
| 'index$u72' = X0
| 'index$u63' = X0
| 'index$u57' = X0
| 'index$u51' = X0
| select('earray$u98',X0) = select('earray$u43',X0) ),
inference(superposition,[status(thm)],[d77,d20]) ).
cnf(d79,plain,
( 'index$u90' = X0
| 'index$u84' = X0
| 'index$u72' = X0
| 'index$u63' = X0
| 'index$u57' = X0
| 'index$u51' = X0
| 'index$u42' = X0
| select('earray$u98',X0) = select('earray$u37',X0) ),
inference(superposition,[status(thm)],[d78,d9]) ).
cnf(d80,plain,
( 'index$u90' = 'index$u36'
| 'index$u84' = 'index$u36'
| 'index$u72' = 'index$u36'
| 'index$u63' = 'index$u36'
| 'index$u57' = 'index$u36'
| 'index$u51' = 'index$u36'
| 'index$u42' = 'index$u36'
| select('earray$u98','index$u36') = e13 ),
inference(superposition,[status(thm)],[d79,d1]) ).
cnf(d81,plain,
select(q17,tail) = 'index$u60',
inference(superposition,[status(thm)],[d30,c0]) ).
cnf(d82,plain,
'index$u63' = 'index$u60',
inference(demodulation,[status(thm)],[d81,c245]) ).
cnf(d83,plain,
'index$u63' = s('index$u57'),
inference(demodulation,[status(thm)],[c244,d82]) ).
cnf(d84,plain,
select(q16,tail) = 'index$u54',
inference(superposition,[status(thm)],[d22,c0]) ).
cnf(d85,plain,
'index$u57' = 'index$u54',
inference(demodulation,[status(thm)],[d84,c242]) ).
cnf(d86,plain,
'index$u57' = s('index$u51'),
inference(demodulation,[status(thm)],[c241,d85]) ).
cnf(d87,plain,
select('queue$u46',tail) = 'index$u45',
inference(superposition,[status(thm)],[c335,c0]) ).
cnf(d88,plain,
( head = tail
| select(q15,tail) = 'index$u45' ),
inference(superposition,[status(thm)],[d15,d87]) ).
cnf(d89,plain,
( head = tail
| 'index$u51' = 'index$u45' ),
inference(demodulation,[status(thm)],[d88,c240]) ).
cnf(d90,plain,
'index$u51' = 'index$u45',
inference(resolution,[status(thm)],[c2,d89]) ).
cnf(d91,plain,
select(q14,tail) = 'index$u39',
inference(superposition,[status(thm)],[d3,c0]) ).
cnf(d92,plain,
'index$u42' = 'index$u39',
inference(demodulation,[status(thm)],[d91,c236]) ).
cnf(d93,plain,
'index$u42' = s('index$u36'),
inference(demodulation,[status(thm)],[c235,d92]) ).
cnf(d94,plain,
s(s(s('index$u42'))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c67]) ).
cnf(d95,plain,
s(s('index$u45')) != 'index$u36',
inference(demodulation,[status(thm)],[d94,c237]) ).
cnf(d96,plain,
s(s('index$u51')) != 'index$u36',
inference(demodulation,[status(thm)],[d95,d90]) ).
cnf(d97,plain,
s('index$u57') != 'index$u36',
inference(demodulation,[status(thm)],[d96,d86]) ).
cnf(d98,plain,
'index$u63' != 'index$u36',
inference(demodulation,[status(thm)],[d97,d83]) ).
cnf(d99,plain,
( 'index$u90' = 'index$u36'
| 'index$u84' = 'index$u36'
| 'index$u72' = 'index$u36'
| 'index$u57' = 'index$u36'
| 'index$u51' = 'index$u36'
| 'index$u42' = 'index$u36'
| select('earray$u98','index$u36') = e13 ),
inference(resolution,[status(thm)],[d98,d80]) ).
cnf(d100,plain,
'index$u39' != 'index$u36',
inference(superposition,[status(thm)],[c235,c70]) ).
cnf(d101,plain,
'index$u42' != 'index$u36',
inference(demodulation,[status(thm)],[d100,d92]) ).
cnf(d102,plain,
( 'index$u90' = 'index$u36'
| 'index$u84' = 'index$u36'
| 'index$u72' = 'index$u36'
| 'index$u57' = 'index$u36'
| 'index$u51' = 'index$u36'
| select('earray$u98','index$u36') = e13 ),
inference(resolution,[status(thm)],[d101,d99]) ).
cnf(d103,plain,
select(q20,tail) = 'index$u87',
inference(superposition,[status(thm)],[d66,c0]) ).
cnf(d104,plain,
'index$u90' = 'index$u87',
inference(demodulation,[status(thm)],[d103,c256]) ).
cnf(d105,plain,
'index$u90' = s('index$u84'),
inference(demodulation,[status(thm)],[c254,d104]) ).
cnf(d106,plain,
select(q19,tail) = 'index$u75',
inference(superposition,[status(thm)],[d49,c0]) ).
cnf(d107,plain,
'index$u84' = 'index$u75',
inference(demodulation,[status(thm)],[d106,c253]) ).
cnf(d108,plain,
'index$u84' = s('index$u72'),
inference(demodulation,[status(thm)],[c250,d107]) ).
cnf(d109,plain,
select('queue$u67',tail) = 'index$u66',
inference(superposition,[status(thm)],[c343,c0]) ).
cnf(d110,plain,
( head = tail
| select(q18,tail) = 'index$u66' ),
inference(superposition,[status(thm)],[d42,d109]) ).
cnf(d111,plain,
( head = tail
| 'index$u72' = 'index$u66' ),
inference(demodulation,[status(thm)],[d110,c249]) ).
cnf(d112,plain,
'index$u72' = 'index$u66',
inference(resolution,[status(thm)],[c2,d111]) ).
cnf(d113,plain,
s(s(s(s(s(s('index$u42')))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c64]) ).
cnf(d114,plain,
s(s(s(s(s('index$u45'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d113,c237]) ).
cnf(d115,plain,
s(s(s(s(s('index$u51'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d114,d90]) ).
cnf(d116,plain,
s(s(s(s('index$u57')))) != 'index$u36',
inference(demodulation,[status(thm)],[d115,d86]) ).
cnf(d117,plain,
s(s(s('index$u63'))) != 'index$u36',
inference(demodulation,[status(thm)],[d116,d83]) ).
cnf(d118,plain,
s(s('index$u66')) != 'index$u36',
inference(demodulation,[status(thm)],[d117,c246]) ).
cnf(d119,plain,
s(s('index$u72')) != 'index$u36',
inference(demodulation,[status(thm)],[d118,d112]) ).
cnf(d120,plain,
s('index$u84') != 'index$u36',
inference(demodulation,[status(thm)],[d119,d108]) ).
cnf(d121,plain,
'index$u90' != 'index$u36',
inference(demodulation,[status(thm)],[d120,d105]) ).
cnf(d122,plain,
( 'index$u84' = 'index$u36'
| 'index$u72' = 'index$u36'
| 'index$u57' = 'index$u36'
| 'index$u51' = 'index$u36'
| select('earray$u98','index$u36') = e13 ),
inference(resolution,[status(thm)],[d121,d102]) ).
cnf(d123,plain,
s('index$u39') != 'index$u36',
inference(superposition,[status(thm)],[c235,c69]) ).
cnf(d124,plain,
s('index$u42') != 'index$u36',
inference(demodulation,[status(thm)],[d123,d92]) ).
cnf(d125,plain,
'index$u45' != 'index$u36',
inference(demodulation,[status(thm)],[d124,c237]) ).
cnf(d126,plain,
'index$u51' != 'index$u36',
inference(demodulation,[status(thm)],[d125,d90]) ).
cnf(d127,plain,
( 'index$u84' = 'index$u36'
| 'index$u72' = 'index$u36'
| 'index$u57' = 'index$u36'
| select('earray$u98','index$u36') = e13 ),
inference(resolution,[status(thm)],[d126,d122]) ).
cnf(d128,plain,
s(s('index$u39')) != 'index$u36',
inference(superposition,[status(thm)],[c235,c68]) ).
cnf(d129,plain,
s(s('index$u42')) != 'index$u36',
inference(demodulation,[status(thm)],[d128,d92]) ).
cnf(d130,plain,
s('index$u45') != 'index$u36',
inference(demodulation,[status(thm)],[d129,c237]) ).
cnf(d131,plain,
s('index$u51') != 'index$u36',
inference(demodulation,[status(thm)],[d130,d90]) ).
cnf(d132,plain,
'index$u57' != 'index$u36',
inference(demodulation,[status(thm)],[d131,d86]) ).
cnf(d133,plain,
( 'index$u84' = 'index$u36'
| 'index$u72' = 'index$u36'
| select('earray$u98','index$u36') = e13 ),
inference(resolution,[status(thm)],[d132,d127]) ).
cnf(d134,plain,
s(s(s(s('index$u42')))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c66]) ).
cnf(d135,plain,
s(s(s('index$u45'))) != 'index$u36',
inference(demodulation,[status(thm)],[d134,c237]) ).
cnf(d136,plain,
s(s(s('index$u51'))) != 'index$u36',
inference(demodulation,[status(thm)],[d135,d90]) ).
cnf(d137,plain,
s(s('index$u57')) != 'index$u36',
inference(demodulation,[status(thm)],[d136,d86]) ).
cnf(d138,plain,
s('index$u63') != 'index$u36',
inference(demodulation,[status(thm)],[d137,d83]) ).
cnf(d139,plain,
'index$u66' != 'index$u36',
inference(demodulation,[status(thm)],[d138,c246]) ).
cnf(d140,plain,
'index$u72' != 'index$u36',
inference(demodulation,[status(thm)],[d139,d112]) ).
cnf(d141,plain,
( 'index$u84' = 'index$u36'
| select('earray$u98','index$u36') = e13 ),
inference(resolution,[status(thm)],[d140,d133]) ).
cnf(d142,plain,
s(s(s(s(s('index$u42'))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c65]) ).
cnf(d143,plain,
s(s(s(s('index$u45')))) != 'index$u36',
inference(demodulation,[status(thm)],[d142,c237]) ).
cnf(d144,plain,
s(s(s(s('index$u51')))) != 'index$u36',
inference(demodulation,[status(thm)],[d143,d90]) ).
cnf(d145,plain,
s(s(s('index$u57'))) != 'index$u36',
inference(demodulation,[status(thm)],[d144,d86]) ).
cnf(d146,plain,
s(s('index$u63')) != 'index$u36',
inference(demodulation,[status(thm)],[d145,d83]) ).
cnf(d147,plain,
s('index$u66') != 'index$u36',
inference(demodulation,[status(thm)],[d146,c246]) ).
cnf(d148,plain,
s('index$u72') != 'index$u36',
inference(demodulation,[status(thm)],[d147,d112]) ).
cnf(d149,plain,
'index$u84' != 'index$u36',
inference(demodulation,[status(thm)],[d148,d108]) ).
cnf(d150,plain,
select('earray$u98','index$u36') = e13,
inference(resolution,[status(thm)],[d149,d141]) ).
cnf(d151,plain,
( 'index$u99' = 'index$u36'
| select('earray$u100','index$u36') = e13 ),
inference(superposition,[status(thm)],[d150,d0]) ).
cnf(d152,plain,
select('queue$u94',tail) = 'index$u93',
inference(superposition,[status(thm)],[c353,c0]) ).
cnf(d153,plain,
( head = tail
| select(q21,tail) = 'index$u93' ),
inference(superposition,[status(thm)],[d61,d152]) ).
cnf(d154,plain,
( head = tail
| 'index$u99' = 'index$u93' ),
inference(demodulation,[status(thm)],[d153,c260]) ).
cnf(d155,plain,
'index$u99' = 'index$u93',
inference(resolution,[status(thm)],[c2,d154]) ).
cnf(d156,plain,
'index$u99' = s('index$u90'),
inference(demodulation,[status(thm)],[c257,d155]) ).
cnf(d157,plain,
'index$u72' = s('index$u63'),
inference(demodulation,[status(thm)],[c246,d112]) ).
cnf(d158,plain,
'index$u51' = s('index$u42'),
inference(demodulation,[status(thm)],[c237,d90]) ).
cnf(d159,plain,
s(s(s(s(s(s(s('index$u42'))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c63]) ).
cnf(d160,plain,
s(s(s(s(s(s('index$u51')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d159,d158]) ).
cnf(d161,plain,
s(s(s(s(s('index$u57'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d160,d86]) ).
cnf(d162,plain,
s(s(s(s('index$u63')))) != 'index$u36',
inference(demodulation,[status(thm)],[d161,d83]) ).
cnf(d163,plain,
s(s(s('index$u72'))) != 'index$u36',
inference(demodulation,[status(thm)],[d162,d157]) ).
cnf(d164,plain,
s(s('index$u84')) != 'index$u36',
inference(demodulation,[status(thm)],[d163,d108]) ).
cnf(d165,plain,
s('index$u90') != 'index$u36',
inference(demodulation,[status(thm)],[d164,d105]) ).
cnf(d166,plain,
'index$u99' != 'index$u36',
inference(demodulation,[status(thm)],[d165,d156]) ).
cnf(d167,plain,
select('earray$u100','index$u36') = e13,
inference(resolution,[status(thm)],[d166,d151]) ).
cnf(d168,plain,
select('queue$u101',seq) = 'earray$u100',
inference(superposition,[status(thm)],[c262,c0]) ).
cnf(d169,plain,
q22 = store('queue$u101',tail,'index$u102'),
inference(demodulation,[status(thm)],[c263,c370]) ).
cnf(d170,plain,
( tail = X0
| select(q22,X0) = select('queue$u101',X0) ),
inference(superposition,[status(thm)],[d169,c1]) ).
cnf(d171,plain,
( tail = seq
| select(q22,seq) = 'earray$u100' ),
inference(superposition,[status(thm)],[d170,d168]) ).
cnf(d172,plain,
( tail = seq
| 'earray$u104' = 'earray$u100' ),
inference(demodulation,[status(thm)],[d171,c73]) ).
cnf(d173,plain,
'earray$u104' = 'earray$u100',
inference(resolution,[status(thm)],[c4,d172]) ).
cnf(d174,plain,
( 'index$u105' = X0
| select('earray$u106',X0) = select('earray$u104',X0) ),
inference(superposition,[status(thm)],[c74,c1]) ).
cnf(d175,plain,
( 'index$u105' = X0
| select('earray$u106',X0) = select('earray$u100',X0) ),
inference(demodulation,[status(thm)],[d174,d173]) ).
cnf(d176,plain,
select('queue$u107',seq) = 'earray$u106',
inference(superposition,[status(thm)],[c264,c0]) ).
cnf(d177,plain,
q23 = store('queue$u107',tail,'index$u108'),
inference(demodulation,[status(thm)],[c265,c371]) ).
cnf(d178,plain,
( tail = X0
| select(q23,X0) = select('queue$u107',X0) ),
inference(superposition,[status(thm)],[d177,c1]) ).
cnf(d179,plain,
( tail = seq
| select(q23,seq) = 'earray$u106' ),
inference(superposition,[status(thm)],[d178,d176]) ).
cnf(d180,plain,
( tail = seq
| 'earray$u110' = 'earray$u106' ),
inference(demodulation,[status(thm)],[d179,c75]) ).
cnf(d181,plain,
'earray$u110' = 'earray$u106',
inference(resolution,[status(thm)],[c4,d180]) ).
cnf(d182,plain,
( 'index$u111' = X0
| select('earray$u112',X0) = select('earray$u110',X0) ),
inference(superposition,[status(thm)],[c76,c1]) ).
cnf(d183,plain,
( 'index$u111' = X0
| select('earray$u112',X0) = select('earray$u106',X0) ),
inference(demodulation,[status(thm)],[d182,d181]) ).
cnf(d184,plain,
select('queue$u113',seq) = 'earray$u112',
inference(superposition,[status(thm)],[c267,c0]) ).
cnf(d185,plain,
( tail = X0
| select('queue$u115',X0) = select('queue$u113',X0) ),
inference(superposition,[status(thm)],[c268,c1]) ).
cnf(d186,plain,
( tail = seq
| select('queue$u115',seq) = 'earray$u112' ),
inference(superposition,[status(thm)],[d185,d184]) ).
cnf(d187,plain,
select('queue$u115',seq) = 'earray$u112',
inference(resolution,[status(thm)],[c4,d186]) ).
cnf(d188,plain,
q24 = store('queue$u115',head,'index$u117'),
inference(demodulation,[status(thm)],[c269,c372]) ).
cnf(d189,plain,
( head = X0
| select(q24,X0) = select('queue$u115',X0) ),
inference(superposition,[status(thm)],[d188,c1]) ).
cnf(d190,plain,
( head = seq
| select(q24,seq) = 'earray$u112' ),
inference(superposition,[status(thm)],[d189,d187]) ).
cnf(d191,plain,
( head = seq
| 'earray$u119' = 'earray$u112' ),
inference(demodulation,[status(thm)],[d190,c77]) ).
cnf(d192,plain,
'earray$u119' = 'earray$u112',
inference(resolution,[status(thm)],[c3,d191]) ).
cnf(d193,plain,
( 'index$u120' = X0
| select('earray$u121',X0) = select('earray$u119',X0) ),
inference(superposition,[status(thm)],[c78,c1]) ).
cnf(d194,plain,
( 'index$u120' = X0
| select('earray$u121',X0) = select('earray$u112',X0) ),
inference(demodulation,[status(thm)],[d193,d192]) ).
cnf(d195,plain,
select('queue$u122',seq) = 'earray$u121',
inference(superposition,[status(thm)],[c270,c0]) ).
cnf(d196,plain,
q25 = store('queue$u122',tail,'index$u123'),
inference(demodulation,[status(thm)],[c271,c373]) ).
cnf(d197,plain,
( tail = X0
| select(q25,X0) = select('queue$u122',X0) ),
inference(superposition,[status(thm)],[d196,c1]) ).
cnf(d198,plain,
( tail = seq
| select(q25,seq) = 'earray$u121' ),
inference(superposition,[status(thm)],[d197,d195]) ).
cnf(d199,plain,
( tail = seq
| 'earray$u125' = 'earray$u121' ),
inference(demodulation,[status(thm)],[d198,c79]) ).
cnf(d200,plain,
'earray$u125' = 'earray$u121',
inference(resolution,[status(thm)],[c4,d199]) ).
cnf(d201,plain,
( 'index$u126' = X0
| select('earray$u127',X0) = select('earray$u125',X0) ),
inference(superposition,[status(thm)],[c80,c1]) ).
cnf(d202,plain,
( 'index$u126' = X0
| select('earray$u127',X0) = select('earray$u121',X0) ),
inference(demodulation,[status(thm)],[d201,d200]) ).
cnf(d203,plain,
select('queue$u128',seq) = 'earray$u127',
inference(superposition,[status(thm)],[c272,c0]) ).
cnf(d204,plain,
q26 = store('queue$u128',tail,'index$u129'),
inference(demodulation,[status(thm)],[c274,c374]) ).
cnf(d205,plain,
( tail = X0
| select(q26,X0) = select('queue$u128',X0) ),
inference(superposition,[status(thm)],[d204,c1]) ).
cnf(d206,plain,
( tail = seq
| select(q26,seq) = 'earray$u127' ),
inference(superposition,[status(thm)],[d205,d203]) ).
cnf(d207,plain,
( tail = seq
| 'earray$u131' = 'earray$u127' ),
inference(demodulation,[status(thm)],[d206,c81]) ).
cnf(d208,plain,
'earray$u131' = 'earray$u127',
inference(resolution,[status(thm)],[c4,d207]) ).
cnf(d209,plain,
( 'index$u132' = X0
| select('earray$u133',X0) = select('earray$u131',X0) ),
inference(superposition,[status(thm)],[c82,c1]) ).
cnf(d210,plain,
( 'index$u132' = X0
| select('earray$u133',X0) = select('earray$u127',X0) ),
inference(demodulation,[status(thm)],[d209,d208]) ).
cnf(d211,plain,
select('queue$u134',seq) = 'earray$u133',
inference(superposition,[status(thm)],[c275,c0]) ).
cnf(d212,plain,
( tail = X0
| select('queue$u136',X0) = select('queue$u134',X0) ),
inference(superposition,[status(thm)],[c276,c1]) ).
cnf(d213,plain,
( tail = seq
| select('queue$u136',seq) = 'earray$u133' ),
inference(superposition,[status(thm)],[d212,d211]) ).
cnf(d214,plain,
select('queue$u136',seq) = 'earray$u133',
inference(resolution,[status(thm)],[c4,d213]) ).
cnf(d215,plain,
q27 = store('queue$u136',head,'index$u138'),
inference(demodulation,[status(thm)],[c277,c375]) ).
cnf(d216,plain,
( head = X0
| select(q27,X0) = select('queue$u136',X0) ),
inference(superposition,[status(thm)],[d215,c1]) ).
cnf(d217,plain,
( head = seq
| select(q27,seq) = 'earray$u133' ),
inference(superposition,[status(thm)],[d216,d214]) ).
cnf(d218,plain,
( head = seq
| 'earray$u140' = 'earray$u133' ),
inference(demodulation,[status(thm)],[d217,c84]) ).
cnf(d219,plain,
'earray$u140' = 'earray$u133',
inference(resolution,[status(thm)],[c3,d218]) ).
cnf(d220,plain,
( 'index$u141' = X0
| select('earray$u142',X0) = select('earray$u140',X0) ),
inference(superposition,[status(thm)],[c85,c1]) ).
cnf(d221,plain,
( 'index$u141' = X0
| select('earray$u142',X0) = select('earray$u133',X0) ),
inference(demodulation,[status(thm)],[d220,d219]) ).
cnf(d222,plain,
select('queue$u143',seq) = 'earray$u142',
inference(superposition,[status(thm)],[c278,c0]) ).
cnf(d223,plain,
q28 = store('queue$u143',tail,'index$u144'),
inference(demodulation,[status(thm)],[c279,c376]) ).
cnf(d224,plain,
( tail = X0
| select(q28,X0) = select('queue$u143',X0) ),
inference(superposition,[status(thm)],[d223,c1]) ).
cnf(d225,plain,
( tail = seq
| select(q28,seq) = 'earray$u142' ),
inference(superposition,[status(thm)],[d224,d222]) ).
cnf(d226,plain,
( tail = seq
| 'earray$u146' = 'earray$u142' ),
inference(demodulation,[status(thm)],[d225,c86]) ).
cnf(d227,plain,
'earray$u146' = 'earray$u142',
inference(resolution,[status(thm)],[c4,d226]) ).
cnf(d228,plain,
( 'index$u147' = X0
| select('earray$u148',X0) = select('earray$u146',X0) ),
inference(superposition,[status(thm)],[c87,c1]) ).
cnf(d229,plain,
( 'index$u147' = X0
| select('earray$u148',X0) = select('earray$u142',X0) ),
inference(demodulation,[status(thm)],[d228,d227]) ).
cnf(d230,plain,
select('queue$u149',seq) = 'earray$u148',
inference(superposition,[status(thm)],[c280,c0]) ).
cnf(d231,plain,
q29 = store('queue$u149',tail,'index$u150'),
inference(demodulation,[status(thm)],[c281,c377]) ).
cnf(d232,plain,
( tail = X0
| select(q29,X0) = select('queue$u149',X0) ),
inference(superposition,[status(thm)],[d231,c1]) ).
cnf(d233,plain,
( tail = seq
| select(q29,seq) = 'earray$u148' ),
inference(superposition,[status(thm)],[d232,d230]) ).
cnf(d234,plain,
( tail = seq
| 'earray$u161' = 'earray$u148' ),
inference(demodulation,[status(thm)],[d233,c91]) ).
cnf(d235,plain,
'earray$u161' = 'earray$u148',
inference(resolution,[status(thm)],[c4,d234]) ).
cnf(d236,plain,
( 'index$u162' = X0
| select('earray$u163',X0) = select('earray$u161',X0) ),
inference(superposition,[status(thm)],[c92,c1]) ).
cnf(d237,plain,
( 'index$u162' = X0
| select('earray$u163',X0) = select('earray$u148',X0) ),
inference(demodulation,[status(thm)],[d236,d235]) ).
cnf(d238,plain,
select('queue$u164',seq) = 'earray$u163',
inference(superposition,[status(thm)],[c285,c0]) ).
cnf(d239,plain,
( tail = X0
| select('queue$u166',X0) = select('queue$u164',X0) ),
inference(superposition,[status(thm)],[c286,c1]) ).
cnf(d240,plain,
( tail = seq
| select('queue$u166',seq) = 'earray$u163' ),
inference(superposition,[status(thm)],[d239,d238]) ).
cnf(d241,plain,
select('queue$u166',seq) = 'earray$u163',
inference(resolution,[status(thm)],[c4,d240]) ).
cnf(d242,plain,
q30 = store('queue$u166',head,'index$u168'),
inference(demodulation,[status(thm)],[c287,c379]) ).
cnf(d243,plain,
( head = X0
| select(q30,X0) = select('queue$u166',X0) ),
inference(superposition,[status(thm)],[d242,c1]) ).
cnf(d244,plain,
( head = seq
| select(q30,seq) = 'earray$u163' ),
inference(superposition,[status(thm)],[d243,d241]) ).
cnf(d245,plain,
( head = seq
| 'earray$u170' = 'earray$u163' ),
inference(demodulation,[status(thm)],[d244,c93]) ).
cnf(d246,plain,
'earray$u170' = 'earray$u163',
inference(resolution,[status(thm)],[c3,d245]) ).
cnf(d247,plain,
( 'index$u171' = X0
| select('earray$u172',X0) = select('earray$u170',X0) ),
inference(superposition,[status(thm)],[c94,c1]) ).
cnf(d248,plain,
( 'index$u171' = X0
| select('earray$u172',X0) = select('earray$u163',X0) ),
inference(demodulation,[status(thm)],[d247,d246]) ).
cnf(d249,plain,
select('queue$u173',seq) = 'earray$u172',
inference(superposition,[status(thm)],[c289,c0]) ).
cnf(d250,plain,
q31 = store('queue$u173',tail,'index$u174'),
inference(demodulation,[status(thm)],[c290,c380]) ).
cnf(d251,plain,
( tail = X0
| select(q31,X0) = select('queue$u173',X0) ),
inference(superposition,[status(thm)],[d250,c1]) ).
cnf(d252,plain,
( tail = seq
| select(q31,seq) = 'earray$u172' ),
inference(superposition,[status(thm)],[d251,d249]) ).
cnf(d253,plain,
( tail = seq
| 'earray$u176' = 'earray$u172' ),
inference(demodulation,[status(thm)],[d252,c95]) ).
cnf(d254,plain,
'earray$u176' = 'earray$u172',
inference(resolution,[status(thm)],[c4,d253]) ).
cnf(d255,plain,
( 'index$u177' = X0
| select('earray$u178',X0) = select('earray$u176',X0) ),
inference(superposition,[status(thm)],[c96,c1]) ).
cnf(d256,plain,
( 'index$u177' = X0
| select('earray$u178',X0) = select('earray$u172',X0) ),
inference(demodulation,[status(thm)],[d255,d254]) ).
cnf(d257,plain,
select('queue$u179',seq) = 'earray$u178',
inference(superposition,[status(thm)],[c291,c0]) ).
cnf(d258,plain,
q32 = store('queue$u179',tail,'index$u180'),
inference(demodulation,[status(thm)],[c292,c381]) ).
cnf(d259,plain,
( tail = X0
| select(q32,X0) = select('queue$u179',X0) ),
inference(superposition,[status(thm)],[d258,c1]) ).
cnf(d260,plain,
( tail = seq
| select(q32,seq) = 'earray$u178' ),
inference(superposition,[status(thm)],[d259,d257]) ).
cnf(d261,plain,
( tail = seq
| 'earray$u182' = 'earray$u178' ),
inference(demodulation,[status(thm)],[d260,c97]) ).
cnf(d262,plain,
'earray$u182' = 'earray$u178',
inference(resolution,[status(thm)],[c4,d261]) ).
cnf(d263,plain,
( 'index$u183' = X0
| select('earray$u184',X0) = select('earray$u182',X0) ),
inference(superposition,[status(thm)],[c98,c1]) ).
cnf(d264,plain,
( 'index$u183' = X0
| select('earray$u184',X0) = select('earray$u178',X0) ),
inference(demodulation,[status(thm)],[d263,d262]) ).
cnf(d265,plain,
select('queue$u185',seq) = 'earray$u184',
inference(superposition,[status(thm)],[c293,c0]) ).
cnf(d266,plain,
( tail = X0
| select('queue$u187',X0) = select('queue$u185',X0) ),
inference(superposition,[status(thm)],[c294,c1]) ).
cnf(d267,plain,
( tail = seq
| select('queue$u187',seq) = 'earray$u184' ),
inference(superposition,[status(thm)],[d266,d265]) ).
cnf(d268,plain,
select('queue$u187',seq) = 'earray$u184',
inference(resolution,[status(thm)],[c4,d267]) ).
cnf(d269,plain,
q33 = store('queue$u187',head,'index$u189'),
inference(demodulation,[status(thm)],[c296,c382]) ).
cnf(d270,plain,
( head = X0
| select(q33,X0) = select('queue$u187',X0) ),
inference(superposition,[status(thm)],[d269,c1]) ).
cnf(d271,plain,
( head = seq
| select(q33,seq) = 'earray$u184' ),
inference(superposition,[status(thm)],[d270,d268]) ).
cnf(d272,plain,
( head = seq
| 'earray$u191' = 'earray$u184' ),
inference(demodulation,[status(thm)],[d271,c99]) ).
cnf(d273,plain,
'earray$u191' = 'earray$u184',
inference(resolution,[status(thm)],[c3,d272]) ).
cnf(d274,plain,
( 'index$u192' = X0
| select('earray$u193',X0) = select('earray$u191',X0) ),
inference(superposition,[status(thm)],[c100,c1]) ).
cnf(d275,plain,
( 'index$u192' = X0
| select('earray$u193',X0) = select('earray$u184',X0) ),
inference(demodulation,[status(thm)],[d274,d273]) ).
cnf(d276,plain,
select('queue$u194',seq) = 'earray$u193',
inference(superposition,[status(thm)],[c297,c0]) ).
cnf(d277,plain,
q34 = store('queue$u194',tail,'index$u195'),
inference(demodulation,[status(thm)],[c298,c383]) ).
cnf(d278,plain,
( tail = X0
| select(q34,X0) = select('queue$u194',X0) ),
inference(superposition,[status(thm)],[d277,c1]) ).
cnf(d279,plain,
( tail = seq
| select(q34,seq) = 'earray$u193' ),
inference(superposition,[status(thm)],[d278,d276]) ).
cnf(d280,plain,
( tail = seq
| 'earray$u197' = 'earray$u193' ),
inference(demodulation,[status(thm)],[d279,c101]) ).
cnf(d281,plain,
'earray$u197' = 'earray$u193',
inference(resolution,[status(thm)],[c4,d280]) ).
cnf(d282,plain,
( 'index$u198' = X0
| select('earray$u199',X0) = select('earray$u197',X0) ),
inference(superposition,[status(thm)],[c102,c1]) ).
cnf(d283,plain,
( 'index$u198' = X0
| select('earray$u199',X0) = select('earray$u193',X0) ),
inference(demodulation,[status(thm)],[d282,d281]) ).
cnf(d284,plain,
select('queue$u200',seq) = 'earray$u199',
inference(superposition,[status(thm)],[c299,c0]) ).
cnf(d285,plain,
q35 = store('queue$u200',tail,'index$u201'),
inference(demodulation,[status(thm)],[c300,c384]) ).
cnf(d286,plain,
( tail = X0
| select(q35,X0) = select('queue$u200',X0) ),
inference(superposition,[status(thm)],[d285,c1]) ).
cnf(d287,plain,
( tail = seq
| select(q35,seq) = 'earray$u199' ),
inference(superposition,[status(thm)],[d286,d284]) ).
cnf(d288,plain,
( tail = seq
| 'earray$u203' = 'earray$u199' ),
inference(demodulation,[status(thm)],[d287,c105]) ).
cnf(d289,plain,
'earray$u203' = 'earray$u199',
inference(resolution,[status(thm)],[c4,d288]) ).
cnf(d290,plain,
( 'index$u204' = X0
| select('earray$u205',X0) = select('earray$u203',X0) ),
inference(superposition,[status(thm)],[c106,c1]) ).
cnf(d291,plain,
( 'index$u204' = X0
| select('earray$u205',X0) = select('earray$u199',X0) ),
inference(demodulation,[status(thm)],[d290,d289]) ).
cnf(d292,plain,
select('queue$u206',seq) = 'earray$u205',
inference(superposition,[status(thm)],[c301,c0]) ).
cnf(d293,plain,
( tail = X0
| select('queue$u208',X0) = select('queue$u206',X0) ),
inference(superposition,[status(thm)],[c302,c1]) ).
cnf(d294,plain,
( tail = seq
| select('queue$u208',seq) = 'earray$u205' ),
inference(superposition,[status(thm)],[d293,d292]) ).
cnf(d295,plain,
select('queue$u208',seq) = 'earray$u205',
inference(resolution,[status(thm)],[c4,d294]) ).
cnf(d296,plain,
q36 = store('queue$u208',head,'index$u210'),
inference(demodulation,[status(thm)],[c303,c385]) ).
cnf(d297,plain,
( head = X0
| select(q36,X0) = select('queue$u208',X0) ),
inference(superposition,[status(thm)],[d296,c1]) ).
cnf(d298,plain,
( head = seq
| select(q36,seq) = 'earray$u205' ),
inference(superposition,[status(thm)],[d297,d295]) ).
cnf(d299,plain,
( head = seq
| 'earray$u212' = 'earray$u205' ),
inference(demodulation,[status(thm)],[d298,c107]) ).
cnf(d300,plain,
'earray$u212' = 'earray$u205',
inference(resolution,[status(thm)],[c3,d299]) ).
cnf(d301,plain,
( 'index$u213' = X0
| select('earray$u214',X0) = select('earray$u212',X0) ),
inference(superposition,[status(thm)],[c108,c1]) ).
cnf(d302,plain,
( 'index$u213' = X0
| select('earray$u214',X0) = select('earray$u205',X0) ),
inference(demodulation,[status(thm)],[d301,d300]) ).
cnf(d303,plain,
select('queue$u215',seq) = 'earray$u214',
inference(superposition,[status(thm)],[c304,c0]) ).
cnf(d304,plain,
q37 = store('queue$u215',tail,'index$u216'),
inference(demodulation,[status(thm)],[c305,c386]) ).
cnf(d305,plain,
( tail = X0
| select(q37,X0) = select('queue$u215',X0) ),
inference(superposition,[status(thm)],[d304,c1]) ).
cnf(d306,plain,
( tail = seq
| select(q37,seq) = 'earray$u214' ),
inference(superposition,[status(thm)],[d305,d303]) ).
cnf(d307,plain,
( tail = seq
| 'earray$u218' = 'earray$u214' ),
inference(demodulation,[status(thm)],[d306,c109]) ).
cnf(d308,plain,
'earray$u218' = 'earray$u214',
inference(resolution,[status(thm)],[c4,d307]) ).
cnf(d309,plain,
( 'index$u219' = X0
| select('earray$u220',X0) = select('earray$u218',X0) ),
inference(superposition,[status(thm)],[c111,c1]) ).
cnf(d310,plain,
( 'index$u219' = X0
| select('earray$u220',X0) = select('earray$u214',X0) ),
inference(demodulation,[status(thm)],[d309,d308]) ).
cnf(d311,plain,
select('queue$u221',seq) = 'earray$u220',
inference(superposition,[status(thm)],[c306,c0]) ).
cnf(d312,plain,
q38 = store('queue$u221',tail,'index$u222'),
inference(demodulation,[status(thm)],[c307,c387]) ).
cnf(d313,plain,
( tail = X0
| select(q38,X0) = select('queue$u221',X0) ),
inference(superposition,[status(thm)],[d312,c1]) ).
cnf(d314,plain,
( tail = seq
| select(q38,seq) = 'earray$u220' ),
inference(superposition,[status(thm)],[d313,d311]) ).
cnf(d315,plain,
( tail = seq
| 'earray$u224' = 'earray$u220' ),
inference(demodulation,[status(thm)],[d314,c112]) ).
cnf(d316,plain,
'earray$u224' = 'earray$u220',
inference(resolution,[status(thm)],[c4,d315]) ).
cnf(d317,plain,
( 'index$u225' = X0
| select('earray$u226',X0) = select('earray$u224',X0) ),
inference(superposition,[status(thm)],[c113,c1]) ).
cnf(d318,plain,
( 'index$u225' = X0
| select('earray$u226',X0) = select('earray$u220',X0) ),
inference(demodulation,[status(thm)],[d317,d316]) ).
cnf(d319,plain,
select('queue$u227',seq) = 'earray$u226',
inference(superposition,[status(thm)],[c308,c0]) ).
cnf(d320,plain,
( tail = X0
| select('queue$u229',X0) = select('queue$u227',X0) ),
inference(superposition,[status(thm)],[c309,c1]) ).
cnf(d321,plain,
( tail = seq
| select('queue$u229',seq) = 'earray$u226' ),
inference(superposition,[status(thm)],[d320,d319]) ).
cnf(d322,plain,
select('queue$u229',seq) = 'earray$u226',
inference(resolution,[status(thm)],[c4,d321]) ).
cnf(d323,plain,
q39 = store('queue$u229',head,'index$u231'),
inference(demodulation,[status(thm)],[c311,c388]) ).
cnf(d324,plain,
( head = X0
| select(q39,X0) = select('queue$u229',X0) ),
inference(superposition,[status(thm)],[d323,c1]) ).
cnf(d325,plain,
( head = seq
| select(q39,seq) = 'earray$u226' ),
inference(superposition,[status(thm)],[d324,d322]) ).
cnf(d326,plain,
( head = seq
| 'earray$u239' = 'earray$u226' ),
inference(demodulation,[status(thm)],[d325,c116]) ).
cnf(d327,plain,
'earray$u239' = 'earray$u226',
inference(resolution,[status(thm)],[c3,d326]) ).
cnf(d328,plain,
( 'index$u240' = X0
| select('earray$u241',X0) = select('earray$u239',X0) ),
inference(superposition,[status(thm)],[c117,c1]) ).
cnf(d329,plain,
( 'index$u240' = X0
| select('earray$u241',X0) = select('earray$u226',X0) ),
inference(demodulation,[status(thm)],[d328,d327]) ).
cnf(d330,plain,
select('queue$u242',seq) = 'earray$u241',
inference(superposition,[status(thm)],[c314,c0]) ).
cnf(d331,plain,
q40 = store('queue$u242',tail,'index$u243'),
inference(demodulation,[status(thm)],[c315,c390]) ).
cnf(d332,plain,
( tail = X0
| select(q40,X0) = select('queue$u242',X0) ),
inference(superposition,[status(thm)],[d331,c1]) ).
cnf(d333,plain,
( tail = seq
| select(q40,seq) = 'earray$u241' ),
inference(superposition,[status(thm)],[d332,d330]) ).
cnf(d334,plain,
( tail = seq
| 'earray$u281' = 'earray$u241' ),
inference(demodulation,[status(thm)],[d333,c128]) ).
cnf(d335,plain,
'earray$u281' = 'earray$u241',
inference(resolution,[status(thm)],[c4,d334]) ).
cnf(d336,plain,
'elem$u283' = select('earray$u241','index$u282'),
inference(demodulation,[status(thm)],[c152,d335]) ).
cnf(d337,plain,
select(q39,head) = 'index$u231',
inference(superposition,[status(thm)],[d323,c0]) ).
cnf(d338,plain,
( seq = X0
| select('queue$u242',X0) = select(q39,X0) ),
inference(superposition,[status(thm)],[c314,c1]) ).
cnf(d339,plain,
( tail = X0
| seq = X0
| select(q40,X0) = select(q39,X0) ),
inference(superposition,[status(thm)],[d332,d338]) ).
cnf(d340,plain,
( seq = head
| tail = head
| 'index$u282' = select(q39,head) ),
inference(superposition,[status(thm)],[d339,c230]) ).
cnf(d341,plain,
( 'index$u282' = 'index$u231'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d340,d337]) ).
cnf(d342,plain,
( seq = head
| tail = head
| q39 = store('queue$u229',head,'index$u282') ),
inference(superposition,[status(thm)],[d341,d323]) ).
cnf(d343,plain,
( seq = head
| tail = head
| select(q39,head) = 'index$u282' ),
inference(superposition,[status(thm)],[d342,c0]) ).
cnf(d344,plain,
( seq = head
| tail = head
| 'index$u231' = 'index$u282' ),
inference(demodulation,[status(thm)],[d343,d337]) ).
cnf(d345,plain,
q13 = store('queue$u32',tail,'index$u33'),
inference(demodulation,[status(thm)],[c331,c360]) ).
cnf(d346,plain,
select(q13,tail) = 'index$u33',
inference(superposition,[status(thm)],[d345,c0]) ).
cnf(d347,plain,
'index$u36' = 'index$u33',
inference(demodulation,[status(thm)],[d346,c234]) ).
cnf(d348,plain,
'index$u36' = s('index$u30'),
inference(demodulation,[status(thm)],[c233,d347]) ).
cnf(d349,plain,
select(q36,head) = 'index$u210',
inference(superposition,[status(thm)],[d296,c0]) ).
cnf(d350,plain,
( seq = X0
| select('queue$u215',X0) = select(q36,X0) ),
inference(superposition,[status(thm)],[c304,c1]) ).
cnf(d351,plain,
( tail = X0
| seq = X0
| select(q37,X0) = select(q36,X0) ),
inference(superposition,[status(thm)],[d305,d350]) ).
cnf(d352,plain,
( seq = X0
| select('queue$u221',X0) = select(q37,X0) ),
inference(superposition,[status(thm)],[c306,c1]) ).
cnf(d353,plain,
( tail = X0
| seq = X0
| select(q38,X0) = select(q37,X0) ),
inference(superposition,[status(thm)],[d313,d352]) ).
cnf(d354,plain,
( seq = X0
| select('queue$u227',X0) = select(q38,X0) ),
inference(superposition,[status(thm)],[c308,c1]) ).
cnf(d355,plain,
( tail = X0
| seq = X0
| select('queue$u229',X0) = select(q38,X0) ),
inference(superposition,[status(thm)],[d320,d354]) ).
cnf(d356,plain,
( seq = head
| tail = head
| 'index$u230' = select(q38,head) ),
inference(superposition,[status(thm)],[d355,c207]) ).
cnf(d357,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u230' = select(q37,head) ),
inference(superposition,[status(thm)],[d356,d353]) ).
cnf(d358,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u230' = select(q36,head) ),
inference(superposition,[status(thm)],[d357,d351]) ).
cnf(d359,plain,
( 'index$u230' = 'index$u210'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d358,d349]) ).
cnf(d360,plain,
( seq = head
| tail = head
| 'index$u231' = s('index$u210') ),
inference(superposition,[status(thm)],[d359,c208]) ).
cnf(d361,plain,
select('queue$u25',tail) = 'index$u24',
inference(superposition,[status(thm)],[c317,c0]) ).
cnf(d362,plain,
q12 = store('queue$u25',head,'index$u27'),
inference(demodulation,[status(thm)],[c328,c359]) ).
cnf(d363,plain,
( head = X0
| select(q12,X0) = select('queue$u25',X0) ),
inference(superposition,[status(thm)],[d362,c1]) ).
cnf(d364,plain,
( head = tail
| select(q12,tail) = 'index$u24' ),
inference(superposition,[status(thm)],[d363,d361]) ).
cnf(d365,plain,
( head = tail
| 'index$u30' = 'index$u24' ),
inference(demodulation,[status(thm)],[d364,c232]) ).
cnf(d366,plain,
'index$u30' = 'index$u24',
inference(resolution,[status(thm)],[c2,d365]) ).
cnf(d367,plain,
'index$u30' = s('index$u21'),
inference(demodulation,[status(thm)],[c211,d366]) ).
cnf(d368,plain,
select(q33,head) = 'index$u189',
inference(superposition,[status(thm)],[d269,c0]) ).
cnf(d369,plain,
( seq = X0
| select('queue$u194',X0) = select(q33,X0) ),
inference(superposition,[status(thm)],[c297,c1]) ).
cnf(d370,plain,
( tail = X0
| seq = X0
| select(q34,X0) = select(q33,X0) ),
inference(superposition,[status(thm)],[d278,d369]) ).
cnf(d371,plain,
( seq = X0
| select('queue$u200',X0) = select(q34,X0) ),
inference(superposition,[status(thm)],[c299,c1]) ).
cnf(d372,plain,
( tail = X0
| seq = X0
| select(q35,X0) = select(q34,X0) ),
inference(superposition,[status(thm)],[d286,d371]) ).
cnf(d373,plain,
( seq = X0
| select('queue$u206',X0) = select(q35,X0) ),
inference(superposition,[status(thm)],[c301,c1]) ).
cnf(d374,plain,
( tail = X0
| seq = X0
| select('queue$u208',X0) = select(q35,X0) ),
inference(superposition,[status(thm)],[d293,d373]) ).
cnf(d375,plain,
( seq = head
| tail = head
| 'index$u209' = select(q35,head) ),
inference(superposition,[status(thm)],[d374,c198]) ).
cnf(d376,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u209' = select(q34,head) ),
inference(superposition,[status(thm)],[d375,d372]) ).
cnf(d377,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u209' = select(q33,head) ),
inference(superposition,[status(thm)],[d376,d370]) ).
cnf(d378,plain,
( 'index$u209' = 'index$u189'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d377,d368]) ).
cnf(d379,plain,
( seq = head
| tail = head
| 'index$u210' = s('index$u189') ),
inference(superposition,[status(thm)],[d378,c200]) ).
cnf(d380,plain,
q11 = store('queue$u17',tail,'index$u18'),
inference(demodulation,[status(thm)],[c295,c358]) ).
cnf(d381,plain,
select(q11,tail) = 'index$u18',
inference(superposition,[status(thm)],[d380,c0]) ).
cnf(d382,plain,
'index$u21' = 'index$u18',
inference(demodulation,[status(thm)],[d381,c199]) ).
cnf(d383,plain,
'index$u21' = s('index$u15'),
inference(demodulation,[status(thm)],[c186,d382]) ).
cnf(d384,plain,
select(q30,head) = 'index$u168',
inference(superposition,[status(thm)],[d242,c0]) ).
cnf(d385,plain,
( seq = X0
| select('queue$u173',X0) = select(q30,X0) ),
inference(superposition,[status(thm)],[c289,c1]) ).
cnf(d386,plain,
( tail = X0
| seq = X0
| select(q31,X0) = select(q30,X0) ),
inference(superposition,[status(thm)],[d251,d385]) ).
cnf(d387,plain,
( seq = X0
| select('queue$u179',X0) = select(q31,X0) ),
inference(superposition,[status(thm)],[c291,c1]) ).
cnf(d388,plain,
( tail = X0
| seq = X0
| select(q32,X0) = select(q31,X0) ),
inference(superposition,[status(thm)],[d259,d387]) ).
cnf(d389,plain,
( seq = X0
| select('queue$u185',X0) = select(q32,X0) ),
inference(superposition,[status(thm)],[c293,c1]) ).
cnf(d390,plain,
( tail = X0
| seq = X0
| select('queue$u187',X0) = select(q32,X0) ),
inference(superposition,[status(thm)],[d266,d389]) ).
cnf(d391,plain,
( seq = head
| tail = head
| 'index$u188' = select(q32,head) ),
inference(superposition,[status(thm)],[d390,c190]) ).
cnf(d392,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u188' = select(q31,head) ),
inference(superposition,[status(thm)],[d391,d388]) ).
cnf(d393,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u188' = select(q30,head) ),
inference(superposition,[status(thm)],[d392,d386]) ).
cnf(d394,plain,
( 'index$u188' = 'index$u168'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d393,d384]) ).
cnf(d395,plain,
( seq = head
| tail = head
| 'index$u189' = s('index$u168') ),
inference(superposition,[status(thm)],[d394,c191]) ).
cnf(d396,plain,
q10 = store('queue$u11',tail,'index$u12'),
inference(demodulation,[status(thm)],[c273,c357]) ).
cnf(d397,plain,
select(q10,tail) = 'index$u12',
inference(superposition,[status(thm)],[d396,c0]) ).
cnf(d398,plain,
'index$u15' = 'index$u12',
inference(demodulation,[status(thm)],[d397,c173]) ).
cnf(d399,plain,
'index$u15' = s('index$u9'),
inference(demodulation,[status(thm)],[c161,d398]) ).
cnf(d400,plain,
select(q27,head) = 'index$u138',
inference(superposition,[status(thm)],[d215,c0]) ).
cnf(d401,plain,
( seq = X0
| select('queue$u143',X0) = select(q27,X0) ),
inference(superposition,[status(thm)],[c278,c1]) ).
cnf(d402,plain,
( tail = X0
| seq = X0
| select(q28,X0) = select(q27,X0) ),
inference(superposition,[status(thm)],[d224,d401]) ).
cnf(d403,plain,
( seq = X0
| select('queue$u149',X0) = select(q28,X0) ),
inference(superposition,[status(thm)],[c280,c1]) ).
cnf(d404,plain,
( tail = X0
| seq = X0
| select(q29,X0) = select(q28,X0) ),
inference(superposition,[status(thm)],[d232,d403]) ).
cnf(d405,plain,
( seq = X0
| select('queue$u164',X0) = select(q29,X0) ),
inference(superposition,[status(thm)],[c285,c1]) ).
cnf(d406,plain,
( tail = X0
| seq = X0
| select('queue$u166',X0) = select(q29,X0) ),
inference(superposition,[status(thm)],[d239,d405]) ).
cnf(d407,plain,
( seq = head
| tail = head
| 'index$u167' = select(q29,head) ),
inference(superposition,[status(thm)],[d406,c181]) ).
cnf(d408,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u167' = select(q28,head) ),
inference(superposition,[status(thm)],[d407,d404]) ).
cnf(d409,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u167' = select(q27,head) ),
inference(superposition,[status(thm)],[d408,d402]) ).
cnf(d410,plain,
( 'index$u167' = 'index$u138'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d409,d400]) ).
cnf(d411,plain,
( seq = head
| tail = head
| 'index$u168' = s('index$u138') ),
inference(superposition,[status(thm)],[d410,c182]) ).
cnf(d412,plain,
select('queue$u277',tail) = 'index$u276',
inference(superposition,[status(thm)],[c327,c0]) ).
cnf(d413,plain,
q9 = store('queue$u277',head,'index$u279'),
inference(demodulation,[status(thm)],[c329,c395]) ).
cnf(d414,plain,
( head = X0
| select(q9,X0) = select('queue$u277',X0) ),
inference(superposition,[status(thm)],[d413,c1]) ).
cnf(d415,plain,
( head = tail
| select(q9,tail) = 'index$u276' ),
inference(superposition,[status(thm)],[d414,d412]) ).
cnf(d416,plain,
( head = tail
| 'index$u9' = 'index$u276' ),
inference(demodulation,[status(thm)],[d415,c255]) ).
cnf(d417,plain,
'index$u9' = 'index$u276',
inference(resolution,[status(thm)],[c2,d416]) ).
cnf(d418,plain,
'index$u9' = s('index$u273'),
inference(demodulation,[status(thm)],[c227,d417]) ).
cnf(d419,plain,
select(q24,head) = 'index$u117',
inference(superposition,[status(thm)],[d188,c0]) ).
cnf(d420,plain,
( seq = X0
| select('queue$u122',X0) = select(q24,X0) ),
inference(superposition,[status(thm)],[c270,c1]) ).
cnf(d421,plain,
( tail = X0
| seq = X0
| select(q25,X0) = select(q24,X0) ),
inference(superposition,[status(thm)],[d197,d420]) ).
cnf(d422,plain,
( seq = X0
| select('queue$u128',X0) = select(q25,X0) ),
inference(superposition,[status(thm)],[c272,c1]) ).
cnf(d423,plain,
( tail = X0
| seq = X0
| select(q26,X0) = select(q25,X0) ),
inference(superposition,[status(thm)],[d205,d422]) ).
cnf(d424,plain,
( seq = X0
| select('queue$u134',X0) = select(q26,X0) ),
inference(superposition,[status(thm)],[c275,c1]) ).
cnf(d425,plain,
( tail = X0
| seq = X0
| select('queue$u136',X0) = select(q26,X0) ),
inference(superposition,[status(thm)],[d212,d424]) ).
cnf(d426,plain,
( seq = head
| tail = head
| 'index$u137' = select(q26,head) ),
inference(superposition,[status(thm)],[d425,c168]) ).
cnf(d427,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u137' = select(q25,head) ),
inference(superposition,[status(thm)],[d426,d423]) ).
cnf(d428,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u137' = select(q24,head) ),
inference(superposition,[status(thm)],[d427,d421]) ).
cnf(d429,plain,
( 'index$u137' = 'index$u117'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d428,d419]) ).
cnf(d430,plain,
( seq = head
| tail = head
| 'index$u138' = s('index$u117') ),
inference(superposition,[status(thm)],[d429,c169]) ).
cnf(d431,plain,
q8 = store('queue$u269',tail,'index$u270'),
inference(demodulation,[status(thm)],[c325,c394]) ).
cnf(d432,plain,
select(q8,tail) = 'index$u270',
inference(superposition,[status(thm)],[d431,c0]) ).
cnf(d433,plain,
'index$u273' = 'index$u270',
inference(demodulation,[status(thm)],[d432,c226]) ).
cnf(d434,plain,
'index$u273' = s('index$u267'),
inference(demodulation,[status(thm)],[c225,d433]) ).
cnf(d435,plain,
select(q21,head) = 'index$u96',
inference(superposition,[status(thm)],[d60,c0]) ).
cnf(d436,plain,
( seq = X0
| select('queue$u101',X0) = select(q21,X0) ),
inference(superposition,[status(thm)],[c262,c1]) ).
cnf(d437,plain,
( tail = X0
| seq = X0
| select(q22,X0) = select(q21,X0) ),
inference(superposition,[status(thm)],[d170,d436]) ).
cnf(d438,plain,
( seq = head
| tail = head
| select(q22,head) = 'index$u96' ),
inference(superposition,[status(thm)],[d437,d435]) ).
cnf(d439,plain,
( seq = X0
| select('queue$u107',X0) = select(q22,X0) ),
inference(superposition,[status(thm)],[c264,c1]) ).
cnf(d440,plain,
( tail = X0
| seq = X0
| select(q23,X0) = select(q22,X0) ),
inference(superposition,[status(thm)],[d178,d439]) ).
cnf(d441,plain,
( seq = X0
| select('queue$u113',X0) = select(q23,X0) ),
inference(superposition,[status(thm)],[c267,c1]) ).
cnf(d442,plain,
( tail = X0
| seq = X0
| select('queue$u115',X0) = select(q23,X0) ),
inference(superposition,[status(thm)],[d185,d441]) ).
cnf(d443,plain,
( seq = head
| tail = head
| 'index$u116' = select(q23,head) ),
inference(superposition,[status(thm)],[d442,c159]) ).
cnf(d444,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u116' = select(q22,head) ),
inference(superposition,[status(thm)],[d443,d440]) ).
cnf(d445,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u116' = 'index$u96' ),
inference(superposition,[status(thm)],[d444,d438]) ).
cnf(d446,plain,
( seq = head
| tail = head
| q21 = store('queue$u94',head,'index$u116') ),
inference(superposition,[status(thm)],[d445,d60]) ).
cnf(d447,plain,
( seq = head
| tail = head
| select(q21,head) = 'index$u116' ),
inference(superposition,[status(thm)],[d446,c0]) ).
cnf(d448,plain,
( seq = head
| tail = head
| 'index$u96' = 'index$u116' ),
inference(demodulation,[status(thm)],[d447,d435]) ).
cnf(d449,plain,
q7 = store('queue$u263',tail,'index$u264'),
inference(demodulation,[status(thm)],[c323,c393]) ).
cnf(d450,plain,
select(q7,tail) = 'index$u264',
inference(superposition,[status(thm)],[d449,c0]) ).
cnf(d451,plain,
'index$u267' = 'index$u264',
inference(demodulation,[status(thm)],[d450,c223]) ).
cnf(d452,plain,
'index$u267' = s('index$u261'),
inference(demodulation,[status(thm)],[c222,d451]) ).
cnf(d453,plain,
select(q18,head) = 'index$u69',
inference(superposition,[status(thm)],[d41,c0]) ).
cnf(d454,plain,
( seq = X0
| select('queue$u74',X0) = select(q18,X0) ),
inference(superposition,[status(thm)],[c346,c1]) ).
cnf(d455,plain,
( tail = X0
| seq = X0
| select(q19,X0) = select(q18,X0) ),
inference(superposition,[status(thm)],[d50,d454]) ).
cnf(d456,plain,
( seq = X0
| select('queue$u86',X0) = select(q19,X0) ),
inference(superposition,[status(thm)],[c350,c1]) ).
cnf(d457,plain,
( tail = X0
| seq = X0
| select(q20,X0) = select(q19,X0) ),
inference(superposition,[status(thm)],[d67,d456]) ).
cnf(d458,plain,
( seq = X0
| select('queue$u92',X0) = select(q20,X0) ),
inference(superposition,[status(thm)],[c352,c1]) ).
cnf(d459,plain,
( tail = X0
| seq = X0
| select('queue$u94',X0) = select(q20,X0) ),
inference(superposition,[status(thm)],[d57,d458]) ).
cnf(d460,plain,
( seq = head
| tail = head
| 'index$u95' = select(q20,head) ),
inference(superposition,[status(thm)],[d459,c258]) ).
cnf(d461,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u95' = select(q19,head) ),
inference(superposition,[status(thm)],[d460,d457]) ).
cnf(d462,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u95' = select(q18,head) ),
inference(superposition,[status(thm)],[d461,d455]) ).
cnf(d463,plain,
( 'index$u95' = 'index$u69'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d462,d453]) ).
cnf(d464,plain,
( seq = head
| tail = head
| 'index$u96' = s('index$u69') ),
inference(superposition,[status(thm)],[d463,c259]) ).
cnf(d465,plain,
select('queue$u256',tail) = 'index$u255',
inference(superposition,[status(thm)],[c320,c0]) ).
cnf(d466,plain,
q6 = store('queue$u256',head,'index$u258'),
inference(demodulation,[status(thm)],[c321,c392]) ).
cnf(d467,plain,
( head = X0
| select(q6,X0) = select('queue$u256',X0) ),
inference(superposition,[status(thm)],[d466,c1]) ).
cnf(d468,plain,
( head = tail
| select(q6,tail) = 'index$u255' ),
inference(superposition,[status(thm)],[d467,d465]) ).
cnf(d469,plain,
( head = tail
| 'index$u261' = 'index$u255' ),
inference(demodulation,[status(thm)],[d468,c221]) ).
cnf(d470,plain,
'index$u261' = 'index$u255',
inference(resolution,[status(thm)],[c2,d469]) ).
cnf(d471,plain,
'index$u261' = s('index$u252'),
inference(demodulation,[status(thm)],[c217,d470]) ).
cnf(d472,plain,
select(q15,head) = 'index$u48',
inference(superposition,[status(thm)],[d14,c0]) ).
cnf(d473,plain,
( seq = X0
| select('queue$u53',X0) = select(q15,X0) ),
inference(superposition,[status(thm)],[c338,c1]) ).
cnf(d474,plain,
( tail = X0
| seq = X0
| select(q16,X0) = select(q15,X0) ),
inference(superposition,[status(thm)],[d23,d473]) ).
cnf(d475,plain,
( seq = X0
| select('queue$u59',X0) = select(q16,X0) ),
inference(superposition,[status(thm)],[c340,c1]) ).
cnf(d476,plain,
( tail = X0
| seq = X0
| select(q17,X0) = select(q16,X0) ),
inference(superposition,[status(thm)],[d31,d475]) ).
cnf(d477,plain,
( seq = X0
| select('queue$u65',X0) = select(q17,X0) ),
inference(superposition,[status(thm)],[c342,c1]) ).
cnf(d478,plain,
( tail = X0
| seq = X0
| select('queue$u67',X0) = select(q17,X0) ),
inference(superposition,[status(thm)],[d38,d477]) ).
cnf(d479,plain,
( seq = head
| tail = head
| 'index$u68' = select(q17,head) ),
inference(superposition,[status(thm)],[d478,c247]) ).
cnf(d480,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u68' = select(q16,head) ),
inference(superposition,[status(thm)],[d479,d476]) ).
cnf(d481,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u68' = select(q15,head) ),
inference(superposition,[status(thm)],[d480,d474]) ).
cnf(d482,plain,
( 'index$u68' = 'index$u48'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d481,d472]) ).
cnf(d483,plain,
( seq = head
| tail = head
| 'index$u69' = s('index$u48') ),
inference(superposition,[status(thm)],[d482,c248]) ).
cnf(d484,plain,
q5 = store('queue$u248',tail,'index$u249'),
inference(demodulation,[status(thm)],[c318,c391]) ).
cnf(d485,plain,
select(q5,tail) = 'index$u249',
inference(superposition,[status(thm)],[d484,c0]) ).
cnf(d486,plain,
'index$u252' = 'index$u249',
inference(demodulation,[status(thm)],[d485,c216]) ).
cnf(d487,plain,
'index$u252' = s('index$u246'),
inference(demodulation,[status(thm)],[c215,d486]) ).
cnf(d488,plain,
select(q12,head) = 'index$u27',
inference(superposition,[status(thm)],[d362,c0]) ).
cnf(d489,plain,
( seq = X0
| select('queue$u32',X0) = select(q12,X0) ),
inference(superposition,[status(thm)],[c330,c1]) ).
cnf(d490,plain,
( tail = X0
| select(q13,X0) = select('queue$u32',X0) ),
inference(superposition,[status(thm)],[d345,c1]) ).
cnf(d491,plain,
( tail = X0
| seq = X0
| select(q13,X0) = select(q12,X0) ),
inference(superposition,[status(thm)],[d490,d489]) ).
cnf(d492,plain,
( seq = X0
| select('queue$u38',X0) = select(q13,X0) ),
inference(superposition,[status(thm)],[c332,c1]) ).
cnf(d493,plain,
( tail = X0
| seq = X0
| select(q14,X0) = select(q13,X0) ),
inference(superposition,[status(thm)],[d4,d492]) ).
cnf(d494,plain,
( seq = X0
| select('queue$u44',X0) = select(q14,X0) ),
inference(superposition,[status(thm)],[c334,c1]) ).
cnf(d495,plain,
( tail = X0
| seq = X0
| select('queue$u46',X0) = select(q14,X0) ),
inference(superposition,[status(thm)],[d11,d494]) ).
cnf(d496,plain,
( seq = head
| tail = head
| 'index$u47' = select(q14,head) ),
inference(superposition,[status(thm)],[d495,c238]) ).
cnf(d497,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u47' = select(q13,head) ),
inference(superposition,[status(thm)],[d496,d493]) ).
cnf(d498,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u47' = select(q12,head) ),
inference(superposition,[status(thm)],[d497,d491]) ).
cnf(d499,plain,
( 'index$u47' = 'index$u27'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d498,d488]) ).
cnf(d500,plain,
( seq = head
| tail = head
| 'index$u48' = s('index$u27') ),
inference(superposition,[status(thm)],[d499,c239]) ).
cnf(d501,plain,
q4 = store('queue$u236',tail,'index$u237'),
inference(demodulation,[status(thm)],[c313,c389]) ).
cnf(d502,plain,
select(q4,tail) = 'index$u237',
inference(superposition,[status(thm)],[d501,c0]) ).
cnf(d503,plain,
'index$u246' = 'index$u237',
inference(demodulation,[status(thm)],[d502,c214]) ).
cnf(d504,plain,
'index$u246' = s('index$u234'),
inference(demodulation,[status(thm)],[c210,d503]) ).
cnf(d505,plain,
select(q9,head) = 'index$u279',
inference(superposition,[status(thm)],[d413,c0]) ).
cnf(d506,plain,
( seq = X0
| select('queue$u11',X0) = select(q9,X0) ),
inference(superposition,[status(thm)],[c266,c1]) ).
cnf(d507,plain,
( tail = X0
| select(q10,X0) = select('queue$u11',X0) ),
inference(superposition,[status(thm)],[d396,c1]) ).
cnf(d508,plain,
( tail = X0
| seq = X0
| select(q10,X0) = select(q9,X0) ),
inference(superposition,[status(thm)],[d507,d506]) ).
cnf(d509,plain,
( seq = head
| tail = head
| select(q10,head) = 'index$u279' ),
inference(superposition,[status(thm)],[d508,d505]) ).
cnf(d510,plain,
( seq = X0
| select('queue$u17',X0) = select(q10,X0) ),
inference(superposition,[status(thm)],[c288,c1]) ).
cnf(d511,plain,
( tail = X0
| select(q11,X0) = select('queue$u17',X0) ),
inference(superposition,[status(thm)],[d380,c1]) ).
cnf(d512,plain,
( tail = X0
| seq = X0
| select(q11,X0) = select(q10,X0) ),
inference(superposition,[status(thm)],[d511,d510]) ).
cnf(d513,plain,
( seq = X0
| select('queue$u23',X0) = select(q11,X0) ),
inference(superposition,[status(thm)],[c310,c1]) ).
cnf(d514,plain,
( tail = X0
| select('queue$u25',X0) = select('queue$u23',X0) ),
inference(superposition,[status(thm)],[c317,c1]) ).
cnf(d515,plain,
( tail = X0
| seq = X0
| select('queue$u25',X0) = select(q11,X0) ),
inference(superposition,[status(thm)],[d514,d513]) ).
cnf(d516,plain,
( seq = head
| tail = head
| 'index$u26' = select(q11,head) ),
inference(superposition,[status(thm)],[d515,c220]) ).
cnf(d517,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u26' = select(q10,head) ),
inference(superposition,[status(thm)],[d516,d512]) ).
cnf(d518,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u26' = 'index$u279' ),
inference(superposition,[status(thm)],[d517,d509]) ).
cnf(d519,plain,
( seq = head
| tail = head
| q9 = store('queue$u277',head,'index$u26') ),
inference(superposition,[status(thm)],[d518,d413]) ).
cnf(d520,plain,
( seq = head
| tail = head
| select(q9,head) = 'index$u26' ),
inference(superposition,[status(thm)],[d519,c0]) ).
cnf(d521,plain,
( seq = head
| tail = head
| 'index$u279' = 'index$u26' ),
inference(demodulation,[status(thm)],[d520,d505]) ).
cnf(d522,plain,
select('queue$u157',tail) = 'index$u156',
inference(superposition,[status(thm)],[c283,c0]) ).
cnf(d523,plain,
q3 = store('queue$u157',head,'index$u159'),
inference(demodulation,[status(thm)],[c284,c378]) ).
cnf(d524,plain,
( head = X0
| select(q3,X0) = select('queue$u157',X0) ),
inference(superposition,[status(thm)],[d523,c1]) ).
cnf(d525,plain,
( head = tail
| select(q3,tail) = 'index$u156' ),
inference(superposition,[status(thm)],[d524,d522]) ).
cnf(d526,plain,
( head = tail
| 'index$u234' = 'index$u156' ),
inference(demodulation,[status(thm)],[d525,c209]) ).
cnf(d527,plain,
'index$u234' = 'index$u156',
inference(resolution,[status(thm)],[c2,d526]) ).
cnf(d528,plain,
'index$u234' = s('index$u153'),
inference(demodulation,[status(thm)],[c176,d527]) ).
cnf(d529,plain,
select(q6,head) = 'index$u258',
inference(superposition,[status(thm)],[d466,c0]) ).
cnf(d530,plain,
( seq = X0
| select('queue$u263',X0) = select(q6,X0) ),
inference(superposition,[status(thm)],[c322,c1]) ).
cnf(d531,plain,
( tail = X0
| select(q7,X0) = select('queue$u263',X0) ),
inference(superposition,[status(thm)],[d449,c1]) ).
cnf(d532,plain,
( tail = X0
| seq = X0
| select(q7,X0) = select(q6,X0) ),
inference(superposition,[status(thm)],[d531,d530]) ).
cnf(d533,plain,
( seq = X0
| select('queue$u269',X0) = select(q7,X0) ),
inference(superposition,[status(thm)],[c324,c1]) ).
cnf(d534,plain,
( tail = X0
| select(q8,X0) = select('queue$u269',X0) ),
inference(superposition,[status(thm)],[d431,c1]) ).
cnf(d535,plain,
( tail = X0
| seq = X0
| select(q8,X0) = select(q7,X0) ),
inference(superposition,[status(thm)],[d534,d533]) ).
cnf(d536,plain,
( seq = X0
| select('queue$u275',X0) = select(q8,X0) ),
inference(superposition,[status(thm)],[c326,c1]) ).
cnf(d537,plain,
( tail = X0
| select('queue$u277',X0) = select('queue$u275',X0) ),
inference(superposition,[status(thm)],[c327,c1]) ).
cnf(d538,plain,
( tail = X0
| seq = X0
| select('queue$u277',X0) = select(q8,X0) ),
inference(superposition,[status(thm)],[d537,d536]) ).
cnf(d539,plain,
( seq = head
| tail = head
| 'index$u278' = select(q8,head) ),
inference(superposition,[status(thm)],[d538,c228]) ).
cnf(d540,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u278' = select(q7,head) ),
inference(superposition,[status(thm)],[d539,d535]) ).
cnf(d541,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u278' = select(q6,head) ),
inference(superposition,[status(thm)],[d540,d532]) ).
cnf(d542,plain,
( 'index$u278' = 'index$u258'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d541,d529]) ).
cnf(d543,plain,
( seq = head
| tail = head
| 'index$u279' = s('index$u258') ),
inference(superposition,[status(thm)],[d542,c229]) ).
cnf(d544,plain,
q2 = store('queue$u80',tail,'index$u81'),
inference(demodulation,[status(thm)],[c349,c367]) ).
cnf(d545,plain,
select(q2,tail) = 'index$u81',
inference(superposition,[status(thm)],[d544,c0]) ).
cnf(d546,plain,
'index$u153' = 'index$u81',
inference(demodulation,[status(thm)],[d545,c175]) ).
cnf(d547,plain,
'index$u153' = s('index$u78'),
inference(demodulation,[status(thm)],[c252,d546]) ).
cnf(d548,plain,
select(q3,head) = 'index$u159',
inference(superposition,[status(thm)],[d523,c0]) ).
cnf(d549,plain,
( seq = X0
| select('queue$u236',X0) = select(q3,X0) ),
inference(superposition,[status(thm)],[c312,c1]) ).
cnf(d550,plain,
( tail = X0
| select(q4,X0) = select('queue$u236',X0) ),
inference(superposition,[status(thm)],[d501,c1]) ).
cnf(d551,plain,
( tail = X0
| seq = X0
| select(q4,X0) = select(q3,X0) ),
inference(superposition,[status(thm)],[d550,d549]) ).
cnf(d552,plain,
( seq = X0
| select('queue$u248',X0) = select(q4,X0) ),
inference(superposition,[status(thm)],[c316,c1]) ).
cnf(d553,plain,
( tail = X0
| select(q5,X0) = select('queue$u248',X0) ),
inference(superposition,[status(thm)],[d484,c1]) ).
cnf(d554,plain,
( tail = X0
| seq = X0
| select(q5,X0) = select(q4,X0) ),
inference(superposition,[status(thm)],[d553,d552]) ).
cnf(d555,plain,
( seq = X0
| select('queue$u254',X0) = select(q5,X0) ),
inference(superposition,[status(thm)],[c319,c1]) ).
cnf(d556,plain,
( tail = X0
| select('queue$u256',X0) = select('queue$u254',X0) ),
inference(superposition,[status(thm)],[c320,c1]) ).
cnf(d557,plain,
( tail = X0
| seq = X0
| select('queue$u256',X0) = select(q5,X0) ),
inference(superposition,[status(thm)],[d556,d555]) ).
cnf(d558,plain,
( seq = head
| tail = head
| 'index$u257' = select(q5,head) ),
inference(superposition,[status(thm)],[d557,c218]) ).
cnf(d559,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u257' = select(q4,head) ),
inference(superposition,[status(thm)],[d558,d554]) ).
cnf(d560,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u257' = select(q3,head) ),
inference(superposition,[status(thm)],[d559,d551]) ).
cnf(d561,plain,
( 'index$u257' = 'index$u159'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d560,d548]) ).
cnf(d562,plain,
( seq = head
| tail = head
| 'index$u258' = s('index$u159') ),
inference(superposition,[status(thm)],[d561,c219]) ).
cnf(d563,plain,
q1 = store('queue$u5',tail,'index$u6'),
inference(demodulation,[status(thm)],[c344,c356]) ).
cnf(d564,plain,
select(q1,tail) = 'index$u6',
inference(superposition,[status(thm)],[d563,c0]) ).
cnf(d565,plain,
'index$u78' = 'index$u6',
inference(demodulation,[status(thm)],[d564,c251]) ).
cnf(d566,plain,
'index$u78' = s('index$u3'),
inference(demodulation,[status(thm)],[c243,d565]) ).
cnf(d567,plain,
( seq = X0
| select('queue$u155',X0) = select(q2,X0) ),
inference(superposition,[status(thm)],[c282,c1]) ).
cnf(d568,plain,
( tail = X0
| select('queue$u157',X0) = select('queue$u155',X0) ),
inference(superposition,[status(thm)],[c283,c1]) ).
cnf(d569,plain,
( tail = X0
| seq = X0
| select('queue$u157',X0) = select(q2,X0) ),
inference(superposition,[status(thm)],[d568,d567]) ).
cnf(d570,plain,
( seq = head
| tail = head
| 'index$u158' = select(q2,head) ),
inference(superposition,[status(thm)],[d569,c177]) ).
cnf(d571,plain,
q0 = store(q,head,'index$u0'),
inference(demodulation,[status(thm)],[c261,c355]) ).
cnf(d572,plain,
( head = X0
| select(q0,X0) = select(q,X0) ),
inference(superposition,[status(thm)],[d571,c1]) ).
cnf(d573,plain,
( head = tail
| 'index$u0' = select(q0,tail) ),
inference(superposition,[status(thm)],[d572,c153]) ).
cnf(d574,plain,
( 'index$u0' = 'index$u3'
| head = tail ),
inference(demodulation,[status(thm)],[d573,c231]) ).
cnf(d575,plain,
'index$u0' = 'index$u3',
inference(resolution,[status(thm)],[c2,d574]) ).
cnf(d576,plain,
select(q0,head) = 'index$u0',
inference(superposition,[status(thm)],[d571,c0]) ).
cnf(d577,plain,
select(q0,head) = 'index$u3',
inference(demodulation,[status(thm)],[d576,d575]) ).
cnf(d578,plain,
( seq = X0
| select('queue$u5',X0) = select(q0,X0) ),
inference(superposition,[status(thm)],[c337,c1]) ).
cnf(d579,plain,
( tail = X0
| select(q1,X0) = select('queue$u5',X0) ),
inference(superposition,[status(thm)],[d563,c1]) ).
cnf(d580,plain,
( tail = X0
| seq = X0
| select(q1,X0) = select(q0,X0) ),
inference(superposition,[status(thm)],[d579,d578]) ).
cnf(d581,plain,
( seq = X0
| select('queue$u80',X0) = select(q1,X0) ),
inference(superposition,[status(thm)],[c348,c1]) ).
cnf(d582,plain,
( tail = X0
| select(q2,X0) = select('queue$u80',X0) ),
inference(superposition,[status(thm)],[d544,c1]) ).
cnf(d583,plain,
( tail = X0
| seq = X0
| select(q2,X0) = select(q1,X0) ),
inference(superposition,[status(thm)],[d582,d581]) ).
cnf(d584,plain,
( seq = X0
| tail = X0
| seq = X0
| tail = X0
| select(q2,X0) = select(q0,X0) ),
inference(superposition,[status(thm)],[d583,d580]) ).
cnf(d585,plain,
( seq = head
| tail = head
| select(q2,head) = 'index$u3' ),
inference(superposition,[status(thm)],[d584,d577]) ).
cnf(d586,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u158' = 'index$u3' ),
inference(superposition,[status(thm)],[d585,d570]) ).
cnf(d587,plain,
( seq = head
| tail = head
| 'index$u159' = s('index$u3') ),
inference(superposition,[status(thm)],[d586,c178]) ).
cnf(d588,plain,
( 'index$u159' = 'index$u78'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d587,d566]) ).
cnf(d589,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u258' = s('index$u78') ),
inference(superposition,[status(thm)],[d588,d562]) ).
cnf(d590,plain,
( 'index$u258' = 'index$u153'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d589,d547]) ).
cnf(d591,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u279' = s('index$u153') ),
inference(superposition,[status(thm)],[d590,d543]) ).
cnf(d592,plain,
( 'index$u279' = 'index$u234'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d591,d528]) ).
cnf(d593,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u234' = 'index$u26' ),
inference(superposition,[status(thm)],[d592,d521]) ).
cnf(d594,plain,
( seq = head
| tail = head
| 'index$u27' = s('index$u234') ),
inference(superposition,[status(thm)],[d593,c224]) ).
cnf(d595,plain,
( 'index$u27' = 'index$u246'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d594,d504]) ).
cnf(d596,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u48' = s('index$u246') ),
inference(superposition,[status(thm)],[d595,d500]) ).
cnf(d597,plain,
( 'index$u48' = 'index$u252'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d596,d487]) ).
cnf(d598,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u69' = s('index$u252') ),
inference(superposition,[status(thm)],[d597,d483]) ).
cnf(d599,plain,
( 'index$u69' = 'index$u261'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d598,d471]) ).
cnf(d600,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u96' = s('index$u261') ),
inference(superposition,[status(thm)],[d599,d464]) ).
cnf(d601,plain,
( 'index$u96' = 'index$u267'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d600,d452]) ).
cnf(d602,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u267' = 'index$u116' ),
inference(superposition,[status(thm)],[d601,d448]) ).
cnf(d603,plain,
( seq = head
| tail = head
| 'index$u117' = s('index$u267') ),
inference(superposition,[status(thm)],[d602,c160]) ).
cnf(d604,plain,
( 'index$u117' = 'index$u273'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d603,d434]) ).
cnf(d605,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u138' = s('index$u273') ),
inference(superposition,[status(thm)],[d604,d430]) ).
cnf(d606,plain,
( 'index$u138' = 'index$u9'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d605,d418]) ).
cnf(d607,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u168' = s('index$u9') ),
inference(superposition,[status(thm)],[d606,d411]) ).
cnf(d608,plain,
( 'index$u168' = 'index$u15'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d607,d399]) ).
cnf(d609,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u189' = s('index$u15') ),
inference(superposition,[status(thm)],[d608,d395]) ).
cnf(d610,plain,
( 'index$u189' = 'index$u21'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d609,d383]) ).
cnf(d611,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u210' = s('index$u21') ),
inference(superposition,[status(thm)],[d610,d379]) ).
cnf(d612,plain,
( 'index$u210' = 'index$u30'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d611,d367]) ).
cnf(d613,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u231' = s('index$u30') ),
inference(superposition,[status(thm)],[d612,d360]) ).
cnf(d614,plain,
( 'index$u231' = 'index$u36'
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d613,d348]) ).
cnf(d615,plain,
( seq = head
| tail = head
| seq = head
| tail = head
| 'index$u36' = 'index$u282' ),
inference(superposition,[status(thm)],[d614,d344]) ).
cnf(d616,plain,
( seq = head
| tail = head
| 'elem$u283' = select('earray$u241','index$u36') ),
inference(superposition,[status(thm)],[d615,d336]) ).
cnf(d617,plain,
( seq = head
| tail = head
| 'index$u240' = 'index$u36'
| 'elem$u283' = select('earray$u226','index$u36') ),
inference(superposition,[status(thm)],[d616,d329]) ).
cnf(d618,plain,
( 'index$u240' = 'index$u36'
| seq = head
| tail = head
| 'index$u225' = 'index$u36'
| 'elem$u283' = select('earray$u220','index$u36') ),
inference(superposition,[status(thm)],[d617,d318]) ).
cnf(d619,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| seq = head
| tail = head
| 'index$u219' = 'index$u36'
| 'elem$u283' = select('earray$u214','index$u36') ),
inference(superposition,[status(thm)],[d618,d310]) ).
cnf(d620,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u213' = 'index$u36'
| 'elem$u283' = select('earray$u205','index$u36') ),
inference(superposition,[status(thm)],[d619,d302]) ).
cnf(d621,plain,
select('queue$u208',tail) = 'index$u207',
inference(superposition,[status(thm)],[c302,c0]) ).
cnf(d622,plain,
( head = tail
| select(q36,tail) = 'index$u207' ),
inference(superposition,[status(thm)],[d297,d621]) ).
cnf(d623,plain,
( head = tail
| 'index$u213' = 'index$u207' ),
inference(demodulation,[status(thm)],[d622,c201]) ).
cnf(d624,plain,
'index$u213' = 'index$u207',
inference(resolution,[status(thm)],[c2,d623]) ).
cnf(d625,plain,
'index$u213' = s('index$u204'),
inference(demodulation,[status(thm)],[c197,d624]) ).
cnf(d626,plain,
select(q35,tail) = 'index$u201',
inference(superposition,[status(thm)],[d285,c0]) ).
cnf(d627,plain,
'index$u204' = 'index$u201',
inference(demodulation,[status(thm)],[d626,c196]) ).
cnf(d628,plain,
'index$u204' = s('index$u198'),
inference(demodulation,[status(thm)],[c195,d627]) ).
cnf(d629,plain,
select(q34,tail) = 'index$u195',
inference(superposition,[status(thm)],[d277,c0]) ).
cnf(d630,plain,
'index$u198' = 'index$u195',
inference(demodulation,[status(thm)],[d629,c194]) ).
cnf(d631,plain,
'index$u198' = s('index$u192'),
inference(demodulation,[status(thm)],[c193,d630]) ).
cnf(d632,plain,
select('queue$u187',tail) = 'index$u186',
inference(superposition,[status(thm)],[c294,c0]) ).
cnf(d633,plain,
( head = tail
| select(q33,tail) = 'index$u186' ),
inference(superposition,[status(thm)],[d270,d632]) ).
cnf(d634,plain,
( head = tail
| 'index$u192' = 'index$u186' ),
inference(demodulation,[status(thm)],[d633,c192]) ).
cnf(d635,plain,
'index$u192' = 'index$u186',
inference(resolution,[status(thm)],[c2,d634]) ).
cnf(d636,plain,
'index$u192' = s('index$u183'),
inference(demodulation,[status(thm)],[c189,d635]) ).
cnf(d637,plain,
select(q32,tail) = 'index$u180',
inference(superposition,[status(thm)],[d258,c0]) ).
cnf(d638,plain,
'index$u183' = 'index$u180',
inference(demodulation,[status(thm)],[d637,c188]) ).
cnf(d639,plain,
'index$u183' = s('index$u177'),
inference(demodulation,[status(thm)],[c187,d638]) ).
cnf(d640,plain,
select(q31,tail) = 'index$u174',
inference(superposition,[status(thm)],[d250,c0]) ).
cnf(d641,plain,
'index$u177' = 'index$u174',
inference(demodulation,[status(thm)],[d640,c185]) ).
cnf(d642,plain,
'index$u177' = s('index$u171'),
inference(demodulation,[status(thm)],[c184,d641]) ).
cnf(d643,plain,
select('queue$u166',tail) = 'index$u165',
inference(superposition,[status(thm)],[c286,c0]) ).
cnf(d644,plain,
( head = tail
| select(q30,tail) = 'index$u165' ),
inference(superposition,[status(thm)],[d243,d643]) ).
cnf(d645,plain,
( head = tail
| 'index$u171' = 'index$u165' ),
inference(demodulation,[status(thm)],[d644,c183]) ).
cnf(d646,plain,
'index$u171' = 'index$u165',
inference(resolution,[status(thm)],[c2,d645]) ).
cnf(d647,plain,
'index$u171' = s('index$u162'),
inference(demodulation,[status(thm)],[c180,d646]) ).
cnf(d648,plain,
select(q29,tail) = 'index$u150',
inference(superposition,[status(thm)],[d231,c0]) ).
cnf(d649,plain,
'index$u162' = 'index$u150',
inference(demodulation,[status(thm)],[d648,c179]) ).
cnf(d650,plain,
'index$u162' = s('index$u147'),
inference(demodulation,[status(thm)],[c174,d649]) ).
cnf(d651,plain,
select(q28,tail) = 'index$u144',
inference(superposition,[status(thm)],[d223,c0]) ).
cnf(d652,plain,
'index$u147' = 'index$u144',
inference(demodulation,[status(thm)],[d651,c172]) ).
cnf(d653,plain,
'index$u147' = s('index$u141'),
inference(demodulation,[status(thm)],[c171,d652]) ).
cnf(d654,plain,
select('queue$u136',tail) = 'index$u135',
inference(superposition,[status(thm)],[c276,c0]) ).
cnf(d655,plain,
( head = tail
| select(q27,tail) = 'index$u135' ),
inference(superposition,[status(thm)],[d216,d654]) ).
cnf(d656,plain,
( head = tail
| 'index$u141' = 'index$u135' ),
inference(demodulation,[status(thm)],[d655,c170]) ).
cnf(d657,plain,
'index$u141' = 'index$u135',
inference(resolution,[status(thm)],[c2,d656]) ).
cnf(d658,plain,
'index$u141' = s('index$u132'),
inference(demodulation,[status(thm)],[c167,d657]) ).
cnf(d659,plain,
select(q26,tail) = 'index$u129',
inference(superposition,[status(thm)],[d204,c0]) ).
cnf(d660,plain,
'index$u132' = 'index$u129',
inference(demodulation,[status(thm)],[d659,c166]) ).
cnf(d661,plain,
'index$u132' = s('index$u126'),
inference(demodulation,[status(thm)],[c165,d660]) ).
cnf(d662,plain,
select(q25,tail) = 'index$u123',
inference(superposition,[status(thm)],[d196,c0]) ).
cnf(d663,plain,
'index$u126' = 'index$u123',
inference(demodulation,[status(thm)],[d662,c164]) ).
cnf(d664,plain,
'index$u126' = s('index$u120'),
inference(demodulation,[status(thm)],[c163,d663]) ).
cnf(d665,plain,
select('queue$u115',tail) = 'index$u114',
inference(superposition,[status(thm)],[c268,c0]) ).
cnf(d666,plain,
( head = tail
| select(q24,tail) = 'index$u114' ),
inference(superposition,[status(thm)],[d189,d665]) ).
cnf(d667,plain,
( head = tail
| 'index$u120' = 'index$u114' ),
inference(demodulation,[status(thm)],[d666,c162]) ).
cnf(d668,plain,
'index$u120' = 'index$u114',
inference(resolution,[status(thm)],[c2,d667]) ).
cnf(d669,plain,
'index$u120' = s('index$u111'),
inference(demodulation,[status(thm)],[c158,d668]) ).
cnf(d670,plain,
select(q23,tail) = 'index$u108',
inference(superposition,[status(thm)],[d177,c0]) ).
cnf(d671,plain,
'index$u111' = 'index$u108',
inference(demodulation,[status(thm)],[d670,c157]) ).
cnf(d672,plain,
'index$u111' = s('index$u105'),
inference(demodulation,[status(thm)],[c156,d671]) ).
cnf(d673,plain,
select(q22,tail) = 'index$u102',
inference(superposition,[status(thm)],[d169,c0]) ).
cnf(d674,plain,
'index$u105' = 'index$u102',
inference(demodulation,[status(thm)],[d673,c155]) ).
cnf(d675,plain,
'index$u105' = s('index$u99'),
inference(demodulation,[status(thm)],[c154,d674]) ).
cnf(d676,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u39')))))))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[c235,c48]) ).
cnf(d677,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42')))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d676,d92]) ).
cnf(d678,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51'))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d677,d158]) ).
cnf(d679,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57')))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d678,d86]) ).
cnf(d680,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63'))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d679,d83]) ).
cnf(d681,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72')))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d680,d157]) ).
cnf(d682,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d681,d108]) ).
cnf(d683,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u90')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d682,d105]) ).
cnf(d684,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u99'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d683,d156]) ).
cnf(d685,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u105')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d684,d675]) ).
cnf(d686,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u111'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d685,d672]) ).
cnf(d687,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u120')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d686,d669]) ).
cnf(d688,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u126'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d687,d664]) ).
cnf(d689,plain,
s(s(s(s(s(s(s(s(s(s('index$u132')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d688,d661]) ).
cnf(d690,plain,
s(s(s(s(s(s(s(s(s('index$u141'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d689,d658]) ).
cnf(d691,plain,
s(s(s(s(s(s(s(s('index$u147')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d690,d653]) ).
cnf(d692,plain,
s(s(s(s(s(s(s('index$u162'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d691,d650]) ).
cnf(d693,plain,
s(s(s(s(s(s('index$u171')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d692,d647]) ).
cnf(d694,plain,
s(s(s(s(s('index$u177'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d693,d642]) ).
cnf(d695,plain,
s(s(s(s('index$u183')))) != 'index$u36',
inference(demodulation,[status(thm)],[d694,d639]) ).
cnf(d696,plain,
s(s(s('index$u192'))) != 'index$u36',
inference(demodulation,[status(thm)],[d695,d636]) ).
cnf(d697,plain,
s(s('index$u198')) != 'index$u36',
inference(demodulation,[status(thm)],[d696,d631]) ).
cnf(d698,plain,
s('index$u204') != 'index$u36',
inference(demodulation,[status(thm)],[d697,d628]) ).
cnf(d699,plain,
'index$u213' != 'index$u36',
inference(demodulation,[status(thm)],[d698,d625]) ).
cnf(d700,plain,
( 'elem$u283' = select('earray$u205','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d699,d620]) ).
cnf(d701,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u204' = 'index$u36'
| 'elem$u283' = select('earray$u199','index$u36') ),
inference(superposition,[status(thm)],[d700,d291]) ).
cnf(d702,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c49]) ).
cnf(d703,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51')))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d702,d158]) ).
cnf(d704,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57'))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d703,d86]) ).
cnf(d705,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63')))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d704,d83]) ).
cnf(d706,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d705,d157]) ).
cnf(d707,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d706,d108]) ).
cnf(d708,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u90'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d707,d105]) ).
cnf(d709,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u99')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d708,d156]) ).
cnf(d710,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u105'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d709,d675]) ).
cnf(d711,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u111')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d710,d672]) ).
cnf(d712,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u120'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d711,d669]) ).
cnf(d713,plain,
s(s(s(s(s(s(s(s(s(s('index$u126')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d712,d664]) ).
cnf(d714,plain,
s(s(s(s(s(s(s(s(s('index$u132'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d713,d661]) ).
cnf(d715,plain,
s(s(s(s(s(s(s(s('index$u141')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d714,d658]) ).
cnf(d716,plain,
s(s(s(s(s(s(s('index$u147'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d715,d653]) ).
cnf(d717,plain,
s(s(s(s(s(s('index$u162')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d716,d650]) ).
cnf(d718,plain,
s(s(s(s(s('index$u171'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d717,d647]) ).
cnf(d719,plain,
s(s(s(s('index$u177')))) != 'index$u36',
inference(demodulation,[status(thm)],[d718,d642]) ).
cnf(d720,plain,
s(s(s('index$u183'))) != 'index$u36',
inference(demodulation,[status(thm)],[d719,d639]) ).
cnf(d721,plain,
s(s('index$u192')) != 'index$u36',
inference(demodulation,[status(thm)],[d720,d636]) ).
cnf(d722,plain,
s('index$u198') != 'index$u36',
inference(demodulation,[status(thm)],[d721,d631]) ).
cnf(d723,plain,
'index$u204' != 'index$u36',
inference(demodulation,[status(thm)],[d722,d628]) ).
cnf(d724,plain,
( 'elem$u283' = select('earray$u199','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d723,d701]) ).
cnf(d725,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u198' = 'index$u36'
| 'elem$u283' = select('earray$u193','index$u36') ),
inference(superposition,[status(thm)],[d724,d283]) ).
cnf(d726,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42')))))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c50]) ).
cnf(d727,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51'))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d726,d158]) ).
cnf(d728,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57')))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d727,d86]) ).
cnf(d729,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d728,d83]) ).
cnf(d730,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d729,d157]) ).
cnf(d731,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d730,d108]) ).
cnf(d732,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u90')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d731,d105]) ).
cnf(d733,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u99'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d732,d156]) ).
cnf(d734,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u105')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d733,d675]) ).
cnf(d735,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u111'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d734,d672]) ).
cnf(d736,plain,
s(s(s(s(s(s(s(s(s(s('index$u120')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d735,d669]) ).
cnf(d737,plain,
s(s(s(s(s(s(s(s(s('index$u126'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d736,d664]) ).
cnf(d738,plain,
s(s(s(s(s(s(s(s('index$u132')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d737,d661]) ).
cnf(d739,plain,
s(s(s(s(s(s(s('index$u141'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d738,d658]) ).
cnf(d740,plain,
s(s(s(s(s(s('index$u147')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d739,d653]) ).
cnf(d741,plain,
s(s(s(s(s('index$u162'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d740,d650]) ).
cnf(d742,plain,
s(s(s(s('index$u171')))) != 'index$u36',
inference(demodulation,[status(thm)],[d741,d647]) ).
cnf(d743,plain,
s(s(s('index$u177'))) != 'index$u36',
inference(demodulation,[status(thm)],[d742,d642]) ).
cnf(d744,plain,
s(s('index$u183')) != 'index$u36',
inference(demodulation,[status(thm)],[d743,d639]) ).
cnf(d745,plain,
s('index$u192') != 'index$u36',
inference(demodulation,[status(thm)],[d744,d636]) ).
cnf(d746,plain,
'index$u198' != 'index$u36',
inference(demodulation,[status(thm)],[d745,d631]) ).
cnf(d747,plain,
( 'elem$u283' = select('earray$u193','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d746,d725]) ).
cnf(d748,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u192' = 'index$u36'
| 'elem$u283' = select('earray$u184','index$u36') ),
inference(superposition,[status(thm)],[d747,d275]) ).
cnf(d749,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c51]) ).
cnf(d750,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51')))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d749,d158]) ).
cnf(d751,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d750,d86]) ).
cnf(d752,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d751,d83]) ).
cnf(d753,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d752,d157]) ).
cnf(d754,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d753,d108]) ).
cnf(d755,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u90'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d754,d105]) ).
cnf(d756,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u99')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d755,d156]) ).
cnf(d757,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u105'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d756,d675]) ).
cnf(d758,plain,
s(s(s(s(s(s(s(s(s(s('index$u111')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d757,d672]) ).
cnf(d759,plain,
s(s(s(s(s(s(s(s(s('index$u120'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d758,d669]) ).
cnf(d760,plain,
s(s(s(s(s(s(s(s('index$u126')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d759,d664]) ).
cnf(d761,plain,
s(s(s(s(s(s(s('index$u132'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d760,d661]) ).
cnf(d762,plain,
s(s(s(s(s(s('index$u141')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d761,d658]) ).
cnf(d763,plain,
s(s(s(s(s('index$u147'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d762,d653]) ).
cnf(d764,plain,
s(s(s(s('index$u162')))) != 'index$u36',
inference(demodulation,[status(thm)],[d763,d650]) ).
cnf(d765,plain,
s(s(s('index$u171'))) != 'index$u36',
inference(demodulation,[status(thm)],[d764,d647]) ).
cnf(d766,plain,
s(s('index$u177')) != 'index$u36',
inference(demodulation,[status(thm)],[d765,d642]) ).
cnf(d767,plain,
s('index$u183') != 'index$u36',
inference(demodulation,[status(thm)],[d766,d639]) ).
cnf(d768,plain,
'index$u192' != 'index$u36',
inference(demodulation,[status(thm)],[d767,d636]) ).
cnf(d769,plain,
( 'elem$u283' = select('earray$u184','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d768,d748]) ).
cnf(d770,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u183' = 'index$u36'
| 'elem$u283' = select('earray$u178','index$u36') ),
inference(superposition,[status(thm)],[d769,d264]) ).
cnf(d771,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42')))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c52]) ).
cnf(d772,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d771,d158]) ).
cnf(d773,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d772,d86]) ).
cnf(d774,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d773,d83]) ).
cnf(d775,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d774,d157]) ).
cnf(d776,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d775,d108]) ).
cnf(d777,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u90')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d776,d105]) ).
cnf(d778,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u99'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d777,d156]) ).
cnf(d779,plain,
s(s(s(s(s(s(s(s(s(s('index$u105')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d778,d675]) ).
cnf(d780,plain,
s(s(s(s(s(s(s(s(s('index$u111'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d779,d672]) ).
cnf(d781,plain,
s(s(s(s(s(s(s(s('index$u120')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d780,d669]) ).
cnf(d782,plain,
s(s(s(s(s(s(s('index$u126'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d781,d664]) ).
cnf(d783,plain,
s(s(s(s(s(s('index$u132')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d782,d661]) ).
cnf(d784,plain,
s(s(s(s(s('index$u141'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d783,d658]) ).
cnf(d785,plain,
s(s(s(s('index$u147')))) != 'index$u36',
inference(demodulation,[status(thm)],[d784,d653]) ).
cnf(d786,plain,
s(s(s('index$u162'))) != 'index$u36',
inference(demodulation,[status(thm)],[d785,d650]) ).
cnf(d787,plain,
s(s('index$u171')) != 'index$u36',
inference(demodulation,[status(thm)],[d786,d647]) ).
cnf(d788,plain,
s('index$u177') != 'index$u36',
inference(demodulation,[status(thm)],[d787,d642]) ).
cnf(d789,plain,
'index$u183' != 'index$u36',
inference(demodulation,[status(thm)],[d788,d639]) ).
cnf(d790,plain,
( 'elem$u283' = select('earray$u178','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d789,d770]) ).
cnf(d791,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u177' = 'index$u36'
| 'elem$u283' = select('earray$u172','index$u36') ),
inference(superposition,[status(thm)],[d790,d256]) ).
cnf(d792,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c53]) ).
cnf(d793,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d792,d158]) ).
cnf(d794,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d793,d86]) ).
cnf(d795,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d794,d83]) ).
cnf(d796,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d795,d157]) ).
cnf(d797,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u84')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d796,d108]) ).
cnf(d798,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u90'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d797,d105]) ).
cnf(d799,plain,
s(s(s(s(s(s(s(s(s(s('index$u99')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d798,d156]) ).
cnf(d800,plain,
s(s(s(s(s(s(s(s(s('index$u105'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d799,d675]) ).
cnf(d801,plain,
s(s(s(s(s(s(s(s('index$u111')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d800,d672]) ).
cnf(d802,plain,
s(s(s(s(s(s(s('index$u120'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d801,d669]) ).
cnf(d803,plain,
s(s(s(s(s(s('index$u126')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d802,d664]) ).
cnf(d804,plain,
s(s(s(s(s('index$u132'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d803,d661]) ).
cnf(d805,plain,
s(s(s(s('index$u141')))) != 'index$u36',
inference(demodulation,[status(thm)],[d804,d658]) ).
cnf(d806,plain,
s(s(s('index$u147'))) != 'index$u36',
inference(demodulation,[status(thm)],[d805,d653]) ).
cnf(d807,plain,
s(s('index$u162')) != 'index$u36',
inference(demodulation,[status(thm)],[d806,d650]) ).
cnf(d808,plain,
s('index$u171') != 'index$u36',
inference(demodulation,[status(thm)],[d807,d647]) ).
cnf(d809,plain,
'index$u177' != 'index$u36',
inference(demodulation,[status(thm)],[d808,d642]) ).
cnf(d810,plain,
( 'elem$u283' = select('earray$u172','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d809,d791]) ).
cnf(d811,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u171' = 'index$u36'
| 'elem$u283' = select('earray$u163','index$u36') ),
inference(superposition,[status(thm)],[d810,d248]) ).
cnf(d812,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42')))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c54]) ).
cnf(d813,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d812,d158]) ).
cnf(d814,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d813,d86]) ).
cnf(d815,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d814,d83]) ).
cnf(d816,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u72')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d815,d157]) ).
cnf(d817,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u84'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d816,d108]) ).
cnf(d818,plain,
s(s(s(s(s(s(s(s(s(s('index$u90')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d817,d105]) ).
cnf(d819,plain,
s(s(s(s(s(s(s(s(s('index$u99'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d818,d156]) ).
cnf(d820,plain,
s(s(s(s(s(s(s(s('index$u105')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d819,d675]) ).
cnf(d821,plain,
s(s(s(s(s(s(s('index$u111'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d820,d672]) ).
cnf(d822,plain,
s(s(s(s(s(s('index$u120')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d821,d669]) ).
cnf(d823,plain,
s(s(s(s(s('index$u126'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d822,d664]) ).
cnf(d824,plain,
s(s(s(s('index$u132')))) != 'index$u36',
inference(demodulation,[status(thm)],[d823,d661]) ).
cnf(d825,plain,
s(s(s('index$u141'))) != 'index$u36',
inference(demodulation,[status(thm)],[d824,d658]) ).
cnf(d826,plain,
s(s('index$u147')) != 'index$u36',
inference(demodulation,[status(thm)],[d825,d653]) ).
cnf(d827,plain,
s('index$u162') != 'index$u36',
inference(demodulation,[status(thm)],[d826,d650]) ).
cnf(d828,plain,
'index$u171' != 'index$u36',
inference(demodulation,[status(thm)],[d827,d647]) ).
cnf(d829,plain,
( 'elem$u283' = select('earray$u163','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d828,d811]) ).
cnf(d830,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u162' = 'index$u36'
| 'elem$u283' = select('earray$u148','index$u36') ),
inference(superposition,[status(thm)],[d829,d237]) ).
cnf(d831,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c55]) ).
cnf(d832,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d831,d158]) ).
cnf(d833,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d832,d86]) ).
cnf(d834,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u63')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d833,d83]) ).
cnf(d835,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u72'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d834,d157]) ).
cnf(d836,plain,
s(s(s(s(s(s(s(s(s(s('index$u84')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d835,d108]) ).
cnf(d837,plain,
s(s(s(s(s(s(s(s(s('index$u90'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d836,d105]) ).
cnf(d838,plain,
s(s(s(s(s(s(s(s('index$u99')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d837,d156]) ).
cnf(d839,plain,
s(s(s(s(s(s(s('index$u105'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d838,d675]) ).
cnf(d840,plain,
s(s(s(s(s(s('index$u111')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d839,d672]) ).
cnf(d841,plain,
s(s(s(s(s('index$u120'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d840,d669]) ).
cnf(d842,plain,
s(s(s(s('index$u126')))) != 'index$u36',
inference(demodulation,[status(thm)],[d841,d664]) ).
cnf(d843,plain,
s(s(s('index$u132'))) != 'index$u36',
inference(demodulation,[status(thm)],[d842,d661]) ).
cnf(d844,plain,
s(s('index$u141')) != 'index$u36',
inference(demodulation,[status(thm)],[d843,d658]) ).
cnf(d845,plain,
s('index$u147') != 'index$u36',
inference(demodulation,[status(thm)],[d844,d653]) ).
cnf(d846,plain,
'index$u162' != 'index$u36',
inference(demodulation,[status(thm)],[d845,d650]) ).
cnf(d847,plain,
( 'elem$u283' = select('earray$u148','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d846,d830]) ).
cnf(d848,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u147' = 'index$u36'
| 'elem$u283' = select('earray$u142','index$u36') ),
inference(superposition,[status(thm)],[d847,d229]) ).
cnf(d849,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42')))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c56]) ).
cnf(d850,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d849,d158]) ).
cnf(d851,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u57')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d850,d86]) ).
cnf(d852,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u63'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d851,d83]) ).
cnf(d853,plain,
s(s(s(s(s(s(s(s(s(s('index$u72')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d852,d157]) ).
cnf(d854,plain,
s(s(s(s(s(s(s(s(s('index$u84'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d853,d108]) ).
cnf(d855,plain,
s(s(s(s(s(s(s(s('index$u90')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d854,d105]) ).
cnf(d856,plain,
s(s(s(s(s(s(s('index$u99'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d855,d156]) ).
cnf(d857,plain,
s(s(s(s(s(s('index$u105')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d856,d675]) ).
cnf(d858,plain,
s(s(s(s(s('index$u111'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d857,d672]) ).
cnf(d859,plain,
s(s(s(s('index$u120')))) != 'index$u36',
inference(demodulation,[status(thm)],[d858,d669]) ).
cnf(d860,plain,
s(s(s('index$u126'))) != 'index$u36',
inference(demodulation,[status(thm)],[d859,d664]) ).
cnf(d861,plain,
s(s('index$u132')) != 'index$u36',
inference(demodulation,[status(thm)],[d860,d661]) ).
cnf(d862,plain,
s('index$u141') != 'index$u36',
inference(demodulation,[status(thm)],[d861,d658]) ).
cnf(d863,plain,
'index$u147' != 'index$u36',
inference(demodulation,[status(thm)],[d862,d653]) ).
cnf(d864,plain,
( 'elem$u283' = select('earray$u142','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d863,d848]) ).
cnf(d865,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u141' = 'index$u36'
| 'elem$u283' = select('earray$u133','index$u36') ),
inference(superposition,[status(thm)],[d864,d221]) ).
cnf(d866,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c57]) ).
cnf(d867,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u51')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d866,d158]) ).
cnf(d868,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u57'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d867,d86]) ).
cnf(d869,plain,
s(s(s(s(s(s(s(s(s(s('index$u63')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d868,d83]) ).
cnf(d870,plain,
s(s(s(s(s(s(s(s(s('index$u72'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d869,d157]) ).
cnf(d871,plain,
s(s(s(s(s(s(s(s('index$u84')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d870,d108]) ).
cnf(d872,plain,
s(s(s(s(s(s(s('index$u90'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d871,d105]) ).
cnf(d873,plain,
s(s(s(s(s(s('index$u99')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d872,d156]) ).
cnf(d874,plain,
s(s(s(s(s('index$u105'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d873,d675]) ).
cnf(d875,plain,
s(s(s(s('index$u111')))) != 'index$u36',
inference(demodulation,[status(thm)],[d874,d672]) ).
cnf(d876,plain,
s(s(s('index$u120'))) != 'index$u36',
inference(demodulation,[status(thm)],[d875,d669]) ).
cnf(d877,plain,
s(s('index$u126')) != 'index$u36',
inference(demodulation,[status(thm)],[d876,d664]) ).
cnf(d878,plain,
s('index$u132') != 'index$u36',
inference(demodulation,[status(thm)],[d877,d661]) ).
cnf(d879,plain,
'index$u141' != 'index$u36',
inference(demodulation,[status(thm)],[d878,d658]) ).
cnf(d880,plain,
( 'elem$u283' = select('earray$u133','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d879,d865]) ).
cnf(d881,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u132' = 'index$u36'
| 'elem$u283' = select('earray$u127','index$u36') ),
inference(superposition,[status(thm)],[d880,d210]) ).
cnf(d882,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u42')))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c58]) ).
cnf(d883,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u51'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d882,d158]) ).
cnf(d884,plain,
s(s(s(s(s(s(s(s(s(s('index$u57')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d883,d86]) ).
cnf(d885,plain,
s(s(s(s(s(s(s(s(s('index$u63'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d884,d83]) ).
cnf(d886,plain,
s(s(s(s(s(s(s(s('index$u72')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d885,d157]) ).
cnf(d887,plain,
s(s(s(s(s(s(s('index$u84'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d886,d108]) ).
cnf(d888,plain,
s(s(s(s(s(s('index$u90')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d887,d105]) ).
cnf(d889,plain,
s(s(s(s(s('index$u99'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d888,d156]) ).
cnf(d890,plain,
s(s(s(s('index$u105')))) != 'index$u36',
inference(demodulation,[status(thm)],[d889,d675]) ).
cnf(d891,plain,
s(s(s('index$u111'))) != 'index$u36',
inference(demodulation,[status(thm)],[d890,d672]) ).
cnf(d892,plain,
s(s('index$u120')) != 'index$u36',
inference(demodulation,[status(thm)],[d891,d669]) ).
cnf(d893,plain,
s('index$u126') != 'index$u36',
inference(demodulation,[status(thm)],[d892,d664]) ).
cnf(d894,plain,
'index$u132' != 'index$u36',
inference(demodulation,[status(thm)],[d893,d661]) ).
cnf(d895,plain,
( 'elem$u283' = select('earray$u127','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d894,d881]) ).
cnf(d896,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u126' = 'index$u36'
| 'elem$u283' = select('earray$u121','index$u36') ),
inference(superposition,[status(thm)],[d895,d202]) ).
cnf(d897,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c59]) ).
cnf(d898,plain,
s(s(s(s(s(s(s(s(s(s('index$u51')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d897,d158]) ).
cnf(d899,plain,
s(s(s(s(s(s(s(s(s('index$u57'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d898,d86]) ).
cnf(d900,plain,
s(s(s(s(s(s(s(s('index$u63')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d899,d83]) ).
cnf(d901,plain,
s(s(s(s(s(s(s('index$u72'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d900,d157]) ).
cnf(d902,plain,
s(s(s(s(s(s('index$u84')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d901,d108]) ).
cnf(d903,plain,
s(s(s(s(s('index$u90'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d902,d105]) ).
cnf(d904,plain,
s(s(s(s('index$u99')))) != 'index$u36',
inference(demodulation,[status(thm)],[d903,d156]) ).
cnf(d905,plain,
s(s(s('index$u105'))) != 'index$u36',
inference(demodulation,[status(thm)],[d904,d675]) ).
cnf(d906,plain,
s(s('index$u111')) != 'index$u36',
inference(demodulation,[status(thm)],[d905,d672]) ).
cnf(d907,plain,
s('index$u120') != 'index$u36',
inference(demodulation,[status(thm)],[d906,d669]) ).
cnf(d908,plain,
'index$u126' != 'index$u36',
inference(demodulation,[status(thm)],[d907,d664]) ).
cnf(d909,plain,
( 'elem$u283' = select('earray$u121','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d908,d896]) ).
cnf(d910,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u120' = 'index$u36'
| 'elem$u283' = select('earray$u112','index$u36') ),
inference(superposition,[status(thm)],[d909,d194]) ).
cnf(d911,plain,
s(s(s(s(s(s(s(s(s(s('index$u42')))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c60]) ).
cnf(d912,plain,
s(s(s(s(s(s(s(s(s('index$u51'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d911,d158]) ).
cnf(d913,plain,
s(s(s(s(s(s(s(s('index$u57')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d912,d86]) ).
cnf(d914,plain,
s(s(s(s(s(s(s('index$u63'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d913,d83]) ).
cnf(d915,plain,
s(s(s(s(s(s('index$u72')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d914,d157]) ).
cnf(d916,plain,
s(s(s(s(s('index$u84'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d915,d108]) ).
cnf(d917,plain,
s(s(s(s('index$u90')))) != 'index$u36',
inference(demodulation,[status(thm)],[d916,d105]) ).
cnf(d918,plain,
s(s(s('index$u99'))) != 'index$u36',
inference(demodulation,[status(thm)],[d917,d156]) ).
cnf(d919,plain,
s(s('index$u105')) != 'index$u36',
inference(demodulation,[status(thm)],[d918,d675]) ).
cnf(d920,plain,
s('index$u111') != 'index$u36',
inference(demodulation,[status(thm)],[d919,d672]) ).
cnf(d921,plain,
'index$u120' != 'index$u36',
inference(demodulation,[status(thm)],[d920,d669]) ).
cnf(d922,plain,
( 'elem$u283' = select('earray$u112','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d921,d910]) ).
cnf(d923,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u111' = 'index$u36'
| 'elem$u283' = select('earray$u106','index$u36') ),
inference(superposition,[status(thm)],[d922,d183]) ).
cnf(d924,plain,
s(s(s(s(s(s(s(s(s('index$u42'))))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c61]) ).
cnf(d925,plain,
s(s(s(s(s(s(s(s('index$u51')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d924,d158]) ).
cnf(d926,plain,
s(s(s(s(s(s(s('index$u57'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d925,d86]) ).
cnf(d927,plain,
s(s(s(s(s(s('index$u63')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d926,d83]) ).
cnf(d928,plain,
s(s(s(s(s('index$u72'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d927,d157]) ).
cnf(d929,plain,
s(s(s(s('index$u84')))) != 'index$u36',
inference(demodulation,[status(thm)],[d928,d108]) ).
cnf(d930,plain,
s(s(s('index$u90'))) != 'index$u36',
inference(demodulation,[status(thm)],[d929,d105]) ).
cnf(d931,plain,
s(s('index$u99')) != 'index$u36',
inference(demodulation,[status(thm)],[d930,d156]) ).
cnf(d932,plain,
s('index$u105') != 'index$u36',
inference(demodulation,[status(thm)],[d931,d675]) ).
cnf(d933,plain,
'index$u111' != 'index$u36',
inference(demodulation,[status(thm)],[d932,d672]) ).
cnf(d934,plain,
( 'elem$u283' = select('earray$u106','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d933,d923]) ).
cnf(d935,plain,
( 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head
| 'index$u105' = 'index$u36'
| 'elem$u283' = select('earray$u100','index$u36') ),
inference(superposition,[status(thm)],[d934,d175]) ).
cnf(d936,plain,
s(s(s(s(s(s(s(s('index$u42')))))))) != 'index$u36',
inference(superposition,[status(thm)],[d93,c62]) ).
cnf(d937,plain,
s(s(s(s(s(s(s('index$u51'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d936,d158]) ).
cnf(d938,plain,
s(s(s(s(s(s('index$u57')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d937,d86]) ).
cnf(d939,plain,
s(s(s(s(s('index$u63'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d938,d83]) ).
cnf(d940,plain,
s(s(s(s('index$u72')))) != 'index$u36',
inference(demodulation,[status(thm)],[d939,d157]) ).
cnf(d941,plain,
s(s(s('index$u84'))) != 'index$u36',
inference(demodulation,[status(thm)],[d940,d108]) ).
cnf(d942,plain,
s(s('index$u90')) != 'index$u36',
inference(demodulation,[status(thm)],[d941,d105]) ).
cnf(d943,plain,
s('index$u99') != 'index$u36',
inference(demodulation,[status(thm)],[d942,d156]) ).
cnf(d944,plain,
'index$u105' != 'index$u36',
inference(demodulation,[status(thm)],[d943,d675]) ).
cnf(d945,plain,
( 'elem$u283' = select('earray$u100','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| 'index$u219' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d944,d935]) ).
cnf(d946,plain,
select(q37,tail) = 'index$u216',
inference(superposition,[status(thm)],[d304,c0]) ).
cnf(d947,plain,
'index$u219' = 'index$u216',
inference(demodulation,[status(thm)],[d946,c203]) ).
cnf(d948,plain,
'index$u219' = s('index$u213'),
inference(demodulation,[status(thm)],[c202,d947]) ).
cnf(d949,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u39'))))))))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[c235,c47]) ).
cnf(d950,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d949,d92]) ).
cnf(d951,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51')))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d950,d158]) ).
cnf(d952,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57'))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d951,d86]) ).
cnf(d953,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63')))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d952,d83]) ).
cnf(d954,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72'))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d953,d157]) ).
cnf(d955,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84')))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d954,d108]) ).
cnf(d956,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u90'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d955,d105]) ).
cnf(d957,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u99')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d956,d156]) ).
cnf(d958,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u105'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d957,d675]) ).
cnf(d959,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u111')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d958,d672]) ).
cnf(d960,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u120'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d959,d669]) ).
cnf(d961,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u126')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d960,d664]) ).
cnf(d962,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u132'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d961,d661]) ).
cnf(d963,plain,
s(s(s(s(s(s(s(s(s(s('index$u141')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d962,d658]) ).
cnf(d964,plain,
s(s(s(s(s(s(s(s(s('index$u147'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d963,d653]) ).
cnf(d965,plain,
s(s(s(s(s(s(s(s('index$u162')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d964,d650]) ).
cnf(d966,plain,
s(s(s(s(s(s(s('index$u171'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d965,d647]) ).
cnf(d967,plain,
s(s(s(s(s(s('index$u177')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d966,d642]) ).
cnf(d968,plain,
s(s(s(s(s('index$u183'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d967,d639]) ).
cnf(d969,plain,
s(s(s(s('index$u192')))) != 'index$u36',
inference(demodulation,[status(thm)],[d968,d636]) ).
cnf(d970,plain,
s(s(s('index$u198'))) != 'index$u36',
inference(demodulation,[status(thm)],[d969,d631]) ).
cnf(d971,plain,
s(s('index$u204')) != 'index$u36',
inference(demodulation,[status(thm)],[d970,d628]) ).
cnf(d972,plain,
s('index$u213') != 'index$u36',
inference(demodulation,[status(thm)],[d971,d625]) ).
cnf(d973,plain,
'index$u219' != 'index$u36',
inference(demodulation,[status(thm)],[d972,d948]) ).
cnf(d974,plain,
( 'elem$u283' = select('earray$u100','index$u36')
| 'index$u240' = 'index$u36'
| 'index$u225' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d973,d945]) ).
cnf(d975,plain,
select(q38,tail) = 'index$u222',
inference(superposition,[status(thm)],[d312,c0]) ).
cnf(d976,plain,
'index$u225' = 'index$u222',
inference(demodulation,[status(thm)],[d975,c205]) ).
cnf(d977,plain,
'index$u225' = s('index$u219'),
inference(demodulation,[status(thm)],[c204,d976]) ).
cnf(d978,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u39')))))))))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[c235,c46]) ).
cnf(d979,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42')))))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d978,d92]) ).
cnf(d980,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51'))))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d979,d158]) ).
cnf(d981,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57')))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d980,d86]) ).
cnf(d982,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63'))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d981,d83]) ).
cnf(d983,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72')))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d982,d157]) ).
cnf(d984,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84'))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d983,d108]) ).
cnf(d985,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u90')))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d984,d105]) ).
cnf(d986,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u99'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d985,d156]) ).
cnf(d987,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u105')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d986,d675]) ).
cnf(d988,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u111'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d987,d672]) ).
cnf(d989,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u120')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d988,d669]) ).
cnf(d990,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u126'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d989,d664]) ).
cnf(d991,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u132')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d990,d661]) ).
cnf(d992,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u141'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d991,d658]) ).
cnf(d993,plain,
s(s(s(s(s(s(s(s(s(s('index$u147')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d992,d653]) ).
cnf(d994,plain,
s(s(s(s(s(s(s(s(s('index$u162'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d993,d650]) ).
cnf(d995,plain,
s(s(s(s(s(s(s(s('index$u171')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d994,d647]) ).
cnf(d996,plain,
s(s(s(s(s(s(s('index$u177'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d995,d642]) ).
cnf(d997,plain,
s(s(s(s(s(s('index$u183')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d996,d639]) ).
cnf(d998,plain,
s(s(s(s(s('index$u192'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d997,d636]) ).
cnf(d999,plain,
s(s(s(s('index$u198')))) != 'index$u36',
inference(demodulation,[status(thm)],[d998,d631]) ).
cnf(d1000,plain,
s(s(s('index$u204'))) != 'index$u36',
inference(demodulation,[status(thm)],[d999,d628]) ).
cnf(d1001,plain,
s(s('index$u213')) != 'index$u36',
inference(demodulation,[status(thm)],[d1000,d625]) ).
cnf(d1002,plain,
s('index$u219') != 'index$u36',
inference(demodulation,[status(thm)],[d1001,d948]) ).
cnf(d1003,plain,
'index$u225' != 'index$u36',
inference(demodulation,[status(thm)],[d1002,d977]) ).
cnf(d1004,plain,
( 'elem$u283' = select('earray$u100','index$u36')
| 'index$u240' = 'index$u36'
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d1003,d974]) ).
cnf(d1005,plain,
select('queue$u229',tail) = 'index$u228',
inference(superposition,[status(thm)],[c309,c0]) ).
cnf(d1006,plain,
( head = tail
| select(q39,tail) = 'index$u228' ),
inference(superposition,[status(thm)],[d324,d1005]) ).
cnf(d1007,plain,
( head = tail
| 'index$u240' = 'index$u228' ),
inference(demodulation,[status(thm)],[d1006,c212]) ).
cnf(d1008,plain,
'index$u240' = 'index$u228',
inference(resolution,[status(thm)],[c2,d1007]) ).
cnf(d1009,plain,
'index$u240' = s('index$u225'),
inference(demodulation,[status(thm)],[c206,d1008]) ).
cnf(d1010,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u39'))))))))))))))))))))))))) != 'index$u36',
inference(superposition,[status(thm)],[c235,c45]) ).
cnf(d1011,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u42'))))))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1010,d92]) ).
cnf(d1012,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u51')))))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1011,d158]) ).
cnf(d1013,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u57'))))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1012,d86]) ).
cnf(d1014,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u63')))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1013,d83]) ).
cnf(d1015,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u72'))))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1014,d157]) ).
cnf(d1016,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u84')))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1015,d108]) ).
cnf(d1017,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u90'))))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1016,d105]) ).
cnf(d1018,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u99')))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1017,d156]) ).
cnf(d1019,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u105'))))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1018,d675]) ).
cnf(d1020,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u111')))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1019,d672]) ).
cnf(d1021,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u120'))))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1020,d669]) ).
cnf(d1022,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s('index$u126')))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1021,d664]) ).
cnf(d1023,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s('index$u132'))))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1022,d661]) ).
cnf(d1024,plain,
s(s(s(s(s(s(s(s(s(s(s(s('index$u141')))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1023,d658]) ).
cnf(d1025,plain,
s(s(s(s(s(s(s(s(s(s(s('index$u147'))))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1024,d653]) ).
cnf(d1026,plain,
s(s(s(s(s(s(s(s(s(s('index$u162')))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1025,d650]) ).
cnf(d1027,plain,
s(s(s(s(s(s(s(s(s('index$u171'))))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1026,d647]) ).
cnf(d1028,plain,
s(s(s(s(s(s(s(s('index$u177')))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1027,d642]) ).
cnf(d1029,plain,
s(s(s(s(s(s(s('index$u183'))))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1028,d639]) ).
cnf(d1030,plain,
s(s(s(s(s(s('index$u192')))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1029,d636]) ).
cnf(d1031,plain,
s(s(s(s(s('index$u198'))))) != 'index$u36',
inference(demodulation,[status(thm)],[d1030,d631]) ).
cnf(d1032,plain,
s(s(s(s('index$u204')))) != 'index$u36',
inference(demodulation,[status(thm)],[d1031,d628]) ).
cnf(d1033,plain,
s(s(s('index$u213'))) != 'index$u36',
inference(demodulation,[status(thm)],[d1032,d625]) ).
cnf(d1034,plain,
s(s('index$u219')) != 'index$u36',
inference(demodulation,[status(thm)],[d1033,d948]) ).
cnf(d1035,plain,
s('index$u225') != 'index$u36',
inference(demodulation,[status(thm)],[d1034,d977]) ).
cnf(d1036,plain,
'index$u240' != 'index$u36',
inference(demodulation,[status(thm)],[d1035,d1009]) ).
cnf(d1037,plain,
( 'elem$u283' = select('earray$u100','index$u36')
| seq = head
| tail = head ),
inference(resolution,[status(thm)],[d1036,d1004]) ).
cnf(d1038,plain,
( 'elem$u283' = e13
| seq = head
| tail = head ),
inference(demodulation,[status(thm)],[d1037,d167]) ).
cnf(d1039,plain,
( seq = head
| tail = head ),
inference(resolution,[status(thm)],[c396,d1038]) ).
cnf(d1040,plain,
( tail = head
| seq != seq ),
inference(superposition,[status(thm)],[d1039,c3]) ).
cnf(d1041,plain,
tail = head,
inference(equality_resolution,[status(thm)],[d1040]) ).
cnf(d1042,plain,
tail != tail,
inference(demodulation,[status(thm)],[c2,d1041]) ).
cnf(d1043,plain,
$false,
inference(equality_resolution,[status(thm)],[d1042]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV569-1.040 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 14:31:03 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 138.89/24.08 % SZS status Unsatisfiable for theBenchmark.p
% 138.89/24.08 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------