%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV570-1.049 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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 63.95s 9.81s
% Output : Proof 63.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 100
% Number of leaves : 159
% Syntax : Number of formulae : 874 ( 874 unt; 0 def)
% Number of atoms : 874 ( 873 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 262 ( 262 usr; 252 con; 0-3 aty)
% Number of variables : 81 ( 16 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f362,hypothesis,
q49 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp346) ).
fof(f362_nnf,plain,
q49 = queue_265,
inference(nnf_transformation,[status(thm)],[f362]) ).
cnf(c362,plain,
q49 = queue_265,
inference(cnf_transformation,[status(esa)],[f362_nnf]) ).
cnf(f281,hypothesis,
queue_265 = rstore_tail(queue_263,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp265) ).
fof(f281_nnf,plain,
queue_265 = rstore_tail(queue_263,index_264),
inference(nnf_transformation,[status(thm)],[f281]) ).
cnf(c281,plain,
queue_265 = rstore_tail(queue_263,index_264),
inference(cnf_transformation,[status(esa)],[f281_nnf]) ).
cnf(f7,axiom,
rselect_head(rstore_tail(A,E)) = rselect_head(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_head_tail) ).
fof(f7_nnf,plain,
! [A,E] : rselect_head(rstore_tail(A,E)) = rselect_head(A),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,E] : rselect_head(rstore_tail(A,E)) = rselect_head(A),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
rselect_head(rstore_tail(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1071,plain,
rselect_head(queue_265) = rselect_head(queue_263),
inference(superposition,[status(thm)],[c281,c7]) ).
cnf(p3123,plain,
index_297 = rselect_head(q48),
inference(superposition,[status(thm)],[c362,p1071]) ).
cnf(p3601,plain,
rselect_head(q48) = index_297,
inference(superposition,[status(thm)],[p3123,c7]) ).
cnf(f361,hypothesis,
q48 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp345) ).
fof(f361_nnf,plain,
q48 = queue_259,
inference(nnf_transformation,[status(thm)],[f361]) ).
cnf(c361,plain,
q48 = queue_259,
inference(cnf_transformation,[status(esa)],[f361_nnf]) ).
cnf(f279,hypothesis,
queue_259 = rstore_tail(queue_257,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp263) ).
fof(f279_nnf,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(nnf_transformation,[status(thm)],[f279]) ).
cnf(c279,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(cnf_transformation,[status(esa)],[f279_nnf]) ).
cnf(p1063,plain,
rselect_head(queue_259) = rselect_head(queue_257),
inference(superposition,[status(thm)],[c279,c7]) ).
cnf(p3112,plain,
rselect_head(q48) = rselect_head(queue_257),
inference(superposition,[status(thm)],[c361,p1063]) ).
cnf(p3603,plain,
index_297 = rselect_head(queue_257),
inference(demodulation,[status(thm)],[p3601,p3112]) ).
cnf(p3652,plain,
rselect_head(queue_257) = index_297,
inference(superposition,[status(thm)],[p3603,c7]) ).
cnf(f360,hypothesis,
q47 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp344) ).
fof(f360_nnf,plain,
q47 = queue_253,
inference(nnf_transformation,[status(thm)],[f360]) ).
cnf(c360,plain,
q47 = queue_253,
inference(cnf_transformation,[status(esa)],[f360_nnf]) ).
cnf(f277,hypothesis,
queue_253 = rstore_tail(queue_251,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp261) ).
fof(f277_nnf,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(nnf_transformation,[status(thm)],[f277]) ).
cnf(c277,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(cnf_transformation,[status(esa)],[f277_nnf]) ).
cnf(p1047,plain,
rselect_head(queue_253) = rselect_head(queue_251),
inference(superposition,[status(thm)],[c277,c7]) ).
cnf(p3102,plain,
rselect_head(q47) = rselect_head(q46),
inference(superposition,[status(thm)],[c360,p1047]) ).
cnf(f278,hypothesis,
queue_257 = rstore_seq(q47,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp262) ).
fof(f278_nnf,plain,
queue_257 = rstore_seq(q47,earray_256),
inference(nnf_transformation,[status(thm)],[f278]) ).
cnf(c278,plain,
queue_257 = rstore_seq(q47,earray_256),
inference(cnf_transformation,[status(esa)],[f278_nnf]) ).
cnf(f8,axiom,
rselect_head(rstore_seq(A,E)) = rselect_head(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_head_seq) ).
fof(f8_nnf,plain,
! [A,E] : rselect_head(rstore_seq(A,E)) = rselect_head(A),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,E] : rselect_head(rstore_seq(A,E)) = rselect_head(A),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
rselect_head(rstore_seq(X0,X1)) = rselect_head(X0),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p1050,plain,
rselect_head(queue_257) = rselect_head(q47),
inference(superposition,[status(thm)],[c278,c8]) ).
cnf(p3103,plain,
rselect_head(queue_257) = rselect_head(q46),
inference(demodulation,[status(thm)],[p3102,p1050]) ).
cnf(p3654,plain,
index_297 = rselect_head(q46),
inference(demodulation,[status(thm)],[p3652,p3103]) ).
cnf(p3659,plain,
rselect_head(q46) = index_297,
inference(superposition,[status(thm)],[p3654,c7]) ).
cnf(f359,hypothesis,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp343) ).
fof(f359_nnf,plain,
q46 = queue_247,
inference(nnf_transformation,[status(thm)],[f359]) ).
cnf(c359,plain,
q46 = queue_247,
inference(cnf_transformation,[status(esa)],[f359_nnf]) ).
cnf(f274,hypothesis,
queue_247 = rstore_tail(queue_245,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp258) ).
fof(f274_nnf,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(nnf_transformation,[status(thm)],[f274]) ).
cnf(c274,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(cnf_transformation,[status(esa)],[f274_nnf]) ).
cnf(p1018,plain,
rselect_head(queue_247) = rselect_head(queue_245),
inference(superposition,[status(thm)],[c274,c7]) ).
cnf(p3078,plain,
rselect_head(q46) = rselect_head(queue_245),
inference(superposition,[status(thm)],[c359,p1018]) ).
cnf(p3661,plain,
index_297 = rselect_head(queue_245),
inference(demodulation,[status(thm)],[p3659,p3078]) ).
cnf(p3666,plain,
rselect_head(queue_245) = index_297,
inference(superposition,[status(thm)],[p3661,c7]) ).
cnf(f358,hypothesis,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp342) ).
fof(f358_nnf,plain,
q45 = queue_241,
inference(nnf_transformation,[status(thm)],[f358]) ).
cnf(c358,plain,
q45 = queue_241,
inference(cnf_transformation,[status(esa)],[f358_nnf]) ).
cnf(f272,hypothesis,
queue_241 = rstore_tail(queue_239,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp256) ).
fof(f272_nnf,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(nnf_transformation,[status(thm)],[f272]) ).
cnf(c272,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(cnf_transformation,[status(esa)],[f272_nnf]) ).
cnf(p993,plain,
rselect_head(queue_241) = rselect_head(queue_239),
inference(superposition,[status(thm)],[c272,c7]) ).
cnf(p3068,plain,
rselect_head(q45) = rselect_head(q44),
inference(superposition,[status(thm)],[c358,p993]) ).
cnf(f273,hypothesis,
queue_245 = rstore_seq(q45,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp257) ).
fof(f273_nnf,plain,
queue_245 = rstore_seq(q45,earray_244),
inference(nnf_transformation,[status(thm)],[f273]) ).
cnf(c273,plain,
queue_245 = rstore_seq(q45,earray_244),
inference(cnf_transformation,[status(esa)],[f273_nnf]) ).
cnf(p1005,plain,
rselect_head(queue_245) = rselect_head(q45),
inference(superposition,[status(thm)],[c273,c8]) ).
cnf(p3069,plain,
rselect_head(queue_245) = rselect_head(q44),
inference(demodulation,[status(thm)],[p3068,p1005]) ).
cnf(p3668,plain,
index_297 = rselect_head(q44),
inference(demodulation,[status(thm)],[p3666,p3069]) ).
cnf(p3671,plain,
rselect_head(q44) = index_297,
inference(superposition,[status(thm)],[p3668,c7]) ).
cnf(f357,hypothesis,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp341) ).
fof(f357_nnf,plain,
q44 = queue_235,
inference(nnf_transformation,[status(thm)],[f357]) ).
cnf(c357,plain,
q44 = queue_235,
inference(cnf_transformation,[status(esa)],[f357_nnf]) ).
cnf(f270,hypothesis,
queue_235 = rstore_tail(queue_233,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp254) ).
fof(f270_nnf,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(nnf_transformation,[status(thm)],[f270]) ).
cnf(c270,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(cnf_transformation,[status(esa)],[f270_nnf]) ).
cnf(p977,plain,
rselect_head(queue_235) = rselect_head(queue_233),
inference(superposition,[status(thm)],[c270,c7]) ).
cnf(p3060,plain,
rselect_head(q44) = rselect_head(queue_233),
inference(superposition,[status(thm)],[c357,p977]) ).
cnf(p3673,plain,
index_297 = rselect_head(queue_233),
inference(demodulation,[status(thm)],[p3671,p3060]) ).
cnf(p3675,plain,
rselect_head(queue_233) = index_297,
inference(superposition,[status(thm)],[p3673,c7]) ).
cnf(f356,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp340) ).
fof(f356_nnf,plain,
q43 = queue_229,
inference(nnf_transformation,[status(thm)],[f356]) ).
cnf(c356,plain,
q43 = queue_229,
inference(cnf_transformation,[status(esa)],[f356_nnf]) ).
cnf(f267,hypothesis,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp251) ).
fof(f267_nnf,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(nnf_transformation,[status(thm)],[f267]) ).
cnf(c267,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(cnf_transformation,[status(esa)],[f267_nnf]) ).
cnf(p949,plain,
rselect_head(queue_229) = rselect_head(queue_227),
inference(superposition,[status(thm)],[c267,c7]) ).
cnf(p3049,plain,
rselect_head(q43) = rselect_head(q42),
inference(superposition,[status(thm)],[c356,p949]) ).
cnf(f269,hypothesis,
queue_233 = rstore_seq(q43,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp253) ).
fof(f269_nnf,plain,
queue_233 = rstore_seq(q43,earray_232),
inference(nnf_transformation,[status(thm)],[f269]) ).
cnf(c269,plain,
queue_233 = rstore_seq(q43,earray_232),
inference(cnf_transformation,[status(esa)],[f269_nnf]) ).
cnf(p965,plain,
rselect_head(queue_233) = rselect_head(q43),
inference(superposition,[status(thm)],[c269,c8]) ).
cnf(p3050,plain,
rselect_head(queue_233) = rselect_head(q42),
inference(demodulation,[status(thm)],[p3049,p965]) ).
cnf(p3676,plain,
index_297 = rselect_head(q42),
inference(demodulation,[status(thm)],[p3675,p3050]) ).
cnf(p3680,plain,
rselect_head(q42) = index_297,
inference(superposition,[status(thm)],[p3676,c7]) ).
cnf(f355,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp339) ).
fof(f355_nnf,plain,
q42 = queue_223,
inference(nnf_transformation,[status(thm)],[f355]) ).
cnf(c355,plain,
q42 = queue_223,
inference(cnf_transformation,[status(esa)],[f355_nnf]) ).
cnf(f265,hypothesis,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp249) ).
fof(f265_nnf,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(nnf_transformation,[status(thm)],[f265]) ).
cnf(c265,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(cnf_transformation,[status(esa)],[f265_nnf]) ).
cnf(p937,plain,
rselect_head(queue_223) = rselect_head(queue_221),
inference(superposition,[status(thm)],[c265,c7]) ).
cnf(p3043,plain,
rselect_head(q42) = rselect_head(queue_221),
inference(superposition,[status(thm)],[c355,p937]) ).
cnf(p3682,plain,
index_297 = rselect_head(queue_221),
inference(demodulation,[status(thm)],[p3680,p3043]) ).
cnf(p3686,plain,
rselect_head(queue_221) = index_297,
inference(superposition,[status(thm)],[p3682,c7]) ).
cnf(f354,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp338) ).
fof(f354_nnf,plain,
q41 = queue_217,
inference(nnf_transformation,[status(thm)],[f354]) ).
cnf(c354,plain,
q41 = queue_217,
inference(cnf_transformation,[status(esa)],[f354_nnf]) ).
cnf(f263,hypothesis,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp247) ).
fof(f263_nnf,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(nnf_transformation,[status(thm)],[f263]) ).
cnf(c263,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(cnf_transformation,[status(esa)],[f263_nnf]) ).
cnf(p926,plain,
rselect_head(queue_217) = rselect_head(queue_215),
inference(superposition,[status(thm)],[c263,c7]) ).
cnf(p2959,plain,
rselect_head(q41) = rselect_head(q40),
inference(superposition,[status(thm)],[c354,p926]) ).
cnf(f264,hypothesis,
queue_221 = rstore_seq(q41,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp248) ).
fof(f264_nnf,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(nnf_transformation,[status(thm)],[f264]) ).
cnf(c264,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(cnf_transformation,[status(esa)],[f264_nnf]) ).
cnf(p931,plain,
rselect_head(queue_221) = rselect_head(q41),
inference(superposition,[status(thm)],[c264,c8]) ).
cnf(p2960,plain,
rselect_head(queue_221) = rselect_head(q40),
inference(demodulation,[status(thm)],[p2959,p931]) ).
cnf(p3688,plain,
index_297 = rselect_head(q40),
inference(demodulation,[status(thm)],[p3686,p2960]) ).
cnf(p3691,plain,
rselect_head(q40) = index_297,
inference(superposition,[status(thm)],[p3688,c7]) ).
cnf(f353,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp337) ).
fof(f353_nnf,plain,
q40 = queue_211,
inference(nnf_transformation,[status(thm)],[f353]) ).
cnf(c353,plain,
q40 = queue_211,
inference(cnf_transformation,[status(esa)],[f353_nnf]) ).
cnf(f261,hypothesis,
queue_211 = rstore_tail(queue_209,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f261_nnf,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(nnf_transformation,[status(thm)],[f261]) ).
cnf(c261,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(cnf_transformation,[status(esa)],[f261_nnf]) ).
cnf(p913,plain,
rselect_head(queue_211) = rselect_head(queue_209),
inference(superposition,[status(thm)],[c261,c7]) ).
cnf(p2953,plain,
rselect_head(q40) = rselect_head(queue_209),
inference(superposition,[status(thm)],[c353,p913]) ).
cnf(p3693,plain,
index_297 = rselect_head(queue_209),
inference(demodulation,[status(thm)],[p3691,p2953]) ).
cnf(p3695,plain,
rselect_head(queue_209) = index_297,
inference(superposition,[status(thm)],[p3693,c7]) ).
cnf(f351,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp335) ).
fof(f351_nnf,plain,
q39 = queue_199,
inference(nnf_transformation,[status(thm)],[f351]) ).
cnf(c351,plain,
q39 = queue_199,
inference(cnf_transformation,[status(esa)],[f351_nnf]) ).
cnf(f257,hypothesis,
queue_199 = rstore_tail(queue_197,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f257_nnf,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(nnf_transformation,[status(thm)],[f257]) ).
cnf(c257,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(cnf_transformation,[status(esa)],[f257_nnf]) ).
cnf(p889,plain,
rselect_head(queue_199) = rselect_head(queue_197),
inference(superposition,[status(thm)],[c257,c7]) ).
cnf(p2815,plain,
rselect_head(q39) = rselect_head(q38),
inference(superposition,[status(thm)],[c351,p889]) ).
cnf(f260,hypothesis,
queue_209 = rstore_seq(q39,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f260_nnf,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(nnf_transformation,[status(thm)],[f260]) ).
cnf(c260,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(cnf_transformation,[status(esa)],[f260_nnf]) ).
cnf(p907,plain,
rselect_head(queue_209) = rselect_head(q39),
inference(superposition,[status(thm)],[c260,c8]) ).
cnf(p2816,plain,
rselect_head(queue_209) = rselect_head(q38),
inference(demodulation,[status(thm)],[p2815,p907]) ).
cnf(p3696,plain,
index_297 = rselect_head(q38),
inference(demodulation,[status(thm)],[p3695,p2816]) ).
cnf(p3700,plain,
rselect_head(q38) = index_297,
inference(superposition,[status(thm)],[p3696,c7]) ).
cnf(f350,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp334) ).
fof(f350_nnf,plain,
q38 = queue_193,
inference(nnf_transformation,[status(thm)],[f350]) ).
cnf(c350,plain,
q38 = queue_193,
inference(cnf_transformation,[status(esa)],[f350_nnf]) ).
cnf(f255,hypothesis,
queue_193 = rstore_tail(queue_191,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f255_nnf,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(nnf_transformation,[status(thm)],[f255]) ).
cnf(c255,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(cnf_transformation,[status(esa)],[f255_nnf]) ).
cnf(p877,plain,
rselect_head(queue_193) = rselect_head(queue_191),
inference(superposition,[status(thm)],[c255,c7]) ).
cnf(p2793,plain,
rselect_head(q38) = rselect_head(queue_191),
inference(superposition,[status(thm)],[c350,p877]) ).
cnf(p3702,plain,
index_297 = rselect_head(queue_191),
inference(demodulation,[status(thm)],[p3700,p2793]) ).
cnf(p3706,plain,
rselect_head(queue_191) = index_297,
inference(superposition,[status(thm)],[p3702,c7]) ).
cnf(f349,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp333) ).
fof(f349_nnf,plain,
q37 = queue_187,
inference(nnf_transformation,[status(thm)],[f349]) ).
cnf(c349,plain,
q37 = queue_187,
inference(cnf_transformation,[status(esa)],[f349_nnf]) ).
cnf(f252,hypothesis,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f252_nnf,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(nnf_transformation,[status(thm)],[f252]) ).
cnf(c252,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(cnf_transformation,[status(esa)],[f252_nnf]) ).
cnf(p859,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(superposition,[status(thm)],[c252,c7]) ).
cnf(p2742,plain,
rselect_head(q37) = rselect_head(q36),
inference(superposition,[status(thm)],[c349,p859]) ).
cnf(f254,hypothesis,
queue_191 = rstore_seq(q37,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp238) ).
fof(f254_nnf,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(nnf_transformation,[status(thm)],[f254]) ).
cnf(c254,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(cnf_transformation,[status(esa)],[f254_nnf]) ).
cnf(p871,plain,
rselect_head(queue_191) = rselect_head(q37),
inference(superposition,[status(thm)],[c254,c8]) ).
cnf(p2743,plain,
rselect_head(queue_191) = rselect_head(q36),
inference(demodulation,[status(thm)],[p2742,p871]) ).
cnf(p3708,plain,
index_297 = rselect_head(q36),
inference(demodulation,[status(thm)],[p3706,p2743]) ).
cnf(p3711,plain,
rselect_head(q36) = index_297,
inference(superposition,[status(thm)],[p3708,c7]) ).
cnf(f348,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp332) ).
fof(f348_nnf,plain,
q36 = queue_181,
inference(nnf_transformation,[status(thm)],[f348]) ).
cnf(c348,plain,
q36 = queue_181,
inference(cnf_transformation,[status(esa)],[f348_nnf]) ).
cnf(f250,hypothesis,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp234) ).
fof(f250_nnf,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(nnf_transformation,[status(thm)],[f250]) ).
cnf(c250,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(cnf_transformation,[status(esa)],[f250_nnf]) ).
cnf(p848,plain,
rselect_head(queue_181) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c250,c7]) ).
cnf(p2735,plain,
rselect_head(q36) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c348,p848]) ).
cnf(p3713,plain,
index_297 = rselect_head(queue_179),
inference(demodulation,[status(thm)],[p3711,p2735]) ).
cnf(p3715,plain,
rselect_head(queue_179) = index_297,
inference(superposition,[status(thm)],[p3713,c7]) ).
cnf(f347,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp331) ).
fof(f347_nnf,plain,
q35 = queue_175,
inference(nnf_transformation,[status(thm)],[f347]) ).
cnf(c347,plain,
q35 = queue_175,
inference(cnf_transformation,[status(esa)],[f347_nnf]) ).
cnf(f248,hypothesis,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f248_nnf,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(nnf_transformation,[status(thm)],[f248]) ).
cnf(c248,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(cnf_transformation,[status(esa)],[f248_nnf]) ).
cnf(p835,plain,
rselect_head(queue_175) = rselect_head(queue_173),
inference(superposition,[status(thm)],[c248,c7]) ).
cnf(p2706,plain,
rselect_head(q35) = rselect_head(q34),
inference(superposition,[status(thm)],[c347,p835]) ).
cnf(f249,hypothesis,
queue_179 = rstore_seq(q35,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f249_nnf,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(nnf_transformation,[status(thm)],[f249]) ).
cnf(c249,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(cnf_transformation,[status(esa)],[f249_nnf]) ).
cnf(p841,plain,
rselect_head(queue_179) = rselect_head(q35),
inference(superposition,[status(thm)],[c249,c8]) ).
cnf(p2707,plain,
rselect_head(queue_179) = rselect_head(q34),
inference(demodulation,[status(thm)],[p2706,p841]) ).
cnf(p3717,plain,
index_297 = rselect_head(q34),
inference(demodulation,[status(thm)],[p3715,p2707]) ).
cnf(p3719,plain,
rselect_head(q34) = index_297,
inference(superposition,[status(thm)],[p3717,c7]) ).
cnf(f346,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp330) ).
fof(f346_nnf,plain,
q34 = queue_169,
inference(nnf_transformation,[status(thm)],[f346]) ).
cnf(c346,plain,
q34 = queue_169,
inference(cnf_transformation,[status(esa)],[f346_nnf]) ).
cnf(f245,hypothesis,
queue_169 = rstore_tail(queue_167,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f245_nnf,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(nnf_transformation,[status(thm)],[f245]) ).
cnf(c245,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(cnf_transformation,[status(esa)],[f245_nnf]) ).
cnf(p817,plain,
rselect_head(queue_169) = rselect_head(queue_167),
inference(superposition,[status(thm)],[c245,c7]) ).
cnf(p2655,plain,
rselect_head(q34) = rselect_head(queue_167),
inference(superposition,[status(thm)],[c346,p817]) ).
cnf(p3721,plain,
index_297 = rselect_head(queue_167),
inference(demodulation,[status(thm)],[p3719,p2655]) ).
cnf(p3723,plain,
rselect_head(queue_167) = index_297,
inference(superposition,[status(thm)],[p3721,c7]) ).
cnf(f345,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp329) ).
fof(f345_nnf,plain,
q33 = queue_163,
inference(nnf_transformation,[status(thm)],[f345]) ).
cnf(c345,plain,
q33 = queue_163,
inference(cnf_transformation,[status(esa)],[f345_nnf]) ).
cnf(f243,hypothesis,
queue_163 = rstore_tail(queue_161,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f243_nnf,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(nnf_transformation,[status(thm)],[f243]) ).
cnf(c243,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(cnf_transformation,[status(esa)],[f243_nnf]) ).
cnf(p806,plain,
rselect_head(queue_163) = rselect_head(queue_161),
inference(superposition,[status(thm)],[c243,c7]) ).
cnf(p2646,plain,
rselect_head(q33) = rselect_head(q32),
inference(superposition,[status(thm)],[c345,p806]) ).
cnf(f244,hypothesis,
queue_167 = rstore_seq(q33,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp228) ).
fof(f244_nnf,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(nnf_transformation,[status(thm)],[f244]) ).
cnf(c244,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(cnf_transformation,[status(esa)],[f244_nnf]) ).
cnf(p810,plain,
rselect_head(queue_167) = rselect_head(q33),
inference(superposition,[status(thm)],[c244,c8]) ).
cnf(p2647,plain,
rselect_head(queue_167) = rselect_head(q32),
inference(demodulation,[status(thm)],[p2646,p810]) ).
cnf(p3725,plain,
index_297 = rselect_head(q32),
inference(demodulation,[status(thm)],[p3723,p2647]) ).
cnf(p3728,plain,
rselect_head(q32) = index_297,
inference(superposition,[status(thm)],[p3725,c7]) ).
cnf(f344,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp328) ).
fof(f344_nnf,plain,
q32 = queue_157,
inference(nnf_transformation,[status(thm)],[f344]) ).
cnf(c344,plain,
q32 = queue_157,
inference(cnf_transformation,[status(esa)],[f344_nnf]) ).
cnf(f241,hypothesis,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f241_nnf,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(nnf_transformation,[status(thm)],[f241]) ).
cnf(c241,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(cnf_transformation,[status(esa)],[f241_nnf]) ).
cnf(p793,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c241,c7]) ).
cnf(p2640,plain,
rselect_head(q32) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c344,p793]) ).
cnf(p3730,plain,
index_297 = rselect_head(queue_155),
inference(demodulation,[status(thm)],[p3728,p2640]) ).
cnf(p3734,plain,
rselect_head(queue_155) = index_297,
inference(superposition,[status(thm)],[p3730,c7]) ).
cnf(f343,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp327) ).
fof(f343_nnf,plain,
q31 = queue_151,
inference(nnf_transformation,[status(thm)],[f343]) ).
cnf(c343,plain,
q31 = queue_151,
inference(cnf_transformation,[status(esa)],[f343_nnf]) ).
cnf(f239,hypothesis,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp223) ).
fof(f239_nnf,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(nnf_transformation,[status(thm)],[f239]) ).
cnf(c239,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(cnf_transformation,[status(esa)],[f239_nnf]) ).
cnf(p780,plain,
rselect_head(queue_151) = rselect_head(queue_149),
inference(superposition,[status(thm)],[c239,c7]) ).
cnf(p2586,plain,
rselect_head(q31) = rselect_head(q30),
inference(superposition,[status(thm)],[c343,p780]) ).
cnf(f240,hypothesis,
queue_155 = rstore_seq(q31,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f240_nnf,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(nnf_transformation,[status(thm)],[f240]) ).
cnf(c240,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(cnf_transformation,[status(esa)],[f240_nnf]) ).
cnf(p786,plain,
rselect_head(queue_155) = rselect_head(q31),
inference(superposition,[status(thm)],[c240,c8]) ).
cnf(p2587,plain,
rselect_head(queue_155) = rselect_head(q30),
inference(demodulation,[status(thm)],[p2586,p786]) ).
cnf(p3735,plain,
index_297 = rselect_head(q30),
inference(demodulation,[status(thm)],[p3734,p2587]) ).
cnf(p3736,plain,
rselect_head(q30) = index_297,
inference(superposition,[status(thm)],[p3735,c7]) ).
cnf(f342,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp326) ).
fof(f342_nnf,plain,
q30 = queue_145,
inference(nnf_transformation,[status(thm)],[f342]) ).
cnf(c342,plain,
q30 = queue_145,
inference(cnf_transformation,[status(esa)],[f342_nnf]) ).
cnf(f237,hypothesis,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f237_nnf,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(nnf_transformation,[status(thm)],[f237]) ).
cnf(c237,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(cnf_transformation,[status(esa)],[f237_nnf]) ).
cnf(p767,plain,
rselect_head(queue_145) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c237,c7]) ).
cnf(p2575,plain,
rselect_head(q30) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c342,p767]) ).
cnf(p3738,plain,
index_297 = rselect_head(queue_143),
inference(demodulation,[status(thm)],[p3736,p2575]) ).
cnf(p3745,plain,
rselect_head(queue_143) = index_297,
inference(superposition,[status(thm)],[p3738,c7]) ).
cnf(f340,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp324) ).
fof(f340_nnf,plain,
q29 = queue_133,
inference(nnf_transformation,[status(thm)],[f340]) ).
cnf(c340,plain,
q29 = queue_133,
inference(cnf_transformation,[status(esa)],[f340_nnf]) ).
cnf(f233,hypothesis,
queue_133 = rstore_tail(queue_131,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f233_nnf,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(nnf_transformation,[status(thm)],[f233]) ).
cnf(c233,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(cnf_transformation,[status(esa)],[f233_nnf]) ).
cnf(p743,plain,
rselect_head(queue_133) = rselect_head(queue_131),
inference(superposition,[status(thm)],[c233,c7]) ).
cnf(p2498,plain,
rselect_head(q29) = rselect_head(q28),
inference(superposition,[status(thm)],[c340,p743]) ).
cnf(f236,hypothesis,
queue_143 = rstore_seq(q29,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f236_nnf,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(nnf_transformation,[status(thm)],[f236]) ).
cnf(c236,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(cnf_transformation,[status(esa)],[f236_nnf]) ).
cnf(p760,plain,
rselect_head(queue_143) = rselect_head(q29),
inference(superposition,[status(thm)],[c236,c8]) ).
cnf(p2499,plain,
rselect_head(queue_143) = rselect_head(q28),
inference(demodulation,[status(thm)],[p2498,p760]) ).
cnf(p3747,plain,
index_297 = rselect_head(q28),
inference(demodulation,[status(thm)],[p3745,p2499]) ).
cnf(p3753,plain,
rselect_head(q28) = index_297,
inference(superposition,[status(thm)],[p3747,c7]) ).
cnf(f339,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp323) ).
fof(f339_nnf,plain,
q28 = queue_127,
inference(nnf_transformation,[status(thm)],[f339]) ).
cnf(c339,plain,
q28 = queue_127,
inference(cnf_transformation,[status(esa)],[f339_nnf]) ).
cnf(f230,hypothesis,
queue_127 = rstore_tail(queue_125,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp214) ).
fof(f230_nnf,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(nnf_transformation,[status(thm)],[f230]) ).
cnf(c230,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(cnf_transformation,[status(esa)],[f230_nnf]) ).
cnf(p724,plain,
rselect_head(queue_127) = rselect_head(queue_125),
inference(superposition,[status(thm)],[c230,c7]) ).
cnf(p2459,plain,
rselect_head(q28) = rselect_head(queue_125),
inference(superposition,[status(thm)],[c339,p724]) ).
cnf(p3755,plain,
index_297 = rselect_head(queue_125),
inference(demodulation,[status(thm)],[p3753,p2459]) ).
cnf(p3759,plain,
rselect_head(queue_125) = index_297,
inference(superposition,[status(thm)],[p3755,c7]) ).
cnf(f338,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp322) ).
fof(f338_nnf,plain,
q27 = queue_121,
inference(nnf_transformation,[status(thm)],[f338]) ).
cnf(c338,plain,
q27 = queue_121,
inference(cnf_transformation,[status(esa)],[f338_nnf]) ).
cnf(f228,hypothesis,
queue_121 = rstore_tail(queue_119,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f228_nnf,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(nnf_transformation,[status(thm)],[f228]) ).
cnf(c228,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(cnf_transformation,[status(esa)],[f228_nnf]) ).
cnf(p713,plain,
rselect_head(queue_121) = rselect_head(queue_119),
inference(superposition,[status(thm)],[c228,c7]) ).
cnf(p2415,plain,
rselect_head(q27) = rselect_head(q26),
inference(superposition,[status(thm)],[c338,p713]) ).
cnf(f229,hypothesis,
queue_125 = rstore_seq(q27,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f229_nnf,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(nnf_transformation,[status(thm)],[f229]) ).
cnf(c229,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(cnf_transformation,[status(esa)],[f229_nnf]) ).
cnf(p717,plain,
rselect_head(queue_125) = rselect_head(q27),
inference(superposition,[status(thm)],[c229,c8]) ).
cnf(p2416,plain,
rselect_head(queue_125) = rselect_head(q26),
inference(demodulation,[status(thm)],[p2415,p717]) ).
cnf(p3760,plain,
index_297 = rselect_head(q26),
inference(demodulation,[status(thm)],[p3759,p2416]) ).
cnf(p3763,plain,
rselect_head(q26) = index_297,
inference(superposition,[status(thm)],[p3760,c7]) ).
cnf(f337,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp321) ).
fof(f337_nnf,plain,
q26 = queue_115,
inference(nnf_transformation,[status(thm)],[f337]) ).
cnf(c337,plain,
q26 = queue_115,
inference(cnf_transformation,[status(esa)],[f337_nnf]) ).
cnf(f226,hypothesis,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp210) ).
fof(f226_nnf,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(nnf_transformation,[status(thm)],[f226]) ).
cnf(c226,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(cnf_transformation,[status(esa)],[f226_nnf]) ).
cnf(p706,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c226,c7]) ).
cnf(p2382,plain,
rselect_head(q26) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c337,p706]) ).
cnf(p3765,plain,
index_297 = rselect_head(queue_113),
inference(demodulation,[status(thm)],[p3763,p2382]) ).
cnf(p3767,plain,
rselect_head(queue_113) = index_297,
inference(superposition,[status(thm)],[p3765,c7]) ).
cnf(f336,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp320) ).
fof(f336_nnf,plain,
q25 = queue_109,
inference(nnf_transformation,[status(thm)],[f336]) ).
cnf(c336,plain,
q25 = queue_109,
inference(cnf_transformation,[status(esa)],[f336_nnf]) ).
cnf(f223,hypothesis,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f223_nnf,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(nnf_transformation,[status(thm)],[f223]) ).
cnf(c223,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(cnf_transformation,[status(esa)],[f223_nnf]) ).
cnf(p696,plain,
rselect_head(queue_109) = rselect_head(queue_107),
inference(superposition,[status(thm)],[c223,c7]) ).
cnf(p2323,plain,
rselect_head(q25) = rselect_head(q24),
inference(superposition,[status(thm)],[c336,p696]) ).
cnf(f225,hypothesis,
queue_113 = rstore_seq(q25,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f225_nnf,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(nnf_transformation,[status(thm)],[f225]) ).
cnf(c225,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(cnf_transformation,[status(esa)],[f225_nnf]) ).
cnf(p701,plain,
rselect_head(queue_113) = rselect_head(q25),
inference(superposition,[status(thm)],[c225,c8]) ).
cnf(p2324,plain,
rselect_head(queue_113) = rselect_head(q24),
inference(demodulation,[status(thm)],[p2323,p701]) ).
cnf(p3768,plain,
index_297 = rselect_head(q24),
inference(demodulation,[status(thm)],[p3767,p2324]) ).
cnf(p3769,plain,
rselect_head(q24) = index_297,
inference(superposition,[status(thm)],[p3768,c7]) ).
cnf(f334,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp318) ).
fof(f334_nnf,plain,
q23 = queue_97,
inference(nnf_transformation,[status(thm)],[f334]) ).
cnf(c334,plain,
q23 = queue_97,
inference(cnf_transformation,[status(esa)],[f334_nnf]) ).
cnf(f317,hypothesis,
queue_97 = rstore_tail(queue_95,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp301) ).
fof(f317_nnf,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(nnf_transformation,[status(thm)],[f317]) ).
cnf(c317,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(cnf_transformation,[status(esa)],[f317_nnf]) ).
cnf(p1333,plain,
rselect_head(queue_97) = rselect_head(queue_95),
inference(superposition,[status(thm)],[c317,c7]) ).
cnf(p3625,plain,
rselect_head(q23) = rselect_head(q22),
inference(superposition,[status(thm)],[c334,p1333]) ).
cnf(f335,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp319) ).
fof(f335_nnf,plain,
q24 = queue_103,
inference(nnf_transformation,[status(thm)],[f335]) ).
cnf(c335,plain,
q24 = queue_103,
inference(cnf_transformation,[status(esa)],[f335_nnf]) ).
cnf(f221,hypothesis,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f221_nnf,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(nnf_transformation,[status(thm)],[f221]) ).
cnf(c221,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(cnf_transformation,[status(esa)],[f221_nnf]) ).
cnf(p689,plain,
rselect_head(queue_103) = rselect_head(queue_101),
inference(superposition,[status(thm)],[c221,c7]) ).
cnf(p2255,plain,
rselect_head(q24) = rselect_head(q23),
inference(superposition,[status(thm)],[c335,p689]) ).
cnf(p3627,plain,
rselect_head(q24) = rselect_head(q22),
inference(demodulation,[status(thm)],[p3625,p2255]) ).
cnf(p3772,plain,
index_297 = rselect_head(q22),
inference(demodulation,[status(thm)],[p3769,p3627]) ).
cnf(p3778,plain,
rselect_head(q22) = index_297,
inference(superposition,[status(thm)],[p3772,c7]) ).
cnf(f333,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp317) ).
fof(f333_nnf,plain,
q22 = queue_91,
inference(nnf_transformation,[status(thm)],[f333]) ).
cnf(c333,plain,
q22 = queue_91,
inference(cnf_transformation,[status(esa)],[f333_nnf]) ).
cnf(f315,hypothesis,
queue_91 = rstore_tail(queue_89,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp299) ).
fof(f315_nnf,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(nnf_transformation,[status(thm)],[f315]) ).
cnf(c315,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(cnf_transformation,[status(esa)],[f315_nnf]) ).
cnf(p1325,plain,
rselect_head(queue_91) = rselect_head(queue_89),
inference(superposition,[status(thm)],[c315,c7]) ).
cnf(p3612,plain,
rselect_head(q22) = rselect_head(queue_89),
inference(superposition,[status(thm)],[c333,p1325]) ).
cnf(p3780,plain,
index_297 = rselect_head(queue_89),
inference(demodulation,[status(thm)],[p3778,p3612]) ).
cnf(p3783,plain,
rselect_head(queue_89) = index_297,
inference(superposition,[status(thm)],[p3780,c7]) ).
cnf(f332,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp316) ).
fof(f332_nnf,plain,
q21 = queue_85,
inference(nnf_transformation,[status(thm)],[f332]) ).
cnf(c332,plain,
q21 = queue_85,
inference(cnf_transformation,[status(esa)],[f332_nnf]) ).
cnf(f313,hypothesis,
queue_85 = rstore_tail(queue_83,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp297) ).
fof(f313_nnf,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(nnf_transformation,[status(thm)],[f313]) ).
cnf(c313,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(cnf_transformation,[status(esa)],[f313_nnf]) ).
cnf(p1309,plain,
rselect_head(queue_85) = rselect_head(queue_83),
inference(superposition,[status(thm)],[c313,c7]) ).
cnf(p3604,plain,
rselect_head(q21) = rselect_head(q20),
inference(superposition,[status(thm)],[c332,p1309]) ).
cnf(f314,hypothesis,
queue_89 = rstore_seq(q21,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp298) ).
fof(f314_nnf,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(nnf_transformation,[status(thm)],[f314]) ).
cnf(c314,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(cnf_transformation,[status(esa)],[f314_nnf]) ).
cnf(p1311,plain,
rselect_head(queue_89) = rselect_head(q21),
inference(superposition,[status(thm)],[c314,c8]) ).
cnf(p3605,plain,
rselect_head(queue_89) = rselect_head(q20),
inference(demodulation,[status(thm)],[p3604,p1311]) ).
cnf(p3784,plain,
index_297 = rselect_head(q20),
inference(demodulation,[status(thm)],[p3783,p3605]) ).
cnf(p3787,plain,
rselect_head(q20) = index_297,
inference(superposition,[status(thm)],[p3784,c7]) ).
cnf(f331,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp315) ).
fof(f331_nnf,plain,
q20 = queue_79,
inference(nnf_transformation,[status(thm)],[f331]) ).
cnf(c331,plain,
q20 = queue_79,
inference(cnf_transformation,[status(esa)],[f331_nnf]) ).
cnf(f311,hypothesis,
queue_79 = rstore_tail(queue_77,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp295) ).
fof(f311_nnf,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(nnf_transformation,[status(thm)],[f311]) ).
cnf(c311,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(cnf_transformation,[status(esa)],[f311_nnf]) ).
cnf(p1293,plain,
rselect_head(queue_79) = rselect_head(queue_77),
inference(superposition,[status(thm)],[c311,c7]) ).
cnf(p3594,plain,
rselect_head(q20) = rselect_head(queue_77),
inference(superposition,[status(thm)],[c331,p1293]) ).
cnf(p3789,plain,
index_297 = rselect_head(queue_77),
inference(demodulation,[status(thm)],[p3787,p3594]) ).
cnf(p3794,plain,
rselect_head(queue_77) = index_297,
inference(superposition,[status(thm)],[p3789,c7]) ).
cnf(f329,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp313) ).
fof(f329_nnf,plain,
q19 = queue_67,
inference(nnf_transformation,[status(thm)],[f329]) ).
cnf(c329,plain,
q19 = queue_67,
inference(cnf_transformation,[status(esa)],[f329_nnf]) ).
cnf(f306,hypothesis,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp290) ).
fof(f306_nnf,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(nnf_transformation,[status(thm)],[f306]) ).
cnf(c306,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(cnf_transformation,[status(esa)],[f306_nnf]) ).
cnf(p1257,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(superposition,[status(thm)],[c306,c7]) ).
cnf(p3562,plain,
rselect_head(q19) = rselect_head(q18),
inference(superposition,[status(thm)],[c329,p1257]) ).
cnf(f310,hypothesis,
queue_77 = rstore_seq(q19,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp294) ).
fof(f310_nnf,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(nnf_transformation,[status(thm)],[f310]) ).
cnf(c310,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(cnf_transformation,[status(esa)],[f310_nnf]) ).
cnf(p1288,plain,
rselect_head(queue_77) = rselect_head(q19),
inference(superposition,[status(thm)],[c310,c8]) ).
cnf(p3563,plain,
rselect_head(queue_77) = rselect_head(q18),
inference(demodulation,[status(thm)],[p3562,p1288]) ).
cnf(p3796,plain,
index_297 = rselect_head(q18),
inference(demodulation,[status(thm)],[p3794,p3563]) ).
cnf(p3799,plain,
rselect_head(q18) = index_297,
inference(superposition,[status(thm)],[p3796,c7]) ).
cnf(f328,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp312) ).
fof(f328_nnf,plain,
q18 = queue_61,
inference(nnf_transformation,[status(thm)],[f328]) ).
cnf(c328,plain,
q18 = queue_61,
inference(cnf_transformation,[status(esa)],[f328_nnf]) ).
cnf(f304,hypothesis,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp288) ).
fof(f304_nnf,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(nnf_transformation,[status(thm)],[f304]) ).
cnf(c304,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(cnf_transformation,[status(esa)],[f304_nnf]) ).
cnf(p1241,plain,
rselect_head(queue_61) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c304,c7]) ).
cnf(p3556,plain,
rselect_head(q18) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c328,p1241]) ).
cnf(p3801,plain,
index_297 = rselect_head(queue_59),
inference(demodulation,[status(thm)],[p3799,p3556]) ).
cnf(p3803,plain,
rselect_head(queue_59) = index_297,
inference(superposition,[status(thm)],[p3801,c7]) ).
cnf(f327,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp311) ).
fof(f327_nnf,plain,
q17 = queue_55,
inference(nnf_transformation,[status(thm)],[f327]) ).
cnf(c327,plain,
q17 = queue_55,
inference(cnf_transformation,[status(esa)],[f327_nnf]) ).
cnf(f302,hypothesis,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp286) ).
fof(f302_nnf,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(nnf_transformation,[status(thm)],[f302]) ).
cnf(c302,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(cnf_transformation,[status(esa)],[f302_nnf]) ).
cnf(p1225,plain,
rselect_head(queue_55) = rselect_head(queue_53),
inference(superposition,[status(thm)],[c302,c7]) ).
cnf(p3549,plain,
rselect_head(q17) = rselect_head(q16),
inference(superposition,[status(thm)],[c327,p1225]) ).
cnf(f303,hypothesis,
queue_59 = rstore_seq(q17,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp287) ).
fof(f303_nnf,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(nnf_transformation,[status(thm)],[f303]) ).
cnf(c303,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(cnf_transformation,[status(esa)],[f303_nnf]) ).
cnf(p1236,plain,
rselect_head(queue_59) = rselect_head(q17),
inference(superposition,[status(thm)],[c303,c8]) ).
cnf(p3550,plain,
rselect_head(queue_59) = rselect_head(q16),
inference(demodulation,[status(thm)],[p3549,p1236]) ).
cnf(p3805,plain,
index_297 = rselect_head(q16),
inference(demodulation,[status(thm)],[p3803,p3550]) ).
cnf(p3806,plain,
rselect_head(q16) = index_297,
inference(superposition,[status(thm)],[p3805,c7]) ).
cnf(f326,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp310) ).
fof(f326_nnf,plain,
q16 = queue_49,
inference(nnf_transformation,[status(thm)],[f326]) ).
cnf(c326,plain,
q16 = queue_49,
inference(cnf_transformation,[status(esa)],[f326_nnf]) ).
cnf(f299,hypothesis,
queue_49 = rstore_tail(queue_47,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp283) ).
fof(f299_nnf,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(nnf_transformation,[status(thm)],[f299]) ).
cnf(c299,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(cnf_transformation,[status(esa)],[f299_nnf]) ).
cnf(p1206,plain,
rselect_head(queue_49) = rselect_head(queue_47),
inference(superposition,[status(thm)],[c299,c7]) ).
cnf(p3468,plain,
rselect_head(q16) = rselect_head(queue_47),
inference(superposition,[status(thm)],[c326,p1206]) ).
cnf(p3808,plain,
index_297 = rselect_head(queue_47),
inference(demodulation,[status(thm)],[p3806,p3468]) ).
cnf(p3810,plain,
rselect_head(queue_47) = index_297,
inference(superposition,[status(thm)],[p3808,c7]) ).
cnf(f325,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp309) ).
fof(f325_nnf,plain,
q15 = queue_43,
inference(nnf_transformation,[status(thm)],[f325]) ).
cnf(c325,plain,
q15 = queue_43,
inference(cnf_transformation,[status(esa)],[f325_nnf]) ).
cnf(f297,hypothesis,
queue_43 = rstore_tail(queue_41,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp281) ).
fof(f297_nnf,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(nnf_transformation,[status(thm)],[f297]) ).
cnf(c297,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(cnf_transformation,[status(esa)],[f297_nnf]) ).
cnf(p1190,plain,
rselect_head(queue_43) = rselect_head(queue_41),
inference(superposition,[status(thm)],[c297,c7]) ).
cnf(p3460,plain,
rselect_head(q15) = rselect_head(q14),
inference(superposition,[status(thm)],[c325,p1190]) ).
cnf(f298,hypothesis,
queue_47 = rstore_seq(q15,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp282) ).
fof(f298_nnf,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(nnf_transformation,[status(thm)],[f298]) ).
cnf(c298,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(cnf_transformation,[status(esa)],[f298_nnf]) ).
cnf(p1192,plain,
rselect_head(queue_47) = rselect_head(q15),
inference(superposition,[status(thm)],[c298,c8]) ).
cnf(p3461,plain,
rselect_head(queue_47) = rselect_head(q14),
inference(demodulation,[status(thm)],[p3460,p1192]) ).
cnf(p3811,plain,
index_297 = rselect_head(q14),
inference(demodulation,[status(thm)],[p3810,p3461]) ).
cnf(p3815,plain,
rselect_head(q14) = index_297,
inference(superposition,[status(thm)],[p3811,c7]) ).
cnf(f324,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp308) ).
fof(f324_nnf,plain,
q14 = queue_37,
inference(nnf_transformation,[status(thm)],[f324]) ).
cnf(c324,plain,
q14 = queue_37,
inference(cnf_transformation,[status(esa)],[f324_nnf]) ).
cnf(f295,hypothesis,
queue_37 = rstore_tail(queue_35,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp279) ).
fof(f295_nnf,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(nnf_transformation,[status(thm)],[f295]) ).
cnf(c295,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(cnf_transformation,[status(esa)],[f295_nnf]) ).
cnf(p1174,plain,
rselect_head(queue_37) = rselect_head(queue_35),
inference(superposition,[status(thm)],[c295,c7]) ).
cnf(p3452,plain,
rselect_head(q14) = rselect_head(queue_35),
inference(superposition,[status(thm)],[c324,p1174]) ).
cnf(p3817,plain,
index_297 = rselect_head(queue_35),
inference(demodulation,[status(thm)],[p3815,p3452]) ).
cnf(p3819,plain,
rselect_head(queue_35) = index_297,
inference(superposition,[status(thm)],[p3817,c7]) ).
cnf(f323,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp307) ).
fof(f323_nnf,plain,
q13 = queue_31,
inference(nnf_transformation,[status(thm)],[f323]) ).
cnf(c323,plain,
q13 = queue_31,
inference(cnf_transformation,[status(esa)],[f323_nnf]) ).
cnf(f293,hypothesis,
queue_31 = rstore_tail(queue_29,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp277) ).
fof(f293_nnf,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(nnf_transformation,[status(thm)],[f293]) ).
cnf(c293,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(cnf_transformation,[status(esa)],[f293_nnf]) ).
cnf(p1158,plain,
rselect_head(queue_31) = rselect_head(queue_29),
inference(superposition,[status(thm)],[c293,c7]) ).
cnf(p3388,plain,
rselect_head(q13) = rselect_head(q12),
inference(superposition,[status(thm)],[c323,p1158]) ).
cnf(f294,hypothesis,
queue_35 = rstore_seq(q13,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp278) ).
fof(f294_nnf,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(nnf_transformation,[status(thm)],[f294]) ).
cnf(c294,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(cnf_transformation,[status(esa)],[f294_nnf]) ).
cnf(p1161,plain,
rselect_head(queue_35) = rselect_head(q13),
inference(superposition,[status(thm)],[c294,c8]) ).
cnf(p3389,plain,
rselect_head(queue_35) = rselect_head(q12),
inference(demodulation,[status(thm)],[p3388,p1161]) ).
cnf(p3821,plain,
index_297 = rselect_head(q12),
inference(demodulation,[status(thm)],[p3819,p3389]) ).
cnf(p3824,plain,
rselect_head(q12) = index_297,
inference(superposition,[status(thm)],[p3821,c7]) ).
cnf(f322,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp306) ).
fof(f322_nnf,plain,
q12 = queue_25,
inference(nnf_transformation,[status(thm)],[f322]) ).
cnf(c322,plain,
q12 = queue_25,
inference(cnf_transformation,[status(esa)],[f322_nnf]) ).
cnf(f275,hypothesis,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp259) ).
fof(f275_nnf,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(nnf_transformation,[status(thm)],[f275]) ).
cnf(c275,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(cnf_transformation,[status(esa)],[f275_nnf]) ).
cnf(p1024,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c275,c7]) ).
cnf(p3083,plain,
rselect_head(q12) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c322,p1024]) ).
cnf(p3826,plain,
index_297 = rselect_head(queue_23),
inference(demodulation,[status(thm)],[p3824,p3083]) ).
cnf(p3829,plain,
rselect_head(queue_23) = index_297,
inference(superposition,[status(thm)],[p3826,c7]) ).
cnf(f321,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp305) ).
fof(f321_nnf,plain,
q11 = queue_19,
inference(nnf_transformation,[status(thm)],[f321]) ).
cnf(c321,plain,
q11 = queue_19,
inference(cnf_transformation,[status(esa)],[f321_nnf]) ).
cnf(f253,hypothesis,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f253_nnf,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(nnf_transformation,[status(thm)],[f253]) ).
cnf(c253,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(cnf_transformation,[status(esa)],[f253_nnf]) ).
cnf(p867,plain,
rselect_head(queue_19) = rselect_head(queue_17),
inference(superposition,[status(thm)],[c253,c7]) ).
cnf(p2751,plain,
rselect_head(q11) = rselect_head(q10),
inference(superposition,[status(thm)],[c321,p867]) ).
cnf(f268,hypothesis,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp252) ).
fof(f268_nnf,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(nnf_transformation,[status(thm)],[f268]) ).
cnf(c268,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(cnf_transformation,[status(esa)],[f268_nnf]) ).
cnf(p961,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(superposition,[status(thm)],[c268,c8]) ).
cnf(p2752,plain,
rselect_head(queue_23) = rselect_head(q10),
inference(demodulation,[status(thm)],[p2751,p961]) ).
cnf(p3830,plain,
index_297 = rselect_head(q10),
inference(demodulation,[status(thm)],[p3829,p2752]) ).
cnf(p3831,plain,
rselect_head(q10) = index_297,
inference(superposition,[status(thm)],[p3830,c7]) ).
cnf(f367,hypothesis,
q9 = queue_295,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp351) ).
fof(f367_nnf,plain,
q9 = queue_295,
inference(nnf_transformation,[status(thm)],[f367]) ).
cnf(c367,plain,
q9 = queue_295,
inference(cnf_transformation,[status(esa)],[f367_nnf]) ).
cnf(f292,hypothesis,
queue_295 = rstore_tail(queue_293,index_294),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp276) ).
fof(f292_nnf,plain,
queue_295 = rstore_tail(queue_293,index_294),
inference(nnf_transformation,[status(thm)],[f292]) ).
cnf(c292,plain,
queue_295 = rstore_tail(queue_293,index_294),
inference(cnf_transformation,[status(esa)],[f292_nnf]) ).
cnf(p1153,plain,
rselect_head(queue_295) = rselect_head(queue_293),
inference(superposition,[status(thm)],[c292,c7]) ).
cnf(p3282,plain,
rselect_head(q9) = rselect_head(q8),
inference(superposition,[status(thm)],[c367,p1153]) ).
cnf(f320,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp304) ).
fof(f320_nnf,plain,
q10 = queue_13,
inference(nnf_transformation,[status(thm)],[f320]) ).
cnf(c320,plain,
q10 = queue_13,
inference(cnf_transformation,[status(esa)],[f320_nnf]) ).
cnf(f231,hypothesis,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f231_nnf,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(nnf_transformation,[status(thm)],[f231]) ).
cnf(c231,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(cnf_transformation,[status(esa)],[f231_nnf]) ).
cnf(p730,plain,
rselect_head(queue_13) = rselect_head(queue_11),
inference(superposition,[status(thm)],[c231,c7]) ).
cnf(p2490,plain,
rselect_head(q10) = rselect_head(q9),
inference(superposition,[status(thm)],[c320,p730]) ).
cnf(p3284,plain,
rselect_head(q10) = rselect_head(q8),
inference(demodulation,[status(thm)],[p3282,p2490]) ).
cnf(p3834,plain,
index_297 = rselect_head(q8),
inference(demodulation,[status(thm)],[p3831,p3284]) ).
cnf(p3835,plain,
rselect_head(q8) = index_297,
inference(superposition,[status(thm)],[p3834,c7]) ).
cnf(f366,hypothesis,
q8 = queue_289,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp350) ).
fof(f366_nnf,plain,
q8 = queue_289,
inference(nnf_transformation,[status(thm)],[f366]) ).
cnf(c366,plain,
q8 = queue_289,
inference(cnf_transformation,[status(esa)],[f366_nnf]) ).
cnf(f289,hypothesis,
queue_289 = rstore_tail(queue_287,index_288),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp273) ).
fof(f289_nnf,plain,
queue_289 = rstore_tail(queue_287,index_288),
inference(nnf_transformation,[status(thm)],[f289]) ).
cnf(c289,plain,
queue_289 = rstore_tail(queue_287,index_288),
inference(cnf_transformation,[status(esa)],[f289_nnf]) ).
cnf(p1134,plain,
rselect_head(queue_289) = rselect_head(queue_287),
inference(superposition,[status(thm)],[c289,c7]) ).
cnf(p3255,plain,
rselect_head(q8) = rselect_head(queue_287),
inference(superposition,[status(thm)],[c366,p1134]) ).
cnf(p3837,plain,
index_297 = rselect_head(queue_287),
inference(demodulation,[status(thm)],[p3835,p3255]) ).
cnf(p3840,plain,
rselect_head(queue_287) = index_297,
inference(superposition,[status(thm)],[p3837,c7]) ).
cnf(f365,hypothesis,
q7 = queue_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp349) ).
fof(f365_nnf,plain,
q7 = queue_283,
inference(nnf_transformation,[status(thm)],[f365]) ).
cnf(c365,plain,
q7 = queue_283,
inference(cnf_transformation,[status(esa)],[f365_nnf]) ).
cnf(f287,hypothesis,
queue_283 = rstore_tail(queue_281,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp271) ).
fof(f287_nnf,plain,
queue_283 = rstore_tail(queue_281,index_282),
inference(nnf_transformation,[status(thm)],[f287]) ).
cnf(c287,plain,
queue_283 = rstore_tail(queue_281,index_282),
inference(cnf_transformation,[status(esa)],[f287_nnf]) ).
cnf(p1118,plain,
rselect_head(queue_283) = rselect_head(queue_281),
inference(superposition,[status(thm)],[c287,c7]) ).
cnf(p3245,plain,
rselect_head(q7) = rselect_head(q6),
inference(superposition,[status(thm)],[c365,p1118]) ).
cnf(f288,hypothesis,
queue_287 = rstore_seq(q7,earray_286),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp272) ).
fof(f288_nnf,plain,
queue_287 = rstore_seq(q7,earray_286),
inference(nnf_transformation,[status(thm)],[f288]) ).
cnf(c288,plain,
queue_287 = rstore_seq(q7,earray_286),
inference(cnf_transformation,[status(esa)],[f288_nnf]) ).
cnf(p1121,plain,
rselect_head(queue_287) = rselect_head(q7),
inference(superposition,[status(thm)],[c288,c8]) ).
cnf(p3246,plain,
rselect_head(queue_287) = rselect_head(q6),
inference(demodulation,[status(thm)],[p3245,p1121]) ).
cnf(p3842,plain,
index_297 = rselect_head(q6),
inference(demodulation,[status(thm)],[p3840,p3246]) ).
cnf(p3844,plain,
rselect_head(q6) = index_297,
inference(superposition,[status(thm)],[p3842,c7]) ).
cnf(f364,hypothesis,
q6 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp348) ).
fof(f364_nnf,plain,
q6 = queue_277,
inference(nnf_transformation,[status(thm)],[f364]) ).
cnf(c364,plain,
q6 = queue_277,
inference(cnf_transformation,[status(esa)],[f364_nnf]) ).
cnf(f285,hypothesis,
queue_277 = rstore_tail(queue_275,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp269) ).
fof(f285_nnf,plain,
queue_277 = rstore_tail(queue_275,index_276),
inference(nnf_transformation,[status(thm)],[f285]) ).
cnf(c285,plain,
queue_277 = rstore_tail(queue_275,index_276),
inference(cnf_transformation,[status(esa)],[f285_nnf]) ).
cnf(p1102,plain,
rselect_head(queue_277) = rselect_head(queue_275),
inference(superposition,[status(thm)],[c285,c7]) ).
cnf(p3138,plain,
rselect_head(q6) = rselect_head(queue_275),
inference(superposition,[status(thm)],[c364,p1102]) ).
cnf(p3846,plain,
index_297 = rselect_head(queue_275),
inference(demodulation,[status(thm)],[p3844,p3138]) ).
cnf(p3848,plain,
rselect_head(queue_275) = index_297,
inference(superposition,[status(thm)],[p3846,c7]) ).
cnf(f363,hypothesis,
q5 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp347) ).
fof(f363_nnf,plain,
q5 = queue_271,
inference(nnf_transformation,[status(thm)],[f363]) ).
cnf(c363,plain,
q5 = queue_271,
inference(cnf_transformation,[status(esa)],[f363_nnf]) ).
cnf(f283,hypothesis,
queue_271 = rstore_tail(queue_269,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp267) ).
fof(f283_nnf,plain,
queue_271 = rstore_tail(queue_269,index_270),
inference(nnf_transformation,[status(thm)],[f283]) ).
cnf(c283,plain,
queue_271 = rstore_tail(queue_269,index_270),
inference(cnf_transformation,[status(esa)],[f283_nnf]) ).
cnf(p1086,plain,
rselect_head(queue_271) = rselect_head(queue_269),
inference(superposition,[status(thm)],[c283,c7]) ).
cnf(p3128,plain,
rselect_head(q5) = rselect_head(q4),
inference(superposition,[status(thm)],[c363,p1086]) ).
cnf(f284,hypothesis,
queue_275 = rstore_seq(q5,earray_274),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp268) ).
fof(f284_nnf,plain,
queue_275 = rstore_seq(q5,earray_274),
inference(nnf_transformation,[status(thm)],[f284]) ).
cnf(c284,plain,
queue_275 = rstore_seq(q5,earray_274),
inference(cnf_transformation,[status(esa)],[f284_nnf]) ).
cnf(p1098,plain,
rselect_head(queue_275) = rselect_head(q5),
inference(superposition,[status(thm)],[c284,c8]) ).
cnf(p3129,plain,
rselect_head(queue_275) = rselect_head(q4),
inference(demodulation,[status(thm)],[p3128,p1098]) ).
cnf(p3850,plain,
index_297 = rselect_head(q4),
inference(demodulation,[status(thm)],[p3848,p3129]) ).
cnf(p3854,plain,
rselect_head(q4) = index_297,
inference(superposition,[status(thm)],[p3850,c7]) ).
cnf(f352,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp336) ).
fof(f352_nnf,plain,
q4 = queue_205,
inference(nnf_transformation,[status(thm)],[f352]) ).
cnf(c352,plain,
q4 = queue_205,
inference(cnf_transformation,[status(esa)],[f352_nnf]) ).
cnf(f259,hypothesis,
queue_205 = rstore_tail(queue_203,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp243) ).
fof(f259_nnf,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(nnf_transformation,[status(thm)],[f259]) ).
cnf(c259,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(cnf_transformation,[status(esa)],[f259_nnf]) ).
cnf(p900,plain,
rselect_head(queue_205) = rselect_head(queue_203),
inference(superposition,[status(thm)],[c259,c7]) ).
cnf(p2946,plain,
rselect_head(q4) = rselect_head(queue_203),
inference(superposition,[status(thm)],[c352,p900]) ).
cnf(p3856,plain,
index_297 = rselect_head(queue_203),
inference(demodulation,[status(thm)],[p3854,p2946]) ).
cnf(p3858,plain,
rselect_head(q2) = index_297,
inference(superposition,[status(thm)],[p3856,c7]) ).
cnf(f330,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp314) ).
fof(f330_nnf,plain,
q2 = queue_73,
inference(nnf_transformation,[status(thm)],[f330]) ).
cnf(c330,plain,
q2 = queue_73,
inference(cnf_transformation,[status(esa)],[f330_nnf]) ).
cnf(f309,hypothesis,
queue_73 = rstore_tail(queue_71,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp293) ).
fof(f309_nnf,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(nnf_transformation,[status(thm)],[f309]) ).
cnf(c309,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(cnf_transformation,[status(esa)],[f309_nnf]) ).
cnf(p1277,plain,
rselect_head(queue_73) = rselect_head(queue_71),
inference(superposition,[status(thm)],[c309,c7]) ).
cnf(p3584,plain,
rselect_head(q2) = rselect_head(queue_71),
inference(superposition,[status(thm)],[c330,p1277]) ).
cnf(p3862,plain,
index_297 = rselect_head(queue_71),
inference(demodulation,[status(thm)],[p3858,p3584]) ).
cnf(p3864,plain,
rselect_head(queue_71) = index_297,
inference(superposition,[status(thm)],[p3862,c7]) ).
cnf(f319,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp303) ).
fof(f319_nnf,plain,
q1 = queue_7,
inference(nnf_transformation,[status(thm)],[f319]) ).
cnf(c319,plain,
q1 = queue_7,
inference(cnf_transformation,[status(esa)],[f319_nnf]) ).
cnf(f307,hypothesis,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp291) ).
fof(f307_nnf,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(nnf_transformation,[status(thm)],[f307]) ).
cnf(c307,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(cnf_transformation,[status(esa)],[f307_nnf]) ).
cnf(p1261,plain,
rselect_head(queue_7) = rselect_head(queue_5),
inference(superposition,[status(thm)],[c307,c7]) ).
cnf(p3570,plain,
rselect_head(q1) = rselect_head(q0),
inference(superposition,[status(thm)],[c319,p1261]) ).
cnf(f308,hypothesis,
queue_71 = rstore_seq(q1,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp292) ).
fof(f308_nnf,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(nnf_transformation,[status(thm)],[f308]) ).
cnf(c308,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(cnf_transformation,[status(esa)],[f308_nnf]) ).
cnf(p1272,plain,
rselect_head(queue_71) = rselect_head(q1),
inference(superposition,[status(thm)],[c308,c8]) ).
cnf(p3571,plain,
rselect_head(queue_71) = rselect_head(q0),
inference(demodulation,[status(thm)],[p3570,p1272]) ).
cnf(p3866,plain,
index_297 = rselect_head(q0),
inference(demodulation,[status(thm)],[p3864,p3571]) ).
cnf(f4,axiom,
rselect_tail(rstore_tail(A,E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_tail) ).
fof(f4_nnf,plain,
! [A,E] : rselect_tail(rstore_tail(A,E)) = E,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,E] : rselect_tail(rstore_tail(A,E)) = E,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
rselect_tail(rstore_tail(X0,X1)) = X1,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p1323,plain,
rselect_tail(queue_91) = index_90,
inference(superposition,[status(thm)],[c315,c4]) ).
cnf(p2014,plain,
index_93 = index_90,
inference(superposition,[status(thm)],[c333,p1323]) ).
cnf(f215,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp199) ).
fof(f215_nnf,plain,
index_90 = s(index_87),
inference(nnf_transformation,[status(thm)],[f215]) ).
cnf(c215,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(esa)],[f215_nnf]) ).
cnf(f11,axiom,
p(s(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ps) ).
fof(f11_nnf,plain,
! [X] : p(s(X)) = X,
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] : p(s(X)) = X,
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
p(s(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p666,plain,
p(index_90) = index_87,
inference(superposition,[status(thm)],[c215,c11]) ).
cnf(p2016,plain,
p(index_93) = index_87,
inference(superposition,[status(thm)],[p2014,p666]) ).
cnf(f12,axiom,
s(p(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sp) ).
fof(f12_nnf,plain,
! [X] : s(p(X)) = X,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X] : s(p(X)) = X,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
s(p(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p2817,plain,
index_15 = index_111,
inference(superposition,[status(thm)],[p2016,c12]) ).
cnf(p1151,plain,
rselect_tail(queue_295) = index_294,
inference(superposition,[status(thm)],[c292,c4]) ).
cnf(p1719,plain,
index_9 = index_294,
inference(superposition,[status(thm)],[c367,p1151]) ).
cnf(f188,hypothesis,
index_294 = s(index_291),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp172) ).
fof(f188_nnf,plain,
index_294 = s(index_291),
inference(nnf_transformation,[status(thm)],[f188]) ).
cnf(c188,plain,
index_294 = s(index_291),
inference(cnf_transformation,[status(esa)],[f188_nnf]) ).
cnf(p606,plain,
p(index_294) = index_291,
inference(superposition,[status(thm)],[c188,c11]) ).
cnf(p1721,plain,
p(index_9) = index_291,
inference(superposition,[status(thm)],[p1719,p606]) ).
cnf(p728,plain,
rselect_tail(queue_13) = index_12,
inference(superposition,[status(thm)],[c231,c4]) ).
cnf(p1020,plain,
index_15 = index_12,
inference(superposition,[status(thm)],[c320,p728]) ).
cnf(p1029,plain,
index_12 = index_15,
inference(superposition,[status(thm)],[p1020,p728]) ).
cnf(f124,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp108) ).
fof(f124_nnf,plain,
index_12 = s(index_9),
inference(nnf_transformation,[status(thm)],[f124]) ).
cnf(c124,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(esa)],[f124_nnf]) ).
cnf(p462,plain,
p(index_12) = index_9,
inference(superposition,[status(thm)],[c124,c11]) ).
cnf(p731,plain,
s(index_9) = index_12,
inference(superposition,[status(thm)],[p462,c12]) ).
cnf(p1032,plain,
s(index_9) = index_15,
inference(demodulation,[status(thm)],[p1029,p731]) ).
cnf(f15,axiom,
s(s(s(X))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circular) ).
fof(f15_nnf,plain,
! [X] : s(s(s(X))) = X,
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X] : s(s(s(X))) = X,
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
s(s(s(X0))) = X0,
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p382,plain,
s(s(X0)) = p(X0),
inference(superposition,[status(thm)],[c12,c15]) ).
cnf(p1564,plain,
s(index_15) = p(index_9),
inference(superposition,[status(thm)],[p1032,p382]) ).
cnf(p1723,plain,
s(index_15) = index_291,
inference(demodulation,[status(thm)],[p1721,p1564]) ).
cnf(p2500,plain,
index_285 = index_15,
inference(superposition,[status(thm)],[p1723,c11]) ).
cnf(p898,plain,
rselect_tail(queue_205) = index_204,
inference(superposition,[status(thm)],[c259,c4]) ).
cnf(p1262,plain,
index_267 = index_204,
inference(superposition,[status(thm)],[c352,p898]) ).
cnf(f155,hypothesis,
index_204 = s(index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp139) ).
fof(f155_nnf,plain,
index_204 = s(index_201),
inference(nnf_transformation,[status(thm)],[f155]) ).
cnf(c155,plain,
index_204 = s(index_201),
inference(cnf_transformation,[status(esa)],[f155_nnf]) ).
cnf(p531,plain,
p(index_204) = index_201,
inference(superposition,[status(thm)],[c155,c11]) ).
cnf(p801,plain,
s(index_201) = index_204,
inference(superposition,[status(thm)],[p531,c12]) ).
cnf(p1267,plain,
index_204 = index_267,
inference(superposition,[status(thm)],[p1262,p801]) ).
cnf(p1268,plain,
s(index_201) = index_267,
inference(demodulation,[status(thm)],[p1267,p801]) ).
cnf(p1911,plain,
s(index_267) = index_135,
inference(superposition,[status(thm)],[p1268,p382]) ).
cnf(p1084,plain,
rselect_tail(queue_271) = index_270,
inference(superposition,[status(thm)],[c283,c4]) ).
cnf(p1631,plain,
index_273 = index_270,
inference(superposition,[status(thm)],[c363,p1084]) ).
cnf(f180,hypothesis,
index_270 = s(index_267),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp164) ).
fof(f180_nnf,plain,
index_270 = s(index_267),
inference(nnf_transformation,[status(thm)],[f180]) ).
cnf(c180,plain,
index_270 = s(index_267),
inference(cnf_transformation,[status(esa)],[f180_nnf]) ).
cnf(p588,plain,
p(index_270) = index_267,
inference(superposition,[status(thm)],[c180,c11]) ).
cnf(p860,plain,
s(index_267) = index_270,
inference(superposition,[status(thm)],[p588,c12]) ).
cnf(p1638,plain,
index_270 = index_273,
inference(superposition,[status(thm)],[p1631,p860]) ).
cnf(p1639,plain,
s(index_267) = index_273,
inference(demodulation,[status(thm)],[p1638,p860]) ).
cnf(p1912,plain,
index_135 = index_273,
inference(demodulation,[status(thm)],[p1911,p1639]) ).
cnf(f181,hypothesis,
index_273 = rselect_tail(q5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp165) ).
fof(f181_nnf,plain,
index_273 = rselect_tail(q5),
inference(nnf_transformation,[status(thm)],[f181]) ).
cnf(c181,plain,
index_273 = rselect_tail(q5),
inference(cnf_transformation,[status(esa)],[f181_nnf]) ).
cnf(f9,axiom,
rselect_tail(rstore_seq(A,E)) = rselect_tail(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_tail_seq) ).
fof(f9_nnf,plain,
! [A,E] : rselect_tail(rstore_seq(A,E)) = rselect_tail(A),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,E] : rselect_tail(rstore_seq(A,E)) = rselect_tail(A),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
rselect_tail(rstore_seq(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p590,plain,
rselect_tail(q5) = index_273,
inference(superposition,[status(thm)],[c181,c9]) ).
cnf(p1915,plain,
index_273 = index_135,
inference(superposition,[status(thm)],[p1912,p590]) ).
cnf(p1116,plain,
rselect_tail(queue_283) = index_282,
inference(superposition,[status(thm)],[c287,c4]) ).
cnf(p1665,plain,
index_285 = index_282,
inference(superposition,[status(thm)],[c365,p1116]) ).
cnf(f184,hypothesis,
index_282 = s(index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp168) ).
fof(f184_nnf,plain,
index_282 = s(index_279),
inference(nnf_transformation,[status(thm)],[f184]) ).
cnf(c184,plain,
index_282 = s(index_279),
inference(cnf_transformation,[status(esa)],[f184_nnf]) ).
cnf(p596,plain,
p(index_282) = index_279,
inference(superposition,[status(thm)],[c184,c11]) ).
cnf(p868,plain,
s(index_279) = index_282,
inference(superposition,[status(thm)],[p596,c12]) ).
cnf(p1672,plain,
index_282 = index_285,
inference(superposition,[status(thm)],[p1665,p868]) ).
cnf(p1100,plain,
rselect_tail(queue_277) = index_276,
inference(superposition,[status(thm)],[c285,c4]) ).
cnf(p1646,plain,
index_279 = index_276,
inference(superposition,[status(thm)],[c364,p1100]) ).
cnf(f182,hypothesis,
index_276 = s(index_273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp166) ).
fof(f182_nnf,plain,
index_276 = s(index_273),
inference(nnf_transformation,[status(thm)],[f182]) ).
cnf(c182,plain,
index_276 = s(index_273),
inference(cnf_transformation,[status(esa)],[f182_nnf]) ).
cnf(p591,plain,
p(index_276) = index_273,
inference(superposition,[status(thm)],[c182,c11]) ).
cnf(p1648,plain,
p(index_279) = index_273,
inference(superposition,[status(thm)],[p1646,p591]) ).
cnf(p1462,plain,
s(index_282) = p(index_279),
inference(superposition,[status(thm)],[p868,p382]) ).
cnf(p1650,plain,
s(index_282) = index_273,
inference(demodulation,[status(thm)],[p1648,p1462]) ).
cnf(p1678,plain,
s(index_285) = index_273,
inference(demodulation,[status(thm)],[p1672,p1650]) ).
cnf(p1936,plain,
s(index_285) = index_135,
inference(demodulation,[status(thm)],[p1915,p1678]) ).
cnf(p2515,plain,
s(index_15) = index_135,
inference(demodulation,[status(thm)],[p2500,p1936]) ).
cnf(p2847,plain,
s(index_111) = index_135,
inference(demodulation,[status(thm)],[p2817,p2515]) ).
cnf(p3165,plain,
index_201 = index_9,
inference(superposition,[status(thm)],[p2847,p382]) ).
cnf(p1259,plain,
rselect_tail(queue_7) = index_6,
inference(superposition,[status(thm)],[c307,c4]) ).
cnf(p1895,plain,
index_69 = index_6,
inference(superposition,[status(thm)],[c319,p1259]) ).
cnf(f203,hypothesis,
index_6 = s(index_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f203_nnf,plain,
index_6 = s(index_3),
inference(nnf_transformation,[status(thm)],[f203]) ).
cnf(c203,plain,
index_6 = s(index_3),
inference(cnf_transformation,[status(esa)],[f203_nnf]) ).
cnf(p638,plain,
p(index_6) = index_3,
inference(superposition,[status(thm)],[c203,c11]) ).
cnf(p1897,plain,
p(index_69) = index_3,
inference(superposition,[status(thm)],[p1895,p638]) ).
cnf(p2711,plain,
index_201 = index_3,
inference(superposition,[status(thm)],[p1897,p382]) ).
cnf(f191,hypothesis,
index_3 = rselect_tail(q0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp175) ).
fof(f191_nnf,plain,
index_3 = rselect_tail(q0),
inference(nnf_transformation,[status(thm)],[f191]) ).
cnf(c191,plain,
index_3 = rselect_tail(q0),
inference(cnf_transformation,[status(esa)],[f191_nnf]) ).
cnf(p612,plain,
rselect_tail(q0) = index_3,
inference(superposition,[status(thm)],[c191,c9]) ).
cnf(p2713,plain,
index_3 = index_201,
inference(superposition,[status(thm)],[p2711,p612]) ).
cnf(f318,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp302) ).
fof(f318_nnf,plain,
q0 = queue_1,
inference(nnf_transformation,[status(thm)],[f318]) ).
cnf(c318,plain,
q0 = queue_1,
inference(cnf_transformation,[status(esa)],[f318_nnf]) ).
cnf(f219,hypothesis,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f219_nnf,plain,
queue_1 = rstore_head(q,index_0),
inference(nnf_transformation,[status(thm)],[f219]) ).
cnf(c219,plain,
queue_1 = rstore_head(q,index_0),
inference(cnf_transformation,[status(esa)],[f219_nnf]) ).
cnf(p679,plain,
q0 = rstore_head(q,index_0),
inference(superposition,[status(thm)],[c318,c219]) ).
cnf(f10,axiom,
rselect_tail(rstore_head(A,E)) = rselect_tail(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_tail_head) ).
fof(f10_nnf,plain,
! [A,E] : rselect_tail(rstore_head(A,E)) = rselect_tail(A),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,E] : rselect_tail(rstore_head(A,E)) = rselect_tail(A),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
rselect_tail(rstore_head(X0,X1)) = rselect_tail(X0),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p2242,plain,
index_3 = index_0,
inference(superposition,[status(thm)],[p679,c10]) ).
cnf(f117,hypothesis,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f117_nnf,plain,
index_0 = rselect_tail(q),
inference(nnf_transformation,[status(thm)],[f117]) ).
cnf(c117,plain,
index_0 = rselect_tail(q),
inference(cnf_transformation,[status(esa)],[f117_nnf]) ).
cnf(p446,plain,
rselect_tail(q) = index_0,
inference(superposition,[status(thm)],[c117,c9]) ).
cnf(p2251,plain,
index_0 = index_3,
inference(superposition,[status(thm)],[p2242,p446]) ).
cnf(f3,axiom,
rselect_head(rstore_head(A,E)) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a1_head) ).
fof(f3_nnf,plain,
! [A,E] : rselect_head(rstore_head(A,E)) = E,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,E] : rselect_head(rstore_head(A,E)) = E,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
rselect_head(rstore_head(X0,X1)) = X1,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p680,plain,
rselect_head(queue_1) = index_0,
inference(superposition,[status(thm)],[c219,c3]) ).
cnf(p946,plain,
rselect_head(q0) = index_0,
inference(superposition,[status(thm)],[c318,p680]) ).
cnf(p2254,plain,
rselect_head(q0) = index_3,
inference(demodulation,[status(thm)],[p2251,p946]) ).
cnf(p2728,plain,
rselect_head(q0) = index_201,
inference(demodulation,[status(thm)],[p2713,p2254]) ).
cnf(p3206,plain,
rselect_head(q0) = index_9,
inference(demodulation,[status(thm)],[p3165,p2728]) ).
cnf(p3868,plain,
index_297 = index_9,
inference(superposition,[status(thm)],[p3866,p3206]) ).
cnf(f6,axiom,
rselect_seq(rstore_tail(A,E)) = rselect_seq(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a2_seq_tail) ).
fof(f6_nnf,plain,
! [A,E] : rselect_seq(rstore_tail(A,E)) = rselect_seq(A),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,E] : rselect_seq(rstore_tail(A,E)) = rselect_seq(A),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
rselect_seq(rstore_tail(X0,X1)) = rselect_seq(X0),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p1070,plain,
rselect_seq(queue_265) = rselect_seq(queue_263),
inference(superposition,[status(thm)],[c281,c6]) ).
cnf(p3113,plain,
earray_296 = earray_262,
inference(superposition,[status(thm)],[c362,p1070]) ).
cnf(f115,hypothesis,
elem_298 = select(earray_296,index_297),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp99) ).
fof(f115_nnf,plain,
elem_298 = select(earray_296,index_297),
inference(nnf_transformation,[status(thm)],[f115]) ).
cnf(c115,plain,
elem_298 = select(earray_296,index_297),
inference(cnf_transformation,[status(esa)],[f115_nnf]) ).
cnf(p3114,plain,
elem_298 = select(earray_262,index_297),
inference(demodulation,[status(thm)],[p3113,c115]) ).
cnf(p3870,plain,
elem_298 = select(earray_262,index_9),
inference(demodulation,[status(thm)],[p3868,p3114]) ).
cnf(p2887,plain,
index_105 = index_9,
inference(superposition,[status(thm)],[p2016,p382]) ).
cnf(p694,plain,
rselect_tail(queue_109) = index_108,
inference(superposition,[status(thm)],[c223,c4]) ).
cnf(p963,plain,
index_111 = index_108,
inference(superposition,[status(thm)],[c336,p694]) ).
cnf(p971,plain,
index_108 = index_111,
inference(superposition,[status(thm)],[p963,p694]) ).
cnf(f120,hypothesis,
index_108 = s(index_105),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f120_nnf,plain,
index_108 = s(index_105),
inference(nnf_transformation,[status(thm)],[f120]) ).
cnf(c120,plain,
index_108 = s(index_105),
inference(cnf_transformation,[status(esa)],[f120_nnf]) ).
cnf(p452,plain,
p(index_108) = index_105,
inference(superposition,[status(thm)],[c120,c11]) ).
cnf(p719,plain,
s(index_105) = index_108,
inference(superposition,[status(thm)],[p452,c12]) ).
cnf(p974,plain,
s(index_105) = index_111,
inference(demodulation,[status(thm)],[p971,p719]) ).
cnf(p1480,plain,
s(index_111) = index_99,
inference(superposition,[status(thm)],[p974,p382]) ).
cnf(p704,plain,
rselect_tail(queue_115) = index_114,
inference(superposition,[status(thm)],[c226,c4]) ).
cnf(p979,plain,
index_117 = index_114,
inference(superposition,[status(thm)],[c337,p704]) ).
cnf(p984,plain,
index_114 = index_117,
inference(superposition,[status(thm)],[p979,p704]) ).
cnf(f122,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp106) ).
fof(f122_nnf,plain,
index_114 = s(index_111),
inference(nnf_transformation,[status(thm)],[f122]) ).
cnf(c122,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(esa)],[f122_nnf]) ).
cnf(p457,plain,
p(index_114) = index_111,
inference(superposition,[status(thm)],[c122,c11]) ).
cnf(p725,plain,
s(index_111) = index_114,
inference(superposition,[status(thm)],[p457,c12]) ).
cnf(p987,plain,
s(index_111) = index_117,
inference(demodulation,[status(thm)],[p984,p725]) ).
cnf(p1481,plain,
index_99 = index_117,
inference(demodulation,[status(thm)],[p1480,p987]) ).
cnf(f123,hypothesis,
index_117 = rselect_tail(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f123_nnf,plain,
index_117 = rselect_tail(q26),
inference(nnf_transformation,[status(thm)],[f123]) ).
cnf(c123,plain,
index_117 = rselect_tail(q26),
inference(cnf_transformation,[status(esa)],[f123_nnf]) ).
cnf(p459,plain,
rselect_tail(q26) = index_117,
inference(superposition,[status(thm)],[c123,c9]) ).
cnf(p1483,plain,
index_117 = index_99,
inference(superposition,[status(thm)],[p1481,p459]) ).
cnf(p710,plain,
rselect_tail(queue_121) = index_120,
inference(superposition,[status(thm)],[c228,c4]) ).
cnf(p995,plain,
index_123 = index_120,
inference(superposition,[status(thm)],[c338,p710]) ).
cnf(f125,hypothesis,
index_120 = s(index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f125_nnf,plain,
index_120 = s(index_117),
inference(nnf_transformation,[status(thm)],[f125]) ).
cnf(c125,plain,
index_120 = s(index_117),
inference(cnf_transformation,[status(esa)],[f125_nnf]) ).
cnf(p464,plain,
p(index_120) = index_117,
inference(superposition,[status(thm)],[c125,c11]) ).
cnf(p998,plain,
p(index_123) = index_117,
inference(superposition,[status(thm)],[p995,p464]) ).
cnf(p1494,plain,
p(index_123) = index_99,
inference(demodulation,[status(thm)],[p1483,p998]) ).
cnf(p2053,plain,
index_105 = index_123,
inference(superposition,[status(thm)],[p1494,c12]) ).
cnf(f126,hypothesis,
index_123 = rselect_tail(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp110) ).
fof(f126_nnf,plain,
index_123 = rselect_tail(q27),
inference(nnf_transformation,[status(thm)],[f126]) ).
cnf(c126,plain,
index_123 = rselect_tail(q27),
inference(cnf_transformation,[status(esa)],[f126_nnf]) ).
cnf(p468,plain,
rselect_tail(q27) = index_123,
inference(superposition,[status(thm)],[c126,c9]) ).
cnf(p2056,plain,
index_123 = index_105,
inference(superposition,[status(thm)],[p2053,p468]) ).
cnf(p740,plain,
rselect_tail(queue_133) = index_132,
inference(superposition,[status(thm)],[c233,c4]) ).
cnf(p1036,plain,
index_141 = index_132,
inference(superposition,[status(thm)],[c340,p740]) ).
cnf(p1041,plain,
index_132 = index_141,
inference(superposition,[status(thm)],[p1036,p740]) ).
cnf(f129,hypothesis,
index_132 = s(index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp113) ).
fof(f129_nnf,plain,
index_132 = s(index_129),
inference(nnf_transformation,[status(thm)],[f129]) ).
cnf(c129,plain,
index_132 = s(index_129),
inference(cnf_transformation,[status(esa)],[f129_nnf]) ).
cnf(p474,plain,
p(index_132) = index_129,
inference(superposition,[status(thm)],[c129,c11]) ).
cnf(p744,plain,
s(index_129) = index_132,
inference(superposition,[status(thm)],[p474,c12]) ).
cnf(p1044,plain,
s(index_129) = index_141,
inference(demodulation,[status(thm)],[p1041,p744]) ).
cnf(p1568,plain,
s(index_141) = index_123,
inference(superposition,[status(thm)],[p1044,p382]) ).
cnf(p764,plain,
rselect_tail(queue_145) = index_144,
inference(superposition,[status(thm)],[c237,c4]) ).
cnf(p1068,plain,
index_147 = index_144,
inference(superposition,[status(thm)],[c342,p764]) ).
cnf(f133,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp117) ).
fof(f133_nnf,plain,
index_144 = s(index_141),
inference(nnf_transformation,[status(thm)],[f133]) ).
cnf(c133,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(esa)],[f133_nnf]) ).
cnf(p482,plain,
p(index_144) = index_141,
inference(superposition,[status(thm)],[c133,c11]) ).
cnf(p751,plain,
s(index_141) = index_144,
inference(superposition,[status(thm)],[p482,c12]) ).
cnf(p1077,plain,
index_144 = index_147,
inference(superposition,[status(thm)],[p1068,p751]) ).
cnf(p1078,plain,
s(index_141) = index_147,
inference(demodulation,[status(thm)],[p1077,p751]) ).
cnf(p1569,plain,
index_123 = index_147,
inference(demodulation,[status(thm)],[p1568,p1078]) ).
cnf(f134,hypothesis,
index_147 = rselect_tail(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp118) ).
fof(f134_nnf,plain,
index_147 = rselect_tail(q30),
inference(nnf_transformation,[status(thm)],[f134]) ).
cnf(c134,plain,
index_147 = rselect_tail(q30),
inference(cnf_transformation,[status(esa)],[f134_nnf]) ).
cnf(p486,plain,
rselect_tail(q30) = index_147,
inference(superposition,[status(thm)],[c134,c9]) ).
cnf(p1571,plain,
index_147 = index_123,
inference(superposition,[status(thm)],[p1569,p486]) ).
cnf(p777,plain,
rselect_tail(queue_151) = index_150,
inference(superposition,[status(thm)],[c239,c4]) ).
cnf(p1088,plain,
index_153 = index_150,
inference(superposition,[status(thm)],[c343,p777]) ).
cnf(f136,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp120) ).
fof(f136_nnf,plain,
index_150 = s(index_147),
inference(nnf_transformation,[status(thm)],[f136]) ).
cnf(c136,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(esa)],[f136_nnf]) ).
cnf(p488,plain,
p(index_150) = index_147,
inference(superposition,[status(thm)],[c136,c11]) ).
cnf(p1090,plain,
p(index_153) = index_147,
inference(superposition,[status(thm)],[p1088,p488]) ).
cnf(p1583,plain,
p(index_153) = index_123,
inference(demodulation,[status(thm)],[p1571,p1090]) ).
cnf(p2088,plain,
p(index_153) = index_105,
inference(demodulation,[status(thm)],[p2056,p1583]) ).
cnf(p2929,plain,
p(index_153) = index_9,
inference(demodulation,[status(thm)],[p2887,p2088]) ).
cnf(p3303,plain,
index_165 = index_9,
inference(superposition,[status(thm)],[p2929,p382]) ).
cnf(p1061,plain,
rselect_tail(queue_259) = index_258,
inference(superposition,[status(thm)],[c279,c4]) ).
cnf(p1606,plain,
index_261 = index_258,
inference(superposition,[status(thm)],[c361,p1061]) ).
cnf(f175,hypothesis,
index_258 = s(index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp159) ).
fof(f175_nnf,plain,
index_258 = s(index_255),
inference(nnf_transformation,[status(thm)],[f175]) ).
cnf(c175,plain,
index_258 = s(index_255),
inference(cnf_transformation,[status(esa)],[f175_nnf]) ).
cnf(p577,plain,
p(index_258) = index_255,
inference(superposition,[status(thm)],[c175,c11]) ).
cnf(p849,plain,
s(index_255) = index_258,
inference(superposition,[status(thm)],[p577,c12]) ).
cnf(p1613,plain,
index_258 = index_261,
inference(superposition,[status(thm)],[p1606,p849]) ).
cnf(p1045,plain,
rselect_tail(queue_253) = index_252,
inference(superposition,[status(thm)],[c277,c4]) ).
cnf(p1588,plain,
index_255 = index_252,
inference(superposition,[status(thm)],[c360,p1045]) ).
cnf(f173,hypothesis,
index_252 = s(index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp157) ).
fof(f173_nnf,plain,
index_252 = s(index_249),
inference(nnf_transformation,[status(thm)],[f173]) ).
cnf(c173,plain,
index_252 = s(index_249),
inference(cnf_transformation,[status(esa)],[f173_nnf]) ).
cnf(p572,plain,
p(index_252) = index_249,
inference(superposition,[status(thm)],[c173,c11]) ).
cnf(p1590,plain,
p(index_255) = index_249,
inference(superposition,[status(thm)],[p1588,p572]) ).
cnf(p1458,plain,
s(index_258) = p(index_255),
inference(superposition,[status(thm)],[p849,p382]) ).
cnf(p1592,plain,
s(index_258) = index_249,
inference(demodulation,[status(thm)],[p1590,p1458]) ).
cnf(p1619,plain,
s(index_261) = index_249,
inference(demodulation,[status(thm)],[p1613,p1592]) ).
cnf(p2417,plain,
index_165 = index_261,
inference(superposition,[status(thm)],[p1619,c11]) ).
cnf(f176,hypothesis,
index_261 = rselect_tail(q48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f176_nnf,plain,
index_261 = rselect_tail(q48),
inference(nnf_transformation,[status(thm)],[f176]) ).
cnf(c176,plain,
index_261 = rselect_tail(q48),
inference(cnf_transformation,[status(esa)],[f176_nnf]) ).
cnf(p579,plain,
rselect_tail(q48) = index_261,
inference(superposition,[status(thm)],[c176,c9]) ).
cnf(p2439,plain,
index_261 = index_165,
inference(superposition,[status(thm)],[p2417,p579]) ).
cnf(f77,hypothesis,
earray_262 = store(earray_260,index_261,e48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp61) ).
fof(f77_nnf,plain,
earray_262 = store(earray_260,index_261,e48),
inference(nnf_transformation,[status(thm)],[f77]) ).
cnf(c77,plain,
earray_262 = store(earray_260,index_261,e48),
inference(cnf_transformation,[status(esa)],[f77_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(p569,plain,
select(earray_262,index_261) = e48,
inference(superposition,[status(thm)],[c77,c0]) ).
cnf(p2440,plain,
select(earray_262,index_165) = e48,
inference(demodulation,[status(thm)],[p2439,p569]) ).
cnf(p3354,plain,
select(earray_262,index_9) = e48,
inference(demodulation,[status(thm)],[p3303,p2440]) ).
cnf(p4155,plain,
elem_298 = e48,
inference(superposition,[status(thm)],[p3870,p3354]) ).
cnf(f177,hypothesis,
index_264 = s(index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp161) ).
fof(f177_nnf,plain,
index_264 = s(index_261),
inference(nnf_transformation,[status(thm)],[f177]) ).
cnf(c177,plain,
index_264 = s(index_261),
inference(cnf_transformation,[status(esa)],[f177_nnf]) ).
cnf(p582,plain,
p(index_264) = index_261,
inference(superposition,[status(thm)],[c177,c11]) ).
cnf(p854,plain,
s(index_261) = index_264,
inference(superposition,[status(thm)],[p582,c12]) ).
cnf(p2420,plain,
index_264 = index_153,
inference(superposition,[status(thm)],[p854,p1619]) ).
cnf(p1069,plain,
rselect_tail(queue_265) = index_264,
inference(superposition,[status(thm)],[c281,c4]) ).
cnf(p1621,plain,
index_299 = index_264,
inference(superposition,[status(thm)],[c362,p1069]) ).
cnf(f193,hypothesis,
s(index_300) = index_299,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp177) ).
fof(f193_nnf,plain,
s(index_300) = index_299,
inference(nnf_transformation,[status(thm)],[f193]) ).
cnf(c193,plain,
s(index_300) = index_299,
inference(cnf_transformation,[status(esa)],[f193_nnf]) ).
cnf(p1622,plain,
s(index_300) = index_264,
inference(demodulation,[status(thm)],[p1621,c193]) ).
cnf(p2428,plain,
s(index_300) = index_153,
inference(demodulation,[status(thm)],[p2420,p1622]) ).
cnf(p3087,plain,
index_165 = index_300,
inference(superposition,[status(thm)],[p2428,c11]) ).
cnf(f116,hypothesis,
elem_301 = select(earray_296,index_300),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f116_nnf,plain,
elem_301 = select(earray_296,index_300),
inference(nnf_transformation,[status(thm)],[f116]) ).
cnf(c116,plain,
elem_301 = select(earray_296,index_300),
inference(cnf_transformation,[status(esa)],[f116_nnf]) ).
cnf(p3089,plain,
elem_301 = select(earray_296,index_165),
inference(superposition,[status(thm)],[p3087,c116]) ).
cnf(p3119,plain,
elem_301 = select(earray_262,index_165),
inference(demodulation,[status(thm)],[p3113,p3089]) ).
cnf(p3384,plain,
elem_301 = select(earray_262,index_9),
inference(demodulation,[status(thm)],[p3303,p3119]) ).
cnf(p4087,plain,
elem_301 = e48,
inference(superposition,[status(thm)],[p3384,p3354]) ).
cnf(f368,negated_conjecture,
elem_298 != elem_301,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f368_nnf,plain,
elem_298 != elem_301,
inference(nnf_transformation,[status(thm)],[f368]) ).
fof(f368_sk,plain,
elem_298 != elem_301,
inference(skolemisation,[status(esa)],[f368_nnf]) ).
cnf(c368,plain,
elem_298 != elem_301,
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
cnf(p4088,plain,
elem_298 != e48,
inference(demodulation,[status(thm)],[p4087,c368]) ).
cnf(p4156,plain,
e48 != e48,
inference(demodulation,[status(thm)],[p4155,p4088]) ).
cnf(p4157,plain,
$false,
inference(equality_resolution,[status(thm)],[p4156]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV570-1.049 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 20:38:07 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 63.95/9.81 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 63.95/9.81 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------