LisaST---0.9.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : LisaST---0.9
% Problem  : SWV571-1.049 : 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 : n001.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:24 AM UTC 2026

% Result   : Unsatisfiable 29.98s 4.69s
% Output   : CNFRefutation 29.98s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   44
%            Number of leaves      :  261
% Syntax   : Number of clauses     : 1132 ( 926 unt; 205 nHn; 946 RR)
%            Number of literals    : 1535 (1534 equ;   8 neg)
%            Maximal clause size   :    5 (   1 avg)
%            Maximal term depth    :    4 (   1 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :  311 ( 311 usr; 307 con; 0-3 aty)
%            Number of variables   :  196 (   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(ps,axiom,
    p(s(X0)) = X0 ).

cnf(sp,axiom,
    s(p(X0)) = X0 ).

cnf(circular,axiom,
    s(s(s(X0))) = X0 ).

cnf(hyp99,hypothesis,
    'elem$u298' = select('earray$u296','index$u297') ).

cnf(hyp100,hypothesis,
    'elem$u301' = select('earray$u296','index$u300') ).

cnf(hyp101,hypothesis,
    'index$u0' = select(q,tail) ).

cnf(hyp102,hypothesis,
    'index$u102' = s('index$u99') ).

cnf(hyp103,hypothesis,
    'index$u105' = select(q24,tail) ).

cnf(hyp104,hypothesis,
    'index$u108' = s('index$u105') ).

cnf(hyp105,hypothesis,
    'index$u111' = select(q25,tail) ).

cnf(hyp106,hypothesis,
    'index$u114' = s('index$u111') ).

cnf(hyp107,hypothesis,
    'index$u117' = select(q26,tail) ).

cnf(hyp108,hypothesis,
    'index$u12' = s('index$u9') ).

cnf(hyp109,hypothesis,
    'index$u120' = s('index$u117') ).

cnf(hyp110,hypothesis,
    'index$u123' = select(q27,tail) ).

cnf(hyp111,hypothesis,
    'index$u126' = s('index$u123') ).

cnf(hyp112,hypothesis,
    'index$u129' = select(q28,tail) ).

cnf(hyp113,hypothesis,
    'index$u132' = s('index$u129') ).

cnf(hyp114,hypothesis,
    'index$u135' = select(q2,tail) ).

cnf(hyp115,hypothesis,
    'index$u138' = s('index$u135') ).

cnf(hyp116,hypothesis,
    'index$u141' = select(q29,tail) ).

cnf(hyp117,hypothesis,
    'index$u144' = s('index$u141') ).

cnf(hyp118,hypothesis,
    'index$u147' = select(q30,tail) ).

cnf(hyp119,hypothesis,
    'index$u15' = select(q10,tail) ).

cnf(hyp120,hypothesis,
    'index$u150' = s('index$u147') ).

cnf(hyp121,hypothesis,
    'index$u153' = select(q31,tail) ).

cnf(hyp122,hypothesis,
    'index$u156' = s('index$u153') ).

cnf(hyp123,hypothesis,
    'index$u159' = select(q32,tail) ).

cnf(hyp124,hypothesis,
    'index$u162' = s('index$u159') ).

cnf(hyp125,hypothesis,
    'index$u165' = select(q33,tail) ).

cnf(hyp126,hypothesis,
    'index$u168' = s('index$u165') ).

cnf(hyp127,hypothesis,
    'index$u171' = select(q34,tail) ).

cnf(hyp128,hypothesis,
    'index$u174' = s('index$u171') ).

cnf(hyp129,hypothesis,
    'index$u177' = select(q35,tail) ).

cnf(hyp130,hypothesis,
    'index$u18' = s('index$u15') ).

cnf(hyp131,hypothesis,
    'index$u180' = s('index$u177') ).

cnf(hyp132,hypothesis,
    'index$u183' = select(q36,tail) ).

cnf(hyp133,hypothesis,
    'index$u186' = s('index$u183') ).

cnf(hyp134,hypothesis,
    'index$u189' = select(q37,tail) ).

cnf(hyp135,hypothesis,
    'index$u192' = s('index$u189') ).

cnf(hyp136,hypothesis,
    'index$u195' = select(q38,tail) ).

cnf(hyp137,hypothesis,
    'index$u198' = s('index$u195') ).

cnf(hyp138,hypothesis,
    'index$u201' = select(q3,tail) ).

cnf(hyp139,hypothesis,
    'index$u204' = s('index$u201') ).

cnf(hyp140,hypothesis,
    'index$u207' = select(q39,tail) ).

cnf(hyp141,hypothesis,
    'index$u21' = select(q11,tail) ).

cnf(hyp142,hypothesis,
    'index$u210' = s('index$u207') ).

cnf(hyp143,hypothesis,
    'index$u213' = select(q40,tail) ).

cnf(hyp144,hypothesis,
    'index$u216' = s('index$u213') ).

cnf(hyp145,hypothesis,
    'index$u219' = select(q41,tail) ).

cnf(hyp146,hypothesis,
    'index$u222' = s('index$u219') ).

cnf(hyp147,hypothesis,
    'index$u225' = select(q42,tail) ).

cnf(hyp148,hypothesis,
    'index$u228' = s('index$u225') ).

cnf(hyp149,hypothesis,
    'index$u231' = select(q43,tail) ).

cnf(hyp150,hypothesis,
    'index$u234' = s('index$u231') ).

cnf(hyp151,hypothesis,
    'index$u237' = select(q44,tail) ).

cnf(hyp152,hypothesis,
    'index$u24' = s('index$u21') ).

cnf(hyp153,hypothesis,
    'index$u240' = s('index$u237') ).

cnf(hyp154,hypothesis,
    'index$u243' = select(q45,tail) ).

cnf(hyp155,hypothesis,
    'index$u246' = s('index$u243') ).

cnf(hyp156,hypothesis,
    'index$u249' = select(q46,tail) ).

cnf(hyp157,hypothesis,
    'index$u252' = s('index$u249') ).

cnf(hyp158,hypothesis,
    'index$u255' = select(q47,tail) ).

cnf(hyp159,hypothesis,
    'index$u258' = s('index$u255') ).

cnf(hyp160,hypothesis,
    'index$u261' = select(q48,tail) ).

cnf(hyp161,hypothesis,
    'index$u264' = s('index$u261') ).

cnf(hyp162,hypothesis,
    'index$u267' = select(q4,tail) ).

cnf(hyp163,hypothesis,
    'index$u27' = select(q12,tail) ).

cnf(hyp164,hypothesis,
    'index$u270' = s('index$u267') ).

cnf(hyp165,hypothesis,
    'index$u273' = select(q5,tail) ).

cnf(hyp166,hypothesis,
    'index$u276' = s('index$u273') ).

cnf(hyp167,hypothesis,
    'index$u279' = select(q6,tail) ).

cnf(hyp168,hypothesis,
    'index$u282' = s('index$u279') ).

cnf(hyp169,hypothesis,
    'index$u285' = select(q7,tail) ).

cnf(hyp170,hypothesis,
    'index$u288' = s('index$u285') ).

cnf(hyp171,hypothesis,
    'index$u291' = select(q8,tail) ).

cnf(hyp172,hypothesis,
    'index$u294' = s('index$u291') ).

cnf(hyp173,hypothesis,
    'index$u297' = select(q49,head) ).

cnf(hyp174,hypothesis,
    'index$u299' = select(q49,tail) ).

cnf(hyp175,hypothesis,
    'index$u3' = select(q0,tail) ).

cnf(hyp176,hypothesis,
    'index$u30' = s('index$u27') ).

cnf(hyp177,hypothesis,
    s('index$u300') = 'index$u299' ).

cnf(hyp178,hypothesis,
    'index$u33' = select(q13,tail) ).

cnf(hyp179,hypothesis,
    'index$u36' = s('index$u33') ).

cnf(hyp180,hypothesis,
    'index$u39' = select(q14,tail) ).

cnf(hyp181,hypothesis,
    'index$u42' = s('index$u39') ).

cnf(hyp182,hypothesis,
    'index$u45' = select(q15,tail) ).

cnf(hyp183,hypothesis,
    'index$u48' = s('index$u45') ).

cnf(hyp184,hypothesis,
    'index$u51' = select(q16,tail) ).

cnf(hyp185,hypothesis,
    'index$u54' = s('index$u51') ).

cnf(hyp186,hypothesis,
    'index$u57' = select(q17,tail) ).

cnf(hyp187,hypothesis,
    'index$u6' = s('index$u3') ).

cnf(hyp188,hypothesis,
    'index$u60' = s('index$u57') ).

cnf(hyp189,hypothesis,
    'index$u63' = select(q18,tail) ).

cnf(hyp190,hypothesis,
    'index$u66' = s('index$u63') ).

cnf(hyp191,hypothesis,
    'index$u69' = select(q1,tail) ).

cnf(hyp192,hypothesis,
    'index$u72' = s('index$u69') ).

cnf(hyp193,hypothesis,
    'index$u75' = select(q19,tail) ).

cnf(hyp194,hypothesis,
    'index$u78' = s('index$u75') ).

cnf(hyp195,hypothesis,
    'index$u81' = select(q20,tail) ).

cnf(hyp196,hypothesis,
    'index$u84' = s('index$u81') ).

cnf(hyp197,hypothesis,
    'index$u87' = select(q21,tail) ).

cnf(hyp198,hypothesis,
    'index$u9' = select(q9,tail) ).

cnf(hyp199,hypothesis,
    'index$u90' = s('index$u87') ).

cnf(hyp200,hypothesis,
    'index$u93' = select(q22,tail) ).

cnf(hyp201,hypothesis,
    'index$u96' = s('index$u93') ).

cnf(hyp202,hypothesis,
    'index$u99' = select(q23,tail) ).

cnf(hyp203,hypothesis,
    'queue$u1' = store(q,head,'index$u0') ).

cnf(hyp204,hypothesis,
    'queue$u101' = store(q23,seq,'earray$u100') ).

cnf(hyp205,hypothesis,
    'queue$u103' = store('queue$u101',tail,'index$u102') ).

cnf(hyp206,hypothesis,
    'queue$u107' = store(q24,seq,'earray$u106') ).

cnf(hyp207,hypothesis,
    'queue$u109' = store('queue$u107',tail,'index$u108') ).

cnf(hyp208,hypothesis,
    'queue$u11' = store(q9,seq,'earray$u10') ).

cnf(hyp209,hypothesis,
    'queue$u113' = store(q25,seq,'earray$u112') ).

cnf(hyp210,hypothesis,
    'queue$u115' = store('queue$u113',tail,'index$u114') ).

cnf(hyp211,hypothesis,
    'queue$u119' = store(q26,seq,'earray$u118') ).

cnf(hyp212,hypothesis,
    'queue$u121' = store('queue$u119',tail,'index$u120') ).

cnf(hyp213,hypothesis,
    'queue$u125' = store(q27,seq,'earray$u124') ).

cnf(hyp214,hypothesis,
    'queue$u127' = store('queue$u125',tail,'index$u126') ).

cnf(hyp215,hypothesis,
    'queue$u13' = store('queue$u11',tail,'index$u12') ).

cnf(hyp216,hypothesis,
    'queue$u131' = store(q28,seq,'earray$u130') ).

cnf(hyp217,hypothesis,
    'queue$u133' = store('queue$u131',tail,'index$u132') ).

cnf(hyp218,hypothesis,
    'queue$u137' = store(q2,seq,'earray$u136') ).

cnf(hyp219,hypothesis,
    'queue$u139' = store('queue$u137',tail,'index$u138') ).

cnf(hyp220,hypothesis,
    'queue$u143' = store(q29,seq,'earray$u142') ).

cnf(hyp221,hypothesis,
    'queue$u145' = store('queue$u143',tail,'index$u144') ).

cnf(hyp222,hypothesis,
    'queue$u149' = store(q30,seq,'earray$u148') ).

cnf(hyp223,hypothesis,
    'queue$u151' = store('queue$u149',tail,'index$u150') ).

cnf(hyp224,hypothesis,
    'queue$u155' = store(q31,seq,'earray$u154') ).

cnf(hyp225,hypothesis,
    'queue$u157' = store('queue$u155',tail,'index$u156') ).

cnf(hyp226,hypothesis,
    'queue$u161' = store(q32,seq,'earray$u160') ).

cnf(hyp227,hypothesis,
    'queue$u163' = store('queue$u161',tail,'index$u162') ).

cnf(hyp228,hypothesis,
    'queue$u167' = store(q33,seq,'earray$u166') ).

cnf(hyp229,hypothesis,
    'queue$u169' = store('queue$u167',tail,'index$u168') ).

cnf(hyp230,hypothesis,
    'queue$u17' = store(q10,seq,'earray$u16') ).

cnf(hyp231,hypothesis,
    'queue$u173' = store(q34,seq,'earray$u172') ).

cnf(hyp232,hypothesis,
    'queue$u175' = store('queue$u173',tail,'index$u174') ).

cnf(hyp233,hypothesis,
    'queue$u179' = store(q35,seq,'earray$u178') ).

cnf(hyp234,hypothesis,
    'queue$u181' = store('queue$u179',tail,'index$u180') ).

cnf(hyp235,hypothesis,
    'queue$u185' = store(q36,seq,'earray$u184') ).

cnf(hyp236,hypothesis,
    'queue$u187' = store('queue$u185',tail,'index$u186') ).

cnf(hyp237,hypothesis,
    'queue$u19' = store('queue$u17',tail,'index$u18') ).

cnf(hyp238,hypothesis,
    'queue$u191' = store(q37,seq,'earray$u190') ).

cnf(hyp239,hypothesis,
    'queue$u193' = store('queue$u191',tail,'index$u192') ).

cnf(hyp240,hypothesis,
    'queue$u197' = store(q38,seq,'earray$u196') ).

cnf(hyp241,hypothesis,
    'queue$u199' = store('queue$u197',tail,'index$u198') ).

cnf(hyp242,hypothesis,
    'queue$u203' = store(q3,seq,'earray$u202') ).

cnf(hyp243,hypothesis,
    'queue$u205' = store('queue$u203',tail,'index$u204') ).

cnf(hyp244,hypothesis,
    'queue$u209' = store(q39,seq,'earray$u208') ).

cnf(hyp245,hypothesis,
    'queue$u211' = store('queue$u209',tail,'index$u210') ).

cnf(hyp246,hypothesis,
    'queue$u215' = store(q40,seq,'earray$u214') ).

cnf(hyp247,hypothesis,
    'queue$u217' = store('queue$u215',tail,'index$u216') ).

cnf(hyp248,hypothesis,
    'queue$u221' = store(q41,seq,'earray$u220') ).

cnf(hyp249,hypothesis,
    'queue$u223' = store('queue$u221',tail,'index$u222') ).

cnf(hyp250,hypothesis,
    'queue$u227' = store(q42,seq,'earray$u226') ).

cnf(hyp251,hypothesis,
    'queue$u229' = store('queue$u227',tail,'index$u228') ).

cnf(hyp252,hypothesis,
    'queue$u23' = store(q11,seq,'earray$u22') ).

cnf(hyp253,hypothesis,
    'queue$u233' = store(q43,seq,'earray$u232') ).

cnf(hyp254,hypothesis,
    'queue$u235' = store('queue$u233',tail,'index$u234') ).

cnf(hyp255,hypothesis,
    'queue$u239' = store(q44,seq,'earray$u238') ).

cnf(hyp256,hypothesis,
    'queue$u241' = store('queue$u239',tail,'index$u240') ).

cnf(hyp257,hypothesis,
    'queue$u245' = store(q45,seq,'earray$u244') ).

cnf(hyp258,hypothesis,
    'queue$u247' = store('queue$u245',tail,'index$u246') ).

cnf(hyp259,hypothesis,
    'queue$u25' = store('queue$u23',tail,'index$u24') ).

cnf(hyp260,hypothesis,
    'queue$u251' = store(q46,seq,'earray$u250') ).

cnf(hyp261,hypothesis,
    'queue$u253' = store('queue$u251',tail,'index$u252') ).

cnf(hyp262,hypothesis,
    'queue$u257' = store(q47,seq,'earray$u256') ).

cnf(hyp263,hypothesis,
    'queue$u259' = store('queue$u257',tail,'index$u258') ).

cnf(hyp264,hypothesis,
    'queue$u263' = store(q48,seq,'earray$u262') ).

cnf(hyp265,hypothesis,
    'queue$u265' = store('queue$u263',tail,'index$u264') ).

cnf(hyp266,hypothesis,
    'queue$u269' = store(q4,seq,'earray$u268') ).

cnf(hyp267,hypothesis,
    'queue$u271' = store('queue$u269',tail,'index$u270') ).

cnf(hyp268,hypothesis,
    'queue$u275' = store(q5,seq,'earray$u274') ).

cnf(hyp269,hypothesis,
    'queue$u277' = store('queue$u275',tail,'index$u276') ).

cnf(hyp270,hypothesis,
    'queue$u281' = store(q6,seq,'earray$u280') ).

cnf(hyp271,hypothesis,
    'queue$u283' = store('queue$u281',tail,'index$u282') ).

cnf(hyp272,hypothesis,
    'queue$u287' = store(q7,seq,'earray$u286') ).

cnf(hyp273,hypothesis,
    'queue$u289' = store('queue$u287',tail,'index$u288') ).

cnf(hyp274,hypothesis,
    'queue$u29' = store(q12,seq,'earray$u28') ).

cnf(hyp275,hypothesis,
    'queue$u293' = store(q8,seq,'earray$u292') ).

cnf(hyp276,hypothesis,
    'queue$u295' = store('queue$u293',tail,'index$u294') ).

cnf(hyp277,hypothesis,
    'queue$u31' = store('queue$u29',tail,'index$u30') ).

cnf(hyp278,hypothesis,
    'queue$u35' = store(q13,seq,'earray$u34') ).

cnf(hyp279,hypothesis,
    'queue$u37' = store('queue$u35',tail,'index$u36') ).

cnf(hyp280,hypothesis,
    'queue$u41' = store(q14,seq,'earray$u40') ).

cnf(hyp281,hypothesis,
    'queue$u43' = store('queue$u41',tail,'index$u42') ).

cnf(hyp282,hypothesis,
    'queue$u47' = store(q15,seq,'earray$u46') ).

cnf(hyp283,hypothesis,
    'queue$u49' = store('queue$u47',tail,'index$u48') ).

cnf(hyp284,hypothesis,
    'queue$u5' = store(q0,seq,'earray$u4') ).

cnf(hyp285,hypothesis,
    'queue$u53' = store(q16,seq,'earray$u52') ).

cnf(hyp286,hypothesis,
    'queue$u55' = store('queue$u53',tail,'index$u54') ).

cnf(hyp287,hypothesis,
    'queue$u59' = store(q17,seq,'earray$u58') ).

cnf(hyp288,hypothesis,
    'queue$u61' = store('queue$u59',tail,'index$u60') ).

cnf(hyp289,hypothesis,
    'queue$u65' = store(q18,seq,'earray$u64') ).

cnf(hyp290,hypothesis,
    'queue$u67' = store('queue$u65',tail,'index$u66') ).

cnf(hyp291,hypothesis,
    'queue$u7' = store('queue$u5',tail,'index$u6') ).

cnf(hyp292,hypothesis,
    'queue$u71' = store(q1,seq,'earray$u70') ).

cnf(hyp293,hypothesis,
    'queue$u73' = store('queue$u71',tail,'index$u72') ).

cnf(hyp294,hypothesis,
    'queue$u77' = store(q19,seq,'earray$u76') ).

cnf(hyp295,hypothesis,
    'queue$u79' = store('queue$u77',tail,'index$u78') ).

cnf(hyp296,hypothesis,
    'queue$u83' = store(q20,seq,'earray$u82') ).

cnf(hyp297,hypothesis,
    'queue$u85' = store('queue$u83',tail,'index$u84') ).

cnf(hyp298,hypothesis,
    'queue$u89' = store(q21,seq,'earray$u88') ).

cnf(hyp299,hypothesis,
    'queue$u91' = store('queue$u89',tail,'index$u90') ).

cnf(hyp300,hypothesis,
    'queue$u95' = store(q22,seq,'earray$u94') ).

cnf(hyp301,hypothesis,
    'queue$u97' = store('queue$u95',tail,'index$u96') ).

cnf(hyp302,hypothesis,
    q0 = 'queue$u1' ).

cnf(hyp303,hypothesis,
    q1 = 'queue$u7' ).

cnf(hyp304,hypothesis,
    q10 = 'queue$u13' ).

cnf(hyp305,hypothesis,
    q11 = 'queue$u19' ).

cnf(hyp306,hypothesis,
    q12 = 'queue$u25' ).

cnf(hyp307,hypothesis,
    q13 = 'queue$u31' ).

cnf(hyp308,hypothesis,
    q14 = 'queue$u37' ).

cnf(hyp309,hypothesis,
    q15 = 'queue$u43' ).

cnf(hyp310,hypothesis,
    q16 = 'queue$u49' ).

cnf(hyp311,hypothesis,
    q17 = 'queue$u55' ).

cnf(hyp312,hypothesis,
    q18 = 'queue$u61' ).

cnf(hyp313,hypothesis,
    q19 = 'queue$u67' ).

cnf(hyp314,hypothesis,
    q2 = 'queue$u73' ).

cnf(hyp315,hypothesis,
    q20 = 'queue$u79' ).

cnf(hyp316,hypothesis,
    q21 = 'queue$u85' ).

cnf(hyp317,hypothesis,
    q22 = 'queue$u91' ).

cnf(hyp318,hypothesis,
    q23 = 'queue$u97' ).

cnf(hyp319,hypothesis,
    q24 = 'queue$u103' ).

cnf(hyp320,hypothesis,
    q25 = 'queue$u109' ).

cnf(hyp321,hypothesis,
    q26 = 'queue$u115' ).

cnf(hyp322,hypothesis,
    q27 = 'queue$u121' ).

cnf(hyp323,hypothesis,
    q28 = 'queue$u127' ).

cnf(hyp324,hypothesis,
    q29 = 'queue$u133' ).

cnf(hyp325,hypothesis,
    q3 = 'queue$u139' ).

cnf(hyp326,hypothesis,
    q30 = 'queue$u145' ).

cnf(hyp327,hypothesis,
    q31 = 'queue$u151' ).

cnf(hyp328,hypothesis,
    q32 = 'queue$u157' ).

cnf(hyp329,hypothesis,
    q33 = 'queue$u163' ).

cnf(hyp330,hypothesis,
    q34 = 'queue$u169' ).

cnf(hyp331,hypothesis,
    q35 = 'queue$u175' ).

cnf(hyp332,hypothesis,
    q36 = 'queue$u181' ).

cnf(hyp333,hypothesis,
    q37 = 'queue$u187' ).

cnf(hyp334,hypothesis,
    q38 = 'queue$u193' ).

cnf(hyp335,hypothesis,
    q39 = 'queue$u199' ).

cnf(hyp336,hypothesis,
    q4 = 'queue$u205' ).

cnf(hyp337,hypothesis,
    q40 = 'queue$u211' ).

cnf(hyp338,hypothesis,
    q41 = 'queue$u217' ).

cnf(hyp339,hypothesis,
    q42 = 'queue$u223' ).

cnf(hyp340,hypothesis,
    q43 = 'queue$u229' ).

cnf(hyp341,hypothesis,
    q44 = 'queue$u235' ).

cnf(hyp342,hypothesis,
    q45 = 'queue$u241' ).

cnf(hyp343,hypothesis,
    q46 = 'queue$u247' ).

cnf(hyp344,hypothesis,
    q47 = 'queue$u253' ).

cnf(hyp345,hypothesis,
    q48 = 'queue$u259' ).

cnf(hyp346,hypothesis,
    q49 = 'queue$u265' ).

cnf(hyp347,hypothesis,
    q5 = 'queue$u271' ).

cnf(hyp348,hypothesis,
    q6 = 'queue$u277' ).

cnf(hyp349,hypothesis,
    q7 = 'queue$u283' ).

cnf(hyp350,hypothesis,
    q8 = 'queue$u289' ).

cnf(hyp351,hypothesis,
    q9 = 'queue$u295' ).

cnf(goal,negated_conjecture,
    'elem$u298' != 'elem$u301' ).

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(c5,plain,
    p(s(X0)) = X0,
    inference(clausification,[status(esa)],[ps]) ).

cnf(c6,plain,
    s(p(X0)) = X0,
    inference(clausification,[status(esa)],[sp]) ).

cnf(c9,plain,
    s(s(s(X0))) = X0,
    inference(clausification,[status(esa)],[circular]) ).

cnf(c109,plain,
    'elem$u298' = select('earray$u296','index$u297'),
    inference(clausification,[status(esa)],[hyp99]) ).

cnf(c110,plain,
    'elem$u301' = select('earray$u296','index$u300'),
    inference(clausification,[status(esa)],[hyp100]) ).

cnf(c111,plain,
    'index$u0' = select(q,tail),
    inference(clausification,[status(esa)],[hyp101]) ).

cnf(c112,plain,
    'index$u102' = s('index$u99'),
    inference(clausification,[status(esa)],[hyp102]) ).

cnf(c113,plain,
    'index$u105' = select(q24,tail),
    inference(clausification,[status(esa)],[hyp103]) ).

cnf(c114,plain,
    'index$u108' = s('index$u105'),
    inference(clausification,[status(esa)],[hyp104]) ).

cnf(c115,plain,
    'index$u111' = select(q25,tail),
    inference(clausification,[status(esa)],[hyp105]) ).

cnf(c116,plain,
    'index$u114' = s('index$u111'),
    inference(clausification,[status(esa)],[hyp106]) ).

cnf(c117,plain,
    'index$u117' = select(q26,tail),
    inference(clausification,[status(esa)],[hyp107]) ).

cnf(c118,plain,
    'index$u12' = s('index$u9'),
    inference(clausification,[status(esa)],[hyp108]) ).

cnf(c119,plain,
    'index$u120' = s('index$u117'),
    inference(clausification,[status(esa)],[hyp109]) ).

cnf(c120,plain,
    'index$u123' = select(q27,tail),
    inference(clausification,[status(esa)],[hyp110]) ).

cnf(c121,plain,
    'index$u126' = s('index$u123'),
    inference(clausification,[status(esa)],[hyp111]) ).

cnf(c122,plain,
    'index$u129' = select(q28,tail),
    inference(clausification,[status(esa)],[hyp112]) ).

cnf(c123,plain,
    'index$u132' = s('index$u129'),
    inference(clausification,[status(esa)],[hyp113]) ).

cnf(c124,plain,
    'index$u135' = select(q2,tail),
    inference(clausification,[status(esa)],[hyp114]) ).

cnf(c125,plain,
    'index$u138' = s('index$u135'),
    inference(clausification,[status(esa)],[hyp115]) ).

cnf(c126,plain,
    'index$u141' = select(q29,tail),
    inference(clausification,[status(esa)],[hyp116]) ).

cnf(c127,plain,
    'index$u144' = s('index$u141'),
    inference(clausification,[status(esa)],[hyp117]) ).

cnf(c128,plain,
    'index$u147' = select(q30,tail),
    inference(clausification,[status(esa)],[hyp118]) ).

cnf(c129,plain,
    'index$u15' = select(q10,tail),
    inference(clausification,[status(esa)],[hyp119]) ).

cnf(c130,plain,
    'index$u150' = s('index$u147'),
    inference(clausification,[status(esa)],[hyp120]) ).

cnf(c131,plain,
    'index$u153' = select(q31,tail),
    inference(clausification,[status(esa)],[hyp121]) ).

cnf(c132,plain,
    'index$u156' = s('index$u153'),
    inference(clausification,[status(esa)],[hyp122]) ).

cnf(c133,plain,
    'index$u159' = select(q32,tail),
    inference(clausification,[status(esa)],[hyp123]) ).

cnf(c134,plain,
    'index$u162' = s('index$u159'),
    inference(clausification,[status(esa)],[hyp124]) ).

cnf(c135,plain,
    'index$u165' = select(q33,tail),
    inference(clausification,[status(esa)],[hyp125]) ).

cnf(c136,plain,
    'index$u168' = s('index$u165'),
    inference(clausification,[status(esa)],[hyp126]) ).

cnf(c137,plain,
    'index$u171' = select(q34,tail),
    inference(clausification,[status(esa)],[hyp127]) ).

cnf(c138,plain,
    'index$u174' = s('index$u171'),
    inference(clausification,[status(esa)],[hyp128]) ).

cnf(c139,plain,
    'index$u177' = select(q35,tail),
    inference(clausification,[status(esa)],[hyp129]) ).

cnf(c140,plain,
    'index$u18' = s('index$u15'),
    inference(clausification,[status(esa)],[hyp130]) ).

cnf(c141,plain,
    'index$u180' = s('index$u177'),
    inference(clausification,[status(esa)],[hyp131]) ).

cnf(c142,plain,
    'index$u183' = select(q36,tail),
    inference(clausification,[status(esa)],[hyp132]) ).

cnf(c143,plain,
    'index$u186' = s('index$u183'),
    inference(clausification,[status(esa)],[hyp133]) ).

cnf(c144,plain,
    'index$u189' = select(q37,tail),
    inference(clausification,[status(esa)],[hyp134]) ).

cnf(c145,plain,
    'index$u192' = s('index$u189'),
    inference(clausification,[status(esa)],[hyp135]) ).

cnf(c146,plain,
    'index$u195' = select(q38,tail),
    inference(clausification,[status(esa)],[hyp136]) ).

cnf(c147,plain,
    'index$u198' = s('index$u195'),
    inference(clausification,[status(esa)],[hyp137]) ).

cnf(c148,plain,
    'index$u201' = select(q3,tail),
    inference(clausification,[status(esa)],[hyp138]) ).

cnf(c149,plain,
    'index$u204' = s('index$u201'),
    inference(clausification,[status(esa)],[hyp139]) ).

cnf(c150,plain,
    'index$u207' = select(q39,tail),
    inference(clausification,[status(esa)],[hyp140]) ).

cnf(c151,plain,
    'index$u21' = select(q11,tail),
    inference(clausification,[status(esa)],[hyp141]) ).

cnf(c152,plain,
    'index$u210' = s('index$u207'),
    inference(clausification,[status(esa)],[hyp142]) ).

cnf(c153,plain,
    'index$u213' = select(q40,tail),
    inference(clausification,[status(esa)],[hyp143]) ).

cnf(c154,plain,
    'index$u216' = s('index$u213'),
    inference(clausification,[status(esa)],[hyp144]) ).

cnf(c155,plain,
    'index$u219' = select(q41,tail),
    inference(clausification,[status(esa)],[hyp145]) ).

cnf(c156,plain,
    'index$u222' = s('index$u219'),
    inference(clausification,[status(esa)],[hyp146]) ).

cnf(c157,plain,
    'index$u225' = select(q42,tail),
    inference(clausification,[status(esa)],[hyp147]) ).

cnf(c158,plain,
    'index$u228' = s('index$u225'),
    inference(clausification,[status(esa)],[hyp148]) ).

cnf(c159,plain,
    'index$u231' = select(q43,tail),
    inference(clausification,[status(esa)],[hyp149]) ).

cnf(c160,plain,
    'index$u234' = s('index$u231'),
    inference(clausification,[status(esa)],[hyp150]) ).

cnf(c161,plain,
    'index$u237' = select(q44,tail),
    inference(clausification,[status(esa)],[hyp151]) ).

cnf(c162,plain,
    'index$u24' = s('index$u21'),
    inference(clausification,[status(esa)],[hyp152]) ).

cnf(c163,plain,
    'index$u240' = s('index$u237'),
    inference(clausification,[status(esa)],[hyp153]) ).

cnf(c164,plain,
    'index$u243' = select(q45,tail),
    inference(clausification,[status(esa)],[hyp154]) ).

cnf(c165,plain,
    'index$u246' = s('index$u243'),
    inference(clausification,[status(esa)],[hyp155]) ).

cnf(c166,plain,
    'index$u249' = select(q46,tail),
    inference(clausification,[status(esa)],[hyp156]) ).

cnf(c167,plain,
    'index$u252' = s('index$u249'),
    inference(clausification,[status(esa)],[hyp157]) ).

cnf(c168,plain,
    'index$u255' = select(q47,tail),
    inference(clausification,[status(esa)],[hyp158]) ).

cnf(c169,plain,
    'index$u258' = s('index$u255'),
    inference(clausification,[status(esa)],[hyp159]) ).

cnf(c170,plain,
    'index$u261' = select(q48,tail),
    inference(clausification,[status(esa)],[hyp160]) ).

cnf(c171,plain,
    'index$u264' = s('index$u261'),
    inference(clausification,[status(esa)],[hyp161]) ).

cnf(c172,plain,
    'index$u267' = select(q4,tail),
    inference(clausification,[status(esa)],[hyp162]) ).

cnf(c173,plain,
    'index$u27' = select(q12,tail),
    inference(clausification,[status(esa)],[hyp163]) ).

cnf(c174,plain,
    'index$u270' = s('index$u267'),
    inference(clausification,[status(esa)],[hyp164]) ).

cnf(c175,plain,
    'index$u273' = select(q5,tail),
    inference(clausification,[status(esa)],[hyp165]) ).

cnf(c176,plain,
    'index$u276' = s('index$u273'),
    inference(clausification,[status(esa)],[hyp166]) ).

cnf(c177,plain,
    'index$u279' = select(q6,tail),
    inference(clausification,[status(esa)],[hyp167]) ).

cnf(c178,plain,
    'index$u282' = s('index$u279'),
    inference(clausification,[status(esa)],[hyp168]) ).

cnf(c179,plain,
    'index$u285' = select(q7,tail),
    inference(clausification,[status(esa)],[hyp169]) ).

cnf(c180,plain,
    'index$u288' = s('index$u285'),
    inference(clausification,[status(esa)],[hyp170]) ).

cnf(c181,plain,
    'index$u291' = select(q8,tail),
    inference(clausification,[status(esa)],[hyp171]) ).

cnf(c182,plain,
    'index$u294' = s('index$u291'),
    inference(clausification,[status(esa)],[hyp172]) ).

cnf(c183,plain,
    'index$u297' = select(q49,head),
    inference(clausification,[status(esa)],[hyp173]) ).

cnf(c184,plain,
    'index$u299' = select(q49,tail),
    inference(clausification,[status(esa)],[hyp174]) ).

cnf(c185,plain,
    'index$u3' = select(q0,tail),
    inference(clausification,[status(esa)],[hyp175]) ).

cnf(c186,plain,
    'index$u30' = s('index$u27'),
    inference(clausification,[status(esa)],[hyp176]) ).

cnf(c187,plain,
    s('index$u300') = 'index$u299',
    inference(clausification,[status(esa)],[hyp177]) ).

cnf(c188,plain,
    'index$u33' = select(q13,tail),
    inference(clausification,[status(esa)],[hyp178]) ).

cnf(c189,plain,
    'index$u36' = s('index$u33'),
    inference(clausification,[status(esa)],[hyp179]) ).

cnf(c190,plain,
    'index$u39' = select(q14,tail),
    inference(clausification,[status(esa)],[hyp180]) ).

cnf(c191,plain,
    'index$u42' = s('index$u39'),
    inference(clausification,[status(esa)],[hyp181]) ).

cnf(c192,plain,
    'index$u45' = select(q15,tail),
    inference(clausification,[status(esa)],[hyp182]) ).

cnf(c193,plain,
    'index$u48' = s('index$u45'),
    inference(clausification,[status(esa)],[hyp183]) ).

cnf(c194,plain,
    'index$u51' = select(q16,tail),
    inference(clausification,[status(esa)],[hyp184]) ).

cnf(c195,plain,
    'index$u54' = s('index$u51'),
    inference(clausification,[status(esa)],[hyp185]) ).

cnf(c196,plain,
    'index$u57' = select(q17,tail),
    inference(clausification,[status(esa)],[hyp186]) ).

cnf(c197,plain,
    'index$u6' = s('index$u3'),
    inference(clausification,[status(esa)],[hyp187]) ).

cnf(c198,plain,
    'index$u60' = s('index$u57'),
    inference(clausification,[status(esa)],[hyp188]) ).

cnf(c199,plain,
    'index$u63' = select(q18,tail),
    inference(clausification,[status(esa)],[hyp189]) ).

cnf(c200,plain,
    'index$u66' = s('index$u63'),
    inference(clausification,[status(esa)],[hyp190]) ).

cnf(c201,plain,
    'index$u69' = select(q1,tail),
    inference(clausification,[status(esa)],[hyp191]) ).

cnf(c202,plain,
    'index$u72' = s('index$u69'),
    inference(clausification,[status(esa)],[hyp192]) ).

cnf(c203,plain,
    'index$u75' = select(q19,tail),
    inference(clausification,[status(esa)],[hyp193]) ).

cnf(c204,plain,
    'index$u78' = s('index$u75'),
    inference(clausification,[status(esa)],[hyp194]) ).

cnf(c205,plain,
    'index$u81' = select(q20,tail),
    inference(clausification,[status(esa)],[hyp195]) ).

cnf(c206,plain,
    'index$u84' = s('index$u81'),
    inference(clausification,[status(esa)],[hyp196]) ).

cnf(c207,plain,
    'index$u87' = select(q21,tail),
    inference(clausification,[status(esa)],[hyp197]) ).

cnf(c208,plain,
    'index$u9' = select(q9,tail),
    inference(clausification,[status(esa)],[hyp198]) ).

cnf(c209,plain,
    'index$u90' = s('index$u87'),
    inference(clausification,[status(esa)],[hyp199]) ).

cnf(c210,plain,
    'index$u93' = select(q22,tail),
    inference(clausification,[status(esa)],[hyp200]) ).

cnf(c211,plain,
    'index$u96' = s('index$u93'),
    inference(clausification,[status(esa)],[hyp201]) ).

cnf(c212,plain,
    'index$u99' = select(q23,tail),
    inference(clausification,[status(esa)],[hyp202]) ).

cnf(c213,plain,
    'queue$u1' = store(q,head,'index$u0'),
    inference(clausification,[status(esa)],[hyp203]) ).

cnf(c214,plain,
    'queue$u101' = store(q23,seq,'earray$u100'),
    inference(clausification,[status(esa)],[hyp204]) ).

cnf(c215,plain,
    'queue$u103' = store('queue$u101',tail,'index$u102'),
    inference(clausification,[status(esa)],[hyp205]) ).

cnf(c216,plain,
    'queue$u107' = store(q24,seq,'earray$u106'),
    inference(clausification,[status(esa)],[hyp206]) ).

cnf(c217,plain,
    'queue$u109' = store('queue$u107',tail,'index$u108'),
    inference(clausification,[status(esa)],[hyp207]) ).

cnf(c218,plain,
    'queue$u11' = store(q9,seq,'earray$u10'),
    inference(clausification,[status(esa)],[hyp208]) ).

cnf(c219,plain,
    'queue$u113' = store(q25,seq,'earray$u112'),
    inference(clausification,[status(esa)],[hyp209]) ).

cnf(c220,plain,
    'queue$u115' = store('queue$u113',tail,'index$u114'),
    inference(clausification,[status(esa)],[hyp210]) ).

cnf(c221,plain,
    'queue$u119' = store(q26,seq,'earray$u118'),
    inference(clausification,[status(esa)],[hyp211]) ).

cnf(c222,plain,
    'queue$u121' = store('queue$u119',tail,'index$u120'),
    inference(clausification,[status(esa)],[hyp212]) ).

cnf(c223,plain,
    'queue$u125' = store(q27,seq,'earray$u124'),
    inference(clausification,[status(esa)],[hyp213]) ).

cnf(c224,plain,
    'queue$u127' = store('queue$u125',tail,'index$u126'),
    inference(clausification,[status(esa)],[hyp214]) ).

cnf(c225,plain,
    'queue$u13' = store('queue$u11',tail,'index$u12'),
    inference(clausification,[status(esa)],[hyp215]) ).

cnf(c226,plain,
    'queue$u131' = store(q28,seq,'earray$u130'),
    inference(clausification,[status(esa)],[hyp216]) ).

cnf(c227,plain,
    'queue$u133' = store('queue$u131',tail,'index$u132'),
    inference(clausification,[status(esa)],[hyp217]) ).

cnf(c228,plain,
    'queue$u137' = store(q2,seq,'earray$u136'),
    inference(clausification,[status(esa)],[hyp218]) ).

cnf(c229,plain,
    'queue$u139' = store('queue$u137',tail,'index$u138'),
    inference(clausification,[status(esa)],[hyp219]) ).

cnf(c230,plain,
    'queue$u143' = store(q29,seq,'earray$u142'),
    inference(clausification,[status(esa)],[hyp220]) ).

cnf(c231,plain,
    'queue$u145' = store('queue$u143',tail,'index$u144'),
    inference(clausification,[status(esa)],[hyp221]) ).

cnf(c232,plain,
    'queue$u149' = store(q30,seq,'earray$u148'),
    inference(clausification,[status(esa)],[hyp222]) ).

cnf(c233,plain,
    'queue$u151' = store('queue$u149',tail,'index$u150'),
    inference(clausification,[status(esa)],[hyp223]) ).

cnf(c234,plain,
    'queue$u155' = store(q31,seq,'earray$u154'),
    inference(clausification,[status(esa)],[hyp224]) ).

cnf(c235,plain,
    'queue$u157' = store('queue$u155',tail,'index$u156'),
    inference(clausification,[status(esa)],[hyp225]) ).

cnf(c236,plain,
    'queue$u161' = store(q32,seq,'earray$u160'),
    inference(clausification,[status(esa)],[hyp226]) ).

cnf(c237,plain,
    'queue$u163' = store('queue$u161',tail,'index$u162'),
    inference(clausification,[status(esa)],[hyp227]) ).

cnf(c238,plain,
    'queue$u167' = store(q33,seq,'earray$u166'),
    inference(clausification,[status(esa)],[hyp228]) ).

cnf(c239,plain,
    'queue$u169' = store('queue$u167',tail,'index$u168'),
    inference(clausification,[status(esa)],[hyp229]) ).

cnf(c240,plain,
    'queue$u17' = store(q10,seq,'earray$u16'),
    inference(clausification,[status(esa)],[hyp230]) ).

cnf(c241,plain,
    'queue$u173' = store(q34,seq,'earray$u172'),
    inference(clausification,[status(esa)],[hyp231]) ).

cnf(c242,plain,
    'queue$u175' = store('queue$u173',tail,'index$u174'),
    inference(clausification,[status(esa)],[hyp232]) ).

cnf(c243,plain,
    'queue$u179' = store(q35,seq,'earray$u178'),
    inference(clausification,[status(esa)],[hyp233]) ).

cnf(c244,plain,
    'queue$u181' = store('queue$u179',tail,'index$u180'),
    inference(clausification,[status(esa)],[hyp234]) ).

cnf(c245,plain,
    'queue$u185' = store(q36,seq,'earray$u184'),
    inference(clausification,[status(esa)],[hyp235]) ).

cnf(c246,plain,
    'queue$u187' = store('queue$u185',tail,'index$u186'),
    inference(clausification,[status(esa)],[hyp236]) ).

cnf(c247,plain,
    'queue$u19' = store('queue$u17',tail,'index$u18'),
    inference(clausification,[status(esa)],[hyp237]) ).

cnf(c248,plain,
    'queue$u191' = store(q37,seq,'earray$u190'),
    inference(clausification,[status(esa)],[hyp238]) ).

cnf(c249,plain,
    'queue$u193' = store('queue$u191',tail,'index$u192'),
    inference(clausification,[status(esa)],[hyp239]) ).

cnf(c250,plain,
    'queue$u197' = store(q38,seq,'earray$u196'),
    inference(clausification,[status(esa)],[hyp240]) ).

cnf(c251,plain,
    'queue$u199' = store('queue$u197',tail,'index$u198'),
    inference(clausification,[status(esa)],[hyp241]) ).

cnf(c252,plain,
    'queue$u203' = store(q3,seq,'earray$u202'),
    inference(clausification,[status(esa)],[hyp242]) ).

cnf(c253,plain,
    'queue$u205' = store('queue$u203',tail,'index$u204'),
    inference(clausification,[status(esa)],[hyp243]) ).

cnf(c254,plain,
    'queue$u209' = store(q39,seq,'earray$u208'),
    inference(clausification,[status(esa)],[hyp244]) ).

cnf(c255,plain,
    'queue$u211' = store('queue$u209',tail,'index$u210'),
    inference(clausification,[status(esa)],[hyp245]) ).

cnf(c256,plain,
    'queue$u215' = store(q40,seq,'earray$u214'),
    inference(clausification,[status(esa)],[hyp246]) ).

cnf(c257,plain,
    'queue$u217' = store('queue$u215',tail,'index$u216'),
    inference(clausification,[status(esa)],[hyp247]) ).

cnf(c258,plain,
    'queue$u221' = store(q41,seq,'earray$u220'),
    inference(clausification,[status(esa)],[hyp248]) ).

cnf(c259,plain,
    'queue$u223' = store('queue$u221',tail,'index$u222'),
    inference(clausification,[status(esa)],[hyp249]) ).

cnf(c260,plain,
    'queue$u227' = store(q42,seq,'earray$u226'),
    inference(clausification,[status(esa)],[hyp250]) ).

cnf(c261,plain,
    'queue$u229' = store('queue$u227',tail,'index$u228'),
    inference(clausification,[status(esa)],[hyp251]) ).

cnf(c262,plain,
    'queue$u23' = store(q11,seq,'earray$u22'),
    inference(clausification,[status(esa)],[hyp252]) ).

cnf(c263,plain,
    'queue$u233' = store(q43,seq,'earray$u232'),
    inference(clausification,[status(esa)],[hyp253]) ).

cnf(c264,plain,
    'queue$u235' = store('queue$u233',tail,'index$u234'),
    inference(clausification,[status(esa)],[hyp254]) ).

cnf(c265,plain,
    'queue$u239' = store(q44,seq,'earray$u238'),
    inference(clausification,[status(esa)],[hyp255]) ).

cnf(c266,plain,
    'queue$u241' = store('queue$u239',tail,'index$u240'),
    inference(clausification,[status(esa)],[hyp256]) ).

cnf(c267,plain,
    'queue$u245' = store(q45,seq,'earray$u244'),
    inference(clausification,[status(esa)],[hyp257]) ).

cnf(c268,plain,
    'queue$u247' = store('queue$u245',tail,'index$u246'),
    inference(clausification,[status(esa)],[hyp258]) ).

cnf(c269,plain,
    'queue$u25' = store('queue$u23',tail,'index$u24'),
    inference(clausification,[status(esa)],[hyp259]) ).

cnf(c270,plain,
    'queue$u251' = store(q46,seq,'earray$u250'),
    inference(clausification,[status(esa)],[hyp260]) ).

cnf(c271,plain,
    'queue$u253' = store('queue$u251',tail,'index$u252'),
    inference(clausification,[status(esa)],[hyp261]) ).

cnf(c272,plain,
    'queue$u257' = store(q47,seq,'earray$u256'),
    inference(clausification,[status(esa)],[hyp262]) ).

cnf(c273,plain,
    'queue$u259' = store('queue$u257',tail,'index$u258'),
    inference(clausification,[status(esa)],[hyp263]) ).

cnf(c274,plain,
    'queue$u263' = store(q48,seq,'earray$u262'),
    inference(clausification,[status(esa)],[hyp264]) ).

cnf(c275,plain,
    'queue$u265' = store('queue$u263',tail,'index$u264'),
    inference(clausification,[status(esa)],[hyp265]) ).

cnf(c276,plain,
    'queue$u269' = store(q4,seq,'earray$u268'),
    inference(clausification,[status(esa)],[hyp266]) ).

cnf(c277,plain,
    'queue$u271' = store('queue$u269',tail,'index$u270'),
    inference(clausification,[status(esa)],[hyp267]) ).

cnf(c278,plain,
    'queue$u275' = store(q5,seq,'earray$u274'),
    inference(clausification,[status(esa)],[hyp268]) ).

cnf(c279,plain,
    'queue$u277' = store('queue$u275',tail,'index$u276'),
    inference(clausification,[status(esa)],[hyp269]) ).

cnf(c280,plain,
    'queue$u281' = store(q6,seq,'earray$u280'),
    inference(clausification,[status(esa)],[hyp270]) ).

cnf(c281,plain,
    'queue$u283' = store('queue$u281',tail,'index$u282'),
    inference(clausification,[status(esa)],[hyp271]) ).

cnf(c282,plain,
    'queue$u287' = store(q7,seq,'earray$u286'),
    inference(clausification,[status(esa)],[hyp272]) ).

cnf(c283,plain,
    'queue$u289' = store('queue$u287',tail,'index$u288'),
    inference(clausification,[status(esa)],[hyp273]) ).

cnf(c284,plain,
    'queue$u29' = store(q12,seq,'earray$u28'),
    inference(clausification,[status(esa)],[hyp274]) ).

cnf(c285,plain,
    'queue$u293' = store(q8,seq,'earray$u292'),
    inference(clausification,[status(esa)],[hyp275]) ).

cnf(c286,plain,
    'queue$u295' = store('queue$u293',tail,'index$u294'),
    inference(clausification,[status(esa)],[hyp276]) ).

cnf(c287,plain,
    'queue$u31' = store('queue$u29',tail,'index$u30'),
    inference(clausification,[status(esa)],[hyp277]) ).

cnf(c288,plain,
    'queue$u35' = store(q13,seq,'earray$u34'),
    inference(clausification,[status(esa)],[hyp278]) ).

cnf(c289,plain,
    'queue$u37' = store('queue$u35',tail,'index$u36'),
    inference(clausification,[status(esa)],[hyp279]) ).

cnf(c290,plain,
    'queue$u41' = store(q14,seq,'earray$u40'),
    inference(clausification,[status(esa)],[hyp280]) ).

cnf(c291,plain,
    'queue$u43' = store('queue$u41',tail,'index$u42'),
    inference(clausification,[status(esa)],[hyp281]) ).

cnf(c292,plain,
    'queue$u47' = store(q15,seq,'earray$u46'),
    inference(clausification,[status(esa)],[hyp282]) ).

cnf(c293,plain,
    'queue$u49' = store('queue$u47',tail,'index$u48'),
    inference(clausification,[status(esa)],[hyp283]) ).

cnf(c294,plain,
    'queue$u5' = store(q0,seq,'earray$u4'),
    inference(clausification,[status(esa)],[hyp284]) ).

cnf(c295,plain,
    'queue$u53' = store(q16,seq,'earray$u52'),
    inference(clausification,[status(esa)],[hyp285]) ).

cnf(c296,plain,
    'queue$u55' = store('queue$u53',tail,'index$u54'),
    inference(clausification,[status(esa)],[hyp286]) ).

cnf(c297,plain,
    'queue$u59' = store(q17,seq,'earray$u58'),
    inference(clausification,[status(esa)],[hyp287]) ).

cnf(c298,plain,
    'queue$u61' = store('queue$u59',tail,'index$u60'),
    inference(clausification,[status(esa)],[hyp288]) ).

cnf(c299,plain,
    'queue$u65' = store(q18,seq,'earray$u64'),
    inference(clausification,[status(esa)],[hyp289]) ).

cnf(c300,plain,
    'queue$u67' = store('queue$u65',tail,'index$u66'),
    inference(clausification,[status(esa)],[hyp290]) ).

cnf(c301,plain,
    'queue$u7' = store('queue$u5',tail,'index$u6'),
    inference(clausification,[status(esa)],[hyp291]) ).

cnf(c302,plain,
    'queue$u71' = store(q1,seq,'earray$u70'),
    inference(clausification,[status(esa)],[hyp292]) ).

cnf(c303,plain,
    'queue$u73' = store('queue$u71',tail,'index$u72'),
    inference(clausification,[status(esa)],[hyp293]) ).

cnf(c304,plain,
    'queue$u77' = store(q19,seq,'earray$u76'),
    inference(clausification,[status(esa)],[hyp294]) ).

cnf(c305,plain,
    'queue$u79' = store('queue$u77',tail,'index$u78'),
    inference(clausification,[status(esa)],[hyp295]) ).

cnf(c306,plain,
    'queue$u83' = store(q20,seq,'earray$u82'),
    inference(clausification,[status(esa)],[hyp296]) ).

cnf(c307,plain,
    'queue$u85' = store('queue$u83',tail,'index$u84'),
    inference(clausification,[status(esa)],[hyp297]) ).

cnf(c308,plain,
    'queue$u89' = store(q21,seq,'earray$u88'),
    inference(clausification,[status(esa)],[hyp298]) ).

cnf(c309,plain,
    'queue$u91' = store('queue$u89',tail,'index$u90'),
    inference(clausification,[status(esa)],[hyp299]) ).

cnf(c310,plain,
    'queue$u95' = store(q22,seq,'earray$u94'),
    inference(clausification,[status(esa)],[hyp300]) ).

cnf(c311,plain,
    'queue$u97' = store('queue$u95',tail,'index$u96'),
    inference(clausification,[status(esa)],[hyp301]) ).

cnf(c312,plain,
    q0 = 'queue$u1',
    inference(clausification,[status(esa)],[hyp302]) ).

cnf(c313,plain,
    q1 = 'queue$u7',
    inference(clausification,[status(esa)],[hyp303]) ).

cnf(c314,plain,
    q10 = 'queue$u13',
    inference(clausification,[status(esa)],[hyp304]) ).

cnf(c315,plain,
    q11 = 'queue$u19',
    inference(clausification,[status(esa)],[hyp305]) ).

cnf(c316,plain,
    q12 = 'queue$u25',
    inference(clausification,[status(esa)],[hyp306]) ).

cnf(c317,plain,
    q13 = 'queue$u31',
    inference(clausification,[status(esa)],[hyp307]) ).

cnf(c318,plain,
    q14 = 'queue$u37',
    inference(clausification,[status(esa)],[hyp308]) ).

cnf(c319,plain,
    q15 = 'queue$u43',
    inference(clausification,[status(esa)],[hyp309]) ).

cnf(c320,plain,
    q16 = 'queue$u49',
    inference(clausification,[status(esa)],[hyp310]) ).

cnf(c321,plain,
    q17 = 'queue$u55',
    inference(clausification,[status(esa)],[hyp311]) ).

cnf(c322,plain,
    q18 = 'queue$u61',
    inference(clausification,[status(esa)],[hyp312]) ).

cnf(c323,plain,
    q19 = 'queue$u67',
    inference(clausification,[status(esa)],[hyp313]) ).

cnf(c324,plain,
    q2 = 'queue$u73',
    inference(clausification,[status(esa)],[hyp314]) ).

cnf(c325,plain,
    q20 = 'queue$u79',
    inference(clausification,[status(esa)],[hyp315]) ).

cnf(c326,plain,
    q21 = 'queue$u85',
    inference(clausification,[status(esa)],[hyp316]) ).

cnf(c327,plain,
    q22 = 'queue$u91',
    inference(clausification,[status(esa)],[hyp317]) ).

cnf(c328,plain,
    q23 = 'queue$u97',
    inference(clausification,[status(esa)],[hyp318]) ).

cnf(c329,plain,
    q24 = 'queue$u103',
    inference(clausification,[status(esa)],[hyp319]) ).

cnf(c330,plain,
    q25 = 'queue$u109',
    inference(clausification,[status(esa)],[hyp320]) ).

cnf(c331,plain,
    q26 = 'queue$u115',
    inference(clausification,[status(esa)],[hyp321]) ).

cnf(c332,plain,
    q27 = 'queue$u121',
    inference(clausification,[status(esa)],[hyp322]) ).

cnf(c333,plain,
    q28 = 'queue$u127',
    inference(clausification,[status(esa)],[hyp323]) ).

cnf(c334,plain,
    q29 = 'queue$u133',
    inference(clausification,[status(esa)],[hyp324]) ).

cnf(c335,plain,
    q3 = 'queue$u139',
    inference(clausification,[status(esa)],[hyp325]) ).

cnf(c336,plain,
    q30 = 'queue$u145',
    inference(clausification,[status(esa)],[hyp326]) ).

cnf(c337,plain,
    q31 = 'queue$u151',
    inference(clausification,[status(esa)],[hyp327]) ).

cnf(c338,plain,
    q32 = 'queue$u157',
    inference(clausification,[status(esa)],[hyp328]) ).

cnf(c339,plain,
    q33 = 'queue$u163',
    inference(clausification,[status(esa)],[hyp329]) ).

cnf(c340,plain,
    q34 = 'queue$u169',
    inference(clausification,[status(esa)],[hyp330]) ).

cnf(c341,plain,
    q35 = 'queue$u175',
    inference(clausification,[status(esa)],[hyp331]) ).

cnf(c342,plain,
    q36 = 'queue$u181',
    inference(clausification,[status(esa)],[hyp332]) ).

cnf(c343,plain,
    q37 = 'queue$u187',
    inference(clausification,[status(esa)],[hyp333]) ).

cnf(c344,plain,
    q38 = 'queue$u193',
    inference(clausification,[status(esa)],[hyp334]) ).

cnf(c345,plain,
    q39 = 'queue$u199',
    inference(clausification,[status(esa)],[hyp335]) ).

cnf(c346,plain,
    q4 = 'queue$u205',
    inference(clausification,[status(esa)],[hyp336]) ).

cnf(c347,plain,
    q40 = 'queue$u211',
    inference(clausification,[status(esa)],[hyp337]) ).

cnf(c348,plain,
    q41 = 'queue$u217',
    inference(clausification,[status(esa)],[hyp338]) ).

cnf(c349,plain,
    q42 = 'queue$u223',
    inference(clausification,[status(esa)],[hyp339]) ).

cnf(c350,plain,
    q43 = 'queue$u229',
    inference(clausification,[status(esa)],[hyp340]) ).

cnf(c351,plain,
    q44 = 'queue$u235',
    inference(clausification,[status(esa)],[hyp341]) ).

cnf(c352,plain,
    q45 = 'queue$u241',
    inference(clausification,[status(esa)],[hyp342]) ).

cnf(c353,plain,
    q46 = 'queue$u247',
    inference(clausification,[status(esa)],[hyp343]) ).

cnf(c354,plain,
    q47 = 'queue$u253',
    inference(clausification,[status(esa)],[hyp344]) ).

cnf(c355,plain,
    q48 = 'queue$u259',
    inference(clausification,[status(esa)],[hyp345]) ).

cnf(c356,plain,
    q49 = 'queue$u265',
    inference(clausification,[status(esa)],[hyp346]) ).

cnf(c357,plain,
    q5 = 'queue$u271',
    inference(clausification,[status(esa)],[hyp347]) ).

cnf(c358,plain,
    q6 = 'queue$u277',
    inference(clausification,[status(esa)],[hyp348]) ).

cnf(c359,plain,
    q7 = 'queue$u283',
    inference(clausification,[status(esa)],[hyp349]) ).

cnf(c360,plain,
    q8 = 'queue$u289',
    inference(clausification,[status(esa)],[hyp350]) ).

cnf(c361,plain,
    q9 = 'queue$u295',
    inference(clausification,[status(esa)],[hyp351]) ).

cnf(c362,plain,
    'elem$u298' != 'elem$u301',
    inference(clausification,[status(esa)],[goal]) ).

cnf(d0,plain,
    q3 = store('queue$u137',tail,'index$u138'),
    inference(demodulation,[status(thm)],[c229,c335]) ).

cnf(d1,plain,
    select(q3,tail) = 'index$u138',
    inference(superposition,[status(thm)],[d0,c0]) ).

cnf(d2,plain,
    'index$u201' = 'index$u138',
    inference(demodulation,[status(thm)],[d1,c148]) ).

cnf(d3,plain,
    p('index$u138') = 'index$u135',
    inference(superposition,[status(thm)],[c125,c5]) ).

cnf(d4,plain,
    s('index$u135') = 'index$u138',
    inference(superposition,[status(thm)],[d3,c6]) ).

cnf(d5,plain,
    p('index$u138') = 'index$u135',
    inference(superposition,[status(thm)],[d4,c5]) ).

cnf(d6,plain,
    p('index$u201') = 'index$u135',
    inference(demodulation,[status(thm)],[d5,d2]) ).

cnf(d7,plain,
    p(X0) = s(s(X0)),
    inference(superposition,[status(thm)],[c9,c5]) ).

cnf(d8,plain,
    q4 = store('queue$u203',tail,'index$u204'),
    inference(demodulation,[status(thm)],[c253,c346]) ).

cnf(d9,plain,
    select(q4,tail) = 'index$u204',
    inference(superposition,[status(thm)],[d8,c0]) ).

cnf(d10,plain,
    'index$u267' = 'index$u204',
    inference(demodulation,[status(thm)],[d9,c172]) ).

cnf(d11,plain,
    p('index$u204') = 'index$u201',
    inference(superposition,[status(thm)],[c149,c5]) ).

cnf(d12,plain,
    s('index$u201') = 'index$u204',
    inference(superposition,[status(thm)],[d11,c6]) ).

cnf(d13,plain,
    s('index$u201') = 'index$u267',
    inference(demodulation,[status(thm)],[d12,d10]) ).

cnf(d14,plain,
    p('index$u201') = s('index$u267'),
    inference(superposition,[status(thm)],[d13,d7]) ).

cnf(d15,plain,
    'index$u135' = s('index$u267'),
    inference(demodulation,[status(thm)],[d14,d6]) ).

cnf(d16,plain,
    p('index$u267') = 'index$u201',
    inference(demodulation,[status(thm)],[d11,d10]) ).

cnf(d17,plain,
    q6 = store('queue$u275',tail,'index$u276'),
    inference(demodulation,[status(thm)],[c279,c358]) ).

cnf(d18,plain,
    select(q6,tail) = 'index$u276',
    inference(superposition,[status(thm)],[d17,c0]) ).

cnf(d19,plain,
    'index$u279' = 'index$u276',
    inference(demodulation,[status(thm)],[d18,c177]) ).

cnf(d20,plain,
    p('index$u276') = 'index$u273',
    inference(superposition,[status(thm)],[c176,c5]) ).

cnf(d21,plain,
    s('index$u273') = 'index$u276',
    inference(superposition,[status(thm)],[d20,c6]) ).

cnf(d22,plain,
    s('index$u273') = 'index$u279',
    inference(demodulation,[status(thm)],[d21,d19]) ).

cnf(d23,plain,
    q5 = store('queue$u269',tail,'index$u270'),
    inference(demodulation,[status(thm)],[c277,c357]) ).

cnf(d24,plain,
    select(q5,tail) = 'index$u270',
    inference(superposition,[status(thm)],[d23,c0]) ).

cnf(d25,plain,
    'index$u273' = 'index$u270',
    inference(demodulation,[status(thm)],[d24,c175]) ).

cnf(d26,plain,
    s(s(X0)) = p(X0),
    inference(superposition,[status(thm)],[c6,c9]) ).

cnf(d27,plain,
    s('index$u270') = p('index$u267'),
    inference(superposition,[status(thm)],[c174,d26]) ).

cnf(d28,plain,
    s('index$u273') = p('index$u267'),
    inference(demodulation,[status(thm)],[d27,d25]) ).

cnf(d29,plain,
    'index$u279' = p('index$u267'),
    inference(demodulation,[status(thm)],[d28,d22]) ).

cnf(d30,plain,
    'index$u279' = 'index$u201',
    inference(demodulation,[status(thm)],[d29,d16]) ).

cnf(d31,plain,
    q7 = store('queue$u281',tail,'index$u282'),
    inference(demodulation,[status(thm)],[c281,c359]) ).

cnf(d32,plain,
    select(q7,tail) = 'index$u282',
    inference(superposition,[status(thm)],[d31,c0]) ).

cnf(d33,plain,
    'index$u285' = 'index$u282',
    inference(demodulation,[status(thm)],[d32,c179]) ).

cnf(d34,plain,
    'index$u285' = s('index$u279'),
    inference(demodulation,[status(thm)],[c178,d33]) ).

cnf(d35,plain,
    'index$u285' = s('index$u201'),
    inference(demodulation,[status(thm)],[d34,d30]) ).

cnf(d36,plain,
    'index$u285' = 'index$u267',
    inference(demodulation,[status(thm)],[d35,d13]) ).

cnf(d37,plain,
    q8 = store('queue$u287',tail,'index$u288'),
    inference(demodulation,[status(thm)],[c283,c360]) ).

cnf(d38,plain,
    select(q8,tail) = 'index$u288',
    inference(superposition,[status(thm)],[d37,c0]) ).

cnf(d39,plain,
    'index$u291' = 'index$u288',
    inference(demodulation,[status(thm)],[d38,c181]) ).

cnf(d40,plain,
    'index$u291' = s('index$u285'),
    inference(demodulation,[status(thm)],[c180,d39]) ).

cnf(d41,plain,
    'index$u291' = s('index$u267'),
    inference(demodulation,[status(thm)],[d40,d36]) ).

cnf(d42,plain,
    'index$u291' = 'index$u135',
    inference(demodulation,[status(thm)],[d41,d15]) ).

cnf(d43,plain,
    q9 = store('queue$u293',tail,'index$u294'),
    inference(demodulation,[status(thm)],[c286,c361]) ).

cnf(d44,plain,
    select(q9,tail) = 'index$u294',
    inference(superposition,[status(thm)],[d43,c0]) ).

cnf(d45,plain,
    'index$u9' = 'index$u294',
    inference(demodulation,[status(thm)],[d44,c208]) ).

cnf(d46,plain,
    'index$u9' = s('index$u291'),
    inference(demodulation,[status(thm)],[c182,d45]) ).

cnf(d47,plain,
    'index$u9' = s('index$u135'),
    inference(demodulation,[status(thm)],[d46,d42]) ).

cnf(d48,plain,
    q10 = store('queue$u11',tail,'index$u12'),
    inference(demodulation,[status(thm)],[c225,c314]) ).

cnf(d49,plain,
    select(q10,tail) = 'index$u12',
    inference(superposition,[status(thm)],[d48,c0]) ).

cnf(d50,plain,
    'index$u15' = 'index$u12',
    inference(demodulation,[status(thm)],[d49,c129]) ).

cnf(d51,plain,
    p('index$u12') = 'index$u9',
    inference(superposition,[status(thm)],[c118,c5]) ).

cnf(d52,plain,
    s('index$u9') = 'index$u12',
    inference(superposition,[status(thm)],[d51,c6]) ).

cnf(d53,plain,
    p('index$u12') = 'index$u9',
    inference(superposition,[status(thm)],[d52,c5]) ).

cnf(d54,plain,
    p('index$u15') = 'index$u9',
    inference(demodulation,[status(thm)],[d53,d50]) ).

cnf(d55,plain,
    q12 = store('queue$u23',tail,'index$u24'),
    inference(demodulation,[status(thm)],[c269,c316]) ).

cnf(d56,plain,
    select(q12,tail) = 'index$u24',
    inference(superposition,[status(thm)],[d55,c0]) ).

cnf(d57,plain,
    'index$u27' = 'index$u24',
    inference(demodulation,[status(thm)],[d56,c173]) ).

cnf(d58,plain,
    p('index$u24') = 'index$u21',
    inference(superposition,[status(thm)],[c162,c5]) ).

cnf(d59,plain,
    s('index$u21') = 'index$u24',
    inference(superposition,[status(thm)],[d58,c6]) ).

cnf(d60,plain,
    s('index$u21') = 'index$u27',
    inference(demodulation,[status(thm)],[d59,d57]) ).

cnf(d61,plain,
    q11 = store('queue$u17',tail,'index$u18'),
    inference(demodulation,[status(thm)],[c247,c315]) ).

cnf(d62,plain,
    select(q11,tail) = 'index$u18',
    inference(superposition,[status(thm)],[d61,c0]) ).

cnf(d63,plain,
    'index$u21' = 'index$u18',
    inference(demodulation,[status(thm)],[d62,c151]) ).

cnf(d64,plain,
    s('index$u18') = p('index$u15'),
    inference(superposition,[status(thm)],[c140,d26]) ).

cnf(d65,plain,
    s('index$u21') = p('index$u15'),
    inference(demodulation,[status(thm)],[d64,d63]) ).

cnf(d66,plain,
    'index$u27' = p('index$u15'),
    inference(demodulation,[status(thm)],[d65,d60]) ).

cnf(d67,plain,
    'index$u27' = 'index$u9',
    inference(demodulation,[status(thm)],[d66,d54]) ).

cnf(d68,plain,
    p('index$u27') = 'index$u21',
    inference(demodulation,[status(thm)],[d58,d57]) ).

cnf(d69,plain,
    p('index$u9') = 'index$u21',
    inference(demodulation,[status(thm)],[d68,d67]) ).

cnf(d70,plain,
    p('index$u294') = 'index$u291',
    inference(superposition,[status(thm)],[c182,c5]) ).

cnf(d71,plain,
    p('index$u9') = 'index$u291',
    inference(demodulation,[status(thm)],[d70,d45]) ).

cnf(d72,plain,
    'index$u21' = 'index$u291',
    inference(demodulation,[status(thm)],[d71,d69]) ).

cnf(d73,plain,
    'index$u21' = 'index$u135',
    inference(demodulation,[status(thm)],[d72,d42]) ).

cnf(d74,plain,
    p('index$u27') = 'index$u21',
    inference(superposition,[status(thm)],[d60,c5]) ).

cnf(d75,plain,
    p('index$u9') = 'index$u21',
    inference(demodulation,[status(thm)],[d74,d67]) ).

cnf(d76,plain,
    p('index$u9') = 'index$u135',
    inference(demodulation,[status(thm)],[d75,d73]) ).

cnf(d77,plain,
    p(p(X0)) = s(X0),
    inference(superposition,[status(thm)],[d7,c5]) ).

cnf(d78,plain,
    p('index$u15') = s('index$u18'),
    inference(superposition,[status(thm)],[c140,d7]) ).

cnf(d79,plain,
    p('index$u15') = s('index$u21'),
    inference(demodulation,[status(thm)],[d78,d63]) ).

cnf(d80,plain,
    p('index$u15') = 'index$u27',
    inference(demodulation,[status(thm)],[d79,d60]) ).

cnf(d81,plain,
    p('index$u27') = s('index$u15'),
    inference(superposition,[status(thm)],[d80,d77]) ).

cnf(d82,plain,
    p('index$u9') = s('index$u15'),
    inference(demodulation,[status(thm)],[d81,d67]) ).

cnf(d83,plain,
    'index$u135' = s('index$u15'),
    inference(demodulation,[status(thm)],[d82,d76]) ).

cnf(d84,plain,
    'index$u15' = s('index$u9'),
    inference(demodulation,[status(thm)],[c118,d50]) ).

cnf(d85,plain,
    q13 = store('queue$u29',tail,'index$u30'),
    inference(demodulation,[status(thm)],[c287,c317]) ).

cnf(d86,plain,
    select(q13,tail) = 'index$u30',
    inference(superposition,[status(thm)],[d85,c0]) ).

cnf(d87,plain,
    'index$u33' = 'index$u30',
    inference(demodulation,[status(thm)],[d86,c188]) ).

cnf(d88,plain,
    'index$u33' = s('index$u27'),
    inference(demodulation,[status(thm)],[c186,d87]) ).

cnf(d89,plain,
    'index$u33' = s('index$u9'),
    inference(demodulation,[status(thm)],[d88,d67]) ).

cnf(d90,plain,
    'index$u33' = 'index$u15',
    inference(demodulation,[status(thm)],[d89,d84]) ).

cnf(d91,plain,
    q14 = store('queue$u35',tail,'index$u36'),
    inference(demodulation,[status(thm)],[c289,c318]) ).

cnf(d92,plain,
    select(q14,tail) = 'index$u36',
    inference(superposition,[status(thm)],[d91,c0]) ).

cnf(d93,plain,
    'index$u39' = 'index$u36',
    inference(demodulation,[status(thm)],[d92,c190]) ).

cnf(d94,plain,
    'index$u39' = s('index$u33'),
    inference(demodulation,[status(thm)],[c189,d93]) ).

cnf(d95,plain,
    'index$u39' = s('index$u15'),
    inference(demodulation,[status(thm)],[d94,d90]) ).

cnf(d96,plain,
    'index$u39' = 'index$u135',
    inference(demodulation,[status(thm)],[d95,d83]) ).

cnf(d97,plain,
    q15 = store('queue$u41',tail,'index$u42'),
    inference(demodulation,[status(thm)],[c291,c319]) ).

cnf(d98,plain,
    select(q15,tail) = 'index$u42',
    inference(superposition,[status(thm)],[d97,c0]) ).

cnf(d99,plain,
    'index$u45' = 'index$u42',
    inference(demodulation,[status(thm)],[d98,c192]) ).

cnf(d100,plain,
    p('index$u39') = s('index$u42'),
    inference(superposition,[status(thm)],[c191,d7]) ).

cnf(d101,plain,
    p('index$u39') = s('index$u45'),
    inference(demodulation,[status(thm)],[d100,d99]) ).

cnf(d102,plain,
    p(s('index$u45')) = s('index$u39'),
    inference(superposition,[status(thm)],[d101,d77]) ).

cnf(d103,plain,
    'index$u45' = s('index$u39'),
    inference(demodulation,[status(thm)],[d102,c5]) ).

cnf(d104,plain,
    'index$u45' = s('index$u135'),
    inference(demodulation,[status(thm)],[d103,d96]) ).

cnf(d105,plain,
    'index$u45' = 'index$u9',
    inference(demodulation,[status(thm)],[d104,d47]) ).

cnf(d106,plain,
    q24 = store('queue$u101',tail,'index$u102'),
    inference(demodulation,[status(thm)],[c215,c329]) ).

cnf(d107,plain,
    select(q24,tail) = 'index$u102',
    inference(superposition,[status(thm)],[d106,c0]) ).

cnf(d108,plain,
    'index$u105' = 'index$u102',
    inference(demodulation,[status(thm)],[d107,c113]) ).

cnf(d109,plain,
    p('index$u102') = 'index$u99',
    inference(superposition,[status(thm)],[c112,c5]) ).

cnf(d110,plain,
    s('index$u99') = 'index$u102',
    inference(superposition,[status(thm)],[d109,c6]) ).

cnf(d111,plain,
    s('index$u99') = 'index$u105',
    inference(demodulation,[status(thm)],[d110,d108]) ).

cnf(d112,plain,
    q25 = store('queue$u107',tail,'index$u108'),
    inference(demodulation,[status(thm)],[c217,c330]) ).

cnf(d113,plain,
    select(q25,tail) = 'index$u108',
    inference(superposition,[status(thm)],[d112,c0]) ).

cnf(d114,plain,
    'index$u111' = 'index$u108',
    inference(demodulation,[status(thm)],[d113,c115]) ).

cnf(d115,plain,
    p('index$u102') = 'index$u99',
    inference(superposition,[status(thm)],[d110,c5]) ).

cnf(d116,plain,
    p('index$u105') = 'index$u99',
    inference(demodulation,[status(thm)],[d115,d108]) ).

cnf(d117,plain,
    p('index$u108') = 'index$u105',
    inference(superposition,[status(thm)],[c114,c5]) ).

cnf(d118,plain,
    s('index$u105') = 'index$u108',
    inference(superposition,[status(thm)],[d117,c6]) ).

cnf(d119,plain,
    p('index$u105') = s('index$u108'),
    inference(superposition,[status(thm)],[d118,d7]) ).

cnf(d120,plain,
    'index$u99' = s('index$u108'),
    inference(demodulation,[status(thm)],[d119,d116]) ).

cnf(d121,plain,
    'index$u99' = s('index$u111'),
    inference(demodulation,[status(thm)],[d120,d114]) ).

cnf(d122,plain,
    q26 = store('queue$u113',tail,'index$u114'),
    inference(demodulation,[status(thm)],[c220,c331]) ).

cnf(d123,plain,
    select(q26,tail) = 'index$u114',
    inference(superposition,[status(thm)],[d122,c0]) ).

cnf(d124,plain,
    'index$u117' = 'index$u114',
    inference(demodulation,[status(thm)],[d123,c117]) ).

cnf(d125,plain,
    'index$u117' = s('index$u111'),
    inference(demodulation,[status(thm)],[c116,d124]) ).

cnf(d126,plain,
    'index$u117' = 'index$u99',
    inference(demodulation,[status(thm)],[d125,d121]) ).

cnf(d127,plain,
    p('index$u114') = 'index$u111',
    inference(superposition,[status(thm)],[c116,c5]) ).

cnf(d128,plain,
    p('index$u117') = 'index$u111',
    inference(demodulation,[status(thm)],[d127,d124]) ).

cnf(d129,plain,
    p('index$u99') = 'index$u111',
    inference(demodulation,[status(thm)],[d128,d126]) ).

cnf(d130,plain,
    p('index$u108') = 'index$u105',
    inference(superposition,[status(thm)],[d118,c5]) ).

cnf(d131,plain,
    p('index$u111') = 'index$u105',
    inference(demodulation,[status(thm)],[d130,d114]) ).

cnf(d132,plain,
    q23 = store('queue$u95',tail,'index$u96'),
    inference(demodulation,[status(thm)],[c311,c328]) ).

cnf(d133,plain,
    select(q23,tail) = 'index$u96',
    inference(superposition,[status(thm)],[d132,c0]) ).

cnf(d134,plain,
    'index$u99' = 'index$u96',
    inference(demodulation,[status(thm)],[d133,c212]) ).

cnf(d135,plain,
    p('index$u96') = 'index$u93',
    inference(superposition,[status(thm)],[c211,c5]) ).

cnf(d136,plain,
    p('index$u99') = 'index$u93',
    inference(demodulation,[status(thm)],[d135,d134]) ).

cnf(d137,plain,
    'index$u111' = 'index$u93',
    inference(demodulation,[status(thm)],[d136,d129]) ).

cnf(d138,plain,
    p(s(X0)) = s(p(X0)),
    inference(superposition,[status(thm)],[d7,d7]) ).

cnf(d139,plain,
    X0 = s(p(X0)),
    inference(demodulation,[status(thm)],[d138,c5]) ).

cnf(d140,plain,
    q22 = store('queue$u89',tail,'index$u90'),
    inference(demodulation,[status(thm)],[c309,c327]) ).

cnf(d141,plain,
    select(q22,tail) = 'index$u90',
    inference(superposition,[status(thm)],[d140,c0]) ).

cnf(d142,plain,
    'index$u93' = 'index$u90',
    inference(demodulation,[status(thm)],[d141,c210]) ).

cnf(d143,plain,
    p('index$u87') = s('index$u90'),
    inference(superposition,[status(thm)],[c209,d7]) ).

cnf(d144,plain,
    p('index$u87') = s('index$u93'),
    inference(demodulation,[status(thm)],[d143,d142]) ).

cnf(d145,plain,
    'index$u87' = s(s('index$u93')),
    inference(superposition,[status(thm)],[d144,d139]) ).

cnf(d146,plain,
    'index$u87' = p('index$u93'),
    inference(demodulation,[status(thm)],[d145,d7]) ).

cnf(d147,plain,
    'index$u87' = p('index$u111'),
    inference(demodulation,[status(thm)],[d146,d137]) ).

cnf(d148,plain,
    'index$u87' = 'index$u105',
    inference(demodulation,[status(thm)],[d147,d131]) ).

cnf(d149,plain,
    q21 = store('queue$u83',tail,'index$u84'),
    inference(demodulation,[status(thm)],[c307,c326]) ).

cnf(d150,plain,
    select(q21,tail) = 'index$u84',
    inference(superposition,[status(thm)],[d149,c0]) ).

cnf(d151,plain,
    'index$u87' = 'index$u84',
    inference(demodulation,[status(thm)],[d150,c207]) ).

cnf(d152,plain,
    p('index$u81') = s('index$u84'),
    inference(superposition,[status(thm)],[c206,d7]) ).

cnf(d153,plain,
    p('index$u81') = s('index$u87'),
    inference(demodulation,[status(thm)],[d152,d151]) ).

cnf(d154,plain,
    'index$u81' = s(s('index$u87')),
    inference(superposition,[status(thm)],[d153,d139]) ).

cnf(d155,plain,
    'index$u81' = p('index$u87'),
    inference(demodulation,[status(thm)],[d154,d7]) ).

cnf(d156,plain,
    'index$u81' = p('index$u105'),
    inference(demodulation,[status(thm)],[d155,d148]) ).

cnf(d157,plain,
    'index$u81' = 'index$u99',
    inference(demodulation,[status(thm)],[d156,d116]) ).

cnf(d158,plain,
    q16 = store('queue$u47',tail,'index$u48'),
    inference(demodulation,[status(thm)],[c293,c320]) ).

cnf(d159,plain,
    select(q16,tail) = 'index$u48',
    inference(superposition,[status(thm)],[d158,c0]) ).

cnf(d160,plain,
    'index$u51' = 'index$u48',
    inference(demodulation,[status(thm)],[d159,c194]) ).

cnf(d161,plain,
    p('index$u45') = s('index$u48'),
    inference(superposition,[status(thm)],[c193,d7]) ).

cnf(d162,plain,
    p('index$u45') = s('index$u51'),
    inference(demodulation,[status(thm)],[d161,d160]) ).

cnf(d163,plain,
    p(s('index$u51')) = s('index$u45'),
    inference(superposition,[status(thm)],[d162,d77]) ).

cnf(d164,plain,
    'index$u51' = s('index$u45'),
    inference(demodulation,[status(thm)],[d163,c5]) ).

cnf(d165,plain,
    'index$u51' = s('index$u9'),
    inference(demodulation,[status(thm)],[d164,d105]) ).

cnf(d166,plain,
    'index$u51' = 'index$u15',
    inference(demodulation,[status(thm)],[d165,d84]) ).

cnf(d167,plain,
    q17 = store('queue$u53',tail,'index$u54'),
    inference(demodulation,[status(thm)],[c296,c321]) ).

cnf(d168,plain,
    select(q17,tail) = 'index$u54',
    inference(superposition,[status(thm)],[d167,c0]) ).

cnf(d169,plain,
    'index$u57' = 'index$u54',
    inference(demodulation,[status(thm)],[d168,c196]) ).

cnf(d170,plain,
    s('index$u54') = p('index$u51'),
    inference(superposition,[status(thm)],[c195,d26]) ).

cnf(d171,plain,
    s('index$u57') = p('index$u51'),
    inference(demodulation,[status(thm)],[d170,d169]) ).

cnf(d172,plain,
    p(s('index$u57')) = s('index$u51'),
    inference(superposition,[status(thm)],[d171,d77]) ).

cnf(d173,plain,
    'index$u57' = s('index$u51'),
    inference(demodulation,[status(thm)],[d172,c5]) ).

cnf(d174,plain,
    'index$u57' = s('index$u15'),
    inference(demodulation,[status(thm)],[d173,d166]) ).

cnf(d175,plain,
    'index$u57' = 'index$u135',
    inference(demodulation,[status(thm)],[d174,d83]) ).

cnf(d176,plain,
    q18 = store('queue$u59',tail,'index$u60'),
    inference(demodulation,[status(thm)],[c298,c322]) ).

cnf(d177,plain,
    select(q18,tail) = 'index$u60',
    inference(superposition,[status(thm)],[d176,c0]) ).

cnf(d178,plain,
    'index$u63' = 'index$u60',
    inference(demodulation,[status(thm)],[d177,c199]) ).

cnf(d179,plain,
    s('index$u60') = p('index$u57'),
    inference(superposition,[status(thm)],[c198,d26]) ).

cnf(d180,plain,
    s('index$u63') = p('index$u57'),
    inference(demodulation,[status(thm)],[d179,d178]) ).

cnf(d181,plain,
    p(s('index$u63')) = s('index$u57'),
    inference(superposition,[status(thm)],[d180,d77]) ).

cnf(d182,plain,
    'index$u63' = s('index$u57'),
    inference(demodulation,[status(thm)],[d181,c5]) ).

cnf(d183,plain,
    'index$u63' = s('index$u135'),
    inference(demodulation,[status(thm)],[d182,d175]) ).

cnf(d184,plain,
    'index$u63' = 'index$u9',
    inference(demodulation,[status(thm)],[d183,d47]) ).

cnf(d185,plain,
    q19 = store('queue$u65',tail,'index$u66'),
    inference(demodulation,[status(thm)],[c300,c323]) ).

cnf(d186,plain,
    select(q19,tail) = 'index$u66',
    inference(superposition,[status(thm)],[d185,c0]) ).

cnf(d187,plain,
    'index$u75' = 'index$u66',
    inference(demodulation,[status(thm)],[d186,c203]) ).

cnf(d188,plain,
    s('index$u66') = p('index$u63'),
    inference(superposition,[status(thm)],[c200,d26]) ).

cnf(d189,plain,
    s('index$u75') = p('index$u63'),
    inference(demodulation,[status(thm)],[d188,d187]) ).

cnf(d190,plain,
    p(s('index$u75')) = s('index$u63'),
    inference(superposition,[status(thm)],[d189,d77]) ).

cnf(d191,plain,
    'index$u75' = s('index$u63'),
    inference(demodulation,[status(thm)],[d190,c5]) ).

cnf(d192,plain,
    'index$u75' = s('index$u9'),
    inference(demodulation,[status(thm)],[d191,d184]) ).

cnf(d193,plain,
    'index$u75' = 'index$u15',
    inference(demodulation,[status(thm)],[d192,d84]) ).

cnf(d194,plain,
    q20 = store('queue$u77',tail,'index$u78'),
    inference(demodulation,[status(thm)],[c305,c325]) ).

cnf(d195,plain,
    select(q20,tail) = 'index$u78',
    inference(superposition,[status(thm)],[d194,c0]) ).

cnf(d196,plain,
    'index$u81' = 'index$u78',
    inference(demodulation,[status(thm)],[d195,c205]) ).

cnf(d197,plain,
    s('index$u78') = p('index$u75'),
    inference(superposition,[status(thm)],[c204,d26]) ).

cnf(d198,plain,
    s('index$u81') = p('index$u75'),
    inference(demodulation,[status(thm)],[d197,d196]) ).

cnf(d199,plain,
    'index$u75' = s(s('index$u81')),
    inference(superposition,[status(thm)],[d198,d139]) ).

cnf(d200,plain,
    'index$u15' = s(s('index$u81')),
    inference(demodulation,[status(thm)],[d199,d193]) ).

cnf(d201,plain,
    'index$u15' = p('index$u81'),
    inference(demodulation,[status(thm)],[d200,d7]) ).

cnf(d202,plain,
    'index$u15' = p('index$u99'),
    inference(demodulation,[status(thm)],[d201,d157]) ).

cnf(d203,plain,
    'index$u15' = 'index$u111',
    inference(demodulation,[status(thm)],[d202,d129]) ).

cnf(d204,plain,
    'index$u33' = 'index$u111',
    inference(demodulation,[status(thm)],[d90,d203]) ).

cnf(d205,plain,
    s(X0) = p(p(X0)),
    inference(superposition,[status(thm)],[c6,d26]) ).

cnf(d206,plain,
    p('index$u33') = s('index$u36'),
    inference(superposition,[status(thm)],[c189,d7]) ).

cnf(d207,plain,
    p('index$u33') = s('index$u39'),
    inference(demodulation,[status(thm)],[d206,d93]) ).

cnf(d208,plain,
    s('index$u33') = p(s('index$u39')),
    inference(superposition,[status(thm)],[d207,d205]) ).

cnf(d209,plain,
    s('index$u111') = p(s('index$u39')),
    inference(demodulation,[status(thm)],[d208,d204]) ).

cnf(d210,plain,
    'index$u99' = p(s('index$u39')),
    inference(demodulation,[status(thm)],[d209,d121]) ).

cnf(d211,plain,
    'index$u99' = 'index$u39',
    inference(demodulation,[status(thm)],[d210,c5]) ).

cnf(d212,plain,
    s('index$u42') = p('index$u39'),
    inference(superposition,[status(thm)],[c191,d26]) ).

cnf(d213,plain,
    s('index$u45') = p('index$u39'),
    inference(demodulation,[status(thm)],[d212,d99]) ).

cnf(d214,plain,
    s('index$u39') = p(s('index$u45')),
    inference(superposition,[status(thm)],[d213,d205]) ).

cnf(d215,plain,
    s('index$u99') = p(s('index$u45')),
    inference(demodulation,[status(thm)],[d214,d211]) ).

cnf(d216,plain,
    'index$u105' = p(s('index$u45')),
    inference(demodulation,[status(thm)],[d215,d111]) ).

cnf(d217,plain,
    'index$u105' = 'index$u45',
    inference(demodulation,[status(thm)],[d216,c5]) ).

cnf(d218,plain,
    'index$u105' = 'index$u9',
    inference(demodulation,[status(thm)],[d217,d105]) ).

cnf(d219,plain,
    s('index$u105') = 'index$u111',
    inference(demodulation,[status(thm)],[d118,d114]) ).

cnf(d220,plain,
    q27 = store('queue$u119',tail,'index$u120'),
    inference(demodulation,[status(thm)],[c222,c332]) ).

cnf(d221,plain,
    select(q27,tail) = 'index$u120',
    inference(superposition,[status(thm)],[d220,c0]) ).

cnf(d222,plain,
    'index$u123' = 'index$u120',
    inference(demodulation,[status(thm)],[d221,c120]) ).

cnf(d223,plain,
    p('index$u120') = 'index$u117',
    inference(superposition,[status(thm)],[c119,c5]) ).

cnf(d224,plain,
    s('index$u117') = 'index$u120',
    inference(superposition,[status(thm)],[d223,c6]) ).

cnf(d225,plain,
    s('index$u117') = 'index$u123',
    inference(demodulation,[status(thm)],[d224,d222]) ).

cnf(d226,plain,
    s('index$u99') = 'index$u123',
    inference(demodulation,[status(thm)],[d225,d126]) ).

cnf(d227,plain,
    'index$u105' = 'index$u123',
    inference(demodulation,[status(thm)],[d226,d111]) ).

cnf(d228,plain,
    q28 = store('queue$u125',tail,'index$u126'),
    inference(demodulation,[status(thm)],[c224,c333]) ).

cnf(d229,plain,
    select(q28,tail) = 'index$u126',
    inference(superposition,[status(thm)],[d228,c0]) ).

cnf(d230,plain,
    'index$u129' = 'index$u126',
    inference(demodulation,[status(thm)],[d229,c122]) ).

cnf(d231,plain,
    p('index$u126') = 'index$u123',
    inference(superposition,[status(thm)],[c121,c5]) ).

cnf(d232,plain,
    s('index$u123') = 'index$u126',
    inference(superposition,[status(thm)],[d231,c6]) ).

cnf(d233,plain,
    s('index$u123') = 'index$u129',
    inference(demodulation,[status(thm)],[d232,d230]) ).

cnf(d234,plain,
    s('index$u105') = 'index$u129',
    inference(demodulation,[status(thm)],[d233,d227]) ).

cnf(d235,plain,
    'index$u111' = 'index$u129',
    inference(demodulation,[status(thm)],[d234,d219]) ).

cnf(d236,plain,
    q29 = store('queue$u131',tail,'index$u132'),
    inference(demodulation,[status(thm)],[c227,c334]) ).

cnf(d237,plain,
    select(q29,tail) = 'index$u132',
    inference(superposition,[status(thm)],[d236,c0]) ).

cnf(d238,plain,
    'index$u141' = 'index$u132',
    inference(demodulation,[status(thm)],[d237,c126]) ).

cnf(d239,plain,
    'index$u141' = s('index$u129'),
    inference(demodulation,[status(thm)],[c123,d238]) ).

cnf(d240,plain,
    'index$u141' = s('index$u111'),
    inference(demodulation,[status(thm)],[d239,d235]) ).

cnf(d241,plain,
    'index$u141' = 'index$u99',
    inference(demodulation,[status(thm)],[d240,d121]) ).

cnf(d242,plain,
    q30 = store('queue$u143',tail,'index$u144'),
    inference(demodulation,[status(thm)],[c231,c336]) ).

cnf(d243,plain,
    select(q30,tail) = 'index$u144',
    inference(superposition,[status(thm)],[d242,c0]) ).

cnf(d244,plain,
    'index$u147' = 'index$u144',
    inference(demodulation,[status(thm)],[d243,c128]) ).

cnf(d245,plain,
    p('index$u144') = 'index$u141',
    inference(superposition,[status(thm)],[c127,c5]) ).

cnf(d246,plain,
    s('index$u141') = 'index$u144',
    inference(superposition,[status(thm)],[d245,c6]) ).

cnf(d247,plain,
    s('index$u141') = 'index$u147',
    inference(demodulation,[status(thm)],[d246,d244]) ).

cnf(d248,plain,
    s('index$u99') = 'index$u147',
    inference(demodulation,[status(thm)],[d247,d241]) ).

cnf(d249,plain,
    'index$u105' = 'index$u147',
    inference(demodulation,[status(thm)],[d248,d111]) ).

cnf(d250,plain,
    q31 = store('queue$u149',tail,'index$u150'),
    inference(demodulation,[status(thm)],[c233,c337]) ).

cnf(d251,plain,
    select(q31,tail) = 'index$u150',
    inference(superposition,[status(thm)],[d250,c0]) ).

cnf(d252,plain,
    'index$u153' = 'index$u150',
    inference(demodulation,[status(thm)],[d251,c131]) ).

cnf(d253,plain,
    'index$u153' = s('index$u147'),
    inference(demodulation,[status(thm)],[c130,d252]) ).

cnf(d254,plain,
    'index$u153' = s('index$u105'),
    inference(demodulation,[status(thm)],[d253,d249]) ).

cnf(d255,plain,
    'index$u153' = 'index$u111',
    inference(demodulation,[status(thm)],[d254,d219]) ).

cnf(d256,plain,
    q32 = store('queue$u155',tail,'index$u156'),
    inference(demodulation,[status(thm)],[c235,c338]) ).

cnf(d257,plain,
    select(q32,tail) = 'index$u156',
    inference(superposition,[status(thm)],[d256,c0]) ).

cnf(d258,plain,
    'index$u159' = 'index$u156',
    inference(demodulation,[status(thm)],[d257,c133]) ).

cnf(d259,plain,
    p('index$u156') = 'index$u153',
    inference(superposition,[status(thm)],[c132,c5]) ).

cnf(d260,plain,
    s('index$u153') = 'index$u156',
    inference(superposition,[status(thm)],[d259,c6]) ).

cnf(d261,plain,
    p('index$u156') = 'index$u153',
    inference(superposition,[status(thm)],[d260,c5]) ).

cnf(d262,plain,
    p('index$u159') = 'index$u153',
    inference(demodulation,[status(thm)],[d261,d258]) ).

cnf(d263,plain,
    p('index$u159') = 'index$u111',
    inference(demodulation,[status(thm)],[d262,d255]) ).

cnf(d264,plain,
    q34 = store('queue$u167',tail,'index$u168'),
    inference(demodulation,[status(thm)],[c239,c340]) ).

cnf(d265,plain,
    select(q34,tail) = 'index$u168',
    inference(superposition,[status(thm)],[d264,c0]) ).

cnf(d266,plain,
    'index$u171' = 'index$u168',
    inference(demodulation,[status(thm)],[d265,c137]) ).

cnf(d267,plain,
    p('index$u168') = 'index$u165',
    inference(superposition,[status(thm)],[c136,c5]) ).

cnf(d268,plain,
    s('index$u165') = 'index$u168',
    inference(superposition,[status(thm)],[d267,c6]) ).

cnf(d269,plain,
    s('index$u165') = 'index$u171',
    inference(demodulation,[status(thm)],[d268,d266]) ).

cnf(d270,plain,
    q33 = store('queue$u161',tail,'index$u162'),
    inference(demodulation,[status(thm)],[c237,c339]) ).

cnf(d271,plain,
    select(q33,tail) = 'index$u162',
    inference(superposition,[status(thm)],[d270,c0]) ).

cnf(d272,plain,
    'index$u165' = 'index$u162',
    inference(demodulation,[status(thm)],[d271,c135]) ).

cnf(d273,plain,
    s('index$u162') = p('index$u159'),
    inference(superposition,[status(thm)],[c134,d26]) ).

cnf(d274,plain,
    s('index$u165') = p('index$u159'),
    inference(demodulation,[status(thm)],[d273,d272]) ).

cnf(d275,plain,
    'index$u171' = p('index$u159'),
    inference(demodulation,[status(thm)],[d274,d269]) ).

cnf(d276,plain,
    'index$u171' = 'index$u111',
    inference(demodulation,[status(thm)],[d275,d263]) ).

cnf(d277,plain,
    q35 = store('queue$u173',tail,'index$u174'),
    inference(demodulation,[status(thm)],[c242,c341]) ).

cnf(d278,plain,
    select(q35,tail) = 'index$u174',
    inference(superposition,[status(thm)],[d277,c0]) ).

cnf(d279,plain,
    'index$u177' = 'index$u174',
    inference(demodulation,[status(thm)],[d278,c139]) ).

cnf(d280,plain,
    'index$u177' = s('index$u171'),
    inference(demodulation,[status(thm)],[c138,d279]) ).

cnf(d281,plain,
    'index$u177' = s('index$u111'),
    inference(demodulation,[status(thm)],[d280,d276]) ).

cnf(d282,plain,
    'index$u177' = 'index$u99',
    inference(demodulation,[status(thm)],[d281,d121]) ).

cnf(d283,plain,
    q36 = store('queue$u179',tail,'index$u180'),
    inference(demodulation,[status(thm)],[c244,c342]) ).

cnf(d284,plain,
    select(q36,tail) = 'index$u180',
    inference(superposition,[status(thm)],[d283,c0]) ).

cnf(d285,plain,
    'index$u183' = 'index$u180',
    inference(demodulation,[status(thm)],[d284,c142]) ).

cnf(d286,plain,
    'index$u183' = s('index$u177'),
    inference(demodulation,[status(thm)],[c141,d285]) ).

cnf(d287,plain,
    'index$u183' = s('index$u99'),
    inference(demodulation,[status(thm)],[d286,d282]) ).

cnf(d288,plain,
    'index$u183' = 'index$u105',
    inference(demodulation,[status(thm)],[d287,d111]) ).

cnf(d289,plain,
    q37 = store('queue$u185',tail,'index$u186'),
    inference(demodulation,[status(thm)],[c246,c343]) ).

cnf(d290,plain,
    select(q37,tail) = 'index$u186',
    inference(superposition,[status(thm)],[d289,c0]) ).

cnf(d291,plain,
    'index$u189' = 'index$u186',
    inference(demodulation,[status(thm)],[d290,c144]) ).

cnf(d292,plain,
    p('index$u186') = 'index$u183',
    inference(superposition,[status(thm)],[c143,c5]) ).

cnf(d293,plain,
    p('index$u189') = 'index$u183',
    inference(demodulation,[status(thm)],[d292,d291]) ).

cnf(d294,plain,
    p('index$u189') = 'index$u105',
    inference(demodulation,[status(thm)],[d293,d288]) ).

cnf(d295,plain,
    q39 = store('queue$u197',tail,'index$u198'),
    inference(demodulation,[status(thm)],[c251,c345]) ).

cnf(d296,plain,
    select(q39,tail) = 'index$u198',
    inference(superposition,[status(thm)],[d295,c0]) ).

cnf(d297,plain,
    'index$u207' = 'index$u198',
    inference(demodulation,[status(thm)],[d296,c150]) ).

cnf(d298,plain,
    p('index$u198') = 'index$u195',
    inference(superposition,[status(thm)],[c147,c5]) ).

cnf(d299,plain,
    s('index$u195') = 'index$u198',
    inference(superposition,[status(thm)],[d298,c6]) ).

cnf(d300,plain,
    s('index$u195') = 'index$u207',
    inference(demodulation,[status(thm)],[d299,d297]) ).

cnf(d301,plain,
    q38 = store('queue$u191',tail,'index$u192'),
    inference(demodulation,[status(thm)],[c249,c344]) ).

cnf(d302,plain,
    select(q38,tail) = 'index$u192',
    inference(superposition,[status(thm)],[d301,c0]) ).

cnf(d303,plain,
    'index$u195' = 'index$u192',
    inference(demodulation,[status(thm)],[d302,c146]) ).

cnf(d304,plain,
    s('index$u192') = p('index$u189'),
    inference(superposition,[status(thm)],[c145,d26]) ).

cnf(d305,plain,
    s('index$u195') = p('index$u189'),
    inference(demodulation,[status(thm)],[d304,d303]) ).

cnf(d306,plain,
    'index$u207' = p('index$u189'),
    inference(demodulation,[status(thm)],[d305,d300]) ).

cnf(d307,plain,
    'index$u207' = 'index$u105',
    inference(demodulation,[status(thm)],[d306,d294]) ).

cnf(d308,plain,
    q40 = store('queue$u209',tail,'index$u210'),
    inference(demodulation,[status(thm)],[c255,c347]) ).

cnf(d309,plain,
    select(q40,tail) = 'index$u210',
    inference(superposition,[status(thm)],[d308,c0]) ).

cnf(d310,plain,
    'index$u213' = 'index$u210',
    inference(demodulation,[status(thm)],[d309,c153]) ).

cnf(d311,plain,
    p('index$u210') = 'index$u207',
    inference(superposition,[status(thm)],[c152,c5]) ).

cnf(d312,plain,
    p('index$u213') = 'index$u207',
    inference(demodulation,[status(thm)],[d311,d310]) ).

cnf(d313,plain,
    p('index$u213') = 'index$u105',
    inference(demodulation,[status(thm)],[d312,d307]) ).

cnf(d314,plain,
    q42 = store('queue$u221',tail,'index$u222'),
    inference(demodulation,[status(thm)],[c259,c349]) ).

cnf(d315,plain,
    select(q42,tail) = 'index$u222',
    inference(superposition,[status(thm)],[d314,c0]) ).

cnf(d316,plain,
    'index$u225' = 'index$u222',
    inference(demodulation,[status(thm)],[d315,c157]) ).

cnf(d317,plain,
    p('index$u222') = 'index$u219',
    inference(superposition,[status(thm)],[c156,c5]) ).

cnf(d318,plain,
    s('index$u219') = 'index$u222',
    inference(superposition,[status(thm)],[d317,c6]) ).

cnf(d319,plain,
    s('index$u219') = 'index$u225',
    inference(demodulation,[status(thm)],[d318,d316]) ).

cnf(d320,plain,
    q41 = store('queue$u215',tail,'index$u216'),
    inference(demodulation,[status(thm)],[c257,c348]) ).

cnf(d321,plain,
    select(q41,tail) = 'index$u216',
    inference(superposition,[status(thm)],[d320,c0]) ).

cnf(d322,plain,
    'index$u219' = 'index$u216',
    inference(demodulation,[status(thm)],[d321,c155]) ).

cnf(d323,plain,
    s('index$u216') = p('index$u213'),
    inference(superposition,[status(thm)],[c154,d26]) ).

cnf(d324,plain,
    s('index$u219') = p('index$u213'),
    inference(demodulation,[status(thm)],[d323,d322]) ).

cnf(d325,plain,
    'index$u225' = p('index$u213'),
    inference(demodulation,[status(thm)],[d324,d319]) ).

cnf(d326,plain,
    'index$u225' = 'index$u105',
    inference(demodulation,[status(thm)],[d325,d313]) ).

cnf(d327,plain,
    q43 = store('queue$u227',tail,'index$u228'),
    inference(demodulation,[status(thm)],[c261,c350]) ).

cnf(d328,plain,
    select(q43,tail) = 'index$u228',
    inference(superposition,[status(thm)],[d327,c0]) ).

cnf(d329,plain,
    'index$u231' = 'index$u228',
    inference(demodulation,[status(thm)],[d328,c159]) ).

cnf(d330,plain,
    'index$u231' = s('index$u225'),
    inference(demodulation,[status(thm)],[c158,d329]) ).

cnf(d331,plain,
    'index$u231' = s('index$u105'),
    inference(demodulation,[status(thm)],[d330,d326]) ).

cnf(d332,plain,
    'index$u231' = 'index$u111',
    inference(demodulation,[status(thm)],[d331,d219]) ).

cnf(d333,plain,
    q44 = store('queue$u233',tail,'index$u234'),
    inference(demodulation,[status(thm)],[c264,c351]) ).

cnf(d334,plain,
    select(q44,tail) = 'index$u234',
    inference(superposition,[status(thm)],[d333,c0]) ).

cnf(d335,plain,
    'index$u237' = 'index$u234',
    inference(demodulation,[status(thm)],[d334,c161]) ).

cnf(d336,plain,
    p('index$u234') = 'index$u231',
    inference(superposition,[status(thm)],[c160,c5]) ).

cnf(d337,plain,
    p('index$u237') = 'index$u231',
    inference(demodulation,[status(thm)],[d336,d335]) ).

cnf(d338,plain,
    p('index$u237') = 'index$u111',
    inference(demodulation,[status(thm)],[d337,d332]) ).

cnf(d339,plain,
    q46 = store('queue$u245',tail,'index$u246'),
    inference(demodulation,[status(thm)],[c268,c353]) ).

cnf(d340,plain,
    select(q46,tail) = 'index$u246',
    inference(superposition,[status(thm)],[d339,c0]) ).

cnf(d341,plain,
    'index$u249' = 'index$u246',
    inference(demodulation,[status(thm)],[d340,c166]) ).

cnf(d342,plain,
    p('index$u246') = 'index$u243',
    inference(superposition,[status(thm)],[c165,c5]) ).

cnf(d343,plain,
    s('index$u243') = 'index$u246',
    inference(superposition,[status(thm)],[d342,c6]) ).

cnf(d344,plain,
    s('index$u243') = 'index$u249',
    inference(demodulation,[status(thm)],[d343,d341]) ).

cnf(d345,plain,
    q45 = store('queue$u239',tail,'index$u240'),
    inference(demodulation,[status(thm)],[c266,c352]) ).

cnf(d346,plain,
    select(q45,tail) = 'index$u240',
    inference(superposition,[status(thm)],[d345,c0]) ).

cnf(d347,plain,
    'index$u243' = 'index$u240',
    inference(demodulation,[status(thm)],[d346,c164]) ).

cnf(d348,plain,
    s('index$u240') = p('index$u237'),
    inference(superposition,[status(thm)],[c163,d26]) ).

cnf(d349,plain,
    s('index$u243') = p('index$u237'),
    inference(demodulation,[status(thm)],[d348,d347]) ).

cnf(d350,plain,
    'index$u249' = p('index$u237'),
    inference(demodulation,[status(thm)],[d349,d344]) ).

cnf(d351,plain,
    'index$u249' = 'index$u111',
    inference(demodulation,[status(thm)],[d350,d338]) ).

cnf(d352,plain,
    q47 = store('queue$u251',tail,'index$u252'),
    inference(demodulation,[status(thm)],[c271,c354]) ).

cnf(d353,plain,
    select(q47,tail) = 'index$u252',
    inference(superposition,[status(thm)],[d352,c0]) ).

cnf(d354,plain,
    'index$u255' = 'index$u252',
    inference(demodulation,[status(thm)],[d353,c168]) ).

cnf(d355,plain,
    p('index$u252') = 'index$u249',
    inference(superposition,[status(thm)],[c167,c5]) ).

cnf(d356,plain,
    p('index$u255') = 'index$u249',
    inference(demodulation,[status(thm)],[d355,d354]) ).

cnf(d357,plain,
    p('index$u255') = 'index$u111',
    inference(demodulation,[status(thm)],[d356,d351]) ).

cnf(d358,plain,
    q48 = store('queue$u257',tail,'index$u258'),
    inference(demodulation,[status(thm)],[c273,c355]) ).

cnf(d359,plain,
    select(q48,tail) = 'index$u258',
    inference(superposition,[status(thm)],[d358,c0]) ).

cnf(d360,plain,
    'index$u261' = 'index$u258',
    inference(demodulation,[status(thm)],[d359,c170]) ).

cnf(d361,plain,
    s('index$u258') = p('index$u255'),
    inference(superposition,[status(thm)],[c169,d26]) ).

cnf(d362,plain,
    s('index$u261') = p('index$u255'),
    inference(demodulation,[status(thm)],[d361,d360]) ).

cnf(d363,plain,
    'index$u264' = p('index$u255'),
    inference(demodulation,[status(thm)],[d362,c171]) ).

cnf(d364,plain,
    'index$u264' = 'index$u111',
    inference(demodulation,[status(thm)],[d363,d357]) ).

cnf(d365,plain,
    q49 = store('queue$u263',tail,'index$u264'),
    inference(demodulation,[status(thm)],[c275,c356]) ).

cnf(d366,plain,
    select(q49,tail) = 'index$u264',
    inference(superposition,[status(thm)],[d365,c0]) ).

cnf(d367,plain,
    'index$u299' = 'index$u264',
    inference(demodulation,[status(thm)],[c184,d366]) ).

cnf(d368,plain,
    p('index$u299') = 'index$u300',
    inference(superposition,[status(thm)],[c187,c5]) ).

cnf(d369,plain,
    p('index$u264') = 'index$u300',
    inference(demodulation,[status(thm)],[d368,d367]) ).

cnf(d370,plain,
    p('index$u111') = 'index$u300',
    inference(demodulation,[status(thm)],[d369,d364]) ).

cnf(d371,plain,
    'index$u105' = 'index$u300',
    inference(demodulation,[status(thm)],[d370,d131]) ).

cnf(d372,plain,
    'elem$u301' = select('earray$u296','index$u105'),
    inference(demodulation,[status(thm)],[c110,d371]) ).

cnf(d373,plain,
    'elem$u301' = select('earray$u296','index$u9'),
    inference(demodulation,[status(thm)],[d372,d218]) ).

cnf(d374,plain,
    ( seq = X0
    | select('queue$u107',X0) = select(q24,X0) ),
    inference(superposition,[status(thm)],[c216,c1]) ).

cnf(d375,plain,
    ( tail = X0
    | select(q25,X0) = select('queue$u107',X0) ),
    inference(superposition,[status(thm)],[d112,c1]) ).

cnf(d376,plain,
    ( tail = X0
    | seq = X0
    | select(q25,X0) = select(q24,X0) ),
    inference(superposition,[status(thm)],[d375,d374]) ).

cnf(d377,plain,
    ( seq = X0
    | select('queue$u113',X0) = select(q25,X0) ),
    inference(superposition,[status(thm)],[c219,c1]) ).

cnf(d378,plain,
    ( tail = X0
    | select(q26,X0) = select('queue$u113',X0) ),
    inference(superposition,[status(thm)],[d122,c1]) ).

cnf(d379,plain,
    ( tail = X0
    | seq = X0
    | select(q26,X0) = select(q25,X0) ),
    inference(superposition,[status(thm)],[d378,d377]) ).

cnf(d380,plain,
    ( seq = X0
    | select('queue$u119',X0) = select(q26,X0) ),
    inference(superposition,[status(thm)],[c221,c1]) ).

cnf(d381,plain,
    ( tail = X0
    | select(q27,X0) = select('queue$u119',X0) ),
    inference(superposition,[status(thm)],[d220,c1]) ).

cnf(d382,plain,
    ( tail = X0
    | seq = X0
    | select(q27,X0) = select(q26,X0) ),
    inference(superposition,[status(thm)],[d381,d380]) ).

cnf(d383,plain,
    ( seq = X0
    | select('queue$u125',X0) = select(q27,X0) ),
    inference(superposition,[status(thm)],[c223,c1]) ).

cnf(d384,plain,
    ( tail = X0
    | select(q28,X0) = select('queue$u125',X0) ),
    inference(superposition,[status(thm)],[d228,c1]) ).

cnf(d385,plain,
    ( tail = X0
    | seq = X0
    | select(q28,X0) = select(q27,X0) ),
    inference(superposition,[status(thm)],[d384,d383]) ).

cnf(d386,plain,
    ( seq = X0
    | select('queue$u131',X0) = select(q28,X0) ),
    inference(superposition,[status(thm)],[c226,c1]) ).

cnf(d387,plain,
    ( tail = X0
    | select(q29,X0) = select('queue$u131',X0) ),
    inference(superposition,[status(thm)],[d236,c1]) ).

cnf(d388,plain,
    ( tail = X0
    | seq = X0
    | select(q29,X0) = select(q28,X0) ),
    inference(superposition,[status(thm)],[d387,d386]) ).

cnf(d389,plain,
    ( seq = X0
    | select('queue$u143',X0) = select(q29,X0) ),
    inference(superposition,[status(thm)],[c230,c1]) ).

cnf(d390,plain,
    ( tail = X0
    | select(q30,X0) = select('queue$u143',X0) ),
    inference(superposition,[status(thm)],[d242,c1]) ).

cnf(d391,plain,
    ( tail = X0
    | seq = X0
    | select(q30,X0) = select(q29,X0) ),
    inference(superposition,[status(thm)],[d390,d389]) ).

cnf(d392,plain,
    ( seq = X0
    | select('queue$u149',X0) = select(q30,X0) ),
    inference(superposition,[status(thm)],[c232,c1]) ).

cnf(d393,plain,
    ( tail = X0
    | select(q31,X0) = select('queue$u149',X0) ),
    inference(superposition,[status(thm)],[d250,c1]) ).

cnf(d394,plain,
    ( tail = X0
    | seq = X0
    | select(q31,X0) = select(q30,X0) ),
    inference(superposition,[status(thm)],[d393,d392]) ).

cnf(d395,plain,
    ( seq = X0
    | select('queue$u155',X0) = select(q31,X0) ),
    inference(superposition,[status(thm)],[c234,c1]) ).

cnf(d396,plain,
    ( tail = X0
    | select(q32,X0) = select('queue$u155',X0) ),
    inference(superposition,[status(thm)],[d256,c1]) ).

cnf(d397,plain,
    ( tail = X0
    | seq = X0
    | select(q32,X0) = select(q31,X0) ),
    inference(superposition,[status(thm)],[d396,d395]) ).

cnf(d398,plain,
    ( seq = X0
    | select('queue$u161',X0) = select(q32,X0) ),
    inference(superposition,[status(thm)],[c236,c1]) ).

cnf(d399,plain,
    ( tail = X0
    | select(q33,X0) = select('queue$u161',X0) ),
    inference(superposition,[status(thm)],[d270,c1]) ).

cnf(d400,plain,
    ( tail = X0
    | seq = X0
    | select(q33,X0) = select(q32,X0) ),
    inference(superposition,[status(thm)],[d399,d398]) ).

cnf(d401,plain,
    ( seq = X0
    | select('queue$u167',X0) = select(q33,X0) ),
    inference(superposition,[status(thm)],[c238,c1]) ).

cnf(d402,plain,
    ( tail = X0
    | select(q34,X0) = select('queue$u167',X0) ),
    inference(superposition,[status(thm)],[d264,c1]) ).

cnf(d403,plain,
    ( tail = X0
    | seq = X0
    | select(q34,X0) = select(q33,X0) ),
    inference(superposition,[status(thm)],[d402,d401]) ).

cnf(d404,plain,
    ( seq = X0
    | select('queue$u173',X0) = select(q34,X0) ),
    inference(superposition,[status(thm)],[c241,c1]) ).

cnf(d405,plain,
    ( tail = X0
    | select(q35,X0) = select('queue$u173',X0) ),
    inference(superposition,[status(thm)],[d277,c1]) ).

cnf(d406,plain,
    ( tail = X0
    | seq = X0
    | select(q35,X0) = select(q34,X0) ),
    inference(superposition,[status(thm)],[d405,d404]) ).

cnf(d407,plain,
    ( seq = X0
    | select('queue$u179',X0) = select(q35,X0) ),
    inference(superposition,[status(thm)],[c243,c1]) ).

cnf(d408,plain,
    ( tail = X0
    | select(q36,X0) = select('queue$u179',X0) ),
    inference(superposition,[status(thm)],[d283,c1]) ).

cnf(d409,plain,
    ( tail = X0
    | seq = X0
    | select(q36,X0) = select(q35,X0) ),
    inference(superposition,[status(thm)],[d408,d407]) ).

cnf(d410,plain,
    ( seq = X0
    | select('queue$u185',X0) = select(q36,X0) ),
    inference(superposition,[status(thm)],[c245,c1]) ).

cnf(d411,plain,
    ( tail = X0
    | select(q37,X0) = select('queue$u185',X0) ),
    inference(superposition,[status(thm)],[d289,c1]) ).

cnf(d412,plain,
    ( tail = X0
    | seq = X0
    | select(q37,X0) = select(q36,X0) ),
    inference(superposition,[status(thm)],[d411,d410]) ).

cnf(d413,plain,
    ( seq = X0
    | select('queue$u191',X0) = select(q37,X0) ),
    inference(superposition,[status(thm)],[c248,c1]) ).

cnf(d414,plain,
    ( tail = X0
    | select(q38,X0) = select('queue$u191',X0) ),
    inference(superposition,[status(thm)],[d301,c1]) ).

cnf(d415,plain,
    ( tail = X0
    | seq = X0
    | select(q38,X0) = select(q37,X0) ),
    inference(superposition,[status(thm)],[d414,d413]) ).

cnf(d416,plain,
    ( seq = X0
    | select('queue$u197',X0) = select(q38,X0) ),
    inference(superposition,[status(thm)],[c250,c1]) ).

cnf(d417,plain,
    ( tail = X0
    | select(q39,X0) = select('queue$u197',X0) ),
    inference(superposition,[status(thm)],[d295,c1]) ).

cnf(d418,plain,
    ( tail = X0
    | seq = X0
    | select(q39,X0) = select(q38,X0) ),
    inference(superposition,[status(thm)],[d417,d416]) ).

cnf(d419,plain,
    ( seq = X0
    | select('queue$u209',X0) = select(q39,X0) ),
    inference(superposition,[status(thm)],[c254,c1]) ).

cnf(d420,plain,
    ( tail = X0
    | select(q40,X0) = select('queue$u209',X0) ),
    inference(superposition,[status(thm)],[d308,c1]) ).

cnf(d421,plain,
    ( tail = X0
    | seq = X0
    | select(q40,X0) = select(q39,X0) ),
    inference(superposition,[status(thm)],[d420,d419]) ).

cnf(d422,plain,
    ( seq = X0
    | select('queue$u215',X0) = select(q40,X0) ),
    inference(superposition,[status(thm)],[c256,c1]) ).

cnf(d423,plain,
    ( tail = X0
    | select(q41,X0) = select('queue$u215',X0) ),
    inference(superposition,[status(thm)],[d320,c1]) ).

cnf(d424,plain,
    ( tail = X0
    | seq = X0
    | select(q41,X0) = select(q40,X0) ),
    inference(superposition,[status(thm)],[d423,d422]) ).

cnf(d425,plain,
    ( seq = X0
    | select('queue$u221',X0) = select(q41,X0) ),
    inference(superposition,[status(thm)],[c258,c1]) ).

cnf(d426,plain,
    ( tail = X0
    | select(q42,X0) = select('queue$u221',X0) ),
    inference(superposition,[status(thm)],[d314,c1]) ).

cnf(d427,plain,
    ( tail = X0
    | seq = X0
    | select(q42,X0) = select(q41,X0) ),
    inference(superposition,[status(thm)],[d426,d425]) ).

cnf(d428,plain,
    ( seq = X0
    | select('queue$u227',X0) = select(q42,X0) ),
    inference(superposition,[status(thm)],[c260,c1]) ).

cnf(d429,plain,
    ( tail = X0
    | select(q43,X0) = select('queue$u227',X0) ),
    inference(superposition,[status(thm)],[d327,c1]) ).

cnf(d430,plain,
    ( tail = X0
    | seq = X0
    | select(q43,X0) = select(q42,X0) ),
    inference(superposition,[status(thm)],[d429,d428]) ).

cnf(d431,plain,
    ( seq = X0
    | select('queue$u233',X0) = select(q43,X0) ),
    inference(superposition,[status(thm)],[c263,c1]) ).

cnf(d432,plain,
    ( tail = X0
    | select(q44,X0) = select('queue$u233',X0) ),
    inference(superposition,[status(thm)],[d333,c1]) ).

cnf(d433,plain,
    ( tail = X0
    | seq = X0
    | select(q44,X0) = select(q43,X0) ),
    inference(superposition,[status(thm)],[d432,d431]) ).

cnf(d434,plain,
    ( seq = X0
    | select('queue$u239',X0) = select(q44,X0) ),
    inference(superposition,[status(thm)],[c265,c1]) ).

cnf(d435,plain,
    ( tail = X0
    | select(q45,X0) = select('queue$u239',X0) ),
    inference(superposition,[status(thm)],[d345,c1]) ).

cnf(d436,plain,
    ( tail = X0
    | seq = X0
    | select(q45,X0) = select(q44,X0) ),
    inference(superposition,[status(thm)],[d435,d434]) ).

cnf(d437,plain,
    ( seq = X0
    | select('queue$u245',X0) = select(q45,X0) ),
    inference(superposition,[status(thm)],[c267,c1]) ).

cnf(d438,plain,
    ( tail = X0
    | select(q46,X0) = select('queue$u245',X0) ),
    inference(superposition,[status(thm)],[d339,c1]) ).

cnf(d439,plain,
    ( tail = X0
    | seq = X0
    | select(q46,X0) = select(q45,X0) ),
    inference(superposition,[status(thm)],[d438,d437]) ).

cnf(d440,plain,
    ( seq = X0
    | select('queue$u251',X0) = select(q46,X0) ),
    inference(superposition,[status(thm)],[c270,c1]) ).

cnf(d441,plain,
    ( tail = X0
    | select(q47,X0) = select('queue$u251',X0) ),
    inference(superposition,[status(thm)],[d352,c1]) ).

cnf(d442,plain,
    ( tail = X0
    | seq = X0
    | select(q47,X0) = select(q46,X0) ),
    inference(superposition,[status(thm)],[d441,d440]) ).

cnf(d443,plain,
    ( seq = X0
    | select('queue$u257',X0) = select(q47,X0) ),
    inference(superposition,[status(thm)],[c272,c1]) ).

cnf(d444,plain,
    ( tail = X0
    | select(q48,X0) = select('queue$u257',X0) ),
    inference(superposition,[status(thm)],[d358,c1]) ).

cnf(d445,plain,
    ( tail = X0
    | seq = X0
    | select(q48,X0) = select(q47,X0) ),
    inference(superposition,[status(thm)],[d444,d443]) ).

cnf(d446,plain,
    ( seq = X0
    | select('queue$u263',X0) = select(q48,X0) ),
    inference(superposition,[status(thm)],[c274,c1]) ).

cnf(d447,plain,
    ( tail = X0
    | select(q49,X0) = select('queue$u263',X0) ),
    inference(superposition,[status(thm)],[d365,c1]) ).

cnf(d448,plain,
    ( tail = X0
    | seq = X0
    | select(q49,X0) = select(q48,X0) ),
    inference(superposition,[status(thm)],[d447,d446]) ).

cnf(d449,plain,
    ( seq = head
    | tail = head
    | 'index$u297' = select(q48,head) ),
    inference(superposition,[status(thm)],[d448,c183]) ).

cnf(d450,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q47,head) ),
    inference(superposition,[status(thm)],[d449,d445]) ).

cnf(d451,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q46,head) ),
    inference(superposition,[status(thm)],[d450,d442]) ).

cnf(d452,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q45,head) ),
    inference(superposition,[status(thm)],[d451,d439]) ).

cnf(d453,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q44,head) ),
    inference(superposition,[status(thm)],[d452,d436]) ).

cnf(d454,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q43,head) ),
    inference(superposition,[status(thm)],[d453,d433]) ).

cnf(d455,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q42,head) ),
    inference(superposition,[status(thm)],[d454,d430]) ).

cnf(d456,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q41,head) ),
    inference(superposition,[status(thm)],[d455,d427]) ).

cnf(d457,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q40,head) ),
    inference(superposition,[status(thm)],[d456,d424]) ).

cnf(d458,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q39,head) ),
    inference(superposition,[status(thm)],[d457,d421]) ).

cnf(d459,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q38,head) ),
    inference(superposition,[status(thm)],[d458,d418]) ).

cnf(d460,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q37,head) ),
    inference(superposition,[status(thm)],[d459,d415]) ).

cnf(d461,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q36,head) ),
    inference(superposition,[status(thm)],[d460,d412]) ).

cnf(d462,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q35,head) ),
    inference(superposition,[status(thm)],[d461,d409]) ).

cnf(d463,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q34,head) ),
    inference(superposition,[status(thm)],[d462,d406]) ).

cnf(d464,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q33,head) ),
    inference(superposition,[status(thm)],[d463,d403]) ).

cnf(d465,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q32,head) ),
    inference(superposition,[status(thm)],[d464,d400]) ).

cnf(d466,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q31,head) ),
    inference(superposition,[status(thm)],[d465,d397]) ).

cnf(d467,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q30,head) ),
    inference(superposition,[status(thm)],[d466,d394]) ).

cnf(d468,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q29,head) ),
    inference(superposition,[status(thm)],[d467,d391]) ).

cnf(d469,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q28,head) ),
    inference(superposition,[status(thm)],[d468,d388]) ).

cnf(d470,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q27,head) ),
    inference(superposition,[status(thm)],[d469,d385]) ).

cnf(d471,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q26,head) ),
    inference(superposition,[status(thm)],[d470,d382]) ).

cnf(d472,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q25,head) ),
    inference(superposition,[status(thm)],[d471,d379]) ).

cnf(d473,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = select(q24,head) ),
    inference(superposition,[status(thm)],[d472,d376]) ).

cnf(d474,plain,
    p('index$u135') = s('index$u138'),
    inference(superposition,[status(thm)],[c125,d7]) ).

cnf(d475,plain,
    p('index$u135') = s('index$u201'),
    inference(demodulation,[status(thm)],[d474,d2]) ).

cnf(d476,plain,
    p('index$u135') = 'index$u267',
    inference(demodulation,[status(thm)],[d475,d13]) ).

cnf(d477,plain,
    p('index$u21') = s('index$u27'),
    inference(superposition,[status(thm)],[d60,d7]) ).

cnf(d478,plain,
    p('index$u135') = s('index$u27'),
    inference(demodulation,[status(thm)],[d477,d73]) ).

cnf(d479,plain,
    'index$u267' = s('index$u27'),
    inference(demodulation,[status(thm)],[d478,d476]) ).

cnf(d480,plain,
    'index$u267' = s('index$u9'),
    inference(demodulation,[status(thm)],[d479,d67]) ).

cnf(d481,plain,
    'index$u267' = 'index$u15',
    inference(demodulation,[status(thm)],[d480,d84]) ).

cnf(d482,plain,
    q2 = store('queue$u71',tail,'index$u72'),
    inference(demodulation,[status(thm)],[c303,c324]) ).

cnf(d483,plain,
    select(q2,tail) = 'index$u72',
    inference(superposition,[status(thm)],[d482,c0]) ).

cnf(d484,plain,
    'index$u135' = 'index$u72',
    inference(demodulation,[status(thm)],[d483,c124]) ).

cnf(d485,plain,
    p('index$u72') = 'index$u69',
    inference(superposition,[status(thm)],[c202,c5]) ).

cnf(d486,plain,
    p('index$u135') = 'index$u69',
    inference(demodulation,[status(thm)],[d485,d484]) ).

cnf(d487,plain,
    'index$u267' = 'index$u69',
    inference(demodulation,[status(thm)],[d486,d476]) ).

cnf(d488,plain,
    'index$u15' = 'index$u69',
    inference(demodulation,[status(thm)],[d487,d481]) ).

cnf(d489,plain,
    q1 = store('queue$u5',tail,'index$u6'),
    inference(demodulation,[status(thm)],[c301,c313]) ).

cnf(d490,plain,
    select(q1,tail) = 'index$u6',
    inference(superposition,[status(thm)],[d489,c0]) ).

cnf(d491,plain,
    'index$u69' = 'index$u6',
    inference(demodulation,[status(thm)],[d490,c201]) ).

cnf(d492,plain,
    p('index$u3') = s('index$u6'),
    inference(superposition,[status(thm)],[c197,d7]) ).

cnf(d493,plain,
    p('index$u3') = s('index$u69'),
    inference(demodulation,[status(thm)],[d492,d491]) ).

cnf(d494,plain,
    'index$u3' = s(s('index$u69')),
    inference(superposition,[status(thm)],[d493,d139]) ).

cnf(d495,plain,
    'index$u3' = p('index$u69'),
    inference(demodulation,[status(thm)],[d494,d7]) ).

cnf(d496,plain,
    'index$u3' = p('index$u15'),
    inference(demodulation,[status(thm)],[d495,d488]) ).

cnf(d497,plain,
    'index$u3' = 'index$u9',
    inference(demodulation,[status(thm)],[d496,d54]) ).

cnf(d498,plain,
    q0 = store(q,head,'index$u0'),
    inference(demodulation,[status(thm)],[c213,c312]) ).

cnf(d499,plain,
    ( head = X0
    | select(q0,X0) = select(q,X0) ),
    inference(superposition,[status(thm)],[d498,c1]) ).

cnf(d500,plain,
    ( head = tail
    | 'index$u0' = select(q0,tail) ),
    inference(superposition,[status(thm)],[d499,c111]) ).

cnf(d501,plain,
    ( 'index$u0' = 'index$u3'
    | head = tail ),
    inference(demodulation,[status(thm)],[d500,c185]) ).

cnf(d502,plain,
    'index$u0' = 'index$u3',
    inference(resolution,[status(thm)],[c2,d501]) ).

cnf(d503,plain,
    select(q0,head) = 'index$u0',
    inference(superposition,[status(thm)],[d498,c0]) ).

cnf(d504,plain,
    select(q0,head) = 'index$u3',
    inference(demodulation,[status(thm)],[d503,d502]) ).

cnf(d505,plain,
    select(q0,head) = 'index$u9',
    inference(demodulation,[status(thm)],[d504,d497]) ).

cnf(d506,plain,
    ( seq = X0
    | select('queue$u5',X0) = select(q0,X0) ),
    inference(superposition,[status(thm)],[c294,c1]) ).

cnf(d507,plain,
    ( tail = X0
    | select(q1,X0) = select('queue$u5',X0) ),
    inference(superposition,[status(thm)],[d489,c1]) ).

cnf(d508,plain,
    ( tail = X0
    | seq = X0
    | select(q1,X0) = select(q0,X0) ),
    inference(superposition,[status(thm)],[d507,d506]) ).

cnf(d509,plain,
    ( seq = X0
    | select('queue$u71',X0) = select(q1,X0) ),
    inference(superposition,[status(thm)],[c302,c1]) ).

cnf(d510,plain,
    ( tail = X0
    | select(q2,X0) = select('queue$u71',X0) ),
    inference(superposition,[status(thm)],[d482,c1]) ).

cnf(d511,plain,
    ( tail = X0
    | seq = X0
    | select(q2,X0) = select(q1,X0) ),
    inference(superposition,[status(thm)],[d510,d509]) ).

cnf(d512,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q2,X0) = select(q0,X0) ),
    inference(superposition,[status(thm)],[d511,d508]) ).

cnf(d513,plain,
    ( seq = head
    | tail = head
    | select(q2,head) = 'index$u9' ),
    inference(superposition,[status(thm)],[d512,d505]) ).

cnf(d514,plain,
    ( seq = X0
    | select('queue$u137',X0) = select(q2,X0) ),
    inference(superposition,[status(thm)],[c228,c1]) ).

cnf(d515,plain,
    ( tail = X0
    | select(q3,X0) = select('queue$u137',X0) ),
    inference(superposition,[status(thm)],[d0,c1]) ).

cnf(d516,plain,
    ( tail = X0
    | seq = X0
    | select(q3,X0) = select(q2,X0) ),
    inference(superposition,[status(thm)],[d515,d514]) ).

cnf(d517,plain,
    ( seq = X0
    | select('queue$u203',X0) = select(q3,X0) ),
    inference(superposition,[status(thm)],[c252,c1]) ).

cnf(d518,plain,
    ( tail = X0
    | select(q4,X0) = select('queue$u203',X0) ),
    inference(superposition,[status(thm)],[d8,c1]) ).

cnf(d519,plain,
    ( tail = X0
    | seq = X0
    | select(q4,X0) = select(q3,X0) ),
    inference(superposition,[status(thm)],[d518,d517]) ).

cnf(d520,plain,
    ( seq = X0
    | select('queue$u269',X0) = select(q4,X0) ),
    inference(superposition,[status(thm)],[c276,c1]) ).

cnf(d521,plain,
    ( tail = X0
    | select(q5,X0) = select('queue$u269',X0) ),
    inference(superposition,[status(thm)],[d23,c1]) ).

cnf(d522,plain,
    ( tail = X0
    | seq = X0
    | select(q5,X0) = select(q4,X0) ),
    inference(superposition,[status(thm)],[d521,d520]) ).

cnf(d523,plain,
    ( seq = X0
    | select('queue$u275',X0) = select(q5,X0) ),
    inference(superposition,[status(thm)],[c278,c1]) ).

cnf(d524,plain,
    ( tail = X0
    | select(q6,X0) = select('queue$u275',X0) ),
    inference(superposition,[status(thm)],[d17,c1]) ).

cnf(d525,plain,
    ( tail = X0
    | seq = X0
    | select(q6,X0) = select(q5,X0) ),
    inference(superposition,[status(thm)],[d524,d523]) ).

cnf(d526,plain,
    ( seq = X0
    | select('queue$u281',X0) = select(q6,X0) ),
    inference(superposition,[status(thm)],[c280,c1]) ).

cnf(d527,plain,
    ( tail = X0
    | select(q7,X0) = select('queue$u281',X0) ),
    inference(superposition,[status(thm)],[d31,c1]) ).

cnf(d528,plain,
    ( tail = X0
    | seq = X0
    | select(q7,X0) = select(q6,X0) ),
    inference(superposition,[status(thm)],[d527,d526]) ).

cnf(d529,plain,
    ( seq = X0
    | select('queue$u287',X0) = select(q7,X0) ),
    inference(superposition,[status(thm)],[c282,c1]) ).

cnf(d530,plain,
    ( tail = X0
    | select(q8,X0) = select('queue$u287',X0) ),
    inference(superposition,[status(thm)],[d37,c1]) ).

cnf(d531,plain,
    ( tail = X0
    | seq = X0
    | select(q8,X0) = select(q7,X0) ),
    inference(superposition,[status(thm)],[d530,d529]) ).

cnf(d532,plain,
    ( seq = X0
    | select('queue$u11',X0) = select(q9,X0) ),
    inference(superposition,[status(thm)],[c218,c1]) ).

cnf(d533,plain,
    ( tail = X0
    | select(q10,X0) = select('queue$u11',X0) ),
    inference(superposition,[status(thm)],[d48,c1]) ).

cnf(d534,plain,
    ( tail = X0
    | seq = X0
    | select(q10,X0) = select(q9,X0) ),
    inference(superposition,[status(thm)],[d533,d532]) ).

cnf(d535,plain,
    ( seq = X0
    | select('queue$u293',X0) = select(q8,X0) ),
    inference(superposition,[status(thm)],[c285,c1]) ).

cnf(d536,plain,
    ( tail = X0
    | select(q9,X0) = select('queue$u293',X0) ),
    inference(superposition,[status(thm)],[d43,c1]) ).

cnf(d537,plain,
    ( tail = X0
    | seq = X0
    | select(q9,X0) = select(q8,X0) ),
    inference(superposition,[status(thm)],[d536,d535]) ).

cnf(d538,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q10,X0) = select(q8,X0) ),
    inference(superposition,[status(thm)],[d537,d534]) ).

cnf(d539,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q10,X0) = select(q7,X0) ),
    inference(superposition,[status(thm)],[d538,d531]) ).

cnf(d540,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q10,X0) = select(q6,X0) ),
    inference(superposition,[status(thm)],[d539,d528]) ).

cnf(d541,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q10,X0) = select(q5,X0) ),
    inference(superposition,[status(thm)],[d540,d525]) ).

cnf(d542,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q10,X0) = select(q4,X0) ),
    inference(superposition,[status(thm)],[d541,d522]) ).

cnf(d543,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q10,X0) = select(q3,X0) ),
    inference(superposition,[status(thm)],[d542,d519]) ).

cnf(d544,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q10,X0) = select(q2,X0) ),
    inference(superposition,[status(thm)],[d543,d516]) ).

cnf(d545,plain,
    ( seq = X0
    | select('queue$u17',X0) = select(q10,X0) ),
    inference(superposition,[status(thm)],[c240,c1]) ).

cnf(d546,plain,
    ( tail = X0
    | select(q11,X0) = select('queue$u17',X0) ),
    inference(superposition,[status(thm)],[d61,c1]) ).

cnf(d547,plain,
    ( tail = X0
    | seq = X0
    | select(q11,X0) = select(q10,X0) ),
    inference(superposition,[status(thm)],[d546,d545]) ).

cnf(d548,plain,
    ( seq = X0
    | select('queue$u23',X0) = select(q11,X0) ),
    inference(superposition,[status(thm)],[c262,c1]) ).

cnf(d549,plain,
    ( tail = X0
    | select(q12,X0) = select('queue$u23',X0) ),
    inference(superposition,[status(thm)],[d55,c1]) ).

cnf(d550,plain,
    ( tail = X0
    | seq = X0
    | select(q12,X0) = select(q11,X0) ),
    inference(superposition,[status(thm)],[d549,d548]) ).

cnf(d551,plain,
    ( seq = X0
    | select('queue$u29',X0) = select(q12,X0) ),
    inference(superposition,[status(thm)],[c284,c1]) ).

cnf(d552,plain,
    ( tail = X0
    | select(q13,X0) = select('queue$u29',X0) ),
    inference(superposition,[status(thm)],[d85,c1]) ).

cnf(d553,plain,
    ( tail = X0
    | seq = X0
    | select(q13,X0) = select(q12,X0) ),
    inference(superposition,[status(thm)],[d552,d551]) ).

cnf(d554,plain,
    ( seq = X0
    | select('queue$u35',X0) = select(q13,X0) ),
    inference(superposition,[status(thm)],[c288,c1]) ).

cnf(d555,plain,
    ( tail = X0
    | select(q14,X0) = select('queue$u35',X0) ),
    inference(superposition,[status(thm)],[d91,c1]) ).

cnf(d556,plain,
    ( tail = X0
    | seq = X0
    | select(q14,X0) = select(q13,X0) ),
    inference(superposition,[status(thm)],[d555,d554]) ).

cnf(d557,plain,
    ( seq = X0
    | select('queue$u41',X0) = select(q14,X0) ),
    inference(superposition,[status(thm)],[c290,c1]) ).

cnf(d558,plain,
    ( tail = X0
    | select(q15,X0) = select('queue$u41',X0) ),
    inference(superposition,[status(thm)],[d97,c1]) ).

cnf(d559,plain,
    ( tail = X0
    | seq = X0
    | select(q15,X0) = select(q14,X0) ),
    inference(superposition,[status(thm)],[d558,d557]) ).

cnf(d560,plain,
    ( seq = X0
    | select('queue$u47',X0) = select(q15,X0) ),
    inference(superposition,[status(thm)],[c292,c1]) ).

cnf(d561,plain,
    ( tail = X0
    | select(q16,X0) = select('queue$u47',X0) ),
    inference(superposition,[status(thm)],[d158,c1]) ).

cnf(d562,plain,
    ( tail = X0
    | seq = X0
    | select(q16,X0) = select(q15,X0) ),
    inference(superposition,[status(thm)],[d561,d560]) ).

cnf(d563,plain,
    ( seq = X0
    | select('queue$u53',X0) = select(q16,X0) ),
    inference(superposition,[status(thm)],[c295,c1]) ).

cnf(d564,plain,
    ( tail = X0
    | select(q17,X0) = select('queue$u53',X0) ),
    inference(superposition,[status(thm)],[d167,c1]) ).

cnf(d565,plain,
    ( tail = X0
    | seq = X0
    | select(q17,X0) = select(q16,X0) ),
    inference(superposition,[status(thm)],[d564,d563]) ).

cnf(d566,plain,
    ( seq = X0
    | select('queue$u59',X0) = select(q17,X0) ),
    inference(superposition,[status(thm)],[c297,c1]) ).

cnf(d567,plain,
    ( tail = X0
    | select(q18,X0) = select('queue$u59',X0) ),
    inference(superposition,[status(thm)],[d176,c1]) ).

cnf(d568,plain,
    ( tail = X0
    | seq = X0
    | select(q18,X0) = select(q17,X0) ),
    inference(superposition,[status(thm)],[d567,d566]) ).

cnf(d569,plain,
    ( seq = X0
    | select('queue$u65',X0) = select(q18,X0) ),
    inference(superposition,[status(thm)],[c299,c1]) ).

cnf(d570,plain,
    ( tail = X0
    | select(q19,X0) = select('queue$u65',X0) ),
    inference(superposition,[status(thm)],[d185,c1]) ).

cnf(d571,plain,
    ( tail = X0
    | seq = X0
    | select(q19,X0) = select(q18,X0) ),
    inference(superposition,[status(thm)],[d570,d569]) ).

cnf(d572,plain,
    ( seq = X0
    | select('queue$u77',X0) = select(q19,X0) ),
    inference(superposition,[status(thm)],[c304,c1]) ).

cnf(d573,plain,
    ( tail = X0
    | select(q20,X0) = select('queue$u77',X0) ),
    inference(superposition,[status(thm)],[d194,c1]) ).

cnf(d574,plain,
    ( tail = X0
    | seq = X0
    | select(q20,X0) = select(q19,X0) ),
    inference(superposition,[status(thm)],[d573,d572]) ).

cnf(d575,plain,
    ( seq = X0
    | select('queue$u83',X0) = select(q20,X0) ),
    inference(superposition,[status(thm)],[c306,c1]) ).

cnf(d576,plain,
    ( tail = X0
    | select(q21,X0) = select('queue$u83',X0) ),
    inference(superposition,[status(thm)],[d149,c1]) ).

cnf(d577,plain,
    ( tail = X0
    | seq = X0
    | select(q21,X0) = select(q20,X0) ),
    inference(superposition,[status(thm)],[d576,d575]) ).

cnf(d578,plain,
    ( seq = X0
    | select('queue$u89',X0) = select(q21,X0) ),
    inference(superposition,[status(thm)],[c308,c1]) ).

cnf(d579,plain,
    ( tail = X0
    | select(q22,X0) = select('queue$u89',X0) ),
    inference(superposition,[status(thm)],[d140,c1]) ).

cnf(d580,plain,
    ( tail = X0
    | seq = X0
    | select(q22,X0) = select(q21,X0) ),
    inference(superposition,[status(thm)],[d579,d578]) ).

cnf(d581,plain,
    ( seq = X0
    | select('queue$u101',X0) = select(q23,X0) ),
    inference(superposition,[status(thm)],[c214,c1]) ).

cnf(d582,plain,
    ( tail = X0
    | select(q24,X0) = select('queue$u101',X0) ),
    inference(superposition,[status(thm)],[d106,c1]) ).

cnf(d583,plain,
    ( tail = X0
    | seq = X0
    | select(q24,X0) = select(q23,X0) ),
    inference(superposition,[status(thm)],[d582,d581]) ).

cnf(d584,plain,
    ( seq = X0
    | select('queue$u95',X0) = select(q22,X0) ),
    inference(superposition,[status(thm)],[c310,c1]) ).

cnf(d585,plain,
    ( tail = X0
    | select(q23,X0) = select('queue$u95',X0) ),
    inference(superposition,[status(thm)],[d132,c1]) ).

cnf(d586,plain,
    ( tail = X0
    | seq = X0
    | select(q23,X0) = select(q22,X0) ),
    inference(superposition,[status(thm)],[d585,d584]) ).

cnf(d587,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q22,X0) ),
    inference(superposition,[status(thm)],[d586,d583]) ).

cnf(d588,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q21,X0) ),
    inference(superposition,[status(thm)],[d587,d580]) ).

cnf(d589,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q20,X0) ),
    inference(superposition,[status(thm)],[d588,d577]) ).

cnf(d590,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q19,X0) ),
    inference(superposition,[status(thm)],[d589,d574]) ).

cnf(d591,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q18,X0) ),
    inference(superposition,[status(thm)],[d590,d571]) ).

cnf(d592,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q17,X0) ),
    inference(superposition,[status(thm)],[d591,d568]) ).

cnf(d593,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q16,X0) ),
    inference(superposition,[status(thm)],[d592,d565]) ).

cnf(d594,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q15,X0) ),
    inference(superposition,[status(thm)],[d593,d562]) ).

cnf(d595,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q14,X0) ),
    inference(superposition,[status(thm)],[d594,d559]) ).

cnf(d596,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q13,X0) ),
    inference(superposition,[status(thm)],[d595,d556]) ).

cnf(d597,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q12,X0) ),
    inference(superposition,[status(thm)],[d596,d553]) ).

cnf(d598,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q11,X0) ),
    inference(superposition,[status(thm)],[d597,d550]) ).

cnf(d599,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q10,X0) ),
    inference(superposition,[status(thm)],[d598,d547]) ).

cnf(d600,plain,
    ( seq = X0
    | tail = X0
    | seq = X0
    | tail = X0
    | select(q24,X0) = select(q2,X0) ),
    inference(superposition,[status(thm)],[d599,d544]) ).

cnf(d601,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | select(q24,head) = 'index$u9' ),
    inference(superposition,[status(thm)],[d600,d513]) ).

cnf(d602,plain,
    ( seq = head
    | tail = head
    | seq = head
    | tail = head
    | 'index$u297' = 'index$u9' ),
    inference(superposition,[status(thm)],[d601,d473]) ).

cnf(d603,plain,
    ( seq = head
    | tail = head
    | 'elem$u298' = select('earray$u296','index$u9') ),
    inference(superposition,[status(thm)],[d602,c109]) ).

cnf(d604,plain,
    ( 'elem$u298' = 'elem$u301'
    | seq = head
    | tail = head ),
    inference(demodulation,[status(thm)],[d603,d373]) ).

cnf(d605,plain,
    ( seq = head
    | tail = head ),
    inference(resolution,[status(thm)],[c362,d604]) ).

cnf(d606,plain,
    ( tail = head
    | seq != seq ),
    inference(superposition,[status(thm)],[d605,c3]) ).

cnf(d607,plain,
    tail = head,
    inference(equality_resolution,[status(thm)],[d606]) ).

cnf(d608,plain,
    tail != tail,
    inference(demodulation,[status(thm)],[c2,d607]) ).

cnf(d609,plain,
    $false,
    inference(equality_resolution,[status(thm)],[d608]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWV571-1.049 : 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.08/0.36  % Computer : n001.cluster.edu
% 0.08/0.36  % Model    : x86_64 x86_64
% 0.08/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36  % Memory   : 8046.5625MB
% 0.08/0.36  % OS       : Linux 6.8.0-71-generic
% 0.08/0.36  % CPULimit : 300
% 0.08/0.36  % WCLimit  : 300
% 0.08/0.36  % DateTime : Sat Sep 26 14:37:27 UTC 2026
% 0.08/0.36  % CPUTime  : 
% 0.08/0.36  Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.98/4.69  % SZS status Unsatisfiable for theBenchmark.p
% 29.98/4.69  % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------