%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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:23 AM UTC 2026
% Result : Unsatisfiable 28.97s 4.47s
% Output : CNFRefutation 28.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 235
% Syntax : Number of clauses : 1007 (1007 unt; 0 nHn; 983 RR)
% Number of literals : 1007 (1006 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 278 ( 278 usr; 269 con; 0-2 aty)
% Number of variables : 38 ( 14 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(a1_seq,axiom,
'rselect$useq'('rstore$useq'(X0,X1)) = X1 ).
cnf(a1_head,axiom,
'rselect$uhead'('rstore$uhead'(X0,X1)) = X1 ).
cnf(a1_tail,axiom,
'rselect$utail'('rstore$utail'(X0,X1)) = X1 ).
cnf(a2_seq_tail,axiom,
'rselect$useq'('rstore$utail'(X0,X1)) = 'rselect$useq'(X0) ).
cnf(a2_head_tail,axiom,
'rselect$uhead'('rstore$utail'(X0,X1)) = 'rselect$uhead'(X0) ).
cnf(a2_head_seq,axiom,
'rselect$uhead'('rstore$useq'(X0,X1)) = 'rselect$uhead'(X0) ).
cnf(a2_tail_head,axiom,
'rselect$utail'('rstore$uhead'(X0,X1)) = 'rselect$utail'(X0) ).
cnf(ps,axiom,
p(s(X0)) = X0 ).
cnf(sp,axiom,
s(p(X0)) = X0 ).
cnf(circular,axiom,
s(s(s(X0))) = X0 ).
cnf(hyp12,hypothesis,
'earray$u134' = 'rselect$useq'(q2) ).
cnf(hyp87,hypothesis,
'elem$u262' = select('earray$u260','index$u261') ).
cnf(hyp88,hypothesis,
'elem$u265' = select('earray$u260','index$u264') ).
cnf(hyp89,hypothesis,
'index$u0' = 'rselect$utail'(q) ).
cnf(hyp90,hypothesis,
'index$u102' = s('index$u99') ).
cnf(hyp91,hypothesis,
'index$u105' = 'rselect$utail'(q24) ).
cnf(hyp92,hypothesis,
'index$u108' = s('index$u105') ).
cnf(hyp93,hypothesis,
'index$u111' = 'rselect$utail'(q25) ).
cnf(hyp94,hypothesis,
'index$u114' = s('index$u111') ).
cnf(hyp95,hypothesis,
'index$u117' = 'rselect$utail'(q26) ).
cnf(hyp96,hypothesis,
'index$u12' = s('index$u9') ).
cnf(hyp97,hypothesis,
'index$u120' = s('index$u117') ).
cnf(hyp98,hypothesis,
'index$u123' = 'rselect$utail'(q27) ).
cnf(hyp99,hypothesis,
'index$u126' = s('index$u123') ).
cnf(hyp100,hypothesis,
'index$u129' = 'rselect$utail'(q28) ).
cnf(hyp101,hypothesis,
'index$u132' = s('index$u129') ).
cnf(hyp102,hypothesis,
'index$u135' = 'rselect$utail'(q2) ).
cnf(hyp103,hypothesis,
'index$u138' = s('index$u135') ).
cnf(hyp104,hypothesis,
'index$u141' = 'rselect$utail'(q29) ).
cnf(hyp105,hypothesis,
'index$u144' = s('index$u141') ).
cnf(hyp106,hypothesis,
'index$u147' = 'rselect$utail'(q30) ).
cnf(hyp107,hypothesis,
'index$u15' = 'rselect$utail'(q10) ).
cnf(hyp108,hypothesis,
'index$u150' = s('index$u147') ).
cnf(hyp109,hypothesis,
'index$u153' = 'rselect$utail'(q31) ).
cnf(hyp110,hypothesis,
'index$u156' = s('index$u153') ).
cnf(hyp111,hypothesis,
'index$u159' = 'rselect$utail'(q32) ).
cnf(hyp112,hypothesis,
'index$u162' = s('index$u159') ).
cnf(hyp113,hypothesis,
'index$u165' = 'rselect$utail'(q33) ).
cnf(hyp114,hypothesis,
'index$u168' = s('index$u165') ).
cnf(hyp115,hypothesis,
'index$u171' = 'rselect$utail'(q34) ).
cnf(hyp116,hypothesis,
'index$u174' = s('index$u171') ).
cnf(hyp117,hypothesis,
'index$u177' = 'rselect$utail'(q35) ).
cnf(hyp118,hypothesis,
'index$u18' = s('index$u15') ).
cnf(hyp119,hypothesis,
'index$u180' = s('index$u177') ).
cnf(hyp120,hypothesis,
'index$u183' = 'rselect$utail'(q36) ).
cnf(hyp121,hypothesis,
'index$u186' = s('index$u183') ).
cnf(hyp122,hypothesis,
'index$u189' = 'rselect$utail'(q37) ).
cnf(hyp123,hypothesis,
'index$u192' = s('index$u189') ).
cnf(hyp124,hypothesis,
'index$u195' = 'rselect$utail'(q38) ).
cnf(hyp125,hypothesis,
'index$u198' = s('index$u195') ).
cnf(hyp126,hypothesis,
'index$u201' = 'rselect$utail'(q3) ).
cnf(hyp127,hypothesis,
'index$u204' = s('index$u201') ).
cnf(hyp128,hypothesis,
'index$u207' = 'rselect$utail'(q39) ).
cnf(hyp129,hypothesis,
'index$u21' = 'rselect$utail'(q11) ).
cnf(hyp130,hypothesis,
'index$u210' = s('index$u207') ).
cnf(hyp131,hypothesis,
'index$u213' = 'rselect$utail'(q40) ).
cnf(hyp132,hypothesis,
'index$u216' = s('index$u213') ).
cnf(hyp133,hypothesis,
'index$u219' = 'rselect$utail'(q41) ).
cnf(hyp134,hypothesis,
'index$u222' = s('index$u219') ).
cnf(hyp135,hypothesis,
'index$u225' = 'rselect$utail'(q42) ).
cnf(hyp136,hypothesis,
'index$u228' = s('index$u225') ).
cnf(hyp137,hypothesis,
'index$u231' = 'rselect$utail'(q4) ).
cnf(hyp138,hypothesis,
'index$u234' = s('index$u231') ).
cnf(hyp139,hypothesis,
'index$u237' = 'rselect$utail'(q5) ).
cnf(hyp140,hypothesis,
'index$u24' = s('index$u21') ).
cnf(hyp141,hypothesis,
'index$u240' = s('index$u237') ).
cnf(hyp142,hypothesis,
'index$u243' = 'rselect$utail'(q6) ).
cnf(hyp143,hypothesis,
'index$u246' = s('index$u243') ).
cnf(hyp144,hypothesis,
'index$u249' = 'rselect$utail'(q7) ).
cnf(hyp145,hypothesis,
'index$u252' = s('index$u249') ).
cnf(hyp146,hypothesis,
'index$u255' = 'rselect$utail'(q8) ).
cnf(hyp147,hypothesis,
'index$u258' = s('index$u255') ).
cnf(hyp148,hypothesis,
'index$u261' = 'rselect$uhead'(q43) ).
cnf(hyp149,hypothesis,
'index$u263' = 'rselect$utail'(q43) ).
cnf(hyp150,hypothesis,
s('index$u264') = 'index$u263' ).
cnf(hyp151,hypothesis,
'index$u27' = 'rselect$utail'(q12) ).
cnf(hyp152,hypothesis,
'index$u3' = 'rselect$utail'(q0) ).
cnf(hyp153,hypothesis,
'index$u30' = s('index$u27') ).
cnf(hyp154,hypothesis,
'index$u33' = 'rselect$utail'(q13) ).
cnf(hyp155,hypothesis,
'index$u36' = s('index$u33') ).
cnf(hyp156,hypothesis,
'index$u39' = 'rselect$utail'(q14) ).
cnf(hyp157,hypothesis,
'index$u42' = s('index$u39') ).
cnf(hyp158,hypothesis,
'index$u45' = 'rselect$utail'(q15) ).
cnf(hyp159,hypothesis,
'index$u48' = s('index$u45') ).
cnf(hyp160,hypothesis,
'index$u51' = 'rselect$utail'(q16) ).
cnf(hyp161,hypothesis,
'index$u54' = s('index$u51') ).
cnf(hyp162,hypothesis,
'index$u57' = 'rselect$utail'(q17) ).
cnf(hyp163,hypothesis,
'index$u6' = s('index$u3') ).
cnf(hyp164,hypothesis,
'index$u60' = s('index$u57') ).
cnf(hyp165,hypothesis,
'index$u63' = 'rselect$utail'(q18) ).
cnf(hyp166,hypothesis,
'index$u66' = s('index$u63') ).
cnf(hyp167,hypothesis,
'index$u69' = 'rselect$utail'(q1) ).
cnf(hyp168,hypothesis,
'index$u72' = s('index$u69') ).
cnf(hyp169,hypothesis,
'index$u75' = 'rselect$utail'(q19) ).
cnf(hyp170,hypothesis,
'index$u78' = s('index$u75') ).
cnf(hyp171,hypothesis,
'index$u81' = 'rselect$utail'(q20) ).
cnf(hyp172,hypothesis,
'index$u84' = s('index$u81') ).
cnf(hyp173,hypothesis,
'index$u87' = 'rselect$utail'(q21) ).
cnf(hyp174,hypothesis,
'index$u9' = 'rselect$utail'(q9) ).
cnf(hyp175,hypothesis,
'index$u90' = s('index$u87') ).
cnf(hyp176,hypothesis,
'index$u93' = 'rselect$utail'(q22) ).
cnf(hyp177,hypothesis,
'index$u96' = s('index$u93') ).
cnf(hyp178,hypothesis,
'index$u99' = 'rselect$utail'(q23) ).
cnf(hyp179,hypothesis,
'queue$u1' = 'rstore$uhead'(q,'index$u0') ).
cnf(hyp180,hypothesis,
'queue$u101' = 'rstore$useq'(q23,'earray$u100') ).
cnf(hyp181,hypothesis,
'queue$u103' = 'rstore$utail'('queue$u101','index$u102') ).
cnf(hyp182,hypothesis,
'queue$u107' = 'rstore$useq'(q24,'earray$u106') ).
cnf(hyp183,hypothesis,
'queue$u109' = 'rstore$utail'('queue$u107','index$u108') ).
cnf(hyp184,hypothesis,
'queue$u11' = 'rstore$useq'(q9,'earray$u10') ).
cnf(hyp185,hypothesis,
'queue$u113' = 'rstore$useq'(q25,'earray$u112') ).
cnf(hyp186,hypothesis,
'queue$u115' = 'rstore$utail'('queue$u113','index$u114') ).
cnf(hyp187,hypothesis,
'queue$u119' = 'rstore$useq'(q26,'earray$u118') ).
cnf(hyp188,hypothesis,
'queue$u121' = 'rstore$utail'('queue$u119','index$u120') ).
cnf(hyp189,hypothesis,
'queue$u125' = 'rstore$useq'(q27,'earray$u124') ).
cnf(hyp190,hypothesis,
'queue$u127' = 'rstore$utail'('queue$u125','index$u126') ).
cnf(hyp191,hypothesis,
'queue$u13' = 'rstore$utail'('queue$u11','index$u12') ).
cnf(hyp192,hypothesis,
'queue$u131' = 'rstore$useq'(q28,'earray$u130') ).
cnf(hyp193,hypothesis,
'queue$u133' = 'rstore$utail'('queue$u131','index$u132') ).
cnf(hyp194,hypothesis,
'queue$u137' = 'rstore$useq'(q2,'earray$u136') ).
cnf(hyp195,hypothesis,
'queue$u139' = 'rstore$utail'('queue$u137','index$u138') ).
cnf(hyp196,hypothesis,
'queue$u143' = 'rstore$useq'(q29,'earray$u142') ).
cnf(hyp197,hypothesis,
'queue$u145' = 'rstore$utail'('queue$u143','index$u144') ).
cnf(hyp198,hypothesis,
'queue$u149' = 'rstore$useq'(q30,'earray$u148') ).
cnf(hyp199,hypothesis,
'queue$u151' = 'rstore$utail'('queue$u149','index$u150') ).
cnf(hyp200,hypothesis,
'queue$u155' = 'rstore$useq'(q31,'earray$u154') ).
cnf(hyp201,hypothesis,
'queue$u157' = 'rstore$utail'('queue$u155','index$u156') ).
cnf(hyp202,hypothesis,
'queue$u161' = 'rstore$useq'(q32,'earray$u160') ).
cnf(hyp203,hypothesis,
'queue$u163' = 'rstore$utail'('queue$u161','index$u162') ).
cnf(hyp204,hypothesis,
'queue$u167' = 'rstore$useq'(q33,'earray$u166') ).
cnf(hyp205,hypothesis,
'queue$u169' = 'rstore$utail'('queue$u167','index$u168') ).
cnf(hyp206,hypothesis,
'queue$u17' = 'rstore$useq'(q10,'earray$u16') ).
cnf(hyp207,hypothesis,
'queue$u173' = 'rstore$useq'(q34,'earray$u172') ).
cnf(hyp208,hypothesis,
'queue$u175' = 'rstore$utail'('queue$u173','index$u174') ).
cnf(hyp209,hypothesis,
'queue$u179' = 'rstore$useq'(q35,'earray$u178') ).
cnf(hyp210,hypothesis,
'queue$u181' = 'rstore$utail'('queue$u179','index$u180') ).
cnf(hyp211,hypothesis,
'queue$u185' = 'rstore$useq'(q36,'earray$u184') ).
cnf(hyp212,hypothesis,
'queue$u187' = 'rstore$utail'('queue$u185','index$u186') ).
cnf(hyp213,hypothesis,
'queue$u19' = 'rstore$utail'('queue$u17','index$u18') ).
cnf(hyp214,hypothesis,
'queue$u191' = 'rstore$useq'(q37,'earray$u190') ).
cnf(hyp215,hypothesis,
'queue$u193' = 'rstore$utail'('queue$u191','index$u192') ).
cnf(hyp216,hypothesis,
'queue$u197' = 'rstore$useq'(q38,'earray$u196') ).
cnf(hyp217,hypothesis,
'queue$u199' = 'rstore$utail'('queue$u197','index$u198') ).
cnf(hyp218,hypothesis,
'queue$u203' = 'rstore$useq'(q3,'earray$u202') ).
cnf(hyp219,hypothesis,
'queue$u205' = 'rstore$utail'('queue$u203','index$u204') ).
cnf(hyp220,hypothesis,
'queue$u209' = 'rstore$useq'(q39,'earray$u208') ).
cnf(hyp221,hypothesis,
'queue$u211' = 'rstore$utail'('queue$u209','index$u210') ).
cnf(hyp222,hypothesis,
'queue$u215' = 'rstore$useq'(q40,'earray$u214') ).
cnf(hyp223,hypothesis,
'queue$u217' = 'rstore$utail'('queue$u215','index$u216') ).
cnf(hyp224,hypothesis,
'queue$u221' = 'rstore$useq'(q41,'earray$u220') ).
cnf(hyp225,hypothesis,
'queue$u223' = 'rstore$utail'('queue$u221','index$u222') ).
cnf(hyp226,hypothesis,
'queue$u227' = 'rstore$useq'(q42,'earray$u226') ).
cnf(hyp227,hypothesis,
'queue$u229' = 'rstore$utail'('queue$u227','index$u228') ).
cnf(hyp228,hypothesis,
'queue$u23' = 'rstore$useq'(q11,'earray$u22') ).
cnf(hyp229,hypothesis,
'queue$u233' = 'rstore$useq'(q4,'earray$u232') ).
cnf(hyp230,hypothesis,
'queue$u235' = 'rstore$utail'('queue$u233','index$u234') ).
cnf(hyp231,hypothesis,
'queue$u239' = 'rstore$useq'(q5,'earray$u238') ).
cnf(hyp232,hypothesis,
'queue$u241' = 'rstore$utail'('queue$u239','index$u240') ).
cnf(hyp233,hypothesis,
'queue$u245' = 'rstore$useq'(q6,'earray$u244') ).
cnf(hyp234,hypothesis,
'queue$u247' = 'rstore$utail'('queue$u245','index$u246') ).
cnf(hyp235,hypothesis,
'queue$u25' = 'rstore$utail'('queue$u23','index$u24') ).
cnf(hyp236,hypothesis,
'queue$u251' = 'rstore$useq'(q7,'earray$u250') ).
cnf(hyp237,hypothesis,
'queue$u253' = 'rstore$utail'('queue$u251','index$u252') ).
cnf(hyp238,hypothesis,
'queue$u257' = 'rstore$useq'(q8,'earray$u256') ).
cnf(hyp239,hypothesis,
'queue$u259' = 'rstore$utail'('queue$u257','index$u258') ).
cnf(hyp240,hypothesis,
'queue$u29' = 'rstore$useq'(q12,'earray$u28') ).
cnf(hyp241,hypothesis,
'queue$u31' = 'rstore$utail'('queue$u29','index$u30') ).
cnf(hyp242,hypothesis,
'queue$u35' = 'rstore$useq'(q13,'earray$u34') ).
cnf(hyp243,hypothesis,
'queue$u37' = 'rstore$utail'('queue$u35','index$u36') ).
cnf(hyp244,hypothesis,
'queue$u41' = 'rstore$useq'(q14,'earray$u40') ).
cnf(hyp245,hypothesis,
'queue$u43' = 'rstore$utail'('queue$u41','index$u42') ).
cnf(hyp246,hypothesis,
'queue$u47' = 'rstore$useq'(q15,'earray$u46') ).
cnf(hyp247,hypothesis,
'queue$u49' = 'rstore$utail'('queue$u47','index$u48') ).
cnf(hyp248,hypothesis,
'queue$u5' = 'rstore$useq'(q0,'earray$u4') ).
cnf(hyp249,hypothesis,
'queue$u53' = 'rstore$useq'(q16,'earray$u52') ).
cnf(hyp250,hypothesis,
'queue$u55' = 'rstore$utail'('queue$u53','index$u54') ).
cnf(hyp251,hypothesis,
'queue$u59' = 'rstore$useq'(q17,'earray$u58') ).
cnf(hyp252,hypothesis,
'queue$u61' = 'rstore$utail'('queue$u59','index$u60') ).
cnf(hyp253,hypothesis,
'queue$u65' = 'rstore$useq'(q18,'earray$u64') ).
cnf(hyp254,hypothesis,
'queue$u67' = 'rstore$utail'('queue$u65','index$u66') ).
cnf(hyp255,hypothesis,
'queue$u7' = 'rstore$utail'('queue$u5','index$u6') ).
cnf(hyp256,hypothesis,
'queue$u71' = 'rstore$useq'(q1,'earray$u70') ).
cnf(hyp257,hypothesis,
'queue$u73' = 'rstore$utail'('queue$u71','index$u72') ).
cnf(hyp258,hypothesis,
'queue$u77' = 'rstore$useq'(q19,'earray$u76') ).
cnf(hyp259,hypothesis,
'queue$u79' = 'rstore$utail'('queue$u77','index$u78') ).
cnf(hyp260,hypothesis,
'queue$u83' = 'rstore$useq'(q20,'earray$u82') ).
cnf(hyp261,hypothesis,
'queue$u85' = 'rstore$utail'('queue$u83','index$u84') ).
cnf(hyp262,hypothesis,
'queue$u89' = 'rstore$useq'(q21,'earray$u88') ).
cnf(hyp263,hypothesis,
'queue$u91' = 'rstore$utail'('queue$u89','index$u90') ).
cnf(hyp264,hypothesis,
'queue$u95' = 'rstore$useq'(q22,'earray$u94') ).
cnf(hyp265,hypothesis,
'queue$u97' = 'rstore$utail'('queue$u95','index$u96') ).
cnf(hyp266,hypothesis,
q0 = 'queue$u1' ).
cnf(hyp267,hypothesis,
q1 = 'queue$u7' ).
cnf(hyp268,hypothesis,
q10 = 'queue$u13' ).
cnf(hyp269,hypothesis,
q11 = 'queue$u19' ).
cnf(hyp270,hypothesis,
q12 = 'queue$u25' ).
cnf(hyp271,hypothesis,
q13 = 'queue$u31' ).
cnf(hyp272,hypothesis,
q14 = 'queue$u37' ).
cnf(hyp273,hypothesis,
q15 = 'queue$u43' ).
cnf(hyp274,hypothesis,
q16 = 'queue$u49' ).
cnf(hyp275,hypothesis,
q17 = 'queue$u55' ).
cnf(hyp276,hypothesis,
q18 = 'queue$u61' ).
cnf(hyp277,hypothesis,
q19 = 'queue$u67' ).
cnf(hyp278,hypothesis,
q2 = 'queue$u73' ).
cnf(hyp279,hypothesis,
q20 = 'queue$u79' ).
cnf(hyp280,hypothesis,
q21 = 'queue$u85' ).
cnf(hyp281,hypothesis,
q22 = 'queue$u91' ).
cnf(hyp282,hypothesis,
q23 = 'queue$u97' ).
cnf(hyp283,hypothesis,
q24 = 'queue$u103' ).
cnf(hyp284,hypothesis,
q25 = 'queue$u109' ).
cnf(hyp285,hypothesis,
q26 = 'queue$u115' ).
cnf(hyp286,hypothesis,
q27 = 'queue$u121' ).
cnf(hyp287,hypothesis,
q28 = 'queue$u127' ).
cnf(hyp288,hypothesis,
q29 = 'queue$u133' ).
cnf(hyp289,hypothesis,
q3 = 'queue$u139' ).
cnf(hyp290,hypothesis,
q30 = 'queue$u145' ).
cnf(hyp291,hypothesis,
q31 = 'queue$u151' ).
cnf(hyp292,hypothesis,
q32 = 'queue$u157' ).
cnf(hyp293,hypothesis,
q33 = 'queue$u163' ).
cnf(hyp294,hypothesis,
q34 = 'queue$u169' ).
cnf(hyp295,hypothesis,
q35 = 'queue$u175' ).
cnf(hyp296,hypothesis,
q36 = 'queue$u181' ).
cnf(hyp297,hypothesis,
q37 = 'queue$u187' ).
cnf(hyp298,hypothesis,
q38 = 'queue$u193' ).
cnf(hyp299,hypothesis,
q39 = 'queue$u199' ).
cnf(hyp300,hypothesis,
q4 = 'queue$u205' ).
cnf(hyp301,hypothesis,
q40 = 'queue$u211' ).
cnf(hyp302,hypothesis,
q41 = 'queue$u217' ).
cnf(hyp303,hypothesis,
q42 = 'queue$u223' ).
cnf(hyp304,hypothesis,
q43 = 'queue$u229' ).
cnf(hyp305,hypothesis,
q5 = 'queue$u235' ).
cnf(hyp306,hypothesis,
q6 = 'queue$u241' ).
cnf(hyp307,hypothesis,
q7 = 'queue$u247' ).
cnf(hyp308,hypothesis,
q8 = 'queue$u253' ).
cnf(hyp309,hypothesis,
q9 = 'queue$u259' ).
cnf(goal,negated_conjecture,
'elem$u262' != 'elem$u265' ).
cnf(c2,plain,
'rselect$useq'('rstore$useq'(X0,X1)) = X1,
inference(clausification,[status(esa)],[a1_seq]) ).
cnf(c3,plain,
'rselect$uhead'('rstore$uhead'(X0,X1)) = X1,
inference(clausification,[status(esa)],[a1_head]) ).
cnf(c4,plain,
'rselect$utail'('rstore$utail'(X0,X1)) = X1,
inference(clausification,[status(esa)],[a1_tail]) ).
cnf(c6,plain,
'rselect$useq'('rstore$utail'(X0,X1)) = 'rselect$useq'(X0),
inference(clausification,[status(esa)],[a2_seq_tail]) ).
cnf(c7,plain,
'rselect$uhead'('rstore$utail'(X0,X1)) = 'rselect$uhead'(X0),
inference(clausification,[status(esa)],[a2_head_tail]) ).
cnf(c8,plain,
'rselect$uhead'('rstore$useq'(X0,X1)) = 'rselect$uhead'(X0),
inference(clausification,[status(esa)],[a2_head_seq]) ).
cnf(c10,plain,
'rselect$utail'('rstore$uhead'(X0,X1)) = 'rselect$utail'(X0),
inference(clausification,[status(esa)],[a2_tail_head]) ).
cnf(c11,plain,
p(s(X0)) = X0,
inference(clausification,[status(esa)],[ps]) ).
cnf(c12,plain,
s(p(X0)) = X0,
inference(clausification,[status(esa)],[sp]) ).
cnf(c15,plain,
s(s(s(X0))) = X0,
inference(clausification,[status(esa)],[circular]) ).
cnf(c28,plain,
'earray$u134' = 'rselect$useq'(q2),
inference(clausification,[status(esa)],[hyp12]) ).
cnf(c103,plain,
'elem$u262' = select('earray$u260','index$u261'),
inference(clausification,[status(esa)],[hyp87]) ).
cnf(c104,plain,
'elem$u265' = select('earray$u260','index$u264'),
inference(clausification,[status(esa)],[hyp88]) ).
cnf(c105,plain,
'index$u0' = 'rselect$utail'(q),
inference(clausification,[status(esa)],[hyp89]) ).
cnf(c106,plain,
'index$u102' = s('index$u99'),
inference(clausification,[status(esa)],[hyp90]) ).
cnf(c107,plain,
'index$u105' = 'rselect$utail'(q24),
inference(clausification,[status(esa)],[hyp91]) ).
cnf(c108,plain,
'index$u108' = s('index$u105'),
inference(clausification,[status(esa)],[hyp92]) ).
cnf(c109,plain,
'index$u111' = 'rselect$utail'(q25),
inference(clausification,[status(esa)],[hyp93]) ).
cnf(c110,plain,
'index$u114' = s('index$u111'),
inference(clausification,[status(esa)],[hyp94]) ).
cnf(c111,plain,
'index$u117' = 'rselect$utail'(q26),
inference(clausification,[status(esa)],[hyp95]) ).
cnf(c112,plain,
'index$u12' = s('index$u9'),
inference(clausification,[status(esa)],[hyp96]) ).
cnf(c113,plain,
'index$u120' = s('index$u117'),
inference(clausification,[status(esa)],[hyp97]) ).
cnf(c114,plain,
'index$u123' = 'rselect$utail'(q27),
inference(clausification,[status(esa)],[hyp98]) ).
cnf(c115,plain,
'index$u126' = s('index$u123'),
inference(clausification,[status(esa)],[hyp99]) ).
cnf(c116,plain,
'index$u129' = 'rselect$utail'(q28),
inference(clausification,[status(esa)],[hyp100]) ).
cnf(c117,plain,
'index$u132' = s('index$u129'),
inference(clausification,[status(esa)],[hyp101]) ).
cnf(c118,plain,
'index$u135' = 'rselect$utail'(q2),
inference(clausification,[status(esa)],[hyp102]) ).
cnf(c119,plain,
'index$u138' = s('index$u135'),
inference(clausification,[status(esa)],[hyp103]) ).
cnf(c120,plain,
'index$u141' = 'rselect$utail'(q29),
inference(clausification,[status(esa)],[hyp104]) ).
cnf(c121,plain,
'index$u144' = s('index$u141'),
inference(clausification,[status(esa)],[hyp105]) ).
cnf(c122,plain,
'index$u147' = 'rselect$utail'(q30),
inference(clausification,[status(esa)],[hyp106]) ).
cnf(c123,plain,
'index$u15' = 'rselect$utail'(q10),
inference(clausification,[status(esa)],[hyp107]) ).
cnf(c124,plain,
'index$u150' = s('index$u147'),
inference(clausification,[status(esa)],[hyp108]) ).
cnf(c125,plain,
'index$u153' = 'rselect$utail'(q31),
inference(clausification,[status(esa)],[hyp109]) ).
cnf(c126,plain,
'index$u156' = s('index$u153'),
inference(clausification,[status(esa)],[hyp110]) ).
cnf(c127,plain,
'index$u159' = 'rselect$utail'(q32),
inference(clausification,[status(esa)],[hyp111]) ).
cnf(c128,plain,
'index$u162' = s('index$u159'),
inference(clausification,[status(esa)],[hyp112]) ).
cnf(c129,plain,
'index$u165' = 'rselect$utail'(q33),
inference(clausification,[status(esa)],[hyp113]) ).
cnf(c130,plain,
'index$u168' = s('index$u165'),
inference(clausification,[status(esa)],[hyp114]) ).
cnf(c131,plain,
'index$u171' = 'rselect$utail'(q34),
inference(clausification,[status(esa)],[hyp115]) ).
cnf(c132,plain,
'index$u174' = s('index$u171'),
inference(clausification,[status(esa)],[hyp116]) ).
cnf(c133,plain,
'index$u177' = 'rselect$utail'(q35),
inference(clausification,[status(esa)],[hyp117]) ).
cnf(c134,plain,
'index$u18' = s('index$u15'),
inference(clausification,[status(esa)],[hyp118]) ).
cnf(c135,plain,
'index$u180' = s('index$u177'),
inference(clausification,[status(esa)],[hyp119]) ).
cnf(c136,plain,
'index$u183' = 'rselect$utail'(q36),
inference(clausification,[status(esa)],[hyp120]) ).
cnf(c137,plain,
'index$u186' = s('index$u183'),
inference(clausification,[status(esa)],[hyp121]) ).
cnf(c138,plain,
'index$u189' = 'rselect$utail'(q37),
inference(clausification,[status(esa)],[hyp122]) ).
cnf(c139,plain,
'index$u192' = s('index$u189'),
inference(clausification,[status(esa)],[hyp123]) ).
cnf(c140,plain,
'index$u195' = 'rselect$utail'(q38),
inference(clausification,[status(esa)],[hyp124]) ).
cnf(c141,plain,
'index$u198' = s('index$u195'),
inference(clausification,[status(esa)],[hyp125]) ).
cnf(c142,plain,
'index$u201' = 'rselect$utail'(q3),
inference(clausification,[status(esa)],[hyp126]) ).
cnf(c143,plain,
'index$u204' = s('index$u201'),
inference(clausification,[status(esa)],[hyp127]) ).
cnf(c144,plain,
'index$u207' = 'rselect$utail'(q39),
inference(clausification,[status(esa)],[hyp128]) ).
cnf(c145,plain,
'index$u21' = 'rselect$utail'(q11),
inference(clausification,[status(esa)],[hyp129]) ).
cnf(c146,plain,
'index$u210' = s('index$u207'),
inference(clausification,[status(esa)],[hyp130]) ).
cnf(c147,plain,
'index$u213' = 'rselect$utail'(q40),
inference(clausification,[status(esa)],[hyp131]) ).
cnf(c148,plain,
'index$u216' = s('index$u213'),
inference(clausification,[status(esa)],[hyp132]) ).
cnf(c149,plain,
'index$u219' = 'rselect$utail'(q41),
inference(clausification,[status(esa)],[hyp133]) ).
cnf(c150,plain,
'index$u222' = s('index$u219'),
inference(clausification,[status(esa)],[hyp134]) ).
cnf(c151,plain,
'index$u225' = 'rselect$utail'(q42),
inference(clausification,[status(esa)],[hyp135]) ).
cnf(c152,plain,
'index$u228' = s('index$u225'),
inference(clausification,[status(esa)],[hyp136]) ).
cnf(c153,plain,
'index$u231' = 'rselect$utail'(q4),
inference(clausification,[status(esa)],[hyp137]) ).
cnf(c154,plain,
'index$u234' = s('index$u231'),
inference(clausification,[status(esa)],[hyp138]) ).
cnf(c155,plain,
'index$u237' = 'rselect$utail'(q5),
inference(clausification,[status(esa)],[hyp139]) ).
cnf(c156,plain,
'index$u24' = s('index$u21'),
inference(clausification,[status(esa)],[hyp140]) ).
cnf(c157,plain,
'index$u240' = s('index$u237'),
inference(clausification,[status(esa)],[hyp141]) ).
cnf(c158,plain,
'index$u243' = 'rselect$utail'(q6),
inference(clausification,[status(esa)],[hyp142]) ).
cnf(c159,plain,
'index$u246' = s('index$u243'),
inference(clausification,[status(esa)],[hyp143]) ).
cnf(c160,plain,
'index$u249' = 'rselect$utail'(q7),
inference(clausification,[status(esa)],[hyp144]) ).
cnf(c161,plain,
'index$u252' = s('index$u249'),
inference(clausification,[status(esa)],[hyp145]) ).
cnf(c162,plain,
'index$u255' = 'rselect$utail'(q8),
inference(clausification,[status(esa)],[hyp146]) ).
cnf(c163,plain,
'index$u258' = s('index$u255'),
inference(clausification,[status(esa)],[hyp147]) ).
cnf(c164,plain,
'index$u261' = 'rselect$uhead'(q43),
inference(clausification,[status(esa)],[hyp148]) ).
cnf(c165,plain,
'index$u263' = 'rselect$utail'(q43),
inference(clausification,[status(esa)],[hyp149]) ).
cnf(c166,plain,
s('index$u264') = 'index$u263',
inference(clausification,[status(esa)],[hyp150]) ).
cnf(c167,plain,
'index$u27' = 'rselect$utail'(q12),
inference(clausification,[status(esa)],[hyp151]) ).
cnf(c168,plain,
'index$u3' = 'rselect$utail'(q0),
inference(clausification,[status(esa)],[hyp152]) ).
cnf(c169,plain,
'index$u30' = s('index$u27'),
inference(clausification,[status(esa)],[hyp153]) ).
cnf(c170,plain,
'index$u33' = 'rselect$utail'(q13),
inference(clausification,[status(esa)],[hyp154]) ).
cnf(c171,plain,
'index$u36' = s('index$u33'),
inference(clausification,[status(esa)],[hyp155]) ).
cnf(c172,plain,
'index$u39' = 'rselect$utail'(q14),
inference(clausification,[status(esa)],[hyp156]) ).
cnf(c173,plain,
'index$u42' = s('index$u39'),
inference(clausification,[status(esa)],[hyp157]) ).
cnf(c174,plain,
'index$u45' = 'rselect$utail'(q15),
inference(clausification,[status(esa)],[hyp158]) ).
cnf(c175,plain,
'index$u48' = s('index$u45'),
inference(clausification,[status(esa)],[hyp159]) ).
cnf(c176,plain,
'index$u51' = 'rselect$utail'(q16),
inference(clausification,[status(esa)],[hyp160]) ).
cnf(c177,plain,
'index$u54' = s('index$u51'),
inference(clausification,[status(esa)],[hyp161]) ).
cnf(c178,plain,
'index$u57' = 'rselect$utail'(q17),
inference(clausification,[status(esa)],[hyp162]) ).
cnf(c179,plain,
'index$u6' = s('index$u3'),
inference(clausification,[status(esa)],[hyp163]) ).
cnf(c180,plain,
'index$u60' = s('index$u57'),
inference(clausification,[status(esa)],[hyp164]) ).
cnf(c181,plain,
'index$u63' = 'rselect$utail'(q18),
inference(clausification,[status(esa)],[hyp165]) ).
cnf(c182,plain,
'index$u66' = s('index$u63'),
inference(clausification,[status(esa)],[hyp166]) ).
cnf(c183,plain,
'index$u69' = 'rselect$utail'(q1),
inference(clausification,[status(esa)],[hyp167]) ).
cnf(c184,plain,
'index$u72' = s('index$u69'),
inference(clausification,[status(esa)],[hyp168]) ).
cnf(c185,plain,
'index$u75' = 'rselect$utail'(q19),
inference(clausification,[status(esa)],[hyp169]) ).
cnf(c186,plain,
'index$u78' = s('index$u75'),
inference(clausification,[status(esa)],[hyp170]) ).
cnf(c187,plain,
'index$u81' = 'rselect$utail'(q20),
inference(clausification,[status(esa)],[hyp171]) ).
cnf(c188,plain,
'index$u84' = s('index$u81'),
inference(clausification,[status(esa)],[hyp172]) ).
cnf(c189,plain,
'index$u87' = 'rselect$utail'(q21),
inference(clausification,[status(esa)],[hyp173]) ).
cnf(c190,plain,
'index$u9' = 'rselect$utail'(q9),
inference(clausification,[status(esa)],[hyp174]) ).
cnf(c191,plain,
'index$u90' = s('index$u87'),
inference(clausification,[status(esa)],[hyp175]) ).
cnf(c192,plain,
'index$u93' = 'rselect$utail'(q22),
inference(clausification,[status(esa)],[hyp176]) ).
cnf(c193,plain,
'index$u96' = s('index$u93'),
inference(clausification,[status(esa)],[hyp177]) ).
cnf(c194,plain,
'index$u99' = 'rselect$utail'(q23),
inference(clausification,[status(esa)],[hyp178]) ).
cnf(c195,plain,
'queue$u1' = 'rstore$uhead'(q,'index$u0'),
inference(clausification,[status(esa)],[hyp179]) ).
cnf(c196,plain,
'queue$u101' = 'rstore$useq'(q23,'earray$u100'),
inference(clausification,[status(esa)],[hyp180]) ).
cnf(c197,plain,
'queue$u103' = 'rstore$utail'('queue$u101','index$u102'),
inference(clausification,[status(esa)],[hyp181]) ).
cnf(c198,plain,
'queue$u107' = 'rstore$useq'(q24,'earray$u106'),
inference(clausification,[status(esa)],[hyp182]) ).
cnf(c199,plain,
'queue$u109' = 'rstore$utail'('queue$u107','index$u108'),
inference(clausification,[status(esa)],[hyp183]) ).
cnf(c200,plain,
'queue$u11' = 'rstore$useq'(q9,'earray$u10'),
inference(clausification,[status(esa)],[hyp184]) ).
cnf(c201,plain,
'queue$u113' = 'rstore$useq'(q25,'earray$u112'),
inference(clausification,[status(esa)],[hyp185]) ).
cnf(c202,plain,
'queue$u115' = 'rstore$utail'('queue$u113','index$u114'),
inference(clausification,[status(esa)],[hyp186]) ).
cnf(c203,plain,
'queue$u119' = 'rstore$useq'(q26,'earray$u118'),
inference(clausification,[status(esa)],[hyp187]) ).
cnf(c204,plain,
'queue$u121' = 'rstore$utail'('queue$u119','index$u120'),
inference(clausification,[status(esa)],[hyp188]) ).
cnf(c205,plain,
'queue$u125' = 'rstore$useq'(q27,'earray$u124'),
inference(clausification,[status(esa)],[hyp189]) ).
cnf(c206,plain,
'queue$u127' = 'rstore$utail'('queue$u125','index$u126'),
inference(clausification,[status(esa)],[hyp190]) ).
cnf(c207,plain,
'queue$u13' = 'rstore$utail'('queue$u11','index$u12'),
inference(clausification,[status(esa)],[hyp191]) ).
cnf(c208,plain,
'queue$u131' = 'rstore$useq'(q28,'earray$u130'),
inference(clausification,[status(esa)],[hyp192]) ).
cnf(c209,plain,
'queue$u133' = 'rstore$utail'('queue$u131','index$u132'),
inference(clausification,[status(esa)],[hyp193]) ).
cnf(c210,plain,
'queue$u137' = 'rstore$useq'(q2,'earray$u136'),
inference(clausification,[status(esa)],[hyp194]) ).
cnf(c211,plain,
'queue$u139' = 'rstore$utail'('queue$u137','index$u138'),
inference(clausification,[status(esa)],[hyp195]) ).
cnf(c212,plain,
'queue$u143' = 'rstore$useq'(q29,'earray$u142'),
inference(clausification,[status(esa)],[hyp196]) ).
cnf(c213,plain,
'queue$u145' = 'rstore$utail'('queue$u143','index$u144'),
inference(clausification,[status(esa)],[hyp197]) ).
cnf(c214,plain,
'queue$u149' = 'rstore$useq'(q30,'earray$u148'),
inference(clausification,[status(esa)],[hyp198]) ).
cnf(c215,plain,
'queue$u151' = 'rstore$utail'('queue$u149','index$u150'),
inference(clausification,[status(esa)],[hyp199]) ).
cnf(c216,plain,
'queue$u155' = 'rstore$useq'(q31,'earray$u154'),
inference(clausification,[status(esa)],[hyp200]) ).
cnf(c217,plain,
'queue$u157' = 'rstore$utail'('queue$u155','index$u156'),
inference(clausification,[status(esa)],[hyp201]) ).
cnf(c218,plain,
'queue$u161' = 'rstore$useq'(q32,'earray$u160'),
inference(clausification,[status(esa)],[hyp202]) ).
cnf(c219,plain,
'queue$u163' = 'rstore$utail'('queue$u161','index$u162'),
inference(clausification,[status(esa)],[hyp203]) ).
cnf(c220,plain,
'queue$u167' = 'rstore$useq'(q33,'earray$u166'),
inference(clausification,[status(esa)],[hyp204]) ).
cnf(c221,plain,
'queue$u169' = 'rstore$utail'('queue$u167','index$u168'),
inference(clausification,[status(esa)],[hyp205]) ).
cnf(c222,plain,
'queue$u17' = 'rstore$useq'(q10,'earray$u16'),
inference(clausification,[status(esa)],[hyp206]) ).
cnf(c223,plain,
'queue$u173' = 'rstore$useq'(q34,'earray$u172'),
inference(clausification,[status(esa)],[hyp207]) ).
cnf(c224,plain,
'queue$u175' = 'rstore$utail'('queue$u173','index$u174'),
inference(clausification,[status(esa)],[hyp208]) ).
cnf(c225,plain,
'queue$u179' = 'rstore$useq'(q35,'earray$u178'),
inference(clausification,[status(esa)],[hyp209]) ).
cnf(c226,plain,
'queue$u181' = 'rstore$utail'('queue$u179','index$u180'),
inference(clausification,[status(esa)],[hyp210]) ).
cnf(c227,plain,
'queue$u185' = 'rstore$useq'(q36,'earray$u184'),
inference(clausification,[status(esa)],[hyp211]) ).
cnf(c228,plain,
'queue$u187' = 'rstore$utail'('queue$u185','index$u186'),
inference(clausification,[status(esa)],[hyp212]) ).
cnf(c229,plain,
'queue$u19' = 'rstore$utail'('queue$u17','index$u18'),
inference(clausification,[status(esa)],[hyp213]) ).
cnf(c230,plain,
'queue$u191' = 'rstore$useq'(q37,'earray$u190'),
inference(clausification,[status(esa)],[hyp214]) ).
cnf(c231,plain,
'queue$u193' = 'rstore$utail'('queue$u191','index$u192'),
inference(clausification,[status(esa)],[hyp215]) ).
cnf(c232,plain,
'queue$u197' = 'rstore$useq'(q38,'earray$u196'),
inference(clausification,[status(esa)],[hyp216]) ).
cnf(c233,plain,
'queue$u199' = 'rstore$utail'('queue$u197','index$u198'),
inference(clausification,[status(esa)],[hyp217]) ).
cnf(c234,plain,
'queue$u203' = 'rstore$useq'(q3,'earray$u202'),
inference(clausification,[status(esa)],[hyp218]) ).
cnf(c235,plain,
'queue$u205' = 'rstore$utail'('queue$u203','index$u204'),
inference(clausification,[status(esa)],[hyp219]) ).
cnf(c236,plain,
'queue$u209' = 'rstore$useq'(q39,'earray$u208'),
inference(clausification,[status(esa)],[hyp220]) ).
cnf(c237,plain,
'queue$u211' = 'rstore$utail'('queue$u209','index$u210'),
inference(clausification,[status(esa)],[hyp221]) ).
cnf(c238,plain,
'queue$u215' = 'rstore$useq'(q40,'earray$u214'),
inference(clausification,[status(esa)],[hyp222]) ).
cnf(c239,plain,
'queue$u217' = 'rstore$utail'('queue$u215','index$u216'),
inference(clausification,[status(esa)],[hyp223]) ).
cnf(c240,plain,
'queue$u221' = 'rstore$useq'(q41,'earray$u220'),
inference(clausification,[status(esa)],[hyp224]) ).
cnf(c241,plain,
'queue$u223' = 'rstore$utail'('queue$u221','index$u222'),
inference(clausification,[status(esa)],[hyp225]) ).
cnf(c242,plain,
'queue$u227' = 'rstore$useq'(q42,'earray$u226'),
inference(clausification,[status(esa)],[hyp226]) ).
cnf(c243,plain,
'queue$u229' = 'rstore$utail'('queue$u227','index$u228'),
inference(clausification,[status(esa)],[hyp227]) ).
cnf(c244,plain,
'queue$u23' = 'rstore$useq'(q11,'earray$u22'),
inference(clausification,[status(esa)],[hyp228]) ).
cnf(c245,plain,
'queue$u233' = 'rstore$useq'(q4,'earray$u232'),
inference(clausification,[status(esa)],[hyp229]) ).
cnf(c246,plain,
'queue$u235' = 'rstore$utail'('queue$u233','index$u234'),
inference(clausification,[status(esa)],[hyp230]) ).
cnf(c247,plain,
'queue$u239' = 'rstore$useq'(q5,'earray$u238'),
inference(clausification,[status(esa)],[hyp231]) ).
cnf(c248,plain,
'queue$u241' = 'rstore$utail'('queue$u239','index$u240'),
inference(clausification,[status(esa)],[hyp232]) ).
cnf(c249,plain,
'queue$u245' = 'rstore$useq'(q6,'earray$u244'),
inference(clausification,[status(esa)],[hyp233]) ).
cnf(c250,plain,
'queue$u247' = 'rstore$utail'('queue$u245','index$u246'),
inference(clausification,[status(esa)],[hyp234]) ).
cnf(c251,plain,
'queue$u25' = 'rstore$utail'('queue$u23','index$u24'),
inference(clausification,[status(esa)],[hyp235]) ).
cnf(c252,plain,
'queue$u251' = 'rstore$useq'(q7,'earray$u250'),
inference(clausification,[status(esa)],[hyp236]) ).
cnf(c253,plain,
'queue$u253' = 'rstore$utail'('queue$u251','index$u252'),
inference(clausification,[status(esa)],[hyp237]) ).
cnf(c254,plain,
'queue$u257' = 'rstore$useq'(q8,'earray$u256'),
inference(clausification,[status(esa)],[hyp238]) ).
cnf(c255,plain,
'queue$u259' = 'rstore$utail'('queue$u257','index$u258'),
inference(clausification,[status(esa)],[hyp239]) ).
cnf(c256,plain,
'queue$u29' = 'rstore$useq'(q12,'earray$u28'),
inference(clausification,[status(esa)],[hyp240]) ).
cnf(c257,plain,
'queue$u31' = 'rstore$utail'('queue$u29','index$u30'),
inference(clausification,[status(esa)],[hyp241]) ).
cnf(c258,plain,
'queue$u35' = 'rstore$useq'(q13,'earray$u34'),
inference(clausification,[status(esa)],[hyp242]) ).
cnf(c259,plain,
'queue$u37' = 'rstore$utail'('queue$u35','index$u36'),
inference(clausification,[status(esa)],[hyp243]) ).
cnf(c260,plain,
'queue$u41' = 'rstore$useq'(q14,'earray$u40'),
inference(clausification,[status(esa)],[hyp244]) ).
cnf(c261,plain,
'queue$u43' = 'rstore$utail'('queue$u41','index$u42'),
inference(clausification,[status(esa)],[hyp245]) ).
cnf(c262,plain,
'queue$u47' = 'rstore$useq'(q15,'earray$u46'),
inference(clausification,[status(esa)],[hyp246]) ).
cnf(c263,plain,
'queue$u49' = 'rstore$utail'('queue$u47','index$u48'),
inference(clausification,[status(esa)],[hyp247]) ).
cnf(c264,plain,
'queue$u5' = 'rstore$useq'(q0,'earray$u4'),
inference(clausification,[status(esa)],[hyp248]) ).
cnf(c265,plain,
'queue$u53' = 'rstore$useq'(q16,'earray$u52'),
inference(clausification,[status(esa)],[hyp249]) ).
cnf(c266,plain,
'queue$u55' = 'rstore$utail'('queue$u53','index$u54'),
inference(clausification,[status(esa)],[hyp250]) ).
cnf(c267,plain,
'queue$u59' = 'rstore$useq'(q17,'earray$u58'),
inference(clausification,[status(esa)],[hyp251]) ).
cnf(c268,plain,
'queue$u61' = 'rstore$utail'('queue$u59','index$u60'),
inference(clausification,[status(esa)],[hyp252]) ).
cnf(c269,plain,
'queue$u65' = 'rstore$useq'(q18,'earray$u64'),
inference(clausification,[status(esa)],[hyp253]) ).
cnf(c270,plain,
'queue$u67' = 'rstore$utail'('queue$u65','index$u66'),
inference(clausification,[status(esa)],[hyp254]) ).
cnf(c271,plain,
'queue$u7' = 'rstore$utail'('queue$u5','index$u6'),
inference(clausification,[status(esa)],[hyp255]) ).
cnf(c272,plain,
'queue$u71' = 'rstore$useq'(q1,'earray$u70'),
inference(clausification,[status(esa)],[hyp256]) ).
cnf(c273,plain,
'queue$u73' = 'rstore$utail'('queue$u71','index$u72'),
inference(clausification,[status(esa)],[hyp257]) ).
cnf(c274,plain,
'queue$u77' = 'rstore$useq'(q19,'earray$u76'),
inference(clausification,[status(esa)],[hyp258]) ).
cnf(c275,plain,
'queue$u79' = 'rstore$utail'('queue$u77','index$u78'),
inference(clausification,[status(esa)],[hyp259]) ).
cnf(c276,plain,
'queue$u83' = 'rstore$useq'(q20,'earray$u82'),
inference(clausification,[status(esa)],[hyp260]) ).
cnf(c277,plain,
'queue$u85' = 'rstore$utail'('queue$u83','index$u84'),
inference(clausification,[status(esa)],[hyp261]) ).
cnf(c278,plain,
'queue$u89' = 'rstore$useq'(q21,'earray$u88'),
inference(clausification,[status(esa)],[hyp262]) ).
cnf(c279,plain,
'queue$u91' = 'rstore$utail'('queue$u89','index$u90'),
inference(clausification,[status(esa)],[hyp263]) ).
cnf(c280,plain,
'queue$u95' = 'rstore$useq'(q22,'earray$u94'),
inference(clausification,[status(esa)],[hyp264]) ).
cnf(c281,plain,
'queue$u97' = 'rstore$utail'('queue$u95','index$u96'),
inference(clausification,[status(esa)],[hyp265]) ).
cnf(c282,plain,
q0 = 'queue$u1',
inference(clausification,[status(esa)],[hyp266]) ).
cnf(c283,plain,
q1 = 'queue$u7',
inference(clausification,[status(esa)],[hyp267]) ).
cnf(c284,plain,
q10 = 'queue$u13',
inference(clausification,[status(esa)],[hyp268]) ).
cnf(c285,plain,
q11 = 'queue$u19',
inference(clausification,[status(esa)],[hyp269]) ).
cnf(c286,plain,
q12 = 'queue$u25',
inference(clausification,[status(esa)],[hyp270]) ).
cnf(c287,plain,
q13 = 'queue$u31',
inference(clausification,[status(esa)],[hyp271]) ).
cnf(c288,plain,
q14 = 'queue$u37',
inference(clausification,[status(esa)],[hyp272]) ).
cnf(c289,plain,
q15 = 'queue$u43',
inference(clausification,[status(esa)],[hyp273]) ).
cnf(c290,plain,
q16 = 'queue$u49',
inference(clausification,[status(esa)],[hyp274]) ).
cnf(c291,plain,
q17 = 'queue$u55',
inference(clausification,[status(esa)],[hyp275]) ).
cnf(c292,plain,
q18 = 'queue$u61',
inference(clausification,[status(esa)],[hyp276]) ).
cnf(c293,plain,
q19 = 'queue$u67',
inference(clausification,[status(esa)],[hyp277]) ).
cnf(c294,plain,
q2 = 'queue$u73',
inference(clausification,[status(esa)],[hyp278]) ).
cnf(c295,plain,
q20 = 'queue$u79',
inference(clausification,[status(esa)],[hyp279]) ).
cnf(c296,plain,
q21 = 'queue$u85',
inference(clausification,[status(esa)],[hyp280]) ).
cnf(c297,plain,
q22 = 'queue$u91',
inference(clausification,[status(esa)],[hyp281]) ).
cnf(c298,plain,
q23 = 'queue$u97',
inference(clausification,[status(esa)],[hyp282]) ).
cnf(c299,plain,
q24 = 'queue$u103',
inference(clausification,[status(esa)],[hyp283]) ).
cnf(c300,plain,
q25 = 'queue$u109',
inference(clausification,[status(esa)],[hyp284]) ).
cnf(c301,plain,
q26 = 'queue$u115',
inference(clausification,[status(esa)],[hyp285]) ).
cnf(c302,plain,
q27 = 'queue$u121',
inference(clausification,[status(esa)],[hyp286]) ).
cnf(c303,plain,
q28 = 'queue$u127',
inference(clausification,[status(esa)],[hyp287]) ).
cnf(c304,plain,
q29 = 'queue$u133',
inference(clausification,[status(esa)],[hyp288]) ).
cnf(c305,plain,
q3 = 'queue$u139',
inference(clausification,[status(esa)],[hyp289]) ).
cnf(c306,plain,
q30 = 'queue$u145',
inference(clausification,[status(esa)],[hyp290]) ).
cnf(c307,plain,
q31 = 'queue$u151',
inference(clausification,[status(esa)],[hyp291]) ).
cnf(c308,plain,
q32 = 'queue$u157',
inference(clausification,[status(esa)],[hyp292]) ).
cnf(c309,plain,
q33 = 'queue$u163',
inference(clausification,[status(esa)],[hyp293]) ).
cnf(c310,plain,
q34 = 'queue$u169',
inference(clausification,[status(esa)],[hyp294]) ).
cnf(c311,plain,
q35 = 'queue$u175',
inference(clausification,[status(esa)],[hyp295]) ).
cnf(c312,plain,
q36 = 'queue$u181',
inference(clausification,[status(esa)],[hyp296]) ).
cnf(c313,plain,
q37 = 'queue$u187',
inference(clausification,[status(esa)],[hyp297]) ).
cnf(c314,plain,
q38 = 'queue$u193',
inference(clausification,[status(esa)],[hyp298]) ).
cnf(c315,plain,
q39 = 'queue$u199',
inference(clausification,[status(esa)],[hyp299]) ).
cnf(c316,plain,
q4 = 'queue$u205',
inference(clausification,[status(esa)],[hyp300]) ).
cnf(c317,plain,
q40 = 'queue$u211',
inference(clausification,[status(esa)],[hyp301]) ).
cnf(c318,plain,
q41 = 'queue$u217',
inference(clausification,[status(esa)],[hyp302]) ).
cnf(c319,plain,
q42 = 'queue$u223',
inference(clausification,[status(esa)],[hyp303]) ).
cnf(c320,plain,
q43 = 'queue$u229',
inference(clausification,[status(esa)],[hyp304]) ).
cnf(c321,plain,
q5 = 'queue$u235',
inference(clausification,[status(esa)],[hyp305]) ).
cnf(c322,plain,
q6 = 'queue$u241',
inference(clausification,[status(esa)],[hyp306]) ).
cnf(c323,plain,
q7 = 'queue$u247',
inference(clausification,[status(esa)],[hyp307]) ).
cnf(c324,plain,
q8 = 'queue$u253',
inference(clausification,[status(esa)],[hyp308]) ).
cnf(c325,plain,
q9 = 'queue$u259',
inference(clausification,[status(esa)],[hyp309]) ).
cnf(c326,plain,
'elem$u262' != 'elem$u265',
inference(clausification,[status(esa)],[goal]) ).
cnf(d0,plain,
q4 = 'rstore$utail'('queue$u203','index$u204'),
inference(demodulation,[status(thm)],[c235,c316]) ).
cnf(d1,plain,
'rselect$utail'(q4) = 'index$u204',
inference(superposition,[status(thm)],[d0,c4]) ).
cnf(d2,plain,
'index$u231' = 'index$u204',
inference(demodulation,[status(thm)],[d1,c153]) ).
cnf(d3,plain,
p('index$u204') = 'index$u201',
inference(superposition,[status(thm)],[c143,c11]) ).
cnf(d4,plain,
s('index$u201') = 'index$u204',
inference(superposition,[status(thm)],[d3,c12]) ).
cnf(d5,plain,
s('index$u201') = 'index$u231',
inference(demodulation,[status(thm)],[d4,d2]) ).
cnf(d6,plain,
p(X0) = s(s(X0)),
inference(superposition,[status(thm)],[c15,c11]) ).
cnf(d7,plain,
q3 = 'rstore$utail'('queue$u137','index$u138'),
inference(demodulation,[status(thm)],[c211,c305]) ).
cnf(d8,plain,
'rselect$utail'(q3) = 'index$u138',
inference(superposition,[status(thm)],[d7,c4]) ).
cnf(d9,plain,
'index$u201' = 'index$u138',
inference(demodulation,[status(thm)],[d8,c142]) ).
cnf(d10,plain,
p('index$u138') = 'index$u135',
inference(superposition,[status(thm)],[c119,c11]) ).
cnf(d11,plain,
s('index$u135') = 'index$u138',
inference(superposition,[status(thm)],[d10,c12]) ).
cnf(d12,plain,
s('index$u135') = 'index$u201',
inference(demodulation,[status(thm)],[d11,d9]) ).
cnf(d13,plain,
p('index$u135') = s('index$u201'),
inference(superposition,[status(thm)],[d12,d6]) ).
cnf(d14,plain,
p('index$u135') = 'index$u231',
inference(demodulation,[status(thm)],[d13,d5]) ).
cnf(d15,plain,
q2 = 'rstore$utail'('queue$u71','index$u72'),
inference(demodulation,[status(thm)],[c273,c294]) ).
cnf(d16,plain,
'rselect$utail'(q2) = 'index$u72',
inference(superposition,[status(thm)],[d15,c4]) ).
cnf(d17,plain,
'index$u135' = 'index$u72',
inference(demodulation,[status(thm)],[d16,c118]) ).
cnf(d18,plain,
p('index$u72') = 'index$u69',
inference(superposition,[status(thm)],[c184,c11]) ).
cnf(d19,plain,
p('index$u135') = 'index$u69',
inference(demodulation,[status(thm)],[d18,d17]) ).
cnf(d20,plain,
'index$u231' = 'index$u69',
inference(demodulation,[status(thm)],[d19,d14]) ).
cnf(d21,plain,
'index$u135' = s('index$u69'),
inference(demodulation,[status(thm)],[c184,d17]) ).
cnf(d22,plain,
'index$u135' = s('index$u231'),
inference(demodulation,[status(thm)],[d21,d20]) ).
cnf(d23,plain,
q5 = 'rstore$utail'('queue$u233','index$u234'),
inference(demodulation,[status(thm)],[c246,c321]) ).
cnf(d24,plain,
'rselect$utail'(q5) = 'index$u234',
inference(superposition,[status(thm)],[d23,c4]) ).
cnf(d25,plain,
'index$u237' = 'index$u234',
inference(demodulation,[status(thm)],[d24,c155]) ).
cnf(d26,plain,
'index$u237' = s('index$u231'),
inference(demodulation,[status(thm)],[c154,d25]) ).
cnf(d27,plain,
'index$u237' = 'index$u135',
inference(demodulation,[status(thm)],[d26,d22]) ).
cnf(d28,plain,
q10 = 'rstore$utail'('queue$u11','index$u12'),
inference(demodulation,[status(thm)],[c207,c284]) ).
cnf(d29,plain,
'rselect$utail'(q10) = 'index$u12',
inference(superposition,[status(thm)],[d28,c4]) ).
cnf(d30,plain,
'index$u15' = 'index$u12',
inference(demodulation,[status(thm)],[d29,c123]) ).
cnf(d31,plain,
p('index$u12') = 'index$u9',
inference(superposition,[status(thm)],[c112,c11]) ).
cnf(d32,plain,
p('index$u15') = 'index$u9',
inference(demodulation,[status(thm)],[d31,d30]) ).
cnf(d33,plain,
s('index$u9') = 'index$u12',
inference(superposition,[status(thm)],[d31,c12]) ).
cnf(d34,plain,
s('index$u9') = 'index$u15',
inference(demodulation,[status(thm)],[d33,d30]) ).
cnf(d35,plain,
q9 = 'rstore$utail'('queue$u257','index$u258'),
inference(demodulation,[status(thm)],[c255,c325]) ).
cnf(d36,plain,
'rselect$utail'(q9) = 'index$u258',
inference(superposition,[status(thm)],[d35,c4]) ).
cnf(d37,plain,
'index$u9' = 'index$u258',
inference(demodulation,[status(thm)],[d36,c190]) ).
cnf(d38,plain,
p('index$u255') = s('index$u258'),
inference(superposition,[status(thm)],[c163,d6]) ).
cnf(d39,plain,
p('index$u255') = s('index$u9'),
inference(demodulation,[status(thm)],[d38,d37]) ).
cnf(d40,plain,
p('index$u255') = 'index$u15',
inference(demodulation,[status(thm)],[d39,d34]) ).
cnf(d41,plain,
q8 = 'rstore$utail'('queue$u251','index$u252'),
inference(demodulation,[status(thm)],[c253,c324]) ).
cnf(d42,plain,
'rselect$utail'(q8) = 'index$u252',
inference(superposition,[status(thm)],[d41,c4]) ).
cnf(d43,plain,
'index$u255' = 'index$u252',
inference(demodulation,[status(thm)],[d42,c162]) ).
cnf(d44,plain,
p('index$u252') = 'index$u249',
inference(superposition,[status(thm)],[c161,c11]) ).
cnf(d45,plain,
p('index$u255') = 'index$u249',
inference(demodulation,[status(thm)],[d44,d43]) ).
cnf(d46,plain,
'index$u15' = 'index$u249',
inference(demodulation,[status(thm)],[d45,d40]) ).
cnf(d47,plain,
q7 = 'rstore$utail'('queue$u245','index$u246'),
inference(demodulation,[status(thm)],[c250,c323]) ).
cnf(d48,plain,
'rselect$utail'(q7) = 'index$u246',
inference(superposition,[status(thm)],[d47,c4]) ).
cnf(d49,plain,
'index$u249' = 'index$u246',
inference(demodulation,[status(thm)],[d48,c160]) ).
cnf(d50,plain,
p('index$u243') = s('index$u246'),
inference(superposition,[status(thm)],[c159,d6]) ).
cnf(d51,plain,
p('index$u243') = s('index$u249'),
inference(demodulation,[status(thm)],[d50,d49]) ).
cnf(d52,plain,
s(s('index$u249')) = 'index$u243',
inference(superposition,[status(thm)],[d51,c12]) ).
cnf(d53,plain,
p('index$u249') = 'index$u243',
inference(demodulation,[status(thm)],[d52,d6]) ).
cnf(d54,plain,
p('index$u15') = 'index$u243',
inference(demodulation,[status(thm)],[d53,d46]) ).
cnf(d55,plain,
'index$u9' = 'index$u243',
inference(demodulation,[status(thm)],[d54,d32]) ).
cnf(d56,plain,
p(p(X0)) = s(X0),
inference(superposition,[status(thm)],[d6,c11]) ).
cnf(d57,plain,
q6 = 'rstore$utail'('queue$u239','index$u240'),
inference(demodulation,[status(thm)],[c248,c322]) ).
cnf(d58,plain,
'rselect$utail'(q6) = 'index$u240',
inference(superposition,[status(thm)],[d57,c4]) ).
cnf(d59,plain,
'index$u243' = 'index$u240',
inference(demodulation,[status(thm)],[d58,c158]) ).
cnf(d60,plain,
p('index$u237') = s('index$u240'),
inference(superposition,[status(thm)],[c157,d6]) ).
cnf(d61,plain,
p('index$u237') = s('index$u243'),
inference(demodulation,[status(thm)],[d60,d59]) ).
cnf(d62,plain,
p(s('index$u243')) = s('index$u237'),
inference(superposition,[status(thm)],[d61,d56]) ).
cnf(d63,plain,
'index$u243' = s('index$u237'),
inference(demodulation,[status(thm)],[d62,c11]) ).
cnf(d64,plain,
'index$u9' = s('index$u237'),
inference(demodulation,[status(thm)],[d63,d55]) ).
cnf(d65,plain,
'index$u9' = s('index$u135'),
inference(demodulation,[status(thm)],[d64,d27]) ).
cnf(d66,plain,
'index$u9' = 'index$u201',
inference(demodulation,[status(thm)],[d12,d65]) ).
cnf(d67,plain,
p('index$u69') = s('index$u72'),
inference(superposition,[status(thm)],[c184,d6]) ).
cnf(d68,plain,
p('index$u69') = s('index$u135'),
inference(demodulation,[status(thm)],[d67,d17]) ).
cnf(d69,plain,
p('index$u69') = 'index$u201',
inference(demodulation,[status(thm)],[d68,d12]) ).
cnf(d70,plain,
q1 = 'rstore$utail'('queue$u5','index$u6'),
inference(demodulation,[status(thm)],[c271,c283]) ).
cnf(d71,plain,
'rselect$utail'(q1) = 'index$u6',
inference(superposition,[status(thm)],[d70,c4]) ).
cnf(d72,plain,
'index$u69' = 'index$u6',
inference(demodulation,[status(thm)],[d71,c183]) ).
cnf(d73,plain,
p('index$u6') = 'index$u3',
inference(superposition,[status(thm)],[c179,c11]) ).
cnf(d74,plain,
p('index$u69') = 'index$u3',
inference(demodulation,[status(thm)],[d73,d72]) ).
cnf(d75,plain,
'index$u201' = 'index$u3',
inference(demodulation,[status(thm)],[d74,d69]) ).
cnf(d76,plain,
'index$u9' = 'index$u3',
inference(demodulation,[status(thm)],[d75,d66]) ).
cnf(d77,plain,
q0 = 'rstore$uhead'(q,'index$u0'),
inference(demodulation,[status(thm)],[c195,c282]) ).
cnf(d78,plain,
'rselect$utail'(q0) = 'rselect$utail'(q),
inference(superposition,[status(thm)],[d77,c10]) ).
cnf(d79,plain,
'index$u3' = 'rselect$utail'(q),
inference(demodulation,[status(thm)],[d78,c168]) ).
cnf(d80,plain,
'index$u0' = 'index$u3',
inference(demodulation,[status(thm)],[c105,d79]) ).
cnf(d81,plain,
'rselect$uhead'(q0) = 'index$u0',
inference(superposition,[status(thm)],[d77,c3]) ).
cnf(d82,plain,
'rselect$uhead'(q0) = 'index$u3',
inference(demodulation,[status(thm)],[d81,d80]) ).
cnf(d83,plain,
'rselect$uhead'('queue$u5') = 'rselect$uhead'(q0),
inference(superposition,[status(thm)],[c264,c8]) ).
cnf(d84,plain,
'rselect$uhead'(q1) = 'rselect$uhead'('queue$u5'),
inference(superposition,[status(thm)],[d70,c7]) ).
cnf(d85,plain,
'rselect$uhead'(q1) = 'rselect$uhead'(q0),
inference(demodulation,[status(thm)],[d84,d83]) ).
cnf(d86,plain,
'rselect$uhead'(q1) = 'index$u3',
inference(demodulation,[status(thm)],[d85,d82]) ).
cnf(d87,plain,
'rselect$uhead'(q1) = 'index$u9',
inference(demodulation,[status(thm)],[d86,d76]) ).
cnf(d88,plain,
q43 = 'rstore$utail'('queue$u227','index$u228'),
inference(demodulation,[status(thm)],[c243,c320]) ).
cnf(d89,plain,
'rselect$uhead'(q43) = 'rselect$uhead'('queue$u227'),
inference(superposition,[status(thm)],[d88,c7]) ).
cnf(d90,plain,
'index$u261' = 'rselect$uhead'('queue$u227'),
inference(demodulation,[status(thm)],[d89,c164]) ).
cnf(d91,plain,
'rselect$uhead'('queue$u107') = 'rselect$uhead'(q24),
inference(superposition,[status(thm)],[c198,c8]) ).
cnf(d92,plain,
q25 = 'rstore$utail'('queue$u107','index$u108'),
inference(demodulation,[status(thm)],[c199,c300]) ).
cnf(d93,plain,
'rselect$uhead'(q25) = 'rselect$uhead'('queue$u107'),
inference(superposition,[status(thm)],[d92,c7]) ).
cnf(d94,plain,
'rselect$uhead'(q25) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d93,d91]) ).
cnf(d95,plain,
'rselect$uhead'('queue$u113') = 'rselect$uhead'(q25),
inference(superposition,[status(thm)],[c201,c8]) ).
cnf(d96,plain,
'rselect$uhead'('queue$u113') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d95,d94]) ).
cnf(d97,plain,
q26 = 'rstore$utail'('queue$u113','index$u114'),
inference(demodulation,[status(thm)],[c202,c301]) ).
cnf(d98,plain,
'rselect$uhead'(q26) = 'rselect$uhead'('queue$u113'),
inference(superposition,[status(thm)],[d97,c7]) ).
cnf(d99,plain,
'rselect$uhead'(q26) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d98,d96]) ).
cnf(d100,plain,
'rselect$uhead'('queue$u119') = 'rselect$uhead'(q26),
inference(superposition,[status(thm)],[c203,c8]) ).
cnf(d101,plain,
'rselect$uhead'('queue$u119') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d100,d99]) ).
cnf(d102,plain,
q27 = 'rstore$utail'('queue$u119','index$u120'),
inference(demodulation,[status(thm)],[c204,c302]) ).
cnf(d103,plain,
'rselect$uhead'(q27) = 'rselect$uhead'('queue$u119'),
inference(superposition,[status(thm)],[d102,c7]) ).
cnf(d104,plain,
'rselect$uhead'(q27) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d103,d101]) ).
cnf(d105,plain,
'rselect$uhead'('queue$u125') = 'rselect$uhead'(q27),
inference(superposition,[status(thm)],[c205,c8]) ).
cnf(d106,plain,
'rselect$uhead'('queue$u125') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d105,d104]) ).
cnf(d107,plain,
q28 = 'rstore$utail'('queue$u125','index$u126'),
inference(demodulation,[status(thm)],[c206,c303]) ).
cnf(d108,plain,
'rselect$uhead'(q28) = 'rselect$uhead'('queue$u125'),
inference(superposition,[status(thm)],[d107,c7]) ).
cnf(d109,plain,
'rselect$uhead'(q28) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d108,d106]) ).
cnf(d110,plain,
'rselect$uhead'('queue$u131') = 'rselect$uhead'(q28),
inference(superposition,[status(thm)],[c208,c8]) ).
cnf(d111,plain,
'rselect$uhead'('queue$u131') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d110,d109]) ).
cnf(d112,plain,
q29 = 'rstore$utail'('queue$u131','index$u132'),
inference(demodulation,[status(thm)],[c209,c304]) ).
cnf(d113,plain,
'rselect$uhead'(q29) = 'rselect$uhead'('queue$u131'),
inference(superposition,[status(thm)],[d112,c7]) ).
cnf(d114,plain,
'rselect$uhead'(q29) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d113,d111]) ).
cnf(d115,plain,
'rselect$uhead'('queue$u143') = 'rselect$uhead'(q29),
inference(superposition,[status(thm)],[c212,c8]) ).
cnf(d116,plain,
'rselect$uhead'('queue$u143') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d115,d114]) ).
cnf(d117,plain,
q30 = 'rstore$utail'('queue$u143','index$u144'),
inference(demodulation,[status(thm)],[c213,c306]) ).
cnf(d118,plain,
'rselect$uhead'(q30) = 'rselect$uhead'('queue$u143'),
inference(superposition,[status(thm)],[d117,c7]) ).
cnf(d119,plain,
'rselect$uhead'(q30) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d118,d116]) ).
cnf(d120,plain,
'rselect$uhead'('queue$u149') = 'rselect$uhead'(q30),
inference(superposition,[status(thm)],[c214,c8]) ).
cnf(d121,plain,
'rselect$uhead'('queue$u149') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d120,d119]) ).
cnf(d122,plain,
q31 = 'rstore$utail'('queue$u149','index$u150'),
inference(demodulation,[status(thm)],[c215,c307]) ).
cnf(d123,plain,
'rselect$uhead'(q31) = 'rselect$uhead'('queue$u149'),
inference(superposition,[status(thm)],[d122,c7]) ).
cnf(d124,plain,
'rselect$uhead'(q31) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d123,d121]) ).
cnf(d125,plain,
'rselect$uhead'('queue$u155') = 'rselect$uhead'(q31),
inference(superposition,[status(thm)],[c216,c8]) ).
cnf(d126,plain,
'rselect$uhead'('queue$u155') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d125,d124]) ).
cnf(d127,plain,
q32 = 'rstore$utail'('queue$u155','index$u156'),
inference(demodulation,[status(thm)],[c217,c308]) ).
cnf(d128,plain,
'rselect$uhead'(q32) = 'rselect$uhead'('queue$u155'),
inference(superposition,[status(thm)],[d127,c7]) ).
cnf(d129,plain,
'rselect$uhead'(q32) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d128,d126]) ).
cnf(d130,plain,
'rselect$uhead'('queue$u161') = 'rselect$uhead'(q32),
inference(superposition,[status(thm)],[c218,c8]) ).
cnf(d131,plain,
'rselect$uhead'('queue$u161') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d130,d129]) ).
cnf(d132,plain,
q33 = 'rstore$utail'('queue$u161','index$u162'),
inference(demodulation,[status(thm)],[c219,c309]) ).
cnf(d133,plain,
'rselect$uhead'(q33) = 'rselect$uhead'('queue$u161'),
inference(superposition,[status(thm)],[d132,c7]) ).
cnf(d134,plain,
'rselect$uhead'(q33) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d133,d131]) ).
cnf(d135,plain,
'rselect$uhead'('queue$u167') = 'rselect$uhead'(q33),
inference(superposition,[status(thm)],[c220,c8]) ).
cnf(d136,plain,
'rselect$uhead'('queue$u167') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d135,d134]) ).
cnf(d137,plain,
q34 = 'rstore$utail'('queue$u167','index$u168'),
inference(demodulation,[status(thm)],[c221,c310]) ).
cnf(d138,plain,
'rselect$uhead'(q34) = 'rselect$uhead'('queue$u167'),
inference(superposition,[status(thm)],[d137,c7]) ).
cnf(d139,plain,
'rselect$uhead'(q34) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d138,d136]) ).
cnf(d140,plain,
'rselect$uhead'('queue$u173') = 'rselect$uhead'(q34),
inference(superposition,[status(thm)],[c223,c8]) ).
cnf(d141,plain,
'rselect$uhead'('queue$u173') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d140,d139]) ).
cnf(d142,plain,
q35 = 'rstore$utail'('queue$u173','index$u174'),
inference(demodulation,[status(thm)],[c224,c311]) ).
cnf(d143,plain,
'rselect$uhead'(q35) = 'rselect$uhead'('queue$u173'),
inference(superposition,[status(thm)],[d142,c7]) ).
cnf(d144,plain,
'rselect$uhead'(q35) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d143,d141]) ).
cnf(d145,plain,
'rselect$uhead'('queue$u179') = 'rselect$uhead'(q35),
inference(superposition,[status(thm)],[c225,c8]) ).
cnf(d146,plain,
'rselect$uhead'('queue$u179') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d145,d144]) ).
cnf(d147,plain,
q36 = 'rstore$utail'('queue$u179','index$u180'),
inference(demodulation,[status(thm)],[c226,c312]) ).
cnf(d148,plain,
'rselect$uhead'(q36) = 'rselect$uhead'('queue$u179'),
inference(superposition,[status(thm)],[d147,c7]) ).
cnf(d149,plain,
'rselect$uhead'(q36) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d148,d146]) ).
cnf(d150,plain,
'rselect$uhead'('queue$u185') = 'rselect$uhead'(q36),
inference(superposition,[status(thm)],[c227,c8]) ).
cnf(d151,plain,
'rselect$uhead'('queue$u185') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d150,d149]) ).
cnf(d152,plain,
q37 = 'rstore$utail'('queue$u185','index$u186'),
inference(demodulation,[status(thm)],[c228,c313]) ).
cnf(d153,plain,
'rselect$uhead'(q37) = 'rselect$uhead'('queue$u185'),
inference(superposition,[status(thm)],[d152,c7]) ).
cnf(d154,plain,
'rselect$uhead'(q37) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d153,d151]) ).
cnf(d155,plain,
'rselect$uhead'('queue$u191') = 'rselect$uhead'(q37),
inference(superposition,[status(thm)],[c230,c8]) ).
cnf(d156,plain,
'rselect$uhead'('queue$u191') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d155,d154]) ).
cnf(d157,plain,
q38 = 'rstore$utail'('queue$u191','index$u192'),
inference(demodulation,[status(thm)],[c231,c314]) ).
cnf(d158,plain,
'rselect$uhead'(q38) = 'rselect$uhead'('queue$u191'),
inference(superposition,[status(thm)],[d157,c7]) ).
cnf(d159,plain,
'rselect$uhead'(q38) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d158,d156]) ).
cnf(d160,plain,
'rselect$uhead'('queue$u197') = 'rselect$uhead'(q38),
inference(superposition,[status(thm)],[c232,c8]) ).
cnf(d161,plain,
'rselect$uhead'('queue$u197') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d160,d159]) ).
cnf(d162,plain,
q39 = 'rstore$utail'('queue$u197','index$u198'),
inference(demodulation,[status(thm)],[c233,c315]) ).
cnf(d163,plain,
'rselect$uhead'(q39) = 'rselect$uhead'('queue$u197'),
inference(superposition,[status(thm)],[d162,c7]) ).
cnf(d164,plain,
'rselect$uhead'(q39) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d163,d161]) ).
cnf(d165,plain,
'rselect$uhead'('queue$u209') = 'rselect$uhead'(q39),
inference(superposition,[status(thm)],[c236,c8]) ).
cnf(d166,plain,
'rselect$uhead'('queue$u209') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d165,d164]) ).
cnf(d167,plain,
q40 = 'rstore$utail'('queue$u209','index$u210'),
inference(demodulation,[status(thm)],[c237,c317]) ).
cnf(d168,plain,
'rselect$uhead'(q40) = 'rselect$uhead'('queue$u209'),
inference(superposition,[status(thm)],[d167,c7]) ).
cnf(d169,plain,
'rselect$uhead'(q40) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d168,d166]) ).
cnf(d170,plain,
'rselect$uhead'('queue$u215') = 'rselect$uhead'(q40),
inference(superposition,[status(thm)],[c238,c8]) ).
cnf(d171,plain,
'rselect$uhead'('queue$u215') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d170,d169]) ).
cnf(d172,plain,
q41 = 'rstore$utail'('queue$u215','index$u216'),
inference(demodulation,[status(thm)],[c239,c318]) ).
cnf(d173,plain,
'rselect$uhead'(q41) = 'rselect$uhead'('queue$u215'),
inference(superposition,[status(thm)],[d172,c7]) ).
cnf(d174,plain,
'rselect$uhead'(q41) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d173,d171]) ).
cnf(d175,plain,
'rselect$uhead'('queue$u221') = 'rselect$uhead'(q41),
inference(superposition,[status(thm)],[c240,c8]) ).
cnf(d176,plain,
'rselect$uhead'('queue$u221') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d175,d174]) ).
cnf(d177,plain,
q42 = 'rstore$utail'('queue$u221','index$u222'),
inference(demodulation,[status(thm)],[c241,c319]) ).
cnf(d178,plain,
'rselect$uhead'(q42) = 'rselect$uhead'('queue$u221'),
inference(superposition,[status(thm)],[d177,c7]) ).
cnf(d179,plain,
'rselect$uhead'(q42) = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d178,d176]) ).
cnf(d180,plain,
'rselect$uhead'('queue$u227') = 'rselect$uhead'(q42),
inference(superposition,[status(thm)],[c242,c8]) ).
cnf(d181,plain,
'rselect$uhead'('queue$u227') = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d180,d179]) ).
cnf(d182,plain,
'index$u261' = 'rselect$uhead'(q24),
inference(demodulation,[status(thm)],[d181,d90]) ).
cnf(d183,plain,
q24 = 'rstore$utail'('queue$u101','index$u102'),
inference(demodulation,[status(thm)],[c197,c299]) ).
cnf(d184,plain,
'rselect$uhead'(q24) = 'rselect$uhead'('queue$u101'),
inference(superposition,[status(thm)],[d183,c7]) ).
cnf(d185,plain,
'rselect$uhead'('queue$u101') = 'rselect$uhead'(q23),
inference(superposition,[status(thm)],[c196,c8]) ).
cnf(d186,plain,
'rselect$uhead'(q24) = 'rselect$uhead'(q23),
inference(demodulation,[status(thm)],[d185,d184]) ).
cnf(d187,plain,
'rselect$uhead'('queue$u17') = 'rselect$uhead'(q10),
inference(superposition,[status(thm)],[c222,c8]) ).
cnf(d188,plain,
q11 = 'rstore$utail'('queue$u17','index$u18'),
inference(demodulation,[status(thm)],[c229,c285]) ).
cnf(d189,plain,
'rselect$uhead'(q11) = 'rselect$uhead'('queue$u17'),
inference(superposition,[status(thm)],[d188,c7]) ).
cnf(d190,plain,
'rselect$uhead'(q11) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d189,d187]) ).
cnf(d191,plain,
'rselect$uhead'('queue$u23') = 'rselect$uhead'(q11),
inference(superposition,[status(thm)],[c244,c8]) ).
cnf(d192,plain,
'rselect$uhead'('queue$u23') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d191,d190]) ).
cnf(d193,plain,
q12 = 'rstore$utail'('queue$u23','index$u24'),
inference(demodulation,[status(thm)],[c251,c286]) ).
cnf(d194,plain,
'rselect$uhead'(q12) = 'rselect$uhead'('queue$u23'),
inference(superposition,[status(thm)],[d193,c7]) ).
cnf(d195,plain,
'rselect$uhead'(q12) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d194,d192]) ).
cnf(d196,plain,
'rselect$uhead'('queue$u29') = 'rselect$uhead'(q12),
inference(superposition,[status(thm)],[c256,c8]) ).
cnf(d197,plain,
'rselect$uhead'('queue$u29') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d196,d195]) ).
cnf(d198,plain,
q13 = 'rstore$utail'('queue$u29','index$u30'),
inference(demodulation,[status(thm)],[c257,c287]) ).
cnf(d199,plain,
'rselect$uhead'(q13) = 'rselect$uhead'('queue$u29'),
inference(superposition,[status(thm)],[d198,c7]) ).
cnf(d200,plain,
'rselect$uhead'(q13) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d199,d197]) ).
cnf(d201,plain,
'rselect$uhead'('queue$u35') = 'rselect$uhead'(q13),
inference(superposition,[status(thm)],[c258,c8]) ).
cnf(d202,plain,
'rselect$uhead'('queue$u35') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d201,d200]) ).
cnf(d203,plain,
q14 = 'rstore$utail'('queue$u35','index$u36'),
inference(demodulation,[status(thm)],[c259,c288]) ).
cnf(d204,plain,
'rselect$uhead'(q14) = 'rselect$uhead'('queue$u35'),
inference(superposition,[status(thm)],[d203,c7]) ).
cnf(d205,plain,
'rselect$uhead'(q14) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d204,d202]) ).
cnf(d206,plain,
'rselect$uhead'('queue$u41') = 'rselect$uhead'(q14),
inference(superposition,[status(thm)],[c260,c8]) ).
cnf(d207,plain,
'rselect$uhead'('queue$u41') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d206,d205]) ).
cnf(d208,plain,
q15 = 'rstore$utail'('queue$u41','index$u42'),
inference(demodulation,[status(thm)],[c261,c289]) ).
cnf(d209,plain,
'rselect$uhead'(q15) = 'rselect$uhead'('queue$u41'),
inference(superposition,[status(thm)],[d208,c7]) ).
cnf(d210,plain,
'rselect$uhead'(q15) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d209,d207]) ).
cnf(d211,plain,
'rselect$uhead'('queue$u47') = 'rselect$uhead'(q15),
inference(superposition,[status(thm)],[c262,c8]) ).
cnf(d212,plain,
'rselect$uhead'('queue$u47') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d211,d210]) ).
cnf(d213,plain,
q16 = 'rstore$utail'('queue$u47','index$u48'),
inference(demodulation,[status(thm)],[c263,c290]) ).
cnf(d214,plain,
'rselect$uhead'(q16) = 'rselect$uhead'('queue$u47'),
inference(superposition,[status(thm)],[d213,c7]) ).
cnf(d215,plain,
'rselect$uhead'(q16) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d214,d212]) ).
cnf(d216,plain,
'rselect$uhead'('queue$u53') = 'rselect$uhead'(q16),
inference(superposition,[status(thm)],[c265,c8]) ).
cnf(d217,plain,
'rselect$uhead'('queue$u53') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d216,d215]) ).
cnf(d218,plain,
q17 = 'rstore$utail'('queue$u53','index$u54'),
inference(demodulation,[status(thm)],[c266,c291]) ).
cnf(d219,plain,
'rselect$uhead'(q17) = 'rselect$uhead'('queue$u53'),
inference(superposition,[status(thm)],[d218,c7]) ).
cnf(d220,plain,
'rselect$uhead'(q17) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d219,d217]) ).
cnf(d221,plain,
'rselect$uhead'('queue$u59') = 'rselect$uhead'(q17),
inference(superposition,[status(thm)],[c267,c8]) ).
cnf(d222,plain,
'rselect$uhead'('queue$u59') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d221,d220]) ).
cnf(d223,plain,
q18 = 'rstore$utail'('queue$u59','index$u60'),
inference(demodulation,[status(thm)],[c268,c292]) ).
cnf(d224,plain,
'rselect$uhead'(q18) = 'rselect$uhead'('queue$u59'),
inference(superposition,[status(thm)],[d223,c7]) ).
cnf(d225,plain,
'rselect$uhead'(q18) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d224,d222]) ).
cnf(d226,plain,
'rselect$uhead'('queue$u65') = 'rselect$uhead'(q18),
inference(superposition,[status(thm)],[c269,c8]) ).
cnf(d227,plain,
'rselect$uhead'('queue$u65') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d226,d225]) ).
cnf(d228,plain,
q19 = 'rstore$utail'('queue$u65','index$u66'),
inference(demodulation,[status(thm)],[c270,c293]) ).
cnf(d229,plain,
'rselect$uhead'(q19) = 'rselect$uhead'('queue$u65'),
inference(superposition,[status(thm)],[d228,c7]) ).
cnf(d230,plain,
'rselect$uhead'(q19) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d229,d227]) ).
cnf(d231,plain,
'rselect$uhead'('queue$u77') = 'rselect$uhead'(q19),
inference(superposition,[status(thm)],[c274,c8]) ).
cnf(d232,plain,
'rselect$uhead'('queue$u77') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d231,d230]) ).
cnf(d233,plain,
q20 = 'rstore$utail'('queue$u77','index$u78'),
inference(demodulation,[status(thm)],[c275,c295]) ).
cnf(d234,plain,
'rselect$uhead'(q20) = 'rselect$uhead'('queue$u77'),
inference(superposition,[status(thm)],[d233,c7]) ).
cnf(d235,plain,
'rselect$uhead'(q20) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d234,d232]) ).
cnf(d236,plain,
'rselect$uhead'('queue$u83') = 'rselect$uhead'(q20),
inference(superposition,[status(thm)],[c276,c8]) ).
cnf(d237,plain,
'rselect$uhead'('queue$u83') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d236,d235]) ).
cnf(d238,plain,
q21 = 'rstore$utail'('queue$u83','index$u84'),
inference(demodulation,[status(thm)],[c277,c296]) ).
cnf(d239,plain,
'rselect$uhead'(q21) = 'rselect$uhead'('queue$u83'),
inference(superposition,[status(thm)],[d238,c7]) ).
cnf(d240,plain,
'rselect$uhead'(q21) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d239,d237]) ).
cnf(d241,plain,
'rselect$uhead'('queue$u89') = 'rselect$uhead'(q21),
inference(superposition,[status(thm)],[c278,c8]) ).
cnf(d242,plain,
'rselect$uhead'('queue$u89') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d241,d240]) ).
cnf(d243,plain,
q22 = 'rstore$utail'('queue$u89','index$u90'),
inference(demodulation,[status(thm)],[c279,c297]) ).
cnf(d244,plain,
'rselect$uhead'(q22) = 'rselect$uhead'('queue$u89'),
inference(superposition,[status(thm)],[d243,c7]) ).
cnf(d245,plain,
'rselect$uhead'(q22) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d244,d242]) ).
cnf(d246,plain,
'rselect$uhead'('queue$u95') = 'rselect$uhead'(q22),
inference(superposition,[status(thm)],[c280,c8]) ).
cnf(d247,plain,
'rselect$uhead'('queue$u95') = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d246,d245]) ).
cnf(d248,plain,
q23 = 'rstore$utail'('queue$u95','index$u96'),
inference(demodulation,[status(thm)],[c281,c298]) ).
cnf(d249,plain,
'rselect$uhead'(q23) = 'rselect$uhead'('queue$u95'),
inference(superposition,[status(thm)],[d248,c7]) ).
cnf(d250,plain,
'rselect$uhead'(q23) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d249,d247]) ).
cnf(d251,plain,
'rselect$uhead'(q24) = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d250,d186]) ).
cnf(d252,plain,
'index$u261' = 'rselect$uhead'(q10),
inference(demodulation,[status(thm)],[d251,d182]) ).
cnf(d253,plain,
q10 = 'rstore$utail'('queue$u11','index$u15'),
inference(demodulation,[status(thm)],[d28,d30]) ).
cnf(d254,plain,
'rselect$uhead'(q10) = 'rselect$uhead'('queue$u11'),
inference(superposition,[status(thm)],[d253,c7]) ).
cnf(d255,plain,
'index$u261' = 'rselect$uhead'('queue$u11'),
inference(demodulation,[status(thm)],[d254,d252]) ).
cnf(d256,plain,
'rselect$uhead'('queue$u137') = 'rselect$uhead'(q2),
inference(superposition,[status(thm)],[c210,c8]) ).
cnf(d257,plain,
'rselect$uhead'(q3) = 'rselect$uhead'('queue$u137'),
inference(superposition,[status(thm)],[d7,c7]) ).
cnf(d258,plain,
'rselect$uhead'(q3) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d257,d256]) ).
cnf(d259,plain,
'rselect$uhead'('queue$u203') = 'rselect$uhead'(q3),
inference(superposition,[status(thm)],[c234,c8]) ).
cnf(d260,plain,
'rselect$uhead'('queue$u203') = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d259,d258]) ).
cnf(d261,plain,
'rselect$uhead'(q4) = 'rselect$uhead'('queue$u203'),
inference(superposition,[status(thm)],[d0,c7]) ).
cnf(d262,plain,
'rselect$uhead'(q4) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d261,d260]) ).
cnf(d263,plain,
'rselect$uhead'('queue$u233') = 'rselect$uhead'(q4),
inference(superposition,[status(thm)],[c245,c8]) ).
cnf(d264,plain,
'rselect$uhead'('queue$u233') = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d263,d262]) ).
cnf(d265,plain,
'rselect$uhead'(q5) = 'rselect$uhead'('queue$u233'),
inference(superposition,[status(thm)],[d23,c7]) ).
cnf(d266,plain,
'rselect$uhead'(q5) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d265,d264]) ).
cnf(d267,plain,
'rselect$uhead'('queue$u239') = 'rselect$uhead'(q5),
inference(superposition,[status(thm)],[c247,c8]) ).
cnf(d268,plain,
'rselect$uhead'('queue$u239') = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d267,d266]) ).
cnf(d269,plain,
'rselect$uhead'(q6) = 'rselect$uhead'('queue$u239'),
inference(superposition,[status(thm)],[d57,c7]) ).
cnf(d270,plain,
'rselect$uhead'(q6) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d269,d268]) ).
cnf(d271,plain,
'rselect$uhead'('queue$u245') = 'rselect$uhead'(q6),
inference(superposition,[status(thm)],[c249,c8]) ).
cnf(d272,plain,
'rselect$uhead'('queue$u245') = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d271,d270]) ).
cnf(d273,plain,
'rselect$uhead'(q7) = 'rselect$uhead'('queue$u245'),
inference(superposition,[status(thm)],[d47,c7]) ).
cnf(d274,plain,
'rselect$uhead'(q7) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d273,d272]) ).
cnf(d275,plain,
'rselect$uhead'('queue$u251') = 'rselect$uhead'(q7),
inference(superposition,[status(thm)],[c252,c8]) ).
cnf(d276,plain,
'rselect$uhead'('queue$u251') = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d275,d274]) ).
cnf(d277,plain,
'rselect$uhead'(q8) = 'rselect$uhead'('queue$u251'),
inference(superposition,[status(thm)],[d41,c7]) ).
cnf(d278,plain,
'rselect$uhead'(q8) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d277,d276]) ).
cnf(d279,plain,
'rselect$uhead'('queue$u257') = 'rselect$uhead'(q8),
inference(superposition,[status(thm)],[c254,c8]) ).
cnf(d280,plain,
'rselect$uhead'('queue$u257') = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d279,d278]) ).
cnf(d281,plain,
'rselect$uhead'(q9) = 'rselect$uhead'('queue$u257'),
inference(superposition,[status(thm)],[d35,c7]) ).
cnf(d282,plain,
'rselect$uhead'(q9) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d281,d280]) ).
cnf(d283,plain,
'rselect$uhead'(q10) = 'rselect$uhead'('queue$u11'),
inference(superposition,[status(thm)],[d28,c7]) ).
cnf(d284,plain,
'rselect$uhead'('queue$u11') = 'rselect$uhead'(q9),
inference(superposition,[status(thm)],[c200,c8]) ).
cnf(d285,plain,
'rselect$uhead'(q10) = 'rselect$uhead'(q9),
inference(demodulation,[status(thm)],[d284,d283]) ).
cnf(d286,plain,
'rselect$uhead'(q10) = 'rselect$uhead'(q2),
inference(demodulation,[status(thm)],[d285,d282]) ).
cnf(d287,plain,
'rselect$uhead'(q2) = 'rselect$uhead'('queue$u11'),
inference(demodulation,[status(thm)],[d283,d286]) ).
cnf(d288,plain,
'rselect$uhead'(q2) = 'index$u261',
inference(demodulation,[status(thm)],[d287,d255]) ).
cnf(d289,plain,
q2 = 'rstore$utail'('queue$u71','index$u135'),
inference(demodulation,[status(thm)],[d15,d17]) ).
cnf(d290,plain,
'rselect$uhead'(q2) = 'rselect$uhead'('queue$u71'),
inference(superposition,[status(thm)],[d289,c7]) ).
cnf(d291,plain,
'index$u261' = 'rselect$uhead'('queue$u71'),
inference(demodulation,[status(thm)],[d290,d288]) ).
cnf(d292,plain,
'rselect$useq'(q2) = 'rselect$useq'('queue$u71'),
inference(superposition,[status(thm)],[d15,c6]) ).
cnf(d293,plain,
'earray$u134' = 'rselect$useq'('queue$u71'),
inference(demodulation,[status(thm)],[d292,c28]) ).
cnf(d294,plain,
'rselect$useq'('queue$u71') = 'earray$u70',
inference(superposition,[status(thm)],[c272,c2]) ).
cnf(d295,plain,
'earray$u134' = 'earray$u70',
inference(demodulation,[status(thm)],[d294,d293]) ).
cnf(d296,plain,
'queue$u71' = 'rstore$useq'(q1,'earray$u134'),
inference(demodulation,[status(thm)],[c272,d295]) ).
cnf(d297,plain,
'rselect$uhead'('queue$u71') = 'rselect$uhead'(q1),
inference(superposition,[status(thm)],[d296,c8]) ).
cnf(d298,plain,
'index$u261' = 'rselect$uhead'(q1),
inference(demodulation,[status(thm)],[d297,d291]) ).
cnf(d299,plain,
'index$u261' = 'index$u9',
inference(demodulation,[status(thm)],[d298,d87]) ).
cnf(d300,plain,
'elem$u262' = select('earray$u260','index$u9'),
inference(demodulation,[status(thm)],[c103,d299]) ).
cnf(d301,plain,
'rselect$utail'(q11) = 'index$u18',
inference(superposition,[status(thm)],[d188,c4]) ).
cnf(d302,plain,
'index$u21' = 'index$u18',
inference(demodulation,[status(thm)],[d301,c145]) ).
cnf(d303,plain,
p('index$u18') = 'index$u15',
inference(superposition,[status(thm)],[c134,c11]) ).
cnf(d304,plain,
s('index$u15') = 'index$u18',
inference(superposition,[status(thm)],[d303,c12]) ).
cnf(d305,plain,
s('index$u15') = 'index$u21',
inference(demodulation,[status(thm)],[d304,d302]) ).
cnf(d306,plain,
p('index$u9') = s('index$u12'),
inference(superposition,[status(thm)],[c112,d6]) ).
cnf(d307,plain,
p('index$u9') = s('index$u15'),
inference(demodulation,[status(thm)],[d306,d30]) ).
cnf(d308,plain,
p('index$u9') = 'index$u21',
inference(demodulation,[status(thm)],[d307,d305]) ).
cnf(d309,plain,
s(s('index$u243')) = 'index$u237',
inference(superposition,[status(thm)],[d61,c12]) ).
cnf(d310,plain,
p('index$u243') = 'index$u237',
inference(demodulation,[status(thm)],[d309,d6]) ).
cnf(d311,plain,
p('index$u9') = 'index$u237',
inference(demodulation,[status(thm)],[d310,d55]) ).
cnf(d312,plain,
'index$u21' = 'index$u237',
inference(demodulation,[status(thm)],[d311,d308]) ).
cnf(d313,plain,
'index$u21' = 'index$u135',
inference(demodulation,[status(thm)],[d312,d27]) ).
cnf(d314,plain,
p('index$u258') = 'index$u255',
inference(superposition,[status(thm)],[c163,c11]) ).
cnf(d315,plain,
p('index$u9') = 'index$u255',
inference(demodulation,[status(thm)],[d314,d37]) ).
cnf(d316,plain,
'index$u21' = 'index$u255',
inference(demodulation,[status(thm)],[d315,d308]) ).
cnf(d317,plain,
'index$u135' = 'index$u255',
inference(demodulation,[status(thm)],[d316,d313]) ).
cnf(d318,plain,
s('index$u15') = 'index$u255',
inference(superposition,[status(thm)],[d40,c12]) ).
cnf(d319,plain,
s('index$u15') = 'index$u135',
inference(demodulation,[status(thm)],[d318,d317]) ).
cnf(d320,plain,
p('index$u15') = s('index$u21'),
inference(superposition,[status(thm)],[d305,d6]) ).
cnf(d321,plain,
'index$u9' = s('index$u21'),
inference(demodulation,[status(thm)],[d320,d32]) ).
cnf(d322,plain,
'rselect$utail'(q12) = 'index$u24',
inference(superposition,[status(thm)],[d193,c4]) ).
cnf(d323,plain,
'index$u27' = 'index$u24',
inference(demodulation,[status(thm)],[d322,c167]) ).
cnf(d324,plain,
p('index$u24') = 'index$u21',
inference(superposition,[status(thm)],[c156,c11]) ).
cnf(d325,plain,
s('index$u21') = 'index$u24',
inference(superposition,[status(thm)],[d324,c12]) ).
cnf(d326,plain,
s('index$u21') = 'index$u27',
inference(demodulation,[status(thm)],[d325,d323]) ).
cnf(d327,plain,
'index$u9' = 'index$u27',
inference(demodulation,[status(thm)],[d326,d321]) ).
cnf(d328,plain,
'rselect$utail'(q13) = 'index$u30',
inference(superposition,[status(thm)],[d198,c4]) ).
cnf(d329,plain,
'index$u33' = 'index$u30',
inference(demodulation,[status(thm)],[d328,c170]) ).
cnf(d330,plain,
p('index$u27') = s('index$u30'),
inference(superposition,[status(thm)],[c169,d6]) ).
cnf(d331,plain,
p('index$u27') = s('index$u33'),
inference(demodulation,[status(thm)],[d330,d329]) ).
cnf(d332,plain,
p(s('index$u33')) = s('index$u27'),
inference(superposition,[status(thm)],[d331,d56]) ).
cnf(d333,plain,
'index$u33' = s('index$u27'),
inference(demodulation,[status(thm)],[d332,c11]) ).
cnf(d334,plain,
'index$u33' = s('index$u9'),
inference(demodulation,[status(thm)],[d333,d327]) ).
cnf(d335,plain,
'index$u33' = 'index$u15',
inference(demodulation,[status(thm)],[d334,d34]) ).
cnf(d336,plain,
s(s(X0)) = p(X0),
inference(superposition,[status(thm)],[c12,c15]) ).
cnf(d337,plain,
s(X0) = p(p(X0)),
inference(superposition,[status(thm)],[c12,d336]) ).
cnf(d338,plain,
'rselect$utail'(q14) = 'index$u36',
inference(superposition,[status(thm)],[d203,c4]) ).
cnf(d339,plain,
'index$u39' = 'index$u36',
inference(demodulation,[status(thm)],[d338,c172]) ).
cnf(d340,plain,
p('index$u33') = s('index$u36'),
inference(superposition,[status(thm)],[c171,d6]) ).
cnf(d341,plain,
p('index$u33') = s('index$u39'),
inference(demodulation,[status(thm)],[d340,d339]) ).
cnf(d342,plain,
s('index$u33') = p(s('index$u39')),
inference(superposition,[status(thm)],[d341,d337]) ).
cnf(d343,plain,
s('index$u15') = p(s('index$u39')),
inference(demodulation,[status(thm)],[d342,d335]) ).
cnf(d344,plain,
'index$u135' = p(s('index$u39')),
inference(demodulation,[status(thm)],[d343,d319]) ).
cnf(d345,plain,
'index$u135' = 'index$u39',
inference(demodulation,[status(thm)],[d344,c11]) ).
cnf(d346,plain,
'rselect$utail'(q15) = 'index$u42',
inference(superposition,[status(thm)],[d208,c4]) ).
cnf(d347,plain,
'index$u45' = 'index$u42',
inference(demodulation,[status(thm)],[d346,c174]) ).
cnf(d348,plain,
p('index$u39') = s('index$u42'),
inference(superposition,[status(thm)],[c173,d6]) ).
cnf(d349,plain,
p('index$u39') = s('index$u45'),
inference(demodulation,[status(thm)],[d348,d347]) ).
cnf(d350,plain,
s('index$u39') = p(s('index$u45')),
inference(superposition,[status(thm)],[d349,d337]) ).
cnf(d351,plain,
s('index$u135') = p(s('index$u45')),
inference(demodulation,[status(thm)],[d350,d345]) ).
cnf(d352,plain,
'index$u9' = p(s('index$u45')),
inference(demodulation,[status(thm)],[d351,d65]) ).
cnf(d353,plain,
'index$u9' = 'index$u45',
inference(demodulation,[status(thm)],[d352,c11]) ).
cnf(d354,plain,
'rselect$utail'(q16) = 'index$u48',
inference(superposition,[status(thm)],[d213,c4]) ).
cnf(d355,plain,
'index$u51' = 'index$u48',
inference(demodulation,[status(thm)],[d354,c176]) ).
cnf(d356,plain,
s('index$u48') = p('index$u45'),
inference(superposition,[status(thm)],[c175,d336]) ).
cnf(d357,plain,
s('index$u51') = p('index$u45'),
inference(demodulation,[status(thm)],[d356,d355]) ).
cnf(d358,plain,
p(s('index$u51')) = s('index$u45'),
inference(superposition,[status(thm)],[d357,d56]) ).
cnf(d359,plain,
'index$u51' = s('index$u45'),
inference(demodulation,[status(thm)],[d358,c11]) ).
cnf(d360,plain,
'index$u51' = s('index$u9'),
inference(demodulation,[status(thm)],[d359,d353]) ).
cnf(d361,plain,
'index$u51' = 'index$u15',
inference(demodulation,[status(thm)],[d360,d34]) ).
cnf(d362,plain,
'rselect$utail'(q25) = 'index$u108',
inference(superposition,[status(thm)],[d92,c4]) ).
cnf(d363,plain,
'index$u111' = 'index$u108',
inference(demodulation,[status(thm)],[d362,c109]) ).
cnf(d364,plain,
p('index$u108') = 'index$u105',
inference(superposition,[status(thm)],[c108,c11]) ).
cnf(d365,plain,
p('index$u111') = 'index$u105',
inference(demodulation,[status(thm)],[d364,d363]) ).
cnf(d366,plain,
s('index$u105') = 'index$u108',
inference(superposition,[status(thm)],[d364,c12]) ).
cnf(d367,plain,
s('index$u105') = 'index$u111',
inference(demodulation,[status(thm)],[d366,d363]) ).
cnf(d368,plain,
'rselect$utail'(q24) = 'index$u102',
inference(superposition,[status(thm)],[d183,c4]) ).
cnf(d369,plain,
'index$u105' = 'index$u102',
inference(demodulation,[status(thm)],[d368,c107]) ).
cnf(d370,plain,
p('index$u99') = s('index$u102'),
inference(superposition,[status(thm)],[c106,d6]) ).
cnf(d371,plain,
p('index$u99') = s('index$u105'),
inference(demodulation,[status(thm)],[d370,d369]) ).
cnf(d372,plain,
p('index$u99') = 'index$u111',
inference(demodulation,[status(thm)],[d371,d367]) ).
cnf(d373,plain,
p('index$u102') = 'index$u99',
inference(superposition,[status(thm)],[c106,c11]) ).
cnf(d374,plain,
p('index$u105') = 'index$u99',
inference(demodulation,[status(thm)],[d373,d369]) ).
cnf(d375,plain,
s('index$u99') = 'index$u102',
inference(superposition,[status(thm)],[d373,c12]) ).
cnf(d376,plain,
s('index$u99') = 'index$u105',
inference(demodulation,[status(thm)],[d375,d369]) ).
cnf(d377,plain,
'rselect$utail'(q23) = 'index$u96',
inference(superposition,[status(thm)],[d248,c4]) ).
cnf(d378,plain,
'index$u99' = 'index$u96',
inference(demodulation,[status(thm)],[d377,c194]) ).
cnf(d379,plain,
p('index$u93') = s('index$u96'),
inference(superposition,[status(thm)],[c193,d6]) ).
cnf(d380,plain,
p('index$u93') = s('index$u99'),
inference(demodulation,[status(thm)],[d379,d378]) ).
cnf(d381,plain,
p('index$u93') = 'index$u105',
inference(demodulation,[status(thm)],[d380,d376]) ).
cnf(d382,plain,
'rselect$utail'(q22) = 'index$u90',
inference(superposition,[status(thm)],[d243,c4]) ).
cnf(d383,plain,
'index$u93' = 'index$u90',
inference(demodulation,[status(thm)],[d382,c192]) ).
cnf(d384,plain,
p('index$u90') = 'index$u87',
inference(superposition,[status(thm)],[c191,c11]) ).
cnf(d385,plain,
p('index$u93') = 'index$u87',
inference(demodulation,[status(thm)],[d384,d383]) ).
cnf(d386,plain,
'index$u105' = 'index$u87',
inference(demodulation,[status(thm)],[d385,d381]) ).
cnf(d387,plain,
'rselect$utail'(q21) = 'index$u84',
inference(superposition,[status(thm)],[d238,c4]) ).
cnf(d388,plain,
'index$u87' = 'index$u84',
inference(demodulation,[status(thm)],[d387,c189]) ).
cnf(d389,plain,
p('index$u81') = s('index$u84'),
inference(superposition,[status(thm)],[c188,d6]) ).
cnf(d390,plain,
p('index$u81') = s('index$u87'),
inference(demodulation,[status(thm)],[d389,d388]) ).
cnf(d391,plain,
s(s('index$u87')) = 'index$u81',
inference(superposition,[status(thm)],[d390,c12]) ).
cnf(d392,plain,
p('index$u87') = 'index$u81',
inference(demodulation,[status(thm)],[d391,d6]) ).
cnf(d393,plain,
p('index$u105') = 'index$u81',
inference(demodulation,[status(thm)],[d392,d386]) ).
cnf(d394,plain,
'index$u99' = 'index$u81',
inference(demodulation,[status(thm)],[d393,d374]) ).
cnf(d395,plain,
'rselect$utail'(q20) = 'index$u78',
inference(superposition,[status(thm)],[d233,c4]) ).
cnf(d396,plain,
'index$u81' = 'index$u78',
inference(demodulation,[status(thm)],[d395,c187]) ).
cnf(d397,plain,
p('index$u75') = s('index$u78'),
inference(superposition,[status(thm)],[c186,d6]) ).
cnf(d398,plain,
p('index$u75') = s('index$u81'),
inference(demodulation,[status(thm)],[d397,d396]) ).
cnf(d399,plain,
s(s('index$u81')) = 'index$u75',
inference(superposition,[status(thm)],[d398,c12]) ).
cnf(d400,plain,
p('index$u81') = 'index$u75',
inference(demodulation,[status(thm)],[d399,d6]) ).
cnf(d401,plain,
p('index$u99') = 'index$u75',
inference(demodulation,[status(thm)],[d400,d394]) ).
cnf(d402,plain,
'index$u111' = 'index$u75',
inference(demodulation,[status(thm)],[d401,d372]) ).
cnf(d403,plain,
'rselect$utail'(q19) = 'index$u66',
inference(superposition,[status(thm)],[d228,c4]) ).
cnf(d404,plain,
'index$u75' = 'index$u66',
inference(demodulation,[status(thm)],[d403,c185]) ).
cnf(d405,plain,
s('index$u66') = p('index$u63'),
inference(superposition,[status(thm)],[c182,d336]) ).
cnf(d406,plain,
s('index$u75') = p('index$u63'),
inference(demodulation,[status(thm)],[d405,d404]) ).
cnf(d407,plain,
s(s('index$u75')) = 'index$u63',
inference(superposition,[status(thm)],[d406,c12]) ).
cnf(d408,plain,
p('index$u75') = 'index$u63',
inference(demodulation,[status(thm)],[d407,d6]) ).
cnf(d409,plain,
p('index$u111') = 'index$u63',
inference(demodulation,[status(thm)],[d408,d402]) ).
cnf(d410,plain,
'index$u105' = 'index$u63',
inference(demodulation,[status(thm)],[d409,d365]) ).
cnf(d411,plain,
'rselect$utail'(q18) = 'index$u60',
inference(superposition,[status(thm)],[d223,c4]) ).
cnf(d412,plain,
'index$u63' = 'index$u60',
inference(demodulation,[status(thm)],[d411,c181]) ).
cnf(d413,plain,
p('index$u60') = 'index$u57',
inference(superposition,[status(thm)],[c180,c11]) ).
cnf(d414,plain,
s('index$u57') = 'index$u60',
inference(superposition,[status(thm)],[d413,c12]) ).
cnf(d415,plain,
s('index$u57') = 'index$u63',
inference(demodulation,[status(thm)],[d414,d412]) ).
cnf(d416,plain,
'rselect$utail'(q17) = 'index$u54',
inference(superposition,[status(thm)],[d218,c4]) ).
cnf(d417,plain,
'index$u57' = 'index$u54',
inference(demodulation,[status(thm)],[d416,c178]) ).
cnf(d418,plain,
s('index$u54') = p('index$u51'),
inference(superposition,[status(thm)],[c177,d336]) ).
cnf(d419,plain,
s('index$u57') = p('index$u51'),
inference(demodulation,[status(thm)],[d418,d417]) ).
cnf(d420,plain,
'index$u63' = p('index$u51'),
inference(demodulation,[status(thm)],[d419,d415]) ).
cnf(d421,plain,
'index$u105' = p('index$u51'),
inference(demodulation,[status(thm)],[d420,d410]) ).
cnf(d422,plain,
'index$u105' = p('index$u15'),
inference(demodulation,[status(thm)],[d421,d361]) ).
cnf(d423,plain,
'index$u105' = 'index$u9',
inference(demodulation,[status(thm)],[d422,d32]) ).
cnf(d424,plain,
'rselect$utail'(q27) = 'index$u120',
inference(superposition,[status(thm)],[d102,c4]) ).
cnf(d425,plain,
'index$u123' = 'index$u120',
inference(demodulation,[status(thm)],[d424,c114]) ).
cnf(d426,plain,
p('index$u120') = 'index$u117',
inference(superposition,[status(thm)],[c113,c11]) ).
cnf(d427,plain,
s('index$u117') = 'index$u120',
inference(superposition,[status(thm)],[d426,c12]) ).
cnf(d428,plain,
s('index$u117') = 'index$u123',
inference(demodulation,[status(thm)],[d427,d425]) ).
cnf(d429,plain,
'rselect$utail'(q26) = 'index$u114',
inference(superposition,[status(thm)],[d97,c4]) ).
cnf(d430,plain,
'index$u117' = 'index$u114',
inference(demodulation,[status(thm)],[d429,c111]) ).
cnf(d431,plain,
s('index$u114') = p('index$u111'),
inference(superposition,[status(thm)],[c110,d336]) ).
cnf(d432,plain,
s('index$u117') = p('index$u111'),
inference(demodulation,[status(thm)],[d431,d430]) ).
cnf(d433,plain,
'index$u123' = p('index$u111'),
inference(demodulation,[status(thm)],[d432,d428]) ).
cnf(d434,plain,
'index$u123' = 'index$u105',
inference(demodulation,[status(thm)],[d433,d365]) ).
cnf(d435,plain,
'rselect$utail'(q28) = 'index$u126',
inference(superposition,[status(thm)],[d107,c4]) ).
cnf(d436,plain,
'index$u129' = 'index$u126',
inference(demodulation,[status(thm)],[d435,c116]) ).
cnf(d437,plain,
p('index$u126') = 'index$u123',
inference(superposition,[status(thm)],[c115,c11]) ).
cnf(d438,plain,
p('index$u129') = 'index$u123',
inference(demodulation,[status(thm)],[d437,d436]) ).
cnf(d439,plain,
'rselect$utail'(q30) = 'index$u144',
inference(superposition,[status(thm)],[d117,c4]) ).
cnf(d440,plain,
'index$u147' = 'index$u144',
inference(demodulation,[status(thm)],[d439,c122]) ).
cnf(d441,plain,
p('index$u144') = 'index$u141',
inference(superposition,[status(thm)],[c121,c11]) ).
cnf(d442,plain,
s('index$u141') = 'index$u144',
inference(superposition,[status(thm)],[d441,c12]) ).
cnf(d443,plain,
s('index$u141') = 'index$u147',
inference(demodulation,[status(thm)],[d442,d440]) ).
cnf(d444,plain,
'rselect$utail'(q29) = 'index$u132',
inference(superposition,[status(thm)],[d112,c4]) ).
cnf(d445,plain,
'index$u141' = 'index$u132',
inference(demodulation,[status(thm)],[d444,c120]) ).
cnf(d446,plain,
p('index$u129') = s('index$u132'),
inference(superposition,[status(thm)],[c117,d6]) ).
cnf(d447,plain,
p('index$u129') = s('index$u141'),
inference(demodulation,[status(thm)],[d446,d445]) ).
cnf(d448,plain,
p('index$u129') = 'index$u147',
inference(demodulation,[status(thm)],[d447,d443]) ).
cnf(d449,plain,
'index$u123' = 'index$u147',
inference(demodulation,[status(thm)],[d448,d438]) ).
cnf(d450,plain,
'index$u105' = 'index$u147',
inference(demodulation,[status(thm)],[d449,d434]) ).
cnf(d451,plain,
'rselect$utail'(q31) = 'index$u150',
inference(superposition,[status(thm)],[d122,c4]) ).
cnf(d452,plain,
'index$u153' = 'index$u150',
inference(demodulation,[status(thm)],[d451,c125]) ).
cnf(d453,plain,
p('index$u150') = 'index$u147',
inference(superposition,[status(thm)],[c124,c11]) ).
cnf(d454,plain,
p('index$u153') = 'index$u147',
inference(demodulation,[status(thm)],[d453,d452]) ).
cnf(d455,plain,
'rselect$utail'(q33) = 'index$u162',
inference(superposition,[status(thm)],[d132,c4]) ).
cnf(d456,plain,
'index$u165' = 'index$u162',
inference(demodulation,[status(thm)],[d455,c129]) ).
cnf(d457,plain,
p('index$u162') = 'index$u159',
inference(superposition,[status(thm)],[c128,c11]) ).
cnf(d458,plain,
s('index$u159') = 'index$u162',
inference(superposition,[status(thm)],[d457,c12]) ).
cnf(d459,plain,
s('index$u159') = 'index$u165',
inference(demodulation,[status(thm)],[d458,d456]) ).
cnf(d460,plain,
'rselect$utail'(q32) = 'index$u156',
inference(superposition,[status(thm)],[d127,c4]) ).
cnf(d461,plain,
'index$u159' = 'index$u156',
inference(demodulation,[status(thm)],[d460,c127]) ).
cnf(d462,plain,
s('index$u156') = p('index$u153'),
inference(superposition,[status(thm)],[c126,d336]) ).
cnf(d463,plain,
s('index$u159') = p('index$u153'),
inference(demodulation,[status(thm)],[d462,d461]) ).
cnf(d464,plain,
'index$u165' = p('index$u153'),
inference(demodulation,[status(thm)],[d463,d459]) ).
cnf(d465,plain,
'index$u165' = 'index$u147',
inference(demodulation,[status(thm)],[d464,d454]) ).
cnf(d466,plain,
'index$u165' = 'index$u105',
inference(demodulation,[status(thm)],[d465,d450]) ).
cnf(d467,plain,
'rselect$utail'(q34) = 'index$u168',
inference(superposition,[status(thm)],[d137,c4]) ).
cnf(d468,plain,
'index$u171' = 'index$u168',
inference(demodulation,[status(thm)],[d467,c131]) ).
cnf(d469,plain,
p('index$u168') = 'index$u165',
inference(superposition,[status(thm)],[c130,c11]) ).
cnf(d470,plain,
p('index$u171') = 'index$u165',
inference(demodulation,[status(thm)],[d469,d468]) ).
cnf(d471,plain,
'rselect$utail'(q36) = 'index$u180',
inference(superposition,[status(thm)],[d147,c4]) ).
cnf(d472,plain,
'index$u183' = 'index$u180',
inference(demodulation,[status(thm)],[d471,c136]) ).
cnf(d473,plain,
p('index$u180') = 'index$u177',
inference(superposition,[status(thm)],[c135,c11]) ).
cnf(d474,plain,
s('index$u177') = 'index$u180',
inference(superposition,[status(thm)],[d473,c12]) ).
cnf(d475,plain,
s('index$u177') = 'index$u183',
inference(demodulation,[status(thm)],[d474,d472]) ).
cnf(d476,plain,
'rselect$utail'(q35) = 'index$u174',
inference(superposition,[status(thm)],[d142,c4]) ).
cnf(d477,plain,
'index$u177' = 'index$u174',
inference(demodulation,[status(thm)],[d476,c133]) ).
cnf(d478,plain,
p('index$u171') = s('index$u174'),
inference(superposition,[status(thm)],[c132,d6]) ).
cnf(d479,plain,
p('index$u171') = s('index$u177'),
inference(demodulation,[status(thm)],[d478,d477]) ).
cnf(d480,plain,
p('index$u171') = 'index$u183',
inference(demodulation,[status(thm)],[d479,d475]) ).
cnf(d481,plain,
'index$u165' = 'index$u183',
inference(demodulation,[status(thm)],[d480,d470]) ).
cnf(d482,plain,
'index$u105' = 'index$u183',
inference(demodulation,[status(thm)],[d481,d466]) ).
cnf(d483,plain,
'rselect$utail'(q37) = 'index$u186',
inference(superposition,[status(thm)],[d152,c4]) ).
cnf(d484,plain,
'index$u189' = 'index$u186',
inference(demodulation,[status(thm)],[d483,c138]) ).
cnf(d485,plain,
p('index$u186') = 'index$u183',
inference(superposition,[status(thm)],[c137,c11]) ).
cnf(d486,plain,
p('index$u189') = 'index$u183',
inference(demodulation,[status(thm)],[d485,d484]) ).
cnf(d487,plain,
'rselect$utail'(q39) = 'index$u198',
inference(superposition,[status(thm)],[d162,c4]) ).
cnf(d488,plain,
'index$u207' = 'index$u198',
inference(demodulation,[status(thm)],[d487,c144]) ).
cnf(d489,plain,
p('index$u198') = 'index$u195',
inference(superposition,[status(thm)],[c141,c11]) ).
cnf(d490,plain,
s('index$u195') = 'index$u198',
inference(superposition,[status(thm)],[d489,c12]) ).
cnf(d491,plain,
s('index$u195') = 'index$u207',
inference(demodulation,[status(thm)],[d490,d488]) ).
cnf(d492,plain,
'rselect$utail'(q38) = 'index$u192',
inference(superposition,[status(thm)],[d157,c4]) ).
cnf(d493,plain,
'index$u195' = 'index$u192',
inference(demodulation,[status(thm)],[d492,c140]) ).
cnf(d494,plain,
s('index$u192') = p('index$u189'),
inference(superposition,[status(thm)],[c139,d336]) ).
cnf(d495,plain,
s('index$u195') = p('index$u189'),
inference(demodulation,[status(thm)],[d494,d493]) ).
cnf(d496,plain,
'index$u207' = p('index$u189'),
inference(demodulation,[status(thm)],[d495,d491]) ).
cnf(d497,plain,
'index$u207' = 'index$u183',
inference(demodulation,[status(thm)],[d496,d486]) ).
cnf(d498,plain,
'index$u207' = 'index$u105',
inference(demodulation,[status(thm)],[d497,d482]) ).
cnf(d499,plain,
'rselect$utail'(q40) = 'index$u210',
inference(superposition,[status(thm)],[d167,c4]) ).
cnf(d500,plain,
'index$u213' = 'index$u210',
inference(demodulation,[status(thm)],[d499,c147]) ).
cnf(d501,plain,
p('index$u207') = s('index$u210'),
inference(superposition,[status(thm)],[c146,d6]) ).
cnf(d502,plain,
p('index$u207') = s('index$u213'),
inference(demodulation,[status(thm)],[d501,d500]) ).
cnf(d503,plain,
p(s('index$u213')) = s('index$u207'),
inference(superposition,[status(thm)],[d502,d56]) ).
cnf(d504,plain,
'index$u213' = s('index$u207'),
inference(demodulation,[status(thm)],[d503,c11]) ).
cnf(d505,plain,
'index$u213' = s('index$u105'),
inference(demodulation,[status(thm)],[d504,d498]) ).
cnf(d506,plain,
'index$u213' = 'index$u111',
inference(demodulation,[status(thm)],[d505,d367]) ).
cnf(d507,plain,
'rselect$utail'(q41) = 'index$u216',
inference(superposition,[status(thm)],[d172,c4]) ).
cnf(d508,plain,
'index$u219' = 'index$u216',
inference(demodulation,[status(thm)],[d507,c149]) ).
cnf(d509,plain,
p('index$u216') = 'index$u213',
inference(superposition,[status(thm)],[c148,c11]) ).
cnf(d510,plain,
p('index$u219') = 'index$u213',
inference(demodulation,[status(thm)],[d509,d508]) ).
cnf(d511,plain,
'rselect$utail'(q42) = 'index$u222',
inference(superposition,[status(thm)],[d177,c4]) ).
cnf(d512,plain,
'index$u225' = 'index$u222',
inference(demodulation,[status(thm)],[d511,c151]) ).
cnf(d513,plain,
p('index$u219') = s('index$u222'),
inference(superposition,[status(thm)],[c150,d6]) ).
cnf(d514,plain,
p('index$u219') = s('index$u225'),
inference(demodulation,[status(thm)],[d513,d512]) ).
cnf(d515,plain,
p('index$u219') = 'index$u228',
inference(demodulation,[status(thm)],[d514,c152]) ).
cnf(d516,plain,
'index$u213' = 'index$u228',
inference(demodulation,[status(thm)],[d515,d510]) ).
cnf(d517,plain,
'index$u111' = 'index$u228',
inference(demodulation,[status(thm)],[d516,d506]) ).
cnf(d518,plain,
'rselect$utail'(q43) = 'index$u228',
inference(superposition,[status(thm)],[d88,c4]) ).
cnf(d519,plain,
'index$u263' = 'index$u228',
inference(demodulation,[status(thm)],[c165,d518]) ).
cnf(d520,plain,
p('index$u264') = s('index$u263'),
inference(superposition,[status(thm)],[c166,d6]) ).
cnf(d521,plain,
p('index$u264') = s('index$u228'),
inference(demodulation,[status(thm)],[d520,d519]) ).
cnf(d522,plain,
s(s('index$u228')) = 'index$u264',
inference(superposition,[status(thm)],[d521,c12]) ).
cnf(d523,plain,
p('index$u228') = 'index$u264',
inference(demodulation,[status(thm)],[d522,d6]) ).
cnf(d524,plain,
p('index$u111') = 'index$u264',
inference(demodulation,[status(thm)],[d523,d517]) ).
cnf(d525,plain,
'index$u105' = 'index$u264',
inference(demodulation,[status(thm)],[d524,d365]) ).
cnf(d526,plain,
p('index$u228') = 'index$u225',
inference(superposition,[status(thm)],[c152,c11]) ).
cnf(d527,plain,
p('index$u263') = 'index$u264',
inference(superposition,[status(thm)],[c166,c11]) ).
cnf(d528,plain,
p('index$u228') = 'index$u264',
inference(demodulation,[status(thm)],[d527,d519]) ).
cnf(d529,plain,
'index$u225' = 'index$u264',
inference(demodulation,[status(thm)],[d528,d526]) ).
cnf(d530,plain,
'index$u225' = 'index$u105',
inference(demodulation,[status(thm)],[d529,d525]) ).
cnf(d531,plain,
'index$u225' = 'index$u9',
inference(demodulation,[status(thm)],[d530,d423]) ).
cnf(d532,plain,
'elem$u265' = select('earray$u260','index$u225'),
inference(demodulation,[status(thm)],[c104,d529]) ).
cnf(d533,plain,
'elem$u265' = select('earray$u260','index$u9'),
inference(demodulation,[status(thm)],[d532,d531]) ).
cnf(d534,plain,
'elem$u265' = 'elem$u262',
inference(demodulation,[status(thm)],[d533,d300]) ).
cnf(d535,plain,
'elem$u262' != 'elem$u262',
inference(demodulation,[status(thm)],[c326,d534]) ).
cnf(d536,plain,
$false,
inference(equality_resolution,[status(thm)],[d535]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n014.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 14:31:02 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.97/4.47 % SZS status Unsatisfiable for theBenchmark.p
% 28.97/4.47 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------