%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV571-1.049 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.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 : Fri Sep 25 03:13:43 PM UTC 2026
% Result : Unsatisfiable 18.93s 71.94s
% Output : Proof 18.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 208
% Number of leaves : 187
% Syntax : Number of formulae : 1027 ( 672 unt; 0 def)
% Number of atoms : 1680 (1679 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 672 ( 19 ~; 653 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 281 ( 281 usr; 277 con; 0-3 aty)
% Number of variables : 194 ( 7 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f183,hypothesis,
index_297 = select(q49,head),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp173) ).
fof(f183_nnf,plain,
index_297 = select(q49,head),
inference(nnf_transformation,[status(thm)],[f183]) ).
cnf(c183,plain,
index_297 = select(q49,head),
inference(cnf_transformation,[status(esa)],[f183_nnf]) ).
cnf(f356,hypothesis,
q49 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp346) ).
fof(f356_nnf,plain,
q49 = queue_265,
inference(nnf_transformation,[status(thm)],[f356]) ).
cnf(c356,plain,
q49 = queue_265,
inference(cnf_transformation,[status(esa)],[f356_nnf]) ).
cnf(f275,hypothesis,
queue_265 = store(queue_263,tail,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp265) ).
fof(f275_nnf,plain,
queue_265 = store(queue_263,tail,index_264),
inference(nnf_transformation,[status(thm)],[f275]) ).
cnf(c275,plain,
queue_265 = store(queue_263,tail,index_264),
inference(cnf_transformation,[status(esa)],[f275_nnf]) ).
cnf(f1,axiom,
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f1_nnf,plain,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p1233,plain,
( select(queue_265,X0) = select(queue_263,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c275,c1]) ).
cnf(p3840,plain,
( select(q49,X0) = select(queue_263,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c356,p1233]) ).
cnf(p5062,plain,
( index_297 = select(queue_263,head)
| tail = head ),
inference(superposition,[status(thm)],[c183,p3840]) ).
cnf(f274,hypothesis,
queue_263 = store(q48,seq,earray_262),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp264) ).
fof(f274_nnf,plain,
queue_263 = store(q48,seq,earray_262),
inference(nnf_transformation,[status(thm)],[f274]) ).
cnf(c274,plain,
queue_263 = store(q48,seq,earray_262),
inference(cnf_transformation,[status(esa)],[f274_nnf]) ).
cnf(p1231,plain,
( select(queue_263,X0) = select(q48,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c274,c1]) ).
cnf(p5064,plain,
( index_297 = select(q48,head)
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p5062,p1231]) ).
cnf(f355,hypothesis,
q48 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp345) ).
fof(f355_nnf,plain,
q48 = queue_259,
inference(nnf_transformation,[status(thm)],[f355]) ).
cnf(c355,plain,
q48 = queue_259,
inference(cnf_transformation,[status(esa)],[f355_nnf]) ).
cnf(f273,hypothesis,
queue_259 = store(queue_257,tail,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp263) ).
fof(f273_nnf,plain,
queue_259 = store(queue_257,tail,index_258),
inference(nnf_transformation,[status(thm)],[f273]) ).
cnf(c273,plain,
queue_259 = store(queue_257,tail,index_258),
inference(cnf_transformation,[status(esa)],[f273_nnf]) ).
cnf(p1215,plain,
( select(queue_259,X0) = select(queue_257,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c273,c1]) ).
cnf(p3834,plain,
( select(q48,X0) = select(queue_257,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c355,p1215]) ).
cnf(p5595,plain,
( index_297 = select(queue_257,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p5064,p3834]) ).
cnf(p11513,plain,
( index_297 = select(queue_257,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p5595]) ).
cnf(f272,hypothesis,
queue_257 = store(q47,seq,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp262) ).
fof(f272_nnf,plain,
queue_257 = store(q47,seq,earray_256),
inference(nnf_transformation,[status(thm)],[f272]) ).
cnf(c272,plain,
queue_257 = store(q47,seq,earray_256),
inference(cnf_transformation,[status(esa)],[f272_nnf]) ).
cnf(p1209,plain,
( select(queue_257,X0) = select(q47,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c272,c1]) ).
cnf(p11515,plain,
( index_297 = select(q47,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p11513,p1209]) ).
cnf(p12117,plain,
( index_297 = select(q47,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p11515]) ).
cnf(f354,hypothesis,
q47 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp344) ).
fof(f354_nnf,plain,
q47 = queue_253,
inference(nnf_transformation,[status(thm)],[f354]) ).
cnf(c354,plain,
q47 = queue_253,
inference(cnf_transformation,[status(esa)],[f354_nnf]) ).
cnf(f271,hypothesis,
queue_253 = store(queue_251,tail,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp261) ).
fof(f271_nnf,plain,
queue_253 = store(queue_251,tail,index_252),
inference(nnf_transformation,[status(thm)],[f271]) ).
cnf(c271,plain,
queue_253 = store(queue_251,tail,index_252),
inference(cnf_transformation,[status(esa)],[f271_nnf]) ).
cnf(p1206,plain,
( select(queue_253,X0) = select(queue_251,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c271,c1]) ).
cnf(p3826,plain,
( select(q47,X0) = select(queue_251,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c354,p1206]) ).
cnf(p12124,plain,
( index_297 = select(queue_251,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12117,p3826]) ).
cnf(p12282,plain,
( index_297 = select(queue_251,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12124]) ).
cnf(f270,hypothesis,
queue_251 = store(q46,seq,earray_250),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp260) ).
fof(f270_nnf,plain,
queue_251 = store(q46,seq,earray_250),
inference(nnf_transformation,[status(thm)],[f270]) ).
cnf(c270,plain,
queue_251 = store(q46,seq,earray_250),
inference(cnf_transformation,[status(esa)],[f270_nnf]) ).
cnf(p1188,plain,
( select(queue_251,X0) = select(q46,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c270,c1]) ).
cnf(p12284,plain,
( index_297 = select(q46,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12282,p1188]) ).
cnf(p12342,plain,
( index_297 = select(q46,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12284]) ).
cnf(f353,hypothesis,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp343) ).
fof(f353_nnf,plain,
q46 = queue_247,
inference(nnf_transformation,[status(thm)],[f353]) ).
cnf(c353,plain,
q46 = queue_247,
inference(cnf_transformation,[status(esa)],[f353_nnf]) ).
cnf(f268,hypothesis,
queue_247 = store(queue_245,tail,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp258) ).
fof(f268_nnf,plain,
queue_247 = store(queue_245,tail,index_246),
inference(nnf_transformation,[status(thm)],[f268]) ).
cnf(c268,plain,
queue_247 = store(queue_245,tail,index_246),
inference(cnf_transformation,[status(esa)],[f268_nnf]) ).
cnf(p1181,plain,
( select(queue_247,X0) = select(queue_245,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c268,c1]) ).
cnf(p3811,plain,
( select(q46,X0) = select(queue_245,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c353,p1181]) ).
cnf(p12344,plain,
( index_297 = select(queue_245,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12342,p3811]) ).
cnf(p12389,plain,
( index_297 = select(queue_245,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12344]) ).
cnf(f267,hypothesis,
queue_245 = store(q45,seq,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp257) ).
fof(f267_nnf,plain,
queue_245 = store(q45,seq,earray_244),
inference(nnf_transformation,[status(thm)],[f267]) ).
cnf(c267,plain,
queue_245 = store(q45,seq,earray_244),
inference(cnf_transformation,[status(esa)],[f267_nnf]) ).
cnf(p1162,plain,
( select(queue_245,X0) = select(q45,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c267,c1]) ).
cnf(p12391,plain,
( index_297 = select(q45,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12389,p1162]) ).
cnf(p12423,plain,
( index_297 = select(q45,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12391]) ).
cnf(f352,hypothesis,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp342) ).
fof(f352_nnf,plain,
q45 = queue_241,
inference(nnf_transformation,[status(thm)],[f352]) ).
cnf(c352,plain,
q45 = queue_241,
inference(cnf_transformation,[status(esa)],[f352_nnf]) ).
cnf(f266,hypothesis,
queue_241 = store(queue_239,tail,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp256) ).
fof(f266_nnf,plain,
queue_241 = store(queue_239,tail,index_240),
inference(nnf_transformation,[status(thm)],[f266]) ).
cnf(c266,plain,
queue_241 = store(queue_239,tail,index_240),
inference(cnf_transformation,[status(esa)],[f266_nnf]) ).
cnf(p1159,plain,
( select(queue_241,X0) = select(queue_239,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c266,c1]) ).
cnf(p3801,plain,
( select(q45,X0) = select(queue_239,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c352,p1159]) ).
cnf(p12428,plain,
( index_297 = select(queue_239,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12423,p3801]) ).
cnf(p12469,plain,
( index_297 = select(queue_239,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12428]) ).
cnf(f265,hypothesis,
queue_239 = store(q44,seq,earray_238),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp255) ).
fof(f265_nnf,plain,
queue_239 = store(q44,seq,earray_238),
inference(nnf_transformation,[status(thm)],[f265]) ).
cnf(c265,plain,
queue_239 = store(q44,seq,earray_238),
inference(cnf_transformation,[status(esa)],[f265_nnf]) ).
cnf(p1157,plain,
( select(queue_239,X0) = select(q44,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c265,c1]) ).
cnf(p12471,plain,
( index_297 = select(q44,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12469,p1157]) ).
cnf(p12511,plain,
( index_297 = select(q44,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12471]) ).
cnf(f351,hypothesis,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp341) ).
fof(f351_nnf,plain,
q44 = queue_235,
inference(nnf_transformation,[status(thm)],[f351]) ).
cnf(c351,plain,
q44 = queue_235,
inference(cnf_transformation,[status(esa)],[f351_nnf]) ).
cnf(f264,hypothesis,
queue_235 = store(queue_233,tail,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp254) ).
fof(f264_nnf,plain,
queue_235 = store(queue_233,tail,index_234),
inference(nnf_transformation,[status(thm)],[f264]) ).
cnf(c264,plain,
queue_235 = store(queue_233,tail,index_234),
inference(cnf_transformation,[status(esa)],[f264_nnf]) ).
cnf(p1138,plain,
( select(queue_235,X0) = select(queue_233,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c264,c1]) ).
cnf(p3788,plain,
( select(q44,X0) = select(queue_233,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c351,p1138]) ).
cnf(p12517,plain,
( index_297 = select(queue_233,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12511,p3788]) ).
cnf(p12562,plain,
( index_297 = select(queue_233,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12517]) ).
cnf(f263,hypothesis,
queue_233 = store(q43,seq,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp253) ).
fof(f263_nnf,plain,
queue_233 = store(q43,seq,earray_232),
inference(nnf_transformation,[status(thm)],[f263]) ).
cnf(c263,plain,
queue_233 = store(q43,seq,earray_232),
inference(cnf_transformation,[status(esa)],[f263_nnf]) ).
cnf(p1136,plain,
( select(queue_233,X0) = select(q43,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c263,c1]) ).
cnf(p12564,plain,
( index_297 = select(q43,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12562,p1136]) ).
cnf(p12608,plain,
( index_297 = select(q43,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12564]) ).
cnf(f350,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp340) ).
fof(f350_nnf,plain,
q43 = queue_229,
inference(nnf_transformation,[status(thm)],[f350]) ).
cnf(c350,plain,
q43 = queue_229,
inference(cnf_transformation,[status(esa)],[f350_nnf]) ).
cnf(f261,hypothesis,
queue_229 = store(queue_227,tail,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp251) ).
fof(f261_nnf,plain,
queue_229 = store(queue_227,tail,index_228),
inference(nnf_transformation,[status(thm)],[f261]) ).
cnf(c261,plain,
queue_229 = store(queue_227,tail,index_228),
inference(cnf_transformation,[status(esa)],[f261_nnf]) ).
cnf(p1114,plain,
( select(queue_229,X0) = select(queue_227,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c261,c1]) ).
cnf(p3778,plain,
( select(q43,X0) = select(queue_227,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c350,p1114]) ).
cnf(p12615,plain,
( index_297 = select(queue_227,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12608,p3778]) ).
cnf(p12651,plain,
( index_297 = select(queue_227,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12615]) ).
cnf(f260,hypothesis,
queue_227 = store(q42,seq,earray_226),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp250) ).
fof(f260_nnf,plain,
queue_227 = store(q42,seq,earray_226),
inference(nnf_transformation,[status(thm)],[f260]) ).
cnf(c260,plain,
queue_227 = store(q42,seq,earray_226),
inference(cnf_transformation,[status(esa)],[f260_nnf]) ).
cnf(p1112,plain,
( select(queue_227,X0) = select(q42,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c260,c1]) ).
cnf(p12653,plain,
( index_297 = select(q42,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12651,p1112]) ).
cnf(p12690,plain,
( index_297 = select(q42,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12653]) ).
cnf(f349,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp339) ).
fof(f349_nnf,plain,
q42 = queue_223,
inference(nnf_transformation,[status(thm)],[f349]) ).
cnf(c349,plain,
q42 = queue_223,
inference(cnf_transformation,[status(esa)],[f349_nnf]) ).
cnf(f259,hypothesis,
queue_223 = store(queue_221,tail,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp249) ).
fof(f259_nnf,plain,
queue_223 = store(queue_221,tail,index_222),
inference(nnf_transformation,[status(thm)],[f259]) ).
cnf(c259,plain,
queue_223 = store(queue_221,tail,index_222),
inference(cnf_transformation,[status(esa)],[f259_nnf]) ).
cnf(p1092,plain,
( select(queue_223,X0) = select(queue_221,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c259,c1]) ).
cnf(p3772,plain,
( select(q42,X0) = select(queue_221,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c349,p1092]) ).
cnf(p12692,plain,
( index_297 = select(queue_221,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12690,p3772]) ).
cnf(p12733,plain,
( index_297 = select(queue_221,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12692]) ).
cnf(f258,hypothesis,
queue_221 = store(q41,seq,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp248) ).
fof(f258_nnf,plain,
queue_221 = store(q41,seq,earray_220),
inference(nnf_transformation,[status(thm)],[f258]) ).
cnf(c258,plain,
queue_221 = store(q41,seq,earray_220),
inference(cnf_transformation,[status(esa)],[f258_nnf]) ).
cnf(p1090,plain,
( select(queue_221,X0) = select(q41,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c258,c1]) ).
cnf(p12739,plain,
( index_297 = select(q41,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12733,p1090]) ).
cnf(p12779,plain,
( index_297 = select(q41,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12739]) ).
cnf(f348,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp338) ).
fof(f348_nnf,plain,
q41 = queue_217,
inference(nnf_transformation,[status(thm)],[f348]) ).
cnf(c348,plain,
q41 = queue_217,
inference(cnf_transformation,[status(esa)],[f348_nnf]) ).
cnf(f257,hypothesis,
queue_217 = store(queue_215,tail,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp247) ).
fof(f257_nnf,plain,
queue_217 = store(queue_215,tail,index_216),
inference(nnf_transformation,[status(thm)],[f257]) ).
cnf(c257,plain,
queue_217 = store(queue_215,tail,index_216),
inference(cnf_transformation,[status(esa)],[f257_nnf]) ).
cnf(p1087,plain,
( select(queue_217,X0) = select(queue_215,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c257,c1]) ).
cnf(p3766,plain,
( select(q41,X0) = select(queue_215,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c348,p1087]) ).
cnf(p12781,plain,
( index_297 = select(queue_215,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12779,p3766]) ).
cnf(p12818,plain,
( index_297 = select(queue_215,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12781]) ).
cnf(f256,hypothesis,
queue_215 = store(q40,seq,earray_214),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp246) ).
fof(f256_nnf,plain,
queue_215 = store(q40,seq,earray_214),
inference(nnf_transformation,[status(thm)],[f256]) ).
cnf(c256,plain,
queue_215 = store(q40,seq,earray_214),
inference(cnf_transformation,[status(esa)],[f256_nnf]) ).
cnf(p1067,plain,
( select(queue_215,X0) = select(q40,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c256,c1]) ).
cnf(p12820,plain,
( index_297 = select(q40,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12818,p1067]) ).
cnf(p12853,plain,
( index_297 = select(q40,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12820]) ).
cnf(f347,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp337) ).
fof(f347_nnf,plain,
q40 = queue_211,
inference(nnf_transformation,[status(thm)],[f347]) ).
cnf(c347,plain,
q40 = queue_211,
inference(cnf_transformation,[status(esa)],[f347_nnf]) ).
cnf(f255,hypothesis,
queue_211 = store(queue_209,tail,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f255_nnf,plain,
queue_211 = store(queue_209,tail,index_210),
inference(nnf_transformation,[status(thm)],[f255]) ).
cnf(c255,plain,
queue_211 = store(queue_209,tail,index_210),
inference(cnf_transformation,[status(esa)],[f255_nnf]) ).
cnf(p1064,plain,
( select(queue_211,X0) = select(queue_209,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c255,c1]) ).
cnf(p3757,plain,
( select(q40,X0) = select(queue_209,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c347,p1064]) ).
cnf(p12855,plain,
( index_297 = select(queue_209,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12853,p3757]) ).
cnf(p12901,plain,
( index_297 = select(queue_209,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12855]) ).
cnf(f254,hypothesis,
queue_209 = store(q39,seq,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f254_nnf,plain,
queue_209 = store(q39,seq,earray_208),
inference(nnf_transformation,[status(thm)],[f254]) ).
cnf(c254,plain,
queue_209 = store(q39,seq,earray_208),
inference(cnf_transformation,[status(esa)],[f254_nnf]) ).
cnf(p1062,plain,
( select(queue_209,X0) = select(q39,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c254,c1]) ).
cnf(p12903,plain,
( index_297 = select(q39,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12901,p1062]) ).
cnf(p12937,plain,
( index_297 = select(q39,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12903]) ).
cnf(f345,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp335) ).
fof(f345_nnf,plain,
q39 = queue_199,
inference(nnf_transformation,[status(thm)],[f345]) ).
cnf(c345,plain,
q39 = queue_199,
inference(cnf_transformation,[status(esa)],[f345_nnf]) ).
cnf(f251,hypothesis,
queue_199 = store(queue_197,tail,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f251_nnf,plain,
queue_199 = store(queue_197,tail,index_198),
inference(nnf_transformation,[status(thm)],[f251]) ).
cnf(c251,plain,
queue_199 = store(queue_197,tail,index_198),
inference(cnf_transformation,[status(esa)],[f251_nnf]) ).
cnf(p1024,plain,
( select(queue_199,X0) = select(queue_197,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c251,c1]) ).
cnf(p3734,plain,
( select(q39,X0) = select(queue_197,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c345,p1024]) ).
cnf(p12939,plain,
( index_297 = select(queue_197,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12937,p3734]) ).
cnf(p12979,plain,
( index_297 = select(queue_197,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12939]) ).
cnf(f250,hypothesis,
queue_197 = store(q38,seq,earray_196),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f250_nnf,plain,
queue_197 = store(q38,seq,earray_196),
inference(nnf_transformation,[status(thm)],[f250]) ).
cnf(c250,plain,
queue_197 = store(q38,seq,earray_196),
inference(cnf_transformation,[status(esa)],[f250_nnf]) ).
cnf(p1016,plain,
( select(queue_197,X0) = select(q38,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c250,c1]) ).
cnf(p12981,plain,
( index_297 = select(q38,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p12979,p1016]) ).
cnf(p13016,plain,
( index_297 = select(q38,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p12981]) ).
cnf(f344,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp334) ).
fof(f344_nnf,plain,
q38 = queue_193,
inference(nnf_transformation,[status(thm)],[f344]) ).
cnf(c344,plain,
q38 = queue_193,
inference(cnf_transformation,[status(esa)],[f344_nnf]) ).
cnf(f249,hypothesis,
queue_193 = store(queue_191,tail,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f249_nnf,plain,
queue_193 = store(queue_191,tail,index_192),
inference(nnf_transformation,[status(thm)],[f249]) ).
cnf(c249,plain,
queue_193 = store(queue_191,tail,index_192),
inference(cnf_transformation,[status(esa)],[f249_nnf]) ).
cnf(p1010,plain,
( select(queue_193,X0) = select(queue_191,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c249,c1]) ).
cnf(p3473,plain,
( select(q38,X0) = select(queue_191,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c344,p1010]) ).
cnf(p13018,plain,
( index_297 = select(queue_191,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13016,p3473]) ).
cnf(p13056,plain,
( index_297 = select(queue_191,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13018]) ).
cnf(f248,hypothesis,
queue_191 = store(q37,seq,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f248_nnf,plain,
queue_191 = store(q37,seq,earray_190),
inference(nnf_transformation,[status(thm)],[f248]) ).
cnf(c248,plain,
queue_191 = store(q37,seq,earray_190),
inference(cnf_transformation,[status(esa)],[f248_nnf]) ).
cnf(p1004,plain,
( select(queue_191,X0) = select(q37,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c248,c1]) ).
cnf(p13058,plain,
( index_297 = select(q37,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13056,p1004]) ).
cnf(p13089,plain,
( index_297 = select(q37,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13058]) ).
cnf(f343,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp333) ).
fof(f343_nnf,plain,
q37 = queue_187,
inference(nnf_transformation,[status(thm)],[f343]) ).
cnf(c343,plain,
q37 = queue_187,
inference(cnf_transformation,[status(esa)],[f343_nnf]) ).
cnf(f246,hypothesis,
queue_187 = store(queue_185,tail,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f246_nnf,plain,
queue_187 = store(queue_185,tail,index_186),
inference(nnf_transformation,[status(thm)],[f246]) ).
cnf(c246,plain,
queue_187 = store(queue_185,tail,index_186),
inference(cnf_transformation,[status(esa)],[f246_nnf]) ).
cnf(p990,plain,
( select(queue_187,X0) = select(queue_185,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c246,c1]) ).
cnf(p3396,plain,
( select(q37,X0) = select(queue_185,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c343,p990]) ).
cnf(p13092,plain,
( index_297 = select(queue_185,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13089,p3396]) ).
cnf(p13131,plain,
( index_297 = select(queue_185,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13092]) ).
cnf(f245,hypothesis,
queue_185 = store(q36,seq,earray_184),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f245_nnf,plain,
queue_185 = store(q36,seq,earray_184),
inference(nnf_transformation,[status(thm)],[f245]) ).
cnf(c245,plain,
queue_185 = store(q36,seq,earray_184),
inference(cnf_transformation,[status(esa)],[f245_nnf]) ).
cnf(p984,plain,
( select(queue_185,X0) = select(q36,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c245,c1]) ).
cnf(p13135,plain,
( index_297 = select(q36,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13131,p984]) ).
cnf(p13169,plain,
( index_297 = select(q36,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13135]) ).
cnf(f342,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp332) ).
fof(f342_nnf,plain,
q36 = queue_181,
inference(nnf_transformation,[status(thm)],[f342]) ).
cnf(c342,plain,
q36 = queue_181,
inference(cnf_transformation,[status(esa)],[f342_nnf]) ).
cnf(f244,hypothesis,
queue_181 = store(queue_179,tail,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f244_nnf,plain,
queue_181 = store(queue_179,tail,index_180),
inference(nnf_transformation,[status(thm)],[f244]) ).
cnf(c244,plain,
queue_181 = store(queue_179,tail,index_180),
inference(cnf_transformation,[status(esa)],[f244_nnf]) ).
cnf(p977,plain,
( select(queue_181,X0) = select(queue_179,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c244,c1]) ).
cnf(p3317,plain,
( select(q36,X0) = select(queue_179,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c342,p977]) ).
cnf(p13171,plain,
( index_297 = select(queue_179,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13169,p3317]) ).
cnf(p13204,plain,
( index_297 = select(queue_179,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13171]) ).
cnf(f243,hypothesis,
queue_179 = store(q35,seq,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f243_nnf,plain,
queue_179 = store(q35,seq,earray_178),
inference(nnf_transformation,[status(thm)],[f243]) ).
cnf(c243,plain,
queue_179 = store(q35,seq,earray_178),
inference(cnf_transformation,[status(esa)],[f243_nnf]) ).
cnf(p971,plain,
( select(queue_179,X0) = select(q35,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c243,c1]) ).
cnf(p13206,plain,
( index_297 = select(q35,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13204,p971]) ).
cnf(p13242,plain,
( index_297 = select(q35,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13206]) ).
cnf(f341,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp331) ).
fof(f341_nnf,plain,
q35 = queue_175,
inference(nnf_transformation,[status(thm)],[f341]) ).
cnf(c341,plain,
q35 = queue_175,
inference(cnf_transformation,[status(esa)],[f341_nnf]) ).
cnf(f242,hypothesis,
queue_175 = store(queue_173,tail,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f242_nnf,plain,
queue_175 = store(queue_173,tail,index_174),
inference(nnf_transformation,[status(thm)],[f242]) ).
cnf(c242,plain,
queue_175 = store(queue_173,tail,index_174),
inference(cnf_transformation,[status(esa)],[f242_nnf]) ).
cnf(p964,plain,
( select(queue_175,X0) = select(queue_173,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c242,c1]) ).
cnf(p3306,plain,
( select(q35,X0) = select(queue_173,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c341,p964]) ).
cnf(p13244,plain,
( index_297 = select(queue_173,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13242,p3306]) ).
cnf(p13279,plain,
( index_297 = select(queue_173,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13244]) ).
cnf(f241,hypothesis,
queue_173 = store(q34,seq,earray_172),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f241_nnf,plain,
queue_173 = store(q34,seq,earray_172),
inference(nnf_transformation,[status(thm)],[f241]) ).
cnf(c241,plain,
queue_173 = store(q34,seq,earray_172),
inference(cnf_transformation,[status(esa)],[f241_nnf]) ).
cnf(p958,plain,
( select(queue_173,X0) = select(q34,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c241,c1]) ).
cnf(p13282,plain,
( index_297 = select(q34,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13279,p958]) ).
cnf(p13322,plain,
( index_297 = select(q34,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13282]) ).
cnf(f340,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp330) ).
fof(f340_nnf,plain,
q34 = queue_169,
inference(nnf_transformation,[status(thm)],[f340]) ).
cnf(c340,plain,
q34 = queue_169,
inference(cnf_transformation,[status(esa)],[f340_nnf]) ).
cnf(f239,hypothesis,
queue_169 = store(queue_167,tail,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f239_nnf,plain,
queue_169 = store(queue_167,tail,index_168),
inference(nnf_transformation,[status(thm)],[f239]) ).
cnf(c239,plain,
queue_169 = store(queue_167,tail,index_168),
inference(cnf_transformation,[status(esa)],[f239_nnf]) ).
cnf(p945,plain,
( select(queue_169,X0) = select(queue_167,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c239,c1]) ).
cnf(p3175,plain,
( select(q34,X0) = select(queue_167,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c340,p945]) ).
cnf(p13324,plain,
( index_297 = select(queue_167,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13322,p3175]) ).
cnf(p13360,plain,
( index_297 = select(queue_167,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13324]) ).
cnf(f238,hypothesis,
queue_167 = store(q33,seq,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f238_nnf,plain,
queue_167 = store(q33,seq,earray_166),
inference(nnf_transformation,[status(thm)],[f238]) ).
cnf(c238,plain,
queue_167 = store(q33,seq,earray_166),
inference(cnf_transformation,[status(esa)],[f238_nnf]) ).
cnf(p939,plain,
( select(queue_167,X0) = select(q33,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c238,c1]) ).
cnf(p13362,plain,
( index_297 = select(q33,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13360,p939]) ).
cnf(p13402,plain,
( index_297 = select(q33,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13362]) ).
cnf(f339,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp329) ).
fof(f339_nnf,plain,
q33 = queue_163,
inference(nnf_transformation,[status(thm)],[f339]) ).
cnf(c339,plain,
q33 = queue_163,
inference(cnf_transformation,[status(esa)],[f339_nnf]) ).
cnf(f237,hypothesis,
queue_163 = store(queue_161,tail,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f237_nnf,plain,
queue_163 = store(queue_161,tail,index_162),
inference(nnf_transformation,[status(thm)],[f237]) ).
cnf(c237,plain,
queue_163 = store(queue_161,tail,index_162),
inference(cnf_transformation,[status(esa)],[f237_nnf]) ).
cnf(p934,plain,
( select(queue_163,X0) = select(queue_161,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c237,c1]) ).
cnf(p3131,plain,
( select(q33,X0) = select(queue_161,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c339,p934]) ).
cnf(p13404,plain,
( index_297 = select(queue_161,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13402,p3131]) ).
cnf(p13439,plain,
( index_297 = select(queue_161,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13404]) ).
cnf(f236,hypothesis,
queue_161 = store(q32,seq,earray_160),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f236_nnf,plain,
queue_161 = store(q32,seq,earray_160),
inference(nnf_transformation,[status(thm)],[f236]) ).
cnf(c236,plain,
queue_161 = store(q32,seq,earray_160),
inference(cnf_transformation,[status(esa)],[f236_nnf]) ).
cnf(p932,plain,
( select(queue_161,X0) = select(q32,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c236,c1]) ).
cnf(p13442,plain,
( index_297 = select(q32,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13439,p932]) ).
cnf(p13476,plain,
( index_297 = select(q32,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13442]) ).
cnf(f338,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp328) ).
fof(f338_nnf,plain,
q32 = queue_157,
inference(nnf_transformation,[status(thm)],[f338]) ).
cnf(c338,plain,
q32 = queue_157,
inference(cnf_transformation,[status(esa)],[f338_nnf]) ).
cnf(f235,hypothesis,
queue_157 = store(queue_155,tail,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f235_nnf,plain,
queue_157 = store(queue_155,tail,index_156),
inference(nnf_transformation,[status(thm)],[f235]) ).
cnf(c235,plain,
queue_157 = store(queue_155,tail,index_156),
inference(cnf_transformation,[status(esa)],[f235_nnf]) ).
cnf(p929,plain,
( select(queue_157,X0) = select(queue_155,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c235,c1]) ).
cnf(p3125,plain,
( select(q32,X0) = select(queue_155,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c338,p929]) ).
cnf(p13478,plain,
( index_297 = select(queue_155,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13476,p3125]) ).
cnf(p13517,plain,
( index_297 = select(queue_155,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13478]) ).
cnf(f234,hypothesis,
queue_155 = store(q31,seq,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f234_nnf,plain,
queue_155 = store(q31,seq,earray_154),
inference(nnf_transformation,[status(thm)],[f234]) ).
cnf(c234,plain,
queue_155 = store(q31,seq,earray_154),
inference(cnf_transformation,[status(esa)],[f234_nnf]) ).
cnf(p927,plain,
( select(queue_155,X0) = select(q31,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c234,c1]) ).
cnf(p13519,plain,
( index_297 = select(q31,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13517,p927]) ).
cnf(p13551,plain,
( index_297 = select(q31,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13519]) ).
cnf(f337,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp327) ).
fof(f337_nnf,plain,
q31 = queue_151,
inference(nnf_transformation,[status(thm)],[f337]) ).
cnf(c337,plain,
q31 = queue_151,
inference(cnf_transformation,[status(esa)],[f337_nnf]) ).
cnf(f233,hypothesis,
queue_151 = store(queue_149,tail,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f233_nnf,plain,
queue_151 = store(queue_149,tail,index_150),
inference(nnf_transformation,[status(thm)],[f233]) ).
cnf(c233,plain,
queue_151 = store(queue_149,tail,index_150),
inference(cnf_transformation,[status(esa)],[f233_nnf]) ).
cnf(p924,plain,
( select(queue_151,X0) = select(queue_149,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c233,c1]) ).
cnf(p3056,plain,
( select(q31,X0) = select(queue_149,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c337,p924]) ).
cnf(p13553,plain,
( index_297 = select(queue_149,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13551,p3056]) ).
cnf(p13592,plain,
( index_297 = select(queue_149,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13553]) ).
cnf(f232,hypothesis,
queue_149 = store(q30,seq,earray_148),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f232_nnf,plain,
queue_149 = store(q30,seq,earray_148),
inference(nnf_transformation,[status(thm)],[f232]) ).
cnf(c232,plain,
queue_149 = store(q30,seq,earray_148),
inference(cnf_transformation,[status(esa)],[f232_nnf]) ).
cnf(p922,plain,
( select(queue_149,X0) = select(q30,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c232,c1]) ).
cnf(p13594,plain,
( index_297 = select(q30,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13592,p922]) ).
cnf(p13638,plain,
( index_297 = select(q30,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13594]) ).
cnf(f336,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp326) ).
fof(f336_nnf,plain,
q30 = queue_145,
inference(nnf_transformation,[status(thm)],[f336]) ).
cnf(c336,plain,
q30 = queue_145,
inference(cnf_transformation,[status(esa)],[f336_nnf]) ).
cnf(f231,hypothesis,
queue_145 = store(queue_143,tail,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f231_nnf,plain,
queue_145 = store(queue_143,tail,index_144),
inference(nnf_transformation,[status(thm)],[f231]) ).
cnf(c231,plain,
queue_145 = store(queue_143,tail,index_144),
inference(cnf_transformation,[status(esa)],[f231_nnf]) ).
cnf(p919,plain,
( select(queue_145,X0) = select(queue_143,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c231,c1]) ).
cnf(p3050,plain,
( select(q30,X0) = select(queue_143,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c336,p919]) ).
cnf(p13640,plain,
( index_297 = select(queue_143,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13638,p3050]) ).
cnf(p13692,plain,
( index_297 = select(queue_143,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13640]) ).
cnf(f230,hypothesis,
queue_143 = store(q29,seq,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f230_nnf,plain,
queue_143 = store(q29,seq,earray_142),
inference(nnf_transformation,[status(thm)],[f230]) ).
cnf(c230,plain,
queue_143 = store(q29,seq,earray_142),
inference(cnf_transformation,[status(esa)],[f230_nnf]) ).
cnf(p917,plain,
( select(queue_143,X0) = select(q29,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c230,c1]) ).
cnf(p13698,plain,
( index_297 = select(q29,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13692,p917]) ).
cnf(p13736,plain,
( index_297 = select(q29,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13698]) ).
cnf(f334,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp324) ).
fof(f334_nnf,plain,
q29 = queue_133,
inference(nnf_transformation,[status(thm)],[f334]) ).
cnf(c334,plain,
q29 = queue_133,
inference(cnf_transformation,[status(esa)],[f334_nnf]) ).
cnf(f227,hypothesis,
queue_133 = store(queue_131,tail,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f227_nnf,plain,
queue_133 = store(queue_131,tail,index_132),
inference(nnf_transformation,[status(thm)],[f227]) ).
cnf(c227,plain,
queue_133 = store(queue_131,tail,index_132),
inference(cnf_transformation,[status(esa)],[f227_nnf]) ).
cnf(p909,plain,
( select(queue_133,X0) = select(queue_131,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c227,c1]) ).
cnf(p3039,plain,
( select(q29,X0) = select(queue_131,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c334,p909]) ).
cnf(p13741,plain,
( index_297 = select(queue_131,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13736,p3039]) ).
cnf(p13777,plain,
( index_297 = select(queue_131,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13741]) ).
cnf(f226,hypothesis,
queue_131 = store(q28,seq,earray_130),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f226_nnf,plain,
queue_131 = store(q28,seq,earray_130),
inference(nnf_transformation,[status(thm)],[f226]) ).
cnf(c226,plain,
queue_131 = store(q28,seq,earray_130),
inference(cnf_transformation,[status(esa)],[f226_nnf]) ).
cnf(p907,plain,
( select(queue_131,X0) = select(q28,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c226,c1]) ).
cnf(p13779,plain,
( index_297 = select(q28,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13777,p907]) ).
cnf(p13816,plain,
( index_297 = select(q28,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13779]) ).
cnf(f333,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp323) ).
fof(f333_nnf,plain,
q28 = queue_127,
inference(nnf_transformation,[status(thm)],[f333]) ).
cnf(c333,plain,
q28 = queue_127,
inference(cnf_transformation,[status(esa)],[f333_nnf]) ).
cnf(f224,hypothesis,
queue_127 = store(queue_125,tail,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f224_nnf,plain,
queue_127 = store(queue_125,tail,index_126),
inference(nnf_transformation,[status(thm)],[f224]) ).
cnf(c224,plain,
queue_127 = store(queue_125,tail,index_126),
inference(cnf_transformation,[status(esa)],[f224_nnf]) ).
cnf(p901,plain,
( select(queue_127,X0) = select(queue_125,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c224,c1]) ).
cnf(p2967,plain,
( select(q28,X0) = select(queue_125,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c333,p901]) ).
cnf(p13818,plain,
( index_297 = select(queue_125,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13816,p2967]) ).
cnf(p13855,plain,
( index_297 = select(queue_125,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13818]) ).
cnf(f223,hypothesis,
queue_125 = store(q27,seq,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f223_nnf,plain,
queue_125 = store(q27,seq,earray_124),
inference(nnf_transformation,[status(thm)],[f223]) ).
cnf(c223,plain,
queue_125 = store(q27,seq,earray_124),
inference(cnf_transformation,[status(esa)],[f223_nnf]) ).
cnf(p899,plain,
( select(queue_125,X0) = select(q27,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c223,c1]) ).
cnf(p13857,plain,
( index_297 = select(q27,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13855,p899]) ).
cnf(p13890,plain,
( index_297 = select(q27,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13857]) ).
cnf(f332,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp322) ).
fof(f332_nnf,plain,
q27 = queue_121,
inference(nnf_transformation,[status(thm)],[f332]) ).
cnf(c332,plain,
q27 = queue_121,
inference(cnf_transformation,[status(esa)],[f332_nnf]) ).
cnf(f222,hypothesis,
queue_121 = store(queue_119,tail,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f222_nnf,plain,
queue_121 = store(queue_119,tail,index_120),
inference(nnf_transformation,[status(thm)],[f222]) ).
cnf(c222,plain,
queue_121 = store(queue_119,tail,index_120),
inference(cnf_transformation,[status(esa)],[f222_nnf]) ).
cnf(p896,plain,
( select(queue_121,X0) = select(queue_119,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c222,c1]) ).
cnf(p2961,plain,
( select(q27,X0) = select(queue_119,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c332,p896]) ).
cnf(p13892,plain,
( index_297 = select(queue_119,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13890,p2961]) ).
cnf(p13923,plain,
( index_297 = select(queue_119,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13892]) ).
cnf(f221,hypothesis,
queue_119 = store(q26,seq,earray_118),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f221_nnf,plain,
queue_119 = store(q26,seq,earray_118),
inference(nnf_transformation,[status(thm)],[f221]) ).
cnf(c221,plain,
queue_119 = store(q26,seq,earray_118),
inference(cnf_transformation,[status(esa)],[f221_nnf]) ).
cnf(p894,plain,
( select(queue_119,X0) = select(q26,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c221,c1]) ).
cnf(p13926,plain,
( index_297 = select(q26,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13923,p894]) ).
cnf(p13964,plain,
( index_297 = select(q26,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13926]) ).
cnf(f331,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp321) ).
fof(f331_nnf,plain,
q26 = queue_115,
inference(nnf_transformation,[status(thm)],[f331]) ).
cnf(c331,plain,
q26 = queue_115,
inference(cnf_transformation,[status(esa)],[f331_nnf]) ).
cnf(f220,hypothesis,
queue_115 = store(queue_113,tail,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f220_nnf,plain,
queue_115 = store(queue_113,tail,index_114),
inference(nnf_transformation,[status(thm)],[f220]) ).
cnf(c220,plain,
queue_115 = store(queue_113,tail,index_114),
inference(cnf_transformation,[status(esa)],[f220_nnf]) ).
cnf(p891,plain,
( select(queue_115,X0) = select(queue_113,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c220,c1]) ).
cnf(p2955,plain,
( select(q26,X0) = select(queue_113,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c331,p891]) ).
cnf(p13966,plain,
( index_297 = select(queue_113,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p13964,p2955]) ).
cnf(p14015,plain,
( index_297 = select(queue_113,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p13966]) ).
cnf(f219,hypothesis,
queue_113 = store(q25,seq,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f219_nnf,plain,
queue_113 = store(q25,seq,earray_112),
inference(nnf_transformation,[status(thm)],[f219]) ).
cnf(c219,plain,
queue_113 = store(q25,seq,earray_112),
inference(cnf_transformation,[status(esa)],[f219_nnf]) ).
cnf(p889,plain,
( select(queue_113,X0) = select(q25,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c219,c1]) ).
cnf(p14017,plain,
( index_297 = select(q25,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14015,p889]) ).
cnf(p14051,plain,
( index_297 = select(q25,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14017]) ).
cnf(f330,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp320) ).
fof(f330_nnf,plain,
q25 = queue_109,
inference(nnf_transformation,[status(thm)],[f330]) ).
cnf(c330,plain,
q25 = queue_109,
inference(cnf_transformation,[status(esa)],[f330_nnf]) ).
cnf(f217,hypothesis,
queue_109 = store(queue_107,tail,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f217_nnf,plain,
queue_109 = store(queue_107,tail,index_108),
inference(nnf_transformation,[status(thm)],[f217]) ).
cnf(c217,plain,
queue_109 = store(queue_107,tail,index_108),
inference(cnf_transformation,[status(esa)],[f217_nnf]) ).
cnf(p884,plain,
( select(queue_109,X0) = select(queue_107,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c217,c1]) ).
cnf(p2949,plain,
( select(q25,X0) = select(queue_107,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c330,p884]) ).
cnf(p14053,plain,
( index_297 = select(queue_107,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14051,p2949]) ).
cnf(p14089,plain,
( index_297 = select(queue_107,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14053]) ).
cnf(f216,hypothesis,
queue_107 = store(q24,seq,earray_106),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp206) ).
fof(f216_nnf,plain,
queue_107 = store(q24,seq,earray_106),
inference(nnf_transformation,[status(thm)],[f216]) ).
cnf(c216,plain,
queue_107 = store(q24,seq,earray_106),
inference(cnf_transformation,[status(esa)],[f216_nnf]) ).
cnf(p882,plain,
( select(queue_107,X0) = select(q24,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c216,c1]) ).
cnf(p14091,plain,
( index_297 = select(q24,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14089,p882]) ).
cnf(p14136,plain,
( index_297 = select(q24,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14091]) ).
cnf(f329,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp319) ).
fof(f329_nnf,plain,
q24 = queue_103,
inference(nnf_transformation,[status(thm)],[f329]) ).
cnf(c329,plain,
q24 = queue_103,
inference(cnf_transformation,[status(esa)],[f329_nnf]) ).
cnf(f215,hypothesis,
queue_103 = store(queue_101,tail,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f215_nnf,plain,
queue_103 = store(queue_101,tail,index_102),
inference(nnf_transformation,[status(thm)],[f215]) ).
cnf(c215,plain,
queue_103 = store(queue_101,tail,index_102),
inference(cnf_transformation,[status(esa)],[f215_nnf]) ).
cnf(p879,plain,
( select(queue_103,X0) = select(queue_101,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c215,c1]) ).
cnf(p2944,plain,
( select(q24,X0) = select(queue_101,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c329,p879]) ).
cnf(p14138,plain,
( index_297 = select(queue_101,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14136,p2944]) ).
cnf(p14186,plain,
( index_297 = select(queue_101,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14138]) ).
cnf(f214,hypothesis,
queue_101 = store(q23,seq,earray_100),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp204) ).
fof(f214_nnf,plain,
queue_101 = store(q23,seq,earray_100),
inference(nnf_transformation,[status(thm)],[f214]) ).
cnf(c214,plain,
queue_101 = store(q23,seq,earray_100),
inference(cnf_transformation,[status(esa)],[f214_nnf]) ).
cnf(p877,plain,
( select(queue_101,X0) = select(q23,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c214,c1]) ).
cnf(p14188,plain,
( index_297 = select(q23,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14186,p877]) ).
cnf(p14222,plain,
( index_297 = select(q23,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14188]) ).
cnf(f328,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp318) ).
fof(f328_nnf,plain,
q23 = queue_97,
inference(nnf_transformation,[status(thm)],[f328]) ).
cnf(c328,plain,
q23 = queue_97,
inference(cnf_transformation,[status(esa)],[f328_nnf]) ).
cnf(f311,hypothesis,
queue_97 = store(queue_95,tail,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp301) ).
fof(f311_nnf,plain,
queue_97 = store(queue_95,tail,index_96),
inference(nnf_transformation,[status(thm)],[f311]) ).
cnf(c311,plain,
queue_97 = store(queue_95,tail,index_96),
inference(cnf_transformation,[status(esa)],[f311_nnf]) ).
cnf(f0,axiom,
select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1) ).
fof(f0_nnf,plain,
! [A,I,E] : select(store(A,I,E),I) = E,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,I,E] : select(store(A,I,E),I) = E,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p1544,plain,
select(queue_97,tail) = index_96,
inference(superposition,[status(thm)],[c311,c0]) ).
cnf(p2731,plain,
select(q23,tail) = index_96,
inference(superposition,[status(thm)],[c328,p1544]) ).
cnf(f212,hypothesis,
index_99 = select(q23,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f212_nnf,plain,
index_99 = select(q23,tail),
inference(nnf_transformation,[status(thm)],[f212]) ).
cnf(c212,plain,
index_99 = select(q23,tail),
inference(cnf_transformation,[status(esa)],[f212_nnf]) ).
cnf(p2732,plain,
index_99 = index_96,
inference(demodulation,[status(thm)],[p2731,c212]) ).
cnf(f211,hypothesis,
index_96 = s(index_93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f211_nnf,plain,
index_96 = s(index_93),
inference(nnf_transformation,[status(thm)],[f211]) ).
cnf(c211,plain,
index_96 = s(index_93),
inference(cnf_transformation,[status(esa)],[f211_nnf]) ).
cnf(f5,axiom,
p(s(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ps) ).
fof(f5_nnf,plain,
! [X] : p(s(X)) = X,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X] : p(s(X)) = X,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
p(s(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p514,plain,
p(index_96) = index_93,
inference(superposition,[status(thm)],[c211,c5]) ).
cnf(f6,axiom,
s(p(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sp) ).
fof(f6_nnf,plain,
! [X] : s(p(X)) = X,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X] : s(p(X)) = X,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
s(p(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p651,plain,
s(index_93) = index_96,
inference(superposition,[status(thm)],[p514,c6]) ).
cnf(p2736,plain,
index_96 = index_99,
inference(superposition,[status(thm)],[p2732,p651]) ).
cnf(p1546,plain,
q23 = store(queue_95,tail,index_96),
inference(superposition,[status(thm)],[c328,c311]) ).
cnf(p2742,plain,
q23 = store(queue_95,tail,index_99),
inference(demodulation,[status(thm)],[p2736,p1546]) ).
cnf(p4087,plain,
( select(q23,X0) = select(queue_95,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[p2742,c1]) ).
cnf(p14224,plain,
( index_297 = select(queue_95,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14222,p4087]) ).
cnf(p14263,plain,
( index_297 = select(queue_95,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14224]) ).
cnf(f310,hypothesis,
queue_95 = store(q22,seq,earray_94),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp300) ).
fof(f310_nnf,plain,
queue_95 = store(q22,seq,earray_94),
inference(nnf_transformation,[status(thm)],[f310]) ).
cnf(c310,plain,
queue_95 = store(q22,seq,earray_94),
inference(cnf_transformation,[status(esa)],[f310_nnf]) ).
cnf(p1527,plain,
( select(queue_95,X0) = select(q22,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c310,c1]) ).
cnf(p14266,plain,
( index_297 = select(q22,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14263,p1527]) ).
cnf(p14302,plain,
( index_297 = select(q22,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14266]) ).
cnf(p2734,plain,
index_111 = index_93,
inference(superposition,[status(thm)],[p2732,p514]) ).
cnf(f327,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp317) ).
fof(f327_nnf,plain,
q22 = queue_91,
inference(nnf_transformation,[status(thm)],[f327]) ).
cnf(c327,plain,
q22 = queue_91,
inference(cnf_transformation,[status(esa)],[f327_nnf]) ).
cnf(f309,hypothesis,
queue_91 = store(queue_89,tail,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp299) ).
fof(f309_nnf,plain,
queue_91 = store(queue_89,tail,index_90),
inference(nnf_transformation,[status(thm)],[f309]) ).
cnf(c309,plain,
queue_91 = store(queue_89,tail,index_90),
inference(cnf_transformation,[status(esa)],[f309_nnf]) ).
cnf(p1522,plain,
select(queue_91,tail) = index_90,
inference(superposition,[status(thm)],[c309,c0]) ).
cnf(p2700,plain,
select(q22,tail) = index_90,
inference(superposition,[status(thm)],[c327,p1522]) ).
cnf(f210,hypothesis,
index_93 = select(q22,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f210_nnf,plain,
index_93 = select(q22,tail),
inference(nnf_transformation,[status(thm)],[f210]) ).
cnf(c210,plain,
index_93 = select(q22,tail),
inference(cnf_transformation,[status(esa)],[f210_nnf]) ).
cnf(p2701,plain,
index_93 = index_90,
inference(demodulation,[status(thm)],[p2700,c210]) ).
cnf(f209,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f209_nnf,plain,
index_90 = s(index_87),
inference(nnf_transformation,[status(thm)],[f209]) ).
cnf(c209,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(esa)],[f209_nnf]) ).
cnf(p511,plain,
p(index_90) = index_87,
inference(superposition,[status(thm)],[c209,c5]) ).
cnf(p649,plain,
s(index_87) = index_90,
inference(superposition,[status(thm)],[p511,c6]) ).
cnf(p2707,plain,
index_90 = index_93,
inference(superposition,[status(thm)],[p2701,p649]) ).
cnf(p2755,plain,
index_93 = index_111,
inference(superposition,[status(thm)],[p2734,p2707]) ).
cnf(p1524,plain,
q22 = store(queue_89,tail,index_90),
inference(superposition,[status(thm)],[c327,c309]) ).
cnf(p2713,plain,
q22 = store(queue_89,tail,index_93),
inference(demodulation,[status(thm)],[p2707,p1524]) ).
cnf(p2765,plain,
q22 = store(queue_89,tail,index_111),
inference(demodulation,[status(thm)],[p2755,p2713]) ).
cnf(p4090,plain,
( select(q22,X0) = select(queue_89,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[p2765,c1]) ).
cnf(p14306,plain,
( index_297 = select(queue_89,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14302,p4090]) ).
cnf(p14346,plain,
( index_297 = select(queue_89,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14306]) ).
cnf(f308,hypothesis,
queue_89 = store(q21,seq,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp298) ).
fof(f308_nnf,plain,
queue_89 = store(q21,seq,earray_88),
inference(nnf_transformation,[status(thm)],[f308]) ).
cnf(c308,plain,
queue_89 = store(q21,seq,earray_88),
inference(cnf_transformation,[status(esa)],[f308_nnf]) ).
cnf(p1521,plain,
( select(queue_89,X0) = select(q21,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c308,c1]) ).
cnf(p14348,plain,
( index_297 = select(q21,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14346,p1521]) ).
cnf(p14386,plain,
( index_297 = select(q21,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14348]) ).
cnf(f325,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp315) ).
fof(f325_nnf,plain,
q20 = queue_79,
inference(nnf_transformation,[status(thm)],[f325]) ).
cnf(c325,plain,
q20 = queue_79,
inference(cnf_transformation,[status(esa)],[f325_nnf]) ).
cnf(f305,hypothesis,
queue_79 = store(queue_77,tail,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp295) ).
fof(f305_nnf,plain,
queue_79 = store(queue_77,tail,index_78),
inference(nnf_transformation,[status(thm)],[f305]) ).
cnf(c305,plain,
queue_79 = store(queue_77,tail,index_78),
inference(cnf_transformation,[status(esa)],[f305_nnf]) ).
cnf(p1495,plain,
select(queue_79,tail) = index_78,
inference(superposition,[status(thm)],[c305,c0]) ).
cnf(p2659,plain,
select(q20,tail) = index_78,
inference(superposition,[status(thm)],[c325,p1495]) ).
cnf(f205,hypothesis,
index_81 = select(q20,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f205_nnf,plain,
index_81 = select(q20,tail),
inference(nnf_transformation,[status(thm)],[f205]) ).
cnf(c205,plain,
index_81 = select(q20,tail),
inference(cnf_transformation,[status(esa)],[f205_nnf]) ).
cnf(p2660,plain,
index_81 = index_78,
inference(demodulation,[status(thm)],[p2659,c205]) ).
cnf(f204,hypothesis,
index_78 = s(index_75),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp194) ).
fof(f204_nnf,plain,
index_78 = s(index_75),
inference(nnf_transformation,[status(thm)],[f204]) ).
cnf(c204,plain,
index_78 = s(index_75),
inference(cnf_transformation,[status(esa)],[f204_nnf]) ).
cnf(p505,plain,
p(index_78) = index_75,
inference(superposition,[status(thm)],[c204,c5]) ).
cnf(p2662,plain,
p(index_81) = index_75,
inference(superposition,[status(thm)],[p2660,p505]) ).
cnf(f206,hypothesis,
index_84 = s(index_81),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp196) ).
fof(f206_nnf,plain,
index_84 = s(index_81),
inference(nnf_transformation,[status(thm)],[f206]) ).
cnf(c206,plain,
index_84 = s(index_81),
inference(cnf_transformation,[status(esa)],[f206_nnf]) ).
cnf(p509,plain,
p(index_84) = index_81,
inference(superposition,[status(thm)],[c206,c5]) ).
cnf(p646,plain,
s(index_81) = index_84,
inference(superposition,[status(thm)],[p509,c6]) ).
cnf(f9,axiom,
s(s(s(X))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circular) ).
fof(f9_nnf,plain,
! [X] : s(s(s(X))) = X,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : s(s(s(X))) = X,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
s(s(s(X0))) = X0,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p367,plain,
s(s(X0)) = p(X0),
inference(superposition,[status(thm)],[c6,c9]) ).
cnf(p1630,plain,
s(index_84) = p(index_81),
inference(superposition,[status(thm)],[p646,p367]) ).
cnf(p2664,plain,
s(index_84) = index_75,
inference(demodulation,[status(thm)],[p2662,p1630]) ).
cnf(p2685,plain,
index_63 = index_84,
inference(superposition,[status(thm)],[p2664,c5]) ).
cnf(p2688,plain,
index_84 = index_63,
inference(superposition,[status(thm)],[p2685,p646]) ).
cnf(f326,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp316) ).
fof(f326_nnf,plain,
q21 = queue_85,
inference(nnf_transformation,[status(thm)],[f326]) ).
cnf(c326,plain,
q21 = queue_85,
inference(cnf_transformation,[status(esa)],[f326_nnf]) ).
cnf(f307,hypothesis,
queue_85 = store(queue_83,tail,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp297) ).
fof(f307_nnf,plain,
queue_85 = store(queue_83,tail,index_84),
inference(nnf_transformation,[status(thm)],[f307]) ).
cnf(c307,plain,
queue_85 = store(queue_83,tail,index_84),
inference(cnf_transformation,[status(esa)],[f307_nnf]) ).
cnf(p1503,plain,
q21 = store(queue_83,tail,index_84),
inference(superposition,[status(thm)],[c326,c307]) ).
cnf(p2691,plain,
q21 = store(queue_83,tail,index_63),
inference(demodulation,[status(thm)],[p2688,p1503]) ).
cnf(p4079,plain,
( select(q21,X0) = select(queue_83,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[p2691,c1]) ).
cnf(p14390,plain,
( index_297 = select(queue_83,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14386,p4079]) ).
cnf(p14430,plain,
( index_297 = select(queue_83,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14390]) ).
cnf(f306,hypothesis,
queue_83 = store(q20,seq,earray_82),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp296) ).
fof(f306_nnf,plain,
queue_83 = store(q20,seq,earray_82),
inference(nnf_transformation,[status(thm)],[f306]) ).
cnf(c306,plain,
queue_83 = store(q20,seq,earray_82),
inference(cnf_transformation,[status(esa)],[f306_nnf]) ).
cnf(p1499,plain,
( select(queue_83,X0) = select(q20,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c306,c1]) ).
cnf(p14433,plain,
( index_297 = select(q20,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14430,p1499]) ).
cnf(p14474,plain,
( index_297 = select(q20,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14433]) ).
cnf(p1496,plain,
( select(queue_79,X0) = select(queue_77,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c305,c1]) ).
cnf(p4134,plain,
( select(q20,X0) = select(queue_77,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c325,p1496]) ).
cnf(p14478,plain,
( index_297 = select(queue_77,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14474,p4134]) ).
cnf(p14516,plain,
( index_297 = select(queue_77,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14478]) ).
cnf(f304,hypothesis,
queue_77 = store(q19,seq,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp294) ).
fof(f304_nnf,plain,
queue_77 = store(q19,seq,earray_76),
inference(nnf_transformation,[status(thm)],[f304]) ).
cnf(c304,plain,
queue_77 = store(q19,seq,earray_76),
inference(cnf_transformation,[status(esa)],[f304_nnf]) ).
cnf(p1481,plain,
( select(queue_77,X0) = select(q19,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c304,c1]) ).
cnf(p14518,plain,
( index_297 = select(q19,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14516,p1481]) ).
cnf(p14558,plain,
( index_297 = select(q19,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14518]) ).
cnf(f323,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp313) ).
fof(f323_nnf,plain,
q19 = queue_67,
inference(nnf_transformation,[status(thm)],[f323]) ).
cnf(c323,plain,
q19 = queue_67,
inference(cnf_transformation,[status(esa)],[f323_nnf]) ).
cnf(f300,hypothesis,
queue_67 = store(queue_65,tail,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp290) ).
fof(f300_nnf,plain,
queue_67 = store(queue_65,tail,index_66),
inference(nnf_transformation,[status(thm)],[f300]) ).
cnf(c300,plain,
queue_67 = store(queue_65,tail,index_66),
inference(cnf_transformation,[status(esa)],[f300_nnf]) ).
cnf(p1448,plain,
( select(queue_67,X0) = select(queue_65,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c300,c1]) ).
cnf(p4084,plain,
( select(q19,X0) = select(queue_65,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c323,p1448]) ).
cnf(p14563,plain,
( index_297 = select(queue_65,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14558,p4084]) ).
cnf(p14607,plain,
( index_297 = select(queue_65,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14563]) ).
cnf(f299,hypothesis,
queue_65 = store(q18,seq,earray_64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp289) ).
fof(f299_nnf,plain,
queue_65 = store(q18,seq,earray_64),
inference(nnf_transformation,[status(thm)],[f299]) ).
cnf(c299,plain,
queue_65 = store(q18,seq,earray_64),
inference(cnf_transformation,[status(esa)],[f299_nnf]) ).
cnf(p1446,plain,
( select(queue_65,X0) = select(q18,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c299,c1]) ).
cnf(p14609,plain,
( index_297 = select(q18,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14607,p1446]) ).
cnf(p14642,plain,
( index_297 = select(q18,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14609]) ).
cnf(f321,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp311) ).
fof(f321_nnf,plain,
q17 = queue_55,
inference(nnf_transformation,[status(thm)],[f321]) ).
cnf(c321,plain,
q17 = queue_55,
inference(cnf_transformation,[status(esa)],[f321_nnf]) ).
cnf(f296,hypothesis,
queue_55 = store(queue_53,tail,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp286) ).
fof(f296_nnf,plain,
queue_55 = store(queue_53,tail,index_54),
inference(nnf_transformation,[status(thm)],[f296]) ).
cnf(c296,plain,
queue_55 = store(queue_53,tail,index_54),
inference(cnf_transformation,[status(esa)],[f296_nnf]) ).
cnf(p1420,plain,
select(queue_55,tail) = index_54,
inference(superposition,[status(thm)],[c296,c0]) ).
cnf(p2499,plain,
select(q17,tail) = index_54,
inference(superposition,[status(thm)],[c321,p1420]) ).
cnf(f196,hypothesis,
index_57 = select(q17,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp186) ).
fof(f196_nnf,plain,
index_57 = select(q17,tail),
inference(nnf_transformation,[status(thm)],[f196]) ).
cnf(c196,plain,
index_57 = select(q17,tail),
inference(cnf_transformation,[status(esa)],[f196_nnf]) ).
cnf(p2500,plain,
index_57 = index_54,
inference(demodulation,[status(thm)],[p2499,c196]) ).
cnf(f195,hypothesis,
index_54 = s(index_51),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp185) ).
fof(f195_nnf,plain,
index_54 = s(index_51),
inference(nnf_transformation,[status(thm)],[f195]) ).
cnf(c195,plain,
index_54 = s(index_51),
inference(cnf_transformation,[status(esa)],[f195_nnf]) ).
cnf(p492,plain,
p(index_54) = index_51,
inference(superposition,[status(thm)],[c195,c5]) ).
cnf(p2502,plain,
p(index_57) = index_51,
inference(superposition,[status(thm)],[p2500,p492]) ).
cnf(f198,hypothesis,
index_60 = s(index_57),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp188) ).
fof(f198_nnf,plain,
index_60 = s(index_57),
inference(nnf_transformation,[status(thm)],[f198]) ).
cnf(c198,plain,
index_60 = s(index_57),
inference(cnf_transformation,[status(esa)],[f198_nnf]) ).
cnf(p498,plain,
p(index_60) = index_57,
inference(superposition,[status(thm)],[c198,c5]) ).
cnf(p635,plain,
s(index_57) = index_60,
inference(superposition,[status(thm)],[p498,c6]) ).
cnf(p1626,plain,
s(index_60) = p(index_57),
inference(superposition,[status(thm)],[p635,p367]) ).
cnf(p2504,plain,
s(index_60) = index_51,
inference(demodulation,[status(thm)],[p2502,p1626]) ).
cnf(p2523,plain,
index_45 = index_60,
inference(superposition,[status(thm)],[p2504,c5]) ).
cnf(p2529,plain,
index_60 = index_45,
inference(superposition,[status(thm)],[p2523,p635]) ).
cnf(f322,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp312) ).
fof(f322_nnf,plain,
q18 = queue_61,
inference(nnf_transformation,[status(thm)],[f322]) ).
cnf(c322,plain,
q18 = queue_61,
inference(cnf_transformation,[status(esa)],[f322_nnf]) ).
cnf(f298,hypothesis,
queue_61 = store(queue_59,tail,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp288) ).
fof(f298_nnf,plain,
queue_61 = store(queue_59,tail,index_60),
inference(nnf_transformation,[status(thm)],[f298]) ).
cnf(c298,plain,
queue_61 = store(queue_59,tail,index_60),
inference(cnf_transformation,[status(esa)],[f298_nnf]) ).
cnf(p1444,plain,
q18 = store(queue_59,tail,index_60),
inference(superposition,[status(thm)],[c322,c298]) ).
cnf(p2532,plain,
q18 = store(queue_59,tail,index_45),
inference(demodulation,[status(thm)],[p2529,p1444]) ).
cnf(p4071,plain,
( select(q18,X0) = select(queue_59,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[p2532,c1]) ).
cnf(p14644,plain,
( index_297 = select(queue_59,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14642,p4071]) ).
cnf(p14682,plain,
( index_297 = select(queue_59,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14644]) ).
cnf(f297,hypothesis,
queue_59 = store(q17,seq,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp287) ).
fof(f297_nnf,plain,
queue_59 = store(q17,seq,earray_58),
inference(nnf_transformation,[status(thm)],[f297]) ).
cnf(c297,plain,
queue_59 = store(q17,seq,earray_58),
inference(cnf_transformation,[status(esa)],[f297_nnf]) ).
cnf(p1424,plain,
( select(queue_59,X0) = select(q17,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c297,c1]) ).
cnf(p14684,plain,
( index_297 = select(q17,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14682,p1424]) ).
cnf(p14723,plain,
( index_297 = select(q17,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14684]) ).
cnf(p1421,plain,
( select(queue_55,X0) = select(queue_53,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c296,c1]) ).
cnf(p4050,plain,
( select(q17,X0) = select(queue_53,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c321,p1421]) ).
cnf(p14725,plain,
( index_297 = select(queue_53,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14723,p4050]) ).
cnf(p14766,plain,
( index_297 = select(queue_53,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14725]) ).
cnf(f295,hypothesis,
queue_53 = store(q16,seq,earray_52),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp285) ).
fof(f295_nnf,plain,
queue_53 = store(q16,seq,earray_52),
inference(nnf_transformation,[status(thm)],[f295]) ).
cnf(c295,plain,
queue_53 = store(q16,seq,earray_52),
inference(cnf_transformation,[status(esa)],[f295_nnf]) ).
cnf(p1406,plain,
( select(queue_53,X0) = select(q16,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c295,c1]) ).
cnf(p14768,plain,
( index_297 = select(q16,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14766,p1406]) ).
cnf(p14799,plain,
( index_297 = select(q16,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14768]) ).
cnf(f320,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp310) ).
fof(f320_nnf,plain,
q16 = queue_49,
inference(nnf_transformation,[status(thm)],[f320]) ).
cnf(c320,plain,
q16 = queue_49,
inference(cnf_transformation,[status(esa)],[f320_nnf]) ).
cnf(f293,hypothesis,
queue_49 = store(queue_47,tail,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp283) ).
fof(f293_nnf,plain,
queue_49 = store(queue_47,tail,index_48),
inference(nnf_transformation,[status(thm)],[f293]) ).
cnf(c293,plain,
queue_49 = store(queue_47,tail,index_48),
inference(cnf_transformation,[status(esa)],[f293_nnf]) ).
cnf(p1398,plain,
( select(queue_49,X0) = select(queue_47,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c293,c1]) ).
cnf(p4012,plain,
( select(q16,X0) = select(queue_47,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c320,p1398]) ).
cnf(p14801,plain,
( index_297 = select(queue_47,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14799,p4012]) ).
cnf(p14849,plain,
( index_297 = select(queue_47,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14801]) ).
cnf(f292,hypothesis,
queue_47 = store(q15,seq,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp282) ).
fof(f292_nnf,plain,
queue_47 = store(q15,seq,earray_46),
inference(nnf_transformation,[status(thm)],[f292]) ).
cnf(c292,plain,
queue_47 = store(q15,seq,earray_46),
inference(cnf_transformation,[status(esa)],[f292_nnf]) ).
cnf(p1379,plain,
( select(queue_47,X0) = select(q15,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c292,c1]) ).
cnf(p14852,plain,
( index_297 = select(q15,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14849,p1379]) ).
cnf(p14889,plain,
( index_297 = select(q15,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14852]) ).
cnf(f319,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp309) ).
fof(f319_nnf,plain,
q15 = queue_43,
inference(nnf_transformation,[status(thm)],[f319]) ).
cnf(c319,plain,
q15 = queue_43,
inference(cnf_transformation,[status(esa)],[f319_nnf]) ).
cnf(f291,hypothesis,
queue_43 = store(queue_41,tail,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp281) ).
fof(f291_nnf,plain,
queue_43 = store(queue_41,tail,index_42),
inference(nnf_transformation,[status(thm)],[f291]) ).
cnf(c291,plain,
queue_43 = store(queue_41,tail,index_42),
inference(cnf_transformation,[status(esa)],[f291_nnf]) ).
cnf(p1376,plain,
( select(queue_43,X0) = select(queue_41,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c291,c1]) ).
cnf(p3993,plain,
( select(q15,X0) = select(queue_41,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c319,p1376]) ).
cnf(p14892,plain,
( index_297 = select(queue_41,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14889,p3993]) ).
cnf(p14924,plain,
( index_297 = select(queue_41,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14892]) ).
cnf(f290,hypothesis,
queue_41 = store(q14,seq,earray_40),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp280) ).
fof(f290_nnf,plain,
queue_41 = store(q14,seq,earray_40),
inference(nnf_transformation,[status(thm)],[f290]) ).
cnf(c290,plain,
queue_41 = store(q14,seq,earray_40),
inference(cnf_transformation,[status(esa)],[f290_nnf]) ).
cnf(p1374,plain,
( select(queue_41,X0) = select(q14,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c290,c1]) ).
cnf(p14926,plain,
( index_297 = select(q14,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14924,p1374]) ).
cnf(p14966,plain,
( index_297 = select(q14,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14926]) ).
cnf(f318,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp308) ).
fof(f318_nnf,plain,
q14 = queue_37,
inference(nnf_transformation,[status(thm)],[f318]) ).
cnf(c318,plain,
q14 = queue_37,
inference(cnf_transformation,[status(esa)],[f318_nnf]) ).
cnf(f289,hypothesis,
queue_37 = store(queue_35,tail,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp279) ).
fof(f289_nnf,plain,
queue_37 = store(queue_35,tail,index_36),
inference(nnf_transformation,[status(thm)],[f289]) ).
cnf(c289,plain,
queue_37 = store(queue_35,tail,index_36),
inference(cnf_transformation,[status(esa)],[f289_nnf]) ).
cnf(p1354,plain,
( select(queue_37,X0) = select(queue_35,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c289,c1]) ).
cnf(p3967,plain,
( select(q14,X0) = select(queue_35,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c318,p1354]) ).
cnf(p14968,plain,
( index_297 = select(queue_35,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p14966,p3967]) ).
cnf(p15005,plain,
( index_297 = select(queue_35,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p14968]) ).
cnf(f288,hypothesis,
queue_35 = store(q13,seq,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp278) ).
fof(f288_nnf,plain,
queue_35 = store(q13,seq,earray_34),
inference(nnf_transformation,[status(thm)],[f288]) ).
cnf(c288,plain,
queue_35 = store(q13,seq,earray_34),
inference(cnf_transformation,[status(esa)],[f288_nnf]) ).
cnf(p1352,plain,
( select(queue_35,X0) = select(q13,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c288,c1]) ).
cnf(p15007,plain,
( index_297 = select(q13,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15005,p1352]) ).
cnf(p15043,plain,
( index_297 = select(q13,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15007]) ).
cnf(f317,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp307) ).
fof(f317_nnf,plain,
q13 = queue_31,
inference(nnf_transformation,[status(thm)],[f317]) ).
cnf(c317,plain,
q13 = queue_31,
inference(cnf_transformation,[status(esa)],[f317_nnf]) ).
cnf(f287,hypothesis,
queue_31 = store(queue_29,tail,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp277) ).
fof(f287_nnf,plain,
queue_31 = store(queue_29,tail,index_30),
inference(nnf_transformation,[status(thm)],[f287]) ).
cnf(c287,plain,
queue_31 = store(queue_29,tail,index_30),
inference(cnf_transformation,[status(esa)],[f287_nnf]) ).
cnf(p1336,plain,
( select(queue_31,X0) = select(queue_29,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c287,c1]) ).
cnf(p3946,plain,
( select(q13,X0) = select(queue_29,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c317,p1336]) ).
cnf(p15045,plain,
( index_297 = select(queue_29,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15043,p3946]) ).
cnf(p15084,plain,
( index_297 = select(queue_29,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15045]) ).
cnf(f284,hypothesis,
queue_29 = store(q12,seq,earray_28),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp274) ).
fof(f284_nnf,plain,
queue_29 = store(q12,seq,earray_28),
inference(nnf_transformation,[status(thm)],[f284]) ).
cnf(c284,plain,
queue_29 = store(q12,seq,earray_28),
inference(cnf_transformation,[status(esa)],[f284_nnf]) ).
cnf(p1311,plain,
( select(queue_29,X0) = select(q12,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c284,c1]) ).
cnf(p15086,plain,
( index_297 = select(q12,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15084,p1311]) ).
cnf(p15125,plain,
( index_297 = select(q12,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15086]) ).
cnf(f316,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp306) ).
fof(f316_nnf,plain,
q12 = queue_25,
inference(nnf_transformation,[status(thm)],[f316]) ).
cnf(c316,plain,
q12 = queue_25,
inference(cnf_transformation,[status(esa)],[f316_nnf]) ).
cnf(f269,hypothesis,
queue_25 = store(queue_23,tail,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp259) ).
fof(f269_nnf,plain,
queue_25 = store(queue_23,tail,index_24),
inference(nnf_transformation,[status(thm)],[f269]) ).
cnf(c269,plain,
queue_25 = store(queue_23,tail,index_24),
inference(cnf_transformation,[status(esa)],[f269_nnf]) ).
cnf(p1184,plain,
( select(queue_25,X0) = select(queue_23,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c269,c1]) ).
cnf(p3818,plain,
( select(q12,X0) = select(queue_23,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c316,p1184]) ).
cnf(p15127,plain,
( index_297 = select(queue_23,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15125,p3818]) ).
cnf(p15165,plain,
( index_297 = select(queue_23,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15127]) ).
cnf(f262,hypothesis,
queue_23 = store(q11,seq,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp252) ).
fof(f262_nnf,plain,
queue_23 = store(q11,seq,earray_22),
inference(nnf_transformation,[status(thm)],[f262]) ).
cnf(c262,plain,
queue_23 = store(q11,seq,earray_22),
inference(cnf_transformation,[status(esa)],[f262_nnf]) ).
cnf(p1118,plain,
( select(queue_23,X0) = select(q11,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c262,c1]) ).
cnf(p15167,plain,
( index_297 = select(q11,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15165,p1118]) ).
cnf(p15209,plain,
( index_297 = select(q11,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15167]) ).
cnf(f315,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp305) ).
fof(f315_nnf,plain,
q11 = queue_19,
inference(nnf_transformation,[status(thm)],[f315]) ).
cnf(c315,plain,
q11 = queue_19,
inference(cnf_transformation,[status(esa)],[f315_nnf]) ).
cnf(f247,hypothesis,
queue_19 = store(queue_17,tail,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f247_nnf,plain,
queue_19 = store(queue_17,tail,index_18),
inference(nnf_transformation,[status(thm)],[f247]) ).
cnf(c247,plain,
queue_19 = store(queue_17,tail,index_18),
inference(cnf_transformation,[status(esa)],[f247_nnf]) ).
cnf(p998,plain,
( select(queue_19,X0) = select(queue_17,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c247,c1]) ).
cnf(p3399,plain,
( select(q11,X0) = select(queue_17,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c315,p998]) ).
cnf(p15211,plain,
( index_297 = select(queue_17,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15209,p3399]) ).
cnf(p15250,plain,
( index_297 = select(queue_17,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15211]) ).
cnf(f240,hypothesis,
queue_17 = store(q10,seq,earray_16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f240_nnf,plain,
queue_17 = store(q10,seq,earray_16),
inference(nnf_transformation,[status(thm)],[f240]) ).
cnf(c240,plain,
queue_17 = store(q10,seq,earray_16),
inference(cnf_transformation,[status(esa)],[f240_nnf]) ).
cnf(p952,plain,
( select(queue_17,X0) = select(q10,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c240,c1]) ).
cnf(p15252,plain,
( index_297 = select(q10,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15250,p952]) ).
cnf(p15290,plain,
( index_297 = select(q10,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15252]) ).
cnf(f314,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp304) ).
fof(f314_nnf,plain,
q10 = queue_13,
inference(nnf_transformation,[status(thm)],[f314]) ).
cnf(c314,plain,
q10 = queue_13,
inference(cnf_transformation,[status(esa)],[f314_nnf]) ).
cnf(f225,hypothesis,
queue_13 = store(queue_11,tail,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f225_nnf,plain,
queue_13 = store(queue_11,tail,index_12),
inference(nnf_transformation,[status(thm)],[f225]) ).
cnf(c225,plain,
queue_13 = store(queue_11,tail,index_12),
inference(cnf_transformation,[status(esa)],[f225_nnf]) ).
cnf(p905,plain,
( select(queue_13,X0) = select(queue_11,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c225,c1]) ).
cnf(p3010,plain,
( select(q10,X0) = select(queue_11,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c314,p905]) ).
cnf(p15296,plain,
( index_297 = select(queue_11,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15290,p3010]) ).
cnf(p15343,plain,
( index_297 = select(queue_11,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15296]) ).
cnf(f218,hypothesis,
queue_11 = store(q9,seq,earray_10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f218_nnf,plain,
queue_11 = store(q9,seq,earray_10),
inference(nnf_transformation,[status(thm)],[f218]) ).
cnf(c218,plain,
queue_11 = store(q9,seq,earray_10),
inference(cnf_transformation,[status(esa)],[f218_nnf]) ).
cnf(p887,plain,
( select(queue_11,X0) = select(q9,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c218,c1]) ).
cnf(p15345,plain,
( index_297 = select(q9,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15343,p887]) ).
cnf(p15379,plain,
( index_297 = select(q9,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15345]) ).
cnf(f361,hypothesis,
q9 = queue_295,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp351) ).
fof(f361_nnf,plain,
q9 = queue_295,
inference(nnf_transformation,[status(thm)],[f361]) ).
cnf(c361,plain,
q9 = queue_295,
inference(cnf_transformation,[status(esa)],[f361_nnf]) ).
cnf(f286,hypothesis,
queue_295 = store(queue_293,tail,index_294),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp276) ).
fof(f286_nnf,plain,
queue_295 = store(queue_293,tail,index_294),
inference(nnf_transformation,[status(thm)],[f286]) ).
cnf(c286,plain,
queue_295 = store(queue_293,tail,index_294),
inference(cnf_transformation,[status(esa)],[f286_nnf]) ).
cnf(p1328,plain,
( select(queue_295,X0) = select(queue_293,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c286,c1]) ).
cnf(p3924,plain,
( select(q9,X0) = select(queue_293,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c361,p1328]) ).
cnf(p15381,plain,
( index_297 = select(queue_293,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15379,p3924]) ).
cnf(p15425,plain,
( index_297 = select(queue_293,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15381]) ).
cnf(f285,hypothesis,
queue_293 = store(q8,seq,earray_292),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp275) ).
fof(f285_nnf,plain,
queue_293 = store(q8,seq,earray_292),
inference(nnf_transformation,[status(thm)],[f285]) ).
cnf(c285,plain,
queue_293 = store(q8,seq,earray_292),
inference(cnf_transformation,[status(esa)],[f285_nnf]) ).
cnf(p1326,plain,
( select(queue_293,X0) = select(q8,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c285,c1]) ).
cnf(p15427,plain,
( index_297 = select(q8,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15425,p1326]) ).
cnf(p15463,plain,
( index_297 = select(q8,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15427]) ).
cnf(f360,hypothesis,
q8 = queue_289,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp350) ).
fof(f360_nnf,plain,
q8 = queue_289,
inference(nnf_transformation,[status(thm)],[f360]) ).
cnf(c360,plain,
q8 = queue_289,
inference(cnf_transformation,[status(esa)],[f360_nnf]) ).
cnf(f283,hypothesis,
queue_289 = store(queue_287,tail,index_288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp273) ).
fof(f283_nnf,plain,
queue_289 = store(queue_287,tail,index_288),
inference(nnf_transformation,[status(thm)],[f283]) ).
cnf(c283,plain,
queue_289 = store(queue_287,tail,index_288),
inference(cnf_transformation,[status(esa)],[f283_nnf]) ).
cnf(p1304,plain,
( select(queue_289,X0) = select(queue_287,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c283,c1]) ).
cnf(p3885,plain,
( select(q8,X0) = select(queue_287,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c360,p1304]) ).
cnf(p15465,plain,
( index_297 = select(queue_287,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15463,p3885]) ).
cnf(p15503,plain,
( index_297 = select(queue_287,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15465]) ).
cnf(f282,hypothesis,
queue_287 = store(q7,seq,earray_286),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp272) ).
fof(f282_nnf,plain,
queue_287 = store(q7,seq,earray_286),
inference(nnf_transformation,[status(thm)],[f282]) ).
cnf(c282,plain,
queue_287 = store(q7,seq,earray_286),
inference(cnf_transformation,[status(esa)],[f282_nnf]) ).
cnf(p1302,plain,
( select(queue_287,X0) = select(q7,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c282,c1]) ).
cnf(p15505,plain,
( index_297 = select(q7,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15503,p1302]) ).
cnf(p15538,plain,
( index_297 = select(q7,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15505]) ).
cnf(f359,hypothesis,
q7 = queue_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp349) ).
fof(f359_nnf,plain,
q7 = queue_283,
inference(nnf_transformation,[status(thm)],[f359]) ).
cnf(c359,plain,
q7 = queue_283,
inference(cnf_transformation,[status(esa)],[f359_nnf]) ).
cnf(f281,hypothesis,
queue_283 = store(queue_281,tail,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp271) ).
fof(f281_nnf,plain,
queue_283 = store(queue_281,tail,index_282),
inference(nnf_transformation,[status(thm)],[f281]) ).
cnf(c281,plain,
queue_283 = store(queue_281,tail,index_282),
inference(cnf_transformation,[status(esa)],[f281_nnf]) ).
cnf(p1283,plain,
( select(queue_283,X0) = select(queue_281,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c281,c1]) ).
cnf(p3872,plain,
( select(q7,X0) = select(queue_281,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c359,p1283]) ).
cnf(p15540,plain,
( index_297 = select(queue_281,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15538,p3872]) ).
cnf(p15580,plain,
( index_297 = select(queue_281,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15540]) ).
cnf(f280,hypothesis,
queue_281 = store(q6,seq,earray_280),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp270) ).
fof(f280_nnf,plain,
queue_281 = store(q6,seq,earray_280),
inference(nnf_transformation,[status(thm)],[f280]) ).
cnf(c280,plain,
queue_281 = store(q6,seq,earray_280),
inference(cnf_transformation,[status(esa)],[f280_nnf]) ).
cnf(p1280,plain,
( select(queue_281,X0) = select(q6,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c280,c1]) ).
cnf(p15582,plain,
( index_297 = select(q6,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15580,p1280]) ).
cnf(p15614,plain,
( index_297 = select(q6,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15582]) ).
cnf(f358,hypothesis,
q6 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp348) ).
fof(f358_nnf,plain,
q6 = queue_277,
inference(nnf_transformation,[status(thm)],[f358]) ).
cnf(c358,plain,
q6 = queue_277,
inference(cnf_transformation,[status(esa)],[f358_nnf]) ).
cnf(f279,hypothesis,
queue_277 = store(queue_275,tail,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp269) ).
fof(f279_nnf,plain,
queue_277 = store(queue_275,tail,index_276),
inference(nnf_transformation,[status(thm)],[f279]) ).
cnf(c279,plain,
queue_277 = store(queue_275,tail,index_276),
inference(cnf_transformation,[status(esa)],[f279_nnf]) ).
cnf(p1277,plain,
( select(queue_277,X0) = select(queue_275,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c279,c1]) ).
cnf(p3858,plain,
( select(q6,X0) = select(queue_275,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c358,p1277]) ).
cnf(p15616,plain,
( index_297 = select(queue_275,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15614,p3858]) ).
cnf(p15653,plain,
( index_297 = select(queue_275,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15616]) ).
cnf(f278,hypothesis,
queue_275 = store(q5,seq,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp268) ).
fof(f278_nnf,plain,
queue_275 = store(q5,seq,earray_274),
inference(nnf_transformation,[status(thm)],[f278]) ).
cnf(c278,plain,
queue_275 = store(q5,seq,earray_274),
inference(cnf_transformation,[status(esa)],[f278_nnf]) ).
cnf(p1258,plain,
( select(queue_275,X0) = select(q5,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c278,c1]) ).
cnf(p15655,plain,
( index_297 = select(q5,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15653,p1258]) ).
cnf(p15690,plain,
( index_297 = select(q5,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15655]) ).
cnf(f357,hypothesis,
q5 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp347) ).
fof(f357_nnf,plain,
q5 = queue_271,
inference(nnf_transformation,[status(thm)],[f357]) ).
cnf(c357,plain,
q5 = queue_271,
inference(cnf_transformation,[status(esa)],[f357_nnf]) ).
cnf(f277,hypothesis,
queue_271 = store(queue_269,tail,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp267) ).
fof(f277_nnf,plain,
queue_271 = store(queue_269,tail,index_270),
inference(nnf_transformation,[status(thm)],[f277]) ).
cnf(c277,plain,
queue_271 = store(queue_269,tail,index_270),
inference(cnf_transformation,[status(esa)],[f277_nnf]) ).
cnf(p1255,plain,
( select(queue_271,X0) = select(queue_269,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c277,c1]) ).
cnf(p3846,plain,
( select(q5,X0) = select(queue_269,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c357,p1255]) ).
cnf(p15692,plain,
( index_297 = select(queue_269,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15690,p3846]) ).
cnf(p15724,plain,
( index_297 = select(queue_269,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15692]) ).
cnf(f276,hypothesis,
queue_269 = store(q4,seq,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp266) ).
fof(f276_nnf,plain,
queue_269 = store(q4,seq,earray_268),
inference(nnf_transformation,[status(thm)],[f276]) ).
cnf(c276,plain,
queue_269 = store(q4,seq,earray_268),
inference(cnf_transformation,[status(esa)],[f276_nnf]) ).
cnf(p1253,plain,
( select(queue_269,X0) = select(q4,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c276,c1]) ).
cnf(p15726,plain,
( index_297 = select(q4,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15724,p1253]) ).
cnf(p15761,plain,
( index_297 = select(q4,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15726]) ).
cnf(f346,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp336) ).
fof(f346_nnf,plain,
q4 = queue_205,
inference(nnf_transformation,[status(thm)],[f346]) ).
cnf(c346,plain,
q4 = queue_205,
inference(cnf_transformation,[status(esa)],[f346_nnf]) ).
cnf(f253,hypothesis,
queue_205 = store(queue_203,tail,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f253_nnf,plain,
queue_205 = store(queue_203,tail,index_204),
inference(nnf_transformation,[status(thm)],[f253]) ).
cnf(c253,plain,
queue_205 = store(queue_203,tail,index_204),
inference(cnf_transformation,[status(esa)],[f253_nnf]) ).
cnf(p1042,plain,
( select(queue_205,X0) = select(queue_203,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c253,c1]) ).
cnf(p3746,plain,
( select(q4,X0) = select(queue_203,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c346,p1042]) ).
cnf(p15763,plain,
( index_297 = select(queue_203,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15761,p3746]) ).
cnf(p15796,plain,
( index_297 = select(queue_203,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15763]) ).
cnf(f252,hypothesis,
queue_203 = store(q3,seq,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f252_nnf,plain,
queue_203 = store(q3,seq,earray_202),
inference(nnf_transformation,[status(thm)],[f252]) ).
cnf(c252,plain,
queue_203 = store(q3,seq,earray_202),
inference(cnf_transformation,[status(esa)],[f252_nnf]) ).
cnf(p1040,plain,
( select(queue_203,X0) = select(q3,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c252,c1]) ).
cnf(p15798,plain,
( index_297 = select(q3,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15796,p1040]) ).
cnf(p15828,plain,
( index_297 = select(q3,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15798]) ).
cnf(f335,hypothesis,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp325) ).
fof(f335_nnf,plain,
q3 = queue_139,
inference(nnf_transformation,[status(thm)],[f335]) ).
cnf(c335,plain,
q3 = queue_139,
inference(cnf_transformation,[status(esa)],[f335_nnf]) ).
cnf(f229,hypothesis,
queue_139 = store(queue_137,tail,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp219) ).
fof(f229_nnf,plain,
queue_139 = store(queue_137,tail,index_138),
inference(nnf_transformation,[status(thm)],[f229]) ).
cnf(c229,plain,
queue_139 = store(queue_137,tail,index_138),
inference(cnf_transformation,[status(esa)],[f229_nnf]) ).
cnf(p914,plain,
( select(queue_139,X0) = select(queue_137,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c229,c1]) ).
cnf(p3044,plain,
( select(q3,X0) = select(queue_137,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c335,p914]) ).
cnf(p15837,plain,
( index_297 = select(queue_137,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15828,p3044]) ).
cnf(p15871,plain,
( index_297 = select(queue_137,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15837]) ).
cnf(f228,hypothesis,
queue_137 = store(q2,seq,earray_136),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp218) ).
fof(f228_nnf,plain,
queue_137 = store(q2,seq,earray_136),
inference(nnf_transformation,[status(thm)],[f228]) ).
cnf(c228,plain,
queue_137 = store(q2,seq,earray_136),
inference(cnf_transformation,[status(esa)],[f228_nnf]) ).
cnf(p912,plain,
( select(queue_137,X0) = select(q2,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c228,c1]) ).
cnf(p15874,plain,
( index_297 = select(q2,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15871,p912]) ).
cnf(p15900,plain,
( index_297 = select(q2,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15874]) ).
cnf(f324,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp314) ).
fof(f324_nnf,plain,
q2 = queue_73,
inference(nnf_transformation,[status(thm)],[f324]) ).
cnf(c324,plain,
q2 = queue_73,
inference(cnf_transformation,[status(esa)],[f324_nnf]) ).
cnf(f303,hypothesis,
queue_73 = store(queue_71,tail,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp293) ).
fof(f303_nnf,plain,
queue_73 = store(queue_71,tail,index_72),
inference(nnf_transformation,[status(thm)],[f303]) ).
cnf(c303,plain,
queue_73 = store(queue_71,tail,index_72),
inference(cnf_transformation,[status(esa)],[f303_nnf]) ).
cnf(p1474,plain,
( select(queue_73,X0) = select(queue_71,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c303,c1]) ).
cnf(p4118,plain,
( select(q2,X0) = select(queue_71,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c324,p1474]) ).
cnf(p15902,plain,
( index_297 = select(queue_71,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15900,p4118]) ).
cnf(p15950,plain,
( index_297 = select(queue_71,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15902]) ).
cnf(f302,hypothesis,
queue_71 = store(q1,seq,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp292) ).
fof(f302_nnf,plain,
queue_71 = store(q1,seq,earray_70),
inference(nnf_transformation,[status(thm)],[f302]) ).
cnf(c302,plain,
queue_71 = store(q1,seq,earray_70),
inference(cnf_transformation,[status(esa)],[f302_nnf]) ).
cnf(p1472,plain,
( select(queue_71,X0) = select(q1,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c302,c1]) ).
cnf(p15952,plain,
( index_297 = select(q1,head)
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15950,p1472]) ).
cnf(p15986,plain,
( index_297 = select(q1,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15952]) ).
cnf(f313,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp303) ).
fof(f313_nnf,plain,
q1 = queue_7,
inference(nnf_transformation,[status(thm)],[f313]) ).
cnf(c313,plain,
q1 = queue_7,
inference(cnf_transformation,[status(esa)],[f313_nnf]) ).
cnf(f301,hypothesis,
queue_7 = store(queue_5,tail,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp291) ).
fof(f301_nnf,plain,
queue_7 = store(queue_5,tail,index_6),
inference(nnf_transformation,[status(thm)],[f301]) ).
cnf(c301,plain,
queue_7 = store(queue_5,tail,index_6),
inference(cnf_transformation,[status(esa)],[f301_nnf]) ).
cnf(p1470,plain,
( select(queue_7,X0) = select(queue_5,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c301,c1]) ).
cnf(p4098,plain,
( select(q1,X0) = select(queue_5,X0)
| tail = X0 ),
inference(superposition,[status(thm)],[c313,p1470]) ).
cnf(p15988,plain,
( index_297 = select(queue_5,head)
| tail = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p15986,p4098]) ).
cnf(p16019,plain,
( index_297 = select(queue_5,head)
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p15988]) ).
cnf(f294,hypothesis,
queue_5 = store(q0,seq,earray_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp284) ).
fof(f294_nnf,plain,
queue_5 = store(q0,seq,earray_4),
inference(nnf_transformation,[status(thm)],[f294]) ).
cnf(c294,plain,
queue_5 = store(q0,seq,earray_4),
inference(cnf_transformation,[status(esa)],[f294_nnf]) ).
cnf(p1401,plain,
( select(queue_5,X0) = select(q0,X0)
| seq = X0 ),
inference(superposition,[status(thm)],[c294,c1]) ).
cnf(p16021,plain,
( index_297 = index_0
| seq = head
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p16019,p1401]) ).
cnf(p16025,plain,
( index_297 = index_0
| seq = head
| tail = head ),
inference(factoring,[status(thm)],[p16021]) ).
cnf(f312,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp302) ).
fof(f312_nnf,plain,
q0 = queue_1,
inference(nnf_transformation,[status(thm)],[f312]) ).
cnf(c312,plain,
q0 = queue_1,
inference(cnf_transformation,[status(esa)],[f312_nnf]) ).
cnf(f213,hypothesis,
queue_1 = store(q,head,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f213_nnf,plain,
queue_1 = store(q,head,index_0),
inference(nnf_transformation,[status(thm)],[f213]) ).
cnf(c213,plain,
queue_1 = store(q,head,index_0),
inference(cnf_transformation,[status(esa)],[f213_nnf]) ).
cnf(p874,plain,
q0 = store(q,head,index_0),
inference(superposition,[status(thm)],[c312,c213]) ).
cnf(p2940,plain,
queue_1 = q0,
inference(superposition,[status(thm)],[p874,c213]) ).
cnf(f111,hypothesis,
index_0 = select(q,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f111_nnf,plain,
index_0 = select(q,tail),
inference(nnf_transformation,[status(thm)],[f111]) ).
cnf(c111,plain,
index_0 = select(q,tail),
inference(cnf_transformation,[status(esa)],[f111_nnf]) ).
cnf(p701,plain,
( select(store(q,X0,X1),tail) = index_0
| X0 = tail ),
inference(superposition,[status(thm)],[c111,c1]) ).
cnf(p2496,plain,
( select(queue_1,tail) = index_0
| head = tail ),
inference(superposition,[status(thm)],[c213,p701]) ).
cnf(p2941,plain,
( select(q0,tail) = index_0
| head = tail ),
inference(demodulation,[status(thm)],[p2940,p2496]) ).
cnf(p1282,plain,
select(queue_283,tail) = index_282,
inference(superposition,[status(thm)],[c281,c0]) ).
cnf(p2330,plain,
select(q7,tail) = index_282,
inference(superposition,[status(thm)],[c359,p1282]) ).
cnf(f179,hypothesis,
index_285 = select(q7,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp169) ).
fof(f179_nnf,plain,
index_285 = select(q7,tail),
inference(nnf_transformation,[status(thm)],[f179]) ).
cnf(c179,plain,
index_285 = select(q7,tail),
inference(cnf_transformation,[status(esa)],[f179_nnf]) ).
cnf(p2331,plain,
index_285 = index_282,
inference(demodulation,[status(thm)],[p2330,c179]) ).
cnf(f178,hypothesis,
index_282 = s(index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f178_nnf,plain,
index_282 = s(index_279),
inference(nnf_transformation,[status(thm)],[f178]) ).
cnf(c178,plain,
index_282 = s(index_279),
inference(cnf_transformation,[status(esa)],[f178_nnf]) ).
cnf(p470,plain,
p(index_282) = index_279,
inference(superposition,[status(thm)],[c178,c5]) ).
cnf(p2333,plain,
p(index_285) = index_279,
inference(superposition,[status(thm)],[p2331,p470]) ).
cnf(f180,hypothesis,
index_288 = s(index_285),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp170) ).
fof(f180_nnf,plain,
index_288 = s(index_285),
inference(nnf_transformation,[status(thm)],[f180]) ).
cnf(c180,plain,
index_288 = s(index_285),
inference(cnf_transformation,[status(esa)],[f180_nnf]) ).
cnf(p472,plain,
p(index_288) = index_285,
inference(superposition,[status(thm)],[c180,c5]) ).
cnf(p612,plain,
s(index_285) = index_288,
inference(superposition,[status(thm)],[p472,c6]) ).
cnf(p1618,plain,
s(index_288) = p(index_285),
inference(superposition,[status(thm)],[p612,p367]) ).
cnf(p2335,plain,
s(index_288) = index_279,
inference(demodulation,[status(thm)],[p2333,p1618]) ).
cnf(p2355,plain,
index_273 = index_288,
inference(superposition,[status(thm)],[p2335,c5]) ).
cnf(p2358,plain,
index_288 = index_273,
inference(superposition,[status(thm)],[p2355,p612]) ).
cnf(p1303,plain,
select(queue_289,tail) = index_288,
inference(superposition,[status(thm)],[c283,c0]) ).
cnf(p2360,plain,
select(queue_289,tail) = index_273,
inference(demodulation,[status(thm)],[p2358,p1303]) ).
cnf(p3181,plain,
select(q8,tail) = index_135,
inference(superposition,[status(thm)],[c360,p2360]) ).
cnf(p1327,plain,
select(queue_295,tail) = index_294,
inference(superposition,[status(thm)],[c286,c0]) ).
cnf(p2368,plain,
select(q9,tail) = index_294,
inference(superposition,[status(thm)],[c361,p1327]) ).
cnf(f208,hypothesis,
index_9 = select(q9,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f208_nnf,plain,
index_9 = select(q9,tail),
inference(nnf_transformation,[status(thm)],[f208]) ).
cnf(c208,plain,
index_9 = select(q9,tail),
inference(cnf_transformation,[status(esa)],[f208_nnf]) ).
cnf(p2369,plain,
index_9 = index_294,
inference(demodulation,[status(thm)],[p2368,c208]) ).
cnf(f182,hypothesis,
index_294 = s(index_291),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f182_nnf,plain,
index_294 = s(index_291),
inference(nnf_transformation,[status(thm)],[f182]) ).
cnf(c182,plain,
index_294 = s(index_291),
inference(cnf_transformation,[status(esa)],[f182_nnf]) ).
cnf(p476,plain,
p(index_294) = index_291,
inference(superposition,[status(thm)],[c182,c5]) ).
cnf(p2371,plain,
index_21 = index_291,
inference(superposition,[status(thm)],[p2369,p476]) ).
cnf(f181,hypothesis,
index_291 = select(q8,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp171) ).
fof(f181_nnf,plain,
index_291 = select(q8,tail),
inference(nnf_transformation,[status(thm)],[f181]) ).
cnf(c181,plain,
index_291 = select(q8,tail),
inference(cnf_transformation,[status(esa)],[f181_nnf]) ).
cnf(p2387,plain,
index_21 = select(q8,tail),
inference(superposition,[status(thm)],[p2371,c181]) ).
cnf(p3182,plain,
index_21 = index_135,
inference(demodulation,[status(thm)],[p3181,p2387]) ).
cnf(p903,plain,
select(queue_13,tail) = index_12,
inference(superposition,[status(thm)],[c225,c0]) ).
cnf(p1140,plain,
select(q10,tail) = index_12,
inference(superposition,[status(thm)],[c314,p903]) ).
cnf(f129,hypothesis,
index_15 = select(q10,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp119) ).
fof(f129_nnf,plain,
index_15 = select(q10,tail),
inference(nnf_transformation,[status(thm)],[f129]) ).
cnf(c129,plain,
index_15 = select(q10,tail),
inference(cnf_transformation,[status(esa)],[f129_nnf]) ).
cnf(p1141,plain,
index_15 = index_12,
inference(demodulation,[status(thm)],[p1140,c129]) ).
cnf(f118,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f118_nnf,plain,
index_12 = s(index_9),
inference(nnf_transformation,[status(thm)],[f118]) ).
cnf(c118,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(esa)],[f118_nnf]) ).
cnf(p388,plain,
p(index_12) = index_9,
inference(superposition,[status(thm)],[c118,c5]) ).
cnf(p1144,plain,
p(index_15) = index_9,
inference(superposition,[status(thm)],[p1141,p388]) ).
cnf(p1679,plain,
index_24 = index_9,
inference(superposition,[status(thm)],[p1144,p367]) ).
cnf(f162,hypothesis,
index_24 = s(index_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f162_nnf,plain,
index_24 = s(index_21),
inference(nnf_transformation,[status(thm)],[f162]) ).
cnf(c162,plain,
index_24 = s(index_21),
inference(cnf_transformation,[status(esa)],[f162_nnf]) ).
cnf(p448,plain,
p(index_24) = index_21,
inference(superposition,[status(thm)],[c162,c5]) ).
cnf(p586,plain,
s(index_21) = index_24,
inference(superposition,[status(thm)],[p448,c6]) ).
cnf(p1683,plain,
s(index_21) = index_9,
inference(demodulation,[status(thm)],[p1679,p586]) ).
cnf(p3249,plain,
index_201 = index_9,
inference(superposition,[status(thm)],[p3182,p1683]) ).
cnf(p1473,plain,
select(queue_73,tail) = index_72,
inference(superposition,[status(thm)],[c303,c0]) ).
cnf(p2595,plain,
select(q2,tail) = index_72,
inference(superposition,[status(thm)],[c324,p1473]) ).
cnf(f124,hypothesis,
index_135 = select(q2,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f124_nnf,plain,
index_135 = select(q2,tail),
inference(nnf_transformation,[status(thm)],[f124]) ).
cnf(c124,plain,
index_135 = select(q2,tail),
inference(cnf_transformation,[status(esa)],[f124_nnf]) ).
cnf(p2596,plain,
index_135 = index_72,
inference(demodulation,[status(thm)],[p2595,c124]) ).
cnf(f202,hypothesis,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp192) ).
fof(f202_nnf,plain,
index_72 = s(index_69),
inference(nnf_transformation,[status(thm)],[f202]) ).
cnf(c202,plain,
index_72 = s(index_69),
inference(cnf_transformation,[status(esa)],[f202_nnf]) ).
cnf(p503,plain,
p(index_72) = index_69,
inference(superposition,[status(thm)],[c202,c5]) ).
cnf(p640,plain,
s(index_69) = index_72,
inference(superposition,[status(thm)],[p503,c6]) ).
cnf(p2601,plain,
index_72 = index_135,
inference(superposition,[status(thm)],[p2596,p640]) ).
cnf(p1468,plain,
select(queue_7,tail) = index_6,
inference(superposition,[status(thm)],[c301,c0]) ).
cnf(p2564,plain,
select(q1,tail) = index_6,
inference(superposition,[status(thm)],[c313,p1468]) ).
cnf(f201,hypothesis,
index_69 = select(q1,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f201_nnf,plain,
index_69 = select(q1,tail),
inference(nnf_transformation,[status(thm)],[f201]) ).
cnf(c201,plain,
index_69 = select(q1,tail),
inference(cnf_transformation,[status(esa)],[f201_nnf]) ).
cnf(p2565,plain,
index_69 = index_6,
inference(demodulation,[status(thm)],[p2564,c201]) ).
cnf(f197,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f197_nnf,plain,
index_6 = s(index_3),
inference(nnf_transformation,[status(thm)],[f197]) ).
cnf(c197,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(esa)],[f197_nnf]) ).
cnf(p494,plain,
p(index_6) = index_3,
inference(superposition,[status(thm)],[c197,c5]) ).
cnf(p2567,plain,
p(index_69) = index_3,
inference(superposition,[status(thm)],[p2565,p494]) ).
cnf(p1628,plain,
s(index_72) = p(index_69),
inference(superposition,[status(thm)],[p640,p367]) ).
cnf(p2569,plain,
s(index_72) = index_3,
inference(demodulation,[status(thm)],[p2567,p1628]) ).
cnf(p2610,plain,
s(index_135) = index_3,
inference(demodulation,[status(thm)],[p2601,p2569]) ).
cnf(p913,plain,
select(queue_139,tail) = index_138,
inference(superposition,[status(thm)],[c229,c0]) ).
cnf(p1190,plain,
select(q3,tail) = index_138,
inference(superposition,[status(thm)],[c335,p913]) ).
cnf(f148,hypothesis,
index_201 = select(q3,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f148_nnf,plain,
index_201 = select(q3,tail),
inference(nnf_transformation,[status(thm)],[f148]) ).
cnf(c148,plain,
index_201 = select(q3,tail),
inference(cnf_transformation,[status(esa)],[f148_nnf]) ).
cnf(p1191,plain,
index_201 = index_138,
inference(demodulation,[status(thm)],[p1190,c148]) ).
cnf(f125,hypothesis,
index_138 = s(index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp115) ).
fof(f125_nnf,plain,
index_138 = s(index_135),
inference(nnf_transformation,[status(thm)],[f125]) ).
cnf(c125,plain,
index_138 = s(index_135),
inference(cnf_transformation,[status(esa)],[f125_nnf]) ).
cnf(p399,plain,
p(index_138) = index_135,
inference(superposition,[status(thm)],[c125,c5]) ).
cnf(p537,plain,
s(index_135) = index_138,
inference(superposition,[status(thm)],[p399,c6]) ).
cnf(p1196,plain,
index_138 = index_201,
inference(superposition,[status(thm)],[p1191,p537]) ).
cnf(p1198,plain,
s(index_135) = index_201,
inference(demodulation,[status(thm)],[p1196,p537]) ).
cnf(p2645,plain,
index_3 = index_201,
inference(superposition,[status(thm)],[p2610,p1198]) ).
cnf(f185,hypothesis,
index_3 = select(q0,tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f185_nnf,plain,
index_3 = select(q0,tail),
inference(nnf_transformation,[status(thm)],[f185]) ).
cnf(c185,plain,
index_3 = select(q0,tail),
inference(cnf_transformation,[status(esa)],[f185_nnf]) ).
cnf(p2647,plain,
index_201 = select(q0,tail),
inference(demodulation,[status(thm)],[p2645,c185]) ).
cnf(p3270,plain,
index_9 = select(q0,tail),
inference(demodulation,[status(thm)],[p3249,p2647]) ).
cnf(p4334,plain,
( index_9 = index_0
| head = tail ),
inference(superposition,[status(thm)],[p2941,p3270]) ).
cnf(p16038,plain,
( index_9 = index_297
| head = tail
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p16025,p4334]) ).
cnf(f109,hypothesis,
elem_298 = select(earray_296,index_297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f109_nnf,plain,
elem_298 = select(earray_296,index_297),
inference(nnf_transformation,[status(thm)],[f109]) ).
cnf(c109,plain,
elem_298 = select(earray_296,index_297),
inference(cnf_transformation,[status(esa)],[f109_nnf]) ).
cnf(p697,plain,
( select(store(earray_296,X0,X1),index_297) = elem_298
| X0 = index_297 ),
inference(superposition,[status(thm)],[c109,c1]) ).
cnf(p2487,plain,
( select(earray_296,index_297) = elem_298
| X0 = index_297
| X0 = index_297 ),
inference(superposition,[status(thm)],[c1,p697]) ).
cnf(p5417,plain,
( select(earray_296,index_297) = elem_298
| X0 = index_297 ),
inference(factoring,[status(thm)],[p2487]) ).
cnf(f8,axiom,
s(X) != X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',as1) ).
fof(f8_nnf,plain,
! [X] : s(X) != X,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : s(X) != X,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
s(X0) != X0,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p5420,plain,
select(earray_296,index_297) = elem_298,
inference(resolution,[status(thm)],[p5417,c8]) ).
cnf(p16069,plain,
( elem_301 = elem_298
| head = tail
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p16038,p5420]) ).
cnf(f362,negated_conjecture,
elem_298 != elem_301,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f362_nnf,plain,
elem_298 != elem_301,
inference(nnf_transformation,[status(thm)],[f362]) ).
fof(f362_sk,plain,
elem_298 != elem_301,
inference(skolemisation,[status(esa)],[f362_nnf]) ).
cnf(c362,plain,
elem_298 != elem_301,
inference(cnf_transformation,[status(esa)],[f362_sk]) ).
cnf(p16104,plain,
( elem_298 != elem_298
| head = tail
| seq = head
| tail = head ),
inference(superposition,[status(thm)],[p16069,c362]) ).
cnf(p16118,plain,
( head = tail
| seq = head
| tail = head ),
inference(equality_resolution,[status(thm)],[p16104]) ).
cnf(f3,axiom,
head != seq,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_seq) ).
fof(f3_nnf,plain,
head != seq,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
head != seq,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
head != seq,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p16119,plain,
( head != head
| head = tail
| tail = head ),
inference(superposition,[status(thm)],[p16118,c3]) ).
cnf(p18055,plain,
( head = tail
| tail = head ),
inference(equality_resolution,[status(thm)],[p16119]) ).
cnf(f2,axiom,
head != tail,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',head_distinct_from_tail) ).
fof(f2_nnf,plain,
head != tail,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
head != tail,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
head != tail,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p18056,plain,
( head != head
| head = tail ),
inference(superposition,[status(thm)],[p18055,c2]) ).
cnf(p19132,plain,
head = tail,
inference(equality_resolution,[status(thm)],[p18056]) ).
cnf(p19133,plain,
$false,
inference(resolution,[status(thm)],[p19132,c2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV571-1.049 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n016.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Thu Sep 24 20:41:42 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.93/71.94 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.93/71.94 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------