%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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:42 PM UTC 2026
% Result : Unsatisfiable 31.15s 4.39s
% Output : Proof 31.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 143
% Syntax : Number of formulae : 790 ( 790 unt; 0 def)
% Number of atoms : 790 ( 789 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 : 232 ( 232 usr; 223 con; 0-3 aty)
% Number of variables : 65 ( 12 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f320,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp304) ).
fof(f320_nnf,plain,
q43 = queue_229,
inference(nnf_transformation,[status(thm)],[f320]) ).
cnf(c320,plain,
q43 = queue_229,
inference(cnf_transformation,[status(esa)],[f320_nnf]) ).
cnf(f243,hypothesis,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp227) ).
fof(f243_nnf,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(nnf_transformation,[status(thm)],[f243]) ).
cnf(c243,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(cnf_transformation,[status(esa)],[f243_nnf]) ).
cnf(f7,axiom,
rselect_head(rstore_tail(A,E)) = rselect_head(A),
file('/export/starexec/sandbox/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(p904,plain,
rselect_head(queue_229) = rselect_head(queue_227),
inference(superposition,[status(thm)],[c243,c7]) ).
cnf(p2685,plain,
index_261 = rselect_head(q42),
inference(superposition,[status(thm)],[c320,p904]) ).
cnf(p3002,plain,
rselect_head(q42) = index_261,
inference(superposition,[status(thm)],[p2685,c7]) ).
cnf(f319,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp303) ).
fof(f319_nnf,plain,
q42 = queue_223,
inference(nnf_transformation,[status(thm)],[f319]) ).
cnf(c319,plain,
q42 = queue_223,
inference(cnf_transformation,[status(esa)],[f319_nnf]) ).
cnf(f241,hypothesis,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp225) ).
fof(f241_nnf,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(nnf_transformation,[status(thm)],[f241]) ).
cnf(c241,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(cnf_transformation,[status(esa)],[f241_nnf]) ).
cnf(p888,plain,
rselect_head(queue_223) = rselect_head(queue_221),
inference(superposition,[status(thm)],[c241,c7]) ).
cnf(p2672,plain,
rselect_head(q42) = rselect_head(queue_221),
inference(superposition,[status(thm)],[c319,p888]) ).
cnf(p3004,plain,
index_261 = rselect_head(queue_221),
inference(demodulation,[status(thm)],[p3002,p2672]) ).
cnf(p3156,plain,
rselect_head(queue_221) = index_261,
inference(superposition,[status(thm)],[p3004,c7]) ).
cnf(f318,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp302) ).
fof(f318_nnf,plain,
q41 = queue_217,
inference(nnf_transformation,[status(thm)],[f318]) ).
cnf(c318,plain,
q41 = queue_217,
inference(cnf_transformation,[status(esa)],[f318_nnf]) ).
cnf(f239,hypothesis,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp223) ).
fof(f239_nnf,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(nnf_transformation,[status(thm)],[f239]) ).
cnf(c239,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(cnf_transformation,[status(esa)],[f239_nnf]) ).
cnf(p863,plain,
rselect_head(queue_217) = rselect_head(queue_215),
inference(superposition,[status(thm)],[c239,c7]) ).
cnf(p2665,plain,
rselect_head(q41) = rselect_head(q40),
inference(superposition,[status(thm)],[c318,p863]) ).
cnf(f240,hypothesis,
queue_221 = rstore_seq(q41,earray_220),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp224) ).
fof(f240_nnf,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(nnf_transformation,[status(thm)],[f240]) ).
cnf(c240,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(cnf_transformation,[status(esa)],[f240_nnf]) ).
cnf(f8,axiom,
rselect_head(rstore_seq(A,E)) = rselect_head(A),
file('/export/starexec/sandbox/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(p875,plain,
rselect_head(queue_221) = rselect_head(q41),
inference(superposition,[status(thm)],[c240,c8]) ).
cnf(p2666,plain,
rselect_head(queue_221) = rselect_head(q40),
inference(demodulation,[status(thm)],[p2665,p875]) ).
cnf(p3158,plain,
index_261 = rselect_head(q40),
inference(demodulation,[status(thm)],[p3156,p2666]) ).
cnf(p3165,plain,
rselect_head(q40) = index_261,
inference(superposition,[status(thm)],[p3158,c7]) ).
cnf(f317,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp301) ).
fof(f317_nnf,plain,
q40 = queue_211,
inference(nnf_transformation,[status(thm)],[f317]) ).
cnf(c317,plain,
q40 = queue_211,
inference(cnf_transformation,[status(esa)],[f317_nnf]) ).
cnf(f237,hypothesis,
queue_211 = rstore_tail(queue_209,index_210),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp221) ).
fof(f237_nnf,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(nnf_transformation,[status(thm)],[f237]) ).
cnf(c237,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(cnf_transformation,[status(esa)],[f237_nnf]) ).
cnf(p847,plain,
rselect_head(queue_211) = rselect_head(queue_209),
inference(superposition,[status(thm)],[c237,c7]) ).
cnf(p2656,plain,
rselect_head(q40) = rselect_head(queue_209),
inference(superposition,[status(thm)],[c317,p847]) ).
cnf(p3167,plain,
index_261 = rselect_head(queue_209),
inference(demodulation,[status(thm)],[p3165,p2656]) ).
cnf(p3169,plain,
rselect_head(queue_209) = index_261,
inference(superposition,[status(thm)],[p3167,c7]) ).
cnf(f315,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp299) ).
fof(f315_nnf,plain,
q39 = queue_199,
inference(nnf_transformation,[status(thm)],[f315]) ).
cnf(c315,plain,
q39 = queue_199,
inference(cnf_transformation,[status(esa)],[f315_nnf]) ).
cnf(f233,hypothesis,
queue_199 = rstore_tail(queue_197,index_198),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp217) ).
fof(f233_nnf,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(nnf_transformation,[status(thm)],[f233]) ).
cnf(c233,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(cnf_transformation,[status(esa)],[f233_nnf]) ).
cnf(p819,plain,
rselect_head(queue_199) = rselect_head(queue_197),
inference(superposition,[status(thm)],[c233,c7]) ).
cnf(p2568,plain,
rselect_head(q39) = rselect_head(q38),
inference(superposition,[status(thm)],[c315,p819]) ).
cnf(f236,hypothesis,
queue_209 = rstore_seq(q39,earray_208),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp220) ).
fof(f236_nnf,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(nnf_transformation,[status(thm)],[f236]) ).
cnf(c236,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(cnf_transformation,[status(esa)],[f236_nnf]) ).
cnf(p835,plain,
rselect_head(queue_209) = rselect_head(q39),
inference(superposition,[status(thm)],[c236,c8]) ).
cnf(p2569,plain,
rselect_head(queue_209) = rselect_head(q38),
inference(demodulation,[status(thm)],[p2568,p835]) ).
cnf(p3171,plain,
index_261 = rselect_head(q38),
inference(demodulation,[status(thm)],[p3169,p2569]) ).
cnf(p3172,plain,
rselect_head(q38) = index_261,
inference(superposition,[status(thm)],[p3171,c7]) ).
cnf(f314,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp298) ).
fof(f314_nnf,plain,
q38 = queue_193,
inference(nnf_transformation,[status(thm)],[f314]) ).
cnf(c314,plain,
q38 = queue_193,
inference(cnf_transformation,[status(esa)],[f314_nnf]) ).
cnf(f231,hypothesis,
queue_193 = rstore_tail(queue_191,index_192),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp215) ).
fof(f231_nnf,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(nnf_transformation,[status(thm)],[f231]) ).
cnf(c231,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(cnf_transformation,[status(esa)],[f231_nnf]) ).
cnf(p806,plain,
rselect_head(queue_193) = rselect_head(queue_191),
inference(superposition,[status(thm)],[c231,c7]) ).
cnf(p2541,plain,
rselect_head(q38) = rselect_head(queue_191),
inference(superposition,[status(thm)],[c314,p806]) ).
cnf(p3174,plain,
index_261 = rselect_head(queue_191),
inference(demodulation,[status(thm)],[p3172,p2541]) ).
cnf(p3176,plain,
rselect_head(queue_191) = index_261,
inference(superposition,[status(thm)],[p3174,c7]) ).
cnf(f313,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp297) ).
fof(f313_nnf,plain,
q37 = queue_187,
inference(nnf_transformation,[status(thm)],[f313]) ).
cnf(c313,plain,
q37 = queue_187,
inference(cnf_transformation,[status(esa)],[f313_nnf]) ).
cnf(f228,hypothesis,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp212) ).
fof(f228_nnf,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(nnf_transformation,[status(thm)],[f228]) ).
cnf(c228,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(cnf_transformation,[status(esa)],[f228_nnf]) ).
cnf(p787,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(superposition,[status(thm)],[c228,c7]) ).
cnf(p2517,plain,
rselect_head(q37) = rselect_head(q36),
inference(superposition,[status(thm)],[c313,p787]) ).
cnf(f230,hypothesis,
queue_191 = rstore_seq(q37,earray_190),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp214) ).
fof(f230_nnf,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(nnf_transformation,[status(thm)],[f230]) ).
cnf(c230,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(cnf_transformation,[status(esa)],[f230_nnf]) ).
cnf(p800,plain,
rselect_head(queue_191) = rselect_head(q37),
inference(superposition,[status(thm)],[c230,c8]) ).
cnf(p2518,plain,
rselect_head(queue_191) = rselect_head(q36),
inference(demodulation,[status(thm)],[p2517,p800]) ).
cnf(p3178,plain,
index_261 = rselect_head(q36),
inference(demodulation,[status(thm)],[p3176,p2518]) ).
cnf(p3181,plain,
rselect_head(q36) = index_261,
inference(superposition,[status(thm)],[p3178,c7]) ).
cnf(f312,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp296) ).
fof(f312_nnf,plain,
q36 = queue_181,
inference(nnf_transformation,[status(thm)],[f312]) ).
cnf(c312,plain,
q36 = queue_181,
inference(cnf_transformation,[status(esa)],[f312_nnf]) ).
cnf(f226,hypothesis,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp210) ).
fof(f226_nnf,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(nnf_transformation,[status(thm)],[f226]) ).
cnf(c226,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(cnf_transformation,[status(esa)],[f226_nnf]) ).
cnf(p775,plain,
rselect_head(queue_181) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c226,c7]) ).
cnf(p2511,plain,
rselect_head(q36) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c312,p775]) ).
cnf(p3183,plain,
index_261 = rselect_head(queue_179),
inference(demodulation,[status(thm)],[p3181,p2511]) ).
cnf(p3186,plain,
rselect_head(queue_179) = index_261,
inference(superposition,[status(thm)],[p3183,c7]) ).
cnf(f311,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp295) ).
fof(f311_nnf,plain,
q35 = queue_175,
inference(nnf_transformation,[status(thm)],[f311]) ).
cnf(c311,plain,
q35 = queue_175,
inference(cnf_transformation,[status(esa)],[f311_nnf]) ).
cnf(f224,hypothesis,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp208) ).
fof(f224_nnf,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(nnf_transformation,[status(thm)],[f224]) ).
cnf(c224,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(cnf_transformation,[status(esa)],[f224_nnf]) ).
cnf(p765,plain,
rselect_head(queue_175) = rselect_head(queue_173),
inference(superposition,[status(thm)],[c224,c7]) ).
cnf(p2504,plain,
rselect_head(q35) = rselect_head(q34),
inference(superposition,[status(thm)],[c311,p765]) ).
cnf(f225,hypothesis,
queue_179 = rstore_seq(q35,earray_178),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp209) ).
fof(f225_nnf,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(nnf_transformation,[status(thm)],[f225]) ).
cnf(c225,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(cnf_transformation,[status(esa)],[f225_nnf]) ).
cnf(p768,plain,
rselect_head(queue_179) = rselect_head(q35),
inference(superposition,[status(thm)],[c225,c8]) ).
cnf(p2505,plain,
rselect_head(queue_179) = rselect_head(q34),
inference(demodulation,[status(thm)],[p2504,p768]) ).
cnf(p3188,plain,
index_261 = rselect_head(q34),
inference(demodulation,[status(thm)],[p3186,p2505]) ).
cnf(p3192,plain,
rselect_head(q34) = index_261,
inference(superposition,[status(thm)],[p3188,c7]) ).
cnf(f310,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp294) ).
fof(f310_nnf,plain,
q34 = queue_169,
inference(nnf_transformation,[status(thm)],[f310]) ).
cnf(c310,plain,
q34 = queue_169,
inference(cnf_transformation,[status(esa)],[f310_nnf]) ).
cnf(f221,hypothesis,
queue_169 = rstore_tail(queue_167,index_168),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp205) ).
fof(f221_nnf,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(nnf_transformation,[status(thm)],[f221]) ).
cnf(c221,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(cnf_transformation,[status(esa)],[f221_nnf]) ).
cnf(p747,plain,
rselect_head(queue_169) = rselect_head(queue_167),
inference(superposition,[status(thm)],[c221,c7]) ).
cnf(p2420,plain,
rselect_head(q34) = rselect_head(queue_167),
inference(superposition,[status(thm)],[c310,p747]) ).
cnf(p3194,plain,
index_261 = rselect_head(queue_167),
inference(demodulation,[status(thm)],[p3192,p2420]) ).
cnf(p3199,plain,
rselect_head(queue_167) = index_261,
inference(superposition,[status(thm)],[p3194,c7]) ).
cnf(f309,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp293) ).
fof(f309_nnf,plain,
q33 = queue_163,
inference(nnf_transformation,[status(thm)],[f309]) ).
cnf(c309,plain,
q33 = queue_163,
inference(cnf_transformation,[status(esa)],[f309_nnf]) ).
cnf(f219,hypothesis,
queue_163 = rstore_tail(queue_161,index_162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp203) ).
fof(f219_nnf,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(nnf_transformation,[status(thm)],[f219]) ).
cnf(c219,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(cnf_transformation,[status(esa)],[f219_nnf]) ).
cnf(p734,plain,
rselect_head(queue_163) = rselect_head(queue_161),
inference(superposition,[status(thm)],[c219,c7]) ).
cnf(p2413,plain,
rselect_head(q33) = rselect_head(q32),
inference(superposition,[status(thm)],[c309,p734]) ).
cnf(f220,hypothesis,
queue_167 = rstore_seq(q33,earray_166),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp204) ).
fof(f220_nnf,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(nnf_transformation,[status(thm)],[f220]) ).
cnf(c220,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(cnf_transformation,[status(esa)],[f220_nnf]) ).
cnf(p740,plain,
rselect_head(queue_167) = rselect_head(q33),
inference(superposition,[status(thm)],[c220,c8]) ).
cnf(p2414,plain,
rselect_head(queue_167) = rselect_head(q32),
inference(demodulation,[status(thm)],[p2413,p740]) ).
cnf(p3201,plain,
index_261 = rselect_head(q32),
inference(demodulation,[status(thm)],[p3199,p2414]) ).
cnf(p3202,plain,
rselect_head(q32) = index_261,
inference(superposition,[status(thm)],[p3201,c7]) ).
cnf(f308,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp292) ).
fof(f308_nnf,plain,
q32 = queue_157,
inference(nnf_transformation,[status(thm)],[f308]) ).
cnf(c308,plain,
q32 = queue_157,
inference(cnf_transformation,[status(esa)],[f308_nnf]) ).
cnf(f217,hypothesis,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp201) ).
fof(f217_nnf,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(nnf_transformation,[status(thm)],[f217]) ).
cnf(c217,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(cnf_transformation,[status(esa)],[f217_nnf]) ).
cnf(p723,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c217,c7]) ).
cnf(p2285,plain,
rselect_head(q32) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c308,p723]) ).
cnf(p3204,plain,
index_261 = rselect_head(queue_155),
inference(demodulation,[status(thm)],[p3202,p2285]) ).
cnf(p3206,plain,
rselect_head(queue_155) = index_261,
inference(superposition,[status(thm)],[p3204,c7]) ).
cnf(f307,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp291) ).
fof(f307_nnf,plain,
q31 = queue_151,
inference(nnf_transformation,[status(thm)],[f307]) ).
cnf(c307,plain,
q31 = queue_151,
inference(cnf_transformation,[status(esa)],[f307_nnf]) ).
cnf(f215,hypothesis,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp199) ).
fof(f215_nnf,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(nnf_transformation,[status(thm)],[f215]) ).
cnf(c215,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(cnf_transformation,[status(esa)],[f215_nnf]) ).
cnf(p710,plain,
rselect_head(queue_151) = rselect_head(queue_149),
inference(superposition,[status(thm)],[c215,c7]) ).
cnf(p2278,plain,
rselect_head(q31) = rselect_head(q30),
inference(superposition,[status(thm)],[c307,p710]) ).
cnf(f216,hypothesis,
queue_155 = rstore_seq(q31,earray_154),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp200) ).
fof(f216_nnf,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(nnf_transformation,[status(thm)],[f216]) ).
cnf(c216,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(cnf_transformation,[status(esa)],[f216_nnf]) ).
cnf(p716,plain,
rselect_head(queue_155) = rselect_head(q31),
inference(superposition,[status(thm)],[c216,c8]) ).
cnf(p2279,plain,
rselect_head(queue_155) = rselect_head(q30),
inference(demodulation,[status(thm)],[p2278,p716]) ).
cnf(p3207,plain,
index_261 = rselect_head(q30),
inference(demodulation,[status(thm)],[p3206,p2279]) ).
cnf(p3211,plain,
rselect_head(q30) = index_261,
inference(superposition,[status(thm)],[p3207,c7]) ).
cnf(f306,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp290) ).
fof(f306_nnf,plain,
q30 = queue_145,
inference(nnf_transformation,[status(thm)],[f306]) ).
cnf(c306,plain,
q30 = queue_145,
inference(cnf_transformation,[status(esa)],[f306_nnf]) ).
cnf(f213,hypothesis,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp197) ).
fof(f213_nnf,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(nnf_transformation,[status(thm)],[f213]) ).
cnf(c213,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(cnf_transformation,[status(esa)],[f213_nnf]) ).
cnf(p699,plain,
rselect_head(queue_145) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c213,c7]) ).
cnf(p2272,plain,
rselect_head(q30) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c306,p699]) ).
cnf(p3213,plain,
index_261 = rselect_head(queue_143),
inference(demodulation,[status(thm)],[p3211,p2272]) ).
cnf(p3217,plain,
rselect_head(queue_143) = index_261,
inference(superposition,[status(thm)],[p3213,c7]) ).
cnf(f304,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp288) ).
fof(f304_nnf,plain,
q29 = queue_133,
inference(nnf_transformation,[status(thm)],[f304]) ).
cnf(c304,plain,
q29 = queue_133,
inference(cnf_transformation,[status(esa)],[f304_nnf]) ).
cnf(f209,hypothesis,
queue_133 = rstore_tail(queue_131,index_132),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp193) ).
fof(f209_nnf,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(nnf_transformation,[status(thm)],[f209]) ).
cnf(c209,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(cnf_transformation,[status(esa)],[f209_nnf]) ).
cnf(p673,plain,
rselect_head(queue_133) = rselect_head(queue_131),
inference(superposition,[status(thm)],[c209,c7]) ).
cnf(p2206,plain,
rselect_head(q29) = rselect_head(q28),
inference(superposition,[status(thm)],[c304,p673]) ).
cnf(f212,hypothesis,
queue_143 = rstore_seq(q29,earray_142),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp196) ).
fof(f212_nnf,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(nnf_transformation,[status(thm)],[f212]) ).
cnf(c212,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(cnf_transformation,[status(esa)],[f212_nnf]) ).
cnf(p690,plain,
rselect_head(queue_143) = rselect_head(q29),
inference(superposition,[status(thm)],[c212,c8]) ).
cnf(p2207,plain,
rselect_head(queue_143) = rselect_head(q28),
inference(demodulation,[status(thm)],[p2206,p690]) ).
cnf(p3219,plain,
index_261 = rselect_head(q28),
inference(demodulation,[status(thm)],[p3217,p2207]) ).
cnf(p3222,plain,
rselect_head(q28) = index_261,
inference(superposition,[status(thm)],[p3219,c7]) ).
cnf(f303,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp287) ).
fof(f303_nnf,plain,
q28 = queue_127,
inference(nnf_transformation,[status(thm)],[f303]) ).
cnf(c303,plain,
q28 = queue_127,
inference(cnf_transformation,[status(esa)],[f303_nnf]) ).
cnf(f206,hypothesis,
queue_127 = rstore_tail(queue_125,index_126),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp190) ).
fof(f206_nnf,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(nnf_transformation,[status(thm)],[f206]) ).
cnf(c206,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(cnf_transformation,[status(esa)],[f206_nnf]) ).
cnf(p654,plain,
rselect_head(queue_127) = rselect_head(queue_125),
inference(superposition,[status(thm)],[c206,c7]) ).
cnf(p2164,plain,
rselect_head(q28) = rselect_head(queue_125),
inference(superposition,[status(thm)],[c303,p654]) ).
cnf(p3224,plain,
index_261 = rselect_head(queue_125),
inference(demodulation,[status(thm)],[p3222,p2164]) ).
cnf(p3226,plain,
rselect_head(queue_125) = index_261,
inference(superposition,[status(thm)],[p3224,c7]) ).
cnf(f302,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp286) ).
fof(f302_nnf,plain,
q27 = queue_121,
inference(nnf_transformation,[status(thm)],[f302]) ).
cnf(c302,plain,
q27 = queue_121,
inference(cnf_transformation,[status(esa)],[f302_nnf]) ).
cnf(f204,hypothesis,
queue_121 = rstore_tail(queue_119,index_120),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp188) ).
fof(f204_nnf,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(nnf_transformation,[status(thm)],[f204]) ).
cnf(c204,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(cnf_transformation,[status(esa)],[f204_nnf]) ).
cnf(p641,plain,
rselect_head(queue_121) = rselect_head(queue_119),
inference(superposition,[status(thm)],[c204,c7]) ).
cnf(p2132,plain,
rselect_head(q27) = rselect_head(q26),
inference(superposition,[status(thm)],[c302,p641]) ).
cnf(f205,hypothesis,
queue_125 = rstore_seq(q27,earray_124),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp189) ).
fof(f205_nnf,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(nnf_transformation,[status(thm)],[f205]) ).
cnf(c205,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(cnf_transformation,[status(esa)],[f205_nnf]) ).
cnf(p647,plain,
rselect_head(queue_125) = rselect_head(q27),
inference(superposition,[status(thm)],[c205,c8]) ).
cnf(p2133,plain,
rselect_head(queue_125) = rselect_head(q26),
inference(demodulation,[status(thm)],[p2132,p647]) ).
cnf(p3227,plain,
index_261 = rselect_head(q26),
inference(demodulation,[status(thm)],[p3226,p2133]) ).
cnf(p3229,plain,
rselect_head(q26) = index_261,
inference(superposition,[status(thm)],[p3227,c7]) ).
cnf(f301,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp285) ).
fof(f301_nnf,plain,
q26 = queue_115,
inference(nnf_transformation,[status(thm)],[f301]) ).
cnf(c301,plain,
q26 = queue_115,
inference(cnf_transformation,[status(esa)],[f301_nnf]) ).
cnf(f202,hypothesis,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp186) ).
fof(f202_nnf,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(nnf_transformation,[status(thm)],[f202]) ).
cnf(c202,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(cnf_transformation,[status(esa)],[f202_nnf]) ).
cnf(p630,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c202,c7]) ).
cnf(p2104,plain,
rselect_head(q26) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c301,p630]) ).
cnf(p3231,plain,
index_261 = rselect_head(queue_113),
inference(demodulation,[status(thm)],[p3229,p2104]) ).
cnf(p3233,plain,
rselect_head(queue_113) = index_261,
inference(superposition,[status(thm)],[p3231,c7]) ).
cnf(f300,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp284) ).
fof(f300_nnf,plain,
q25 = queue_109,
inference(nnf_transformation,[status(thm)],[f300]) ).
cnf(c300,plain,
q25 = queue_109,
inference(cnf_transformation,[status(esa)],[f300_nnf]) ).
cnf(f199,hypothesis,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp183) ).
fof(f199_nnf,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(nnf_transformation,[status(thm)],[f199]) ).
cnf(c199,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(cnf_transformation,[status(esa)],[f199_nnf]) ).
cnf(p618,plain,
rselect_head(queue_109) = rselect_head(queue_107),
inference(superposition,[status(thm)],[c199,c7]) ).
cnf(p2046,plain,
rselect_head(q25) = rselect_head(q24),
inference(superposition,[status(thm)],[c300,p618]) ).
cnf(f201,hypothesis,
queue_113 = rstore_seq(q25,earray_112),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp185) ).
fof(f201_nnf,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(nnf_transformation,[status(thm)],[f201]) ).
cnf(c201,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(cnf_transformation,[status(esa)],[f201_nnf]) ).
cnf(p623,plain,
rselect_head(queue_113) = rselect_head(q25),
inference(superposition,[status(thm)],[c201,c8]) ).
cnf(p2047,plain,
rselect_head(queue_113) = rselect_head(q24),
inference(demodulation,[status(thm)],[p2046,p623]) ).
cnf(p3234,plain,
index_261 = rselect_head(q24),
inference(demodulation,[status(thm)],[p3233,p2047]) ).
cnf(p3235,plain,
rselect_head(q24) = index_261,
inference(superposition,[status(thm)],[p3234,c7]) ).
cnf(f298,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp282) ).
fof(f298_nnf,plain,
q23 = queue_97,
inference(nnf_transformation,[status(thm)],[f298]) ).
cnf(c298,plain,
q23 = queue_97,
inference(cnf_transformation,[status(esa)],[f298_nnf]) ).
cnf(f281,hypothesis,
queue_97 = rstore_tail(queue_95,index_96),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp265) ).
fof(f281_nnf,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(nnf_transformation,[status(thm)],[f281]) ).
cnf(c281,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(cnf_transformation,[status(esa)],[f281_nnf]) ).
cnf(p1182,plain,
rselect_head(queue_97) = rselect_head(queue_95),
inference(superposition,[status(thm)],[c281,c7]) ).
cnf(p3148,plain,
rselect_head(q23) = rselect_head(q22),
inference(superposition,[status(thm)],[c298,p1182]) ).
cnf(f299,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp283) ).
fof(f299_nnf,plain,
q24 = queue_103,
inference(nnf_transformation,[status(thm)],[f299]) ).
cnf(c299,plain,
q24 = queue_103,
inference(cnf_transformation,[status(esa)],[f299_nnf]) ).
cnf(f197,hypothesis,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp181) ).
fof(f197_nnf,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(nnf_transformation,[status(thm)],[f197]) ).
cnf(c197,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(cnf_transformation,[status(esa)],[f197_nnf]) ).
cnf(p611,plain,
rselect_head(queue_103) = rselect_head(queue_101),
inference(superposition,[status(thm)],[c197,c7]) ).
cnf(p1999,plain,
rselect_head(q24) = rselect_head(q23),
inference(superposition,[status(thm)],[c299,p611]) ).
cnf(p3150,plain,
rselect_head(q24) = rselect_head(q22),
inference(demodulation,[status(thm)],[p3148,p1999]) ).
cnf(p3238,plain,
index_261 = rselect_head(q22),
inference(demodulation,[status(thm)],[p3235,p3150]) ).
cnf(p3243,plain,
rselect_head(q22) = index_261,
inference(superposition,[status(thm)],[p3238,c7]) ).
cnf(f297,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp281) ).
fof(f297_nnf,plain,
q22 = queue_91,
inference(nnf_transformation,[status(thm)],[f297]) ).
cnf(c297,plain,
q22 = queue_91,
inference(cnf_transformation,[status(esa)],[f297_nnf]) ).
cnf(f279,hypothesis,
queue_91 = rstore_tail(queue_89,index_90),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp263) ).
fof(f279_nnf,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(nnf_transformation,[status(thm)],[f279]) ).
cnf(c279,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(cnf_transformation,[status(esa)],[f279_nnf]) ).
cnf(p1166,plain,
rselect_head(queue_91) = rselect_head(queue_89),
inference(superposition,[status(thm)],[c279,c7]) ).
cnf(p3135,plain,
rselect_head(q22) = rselect_head(queue_89),
inference(superposition,[status(thm)],[c297,p1166]) ).
cnf(p3245,plain,
index_261 = rselect_head(queue_89),
inference(demodulation,[status(thm)],[p3243,p3135]) ).
cnf(p3248,plain,
rselect_head(queue_89) = index_261,
inference(superposition,[status(thm)],[p3245,c7]) ).
cnf(f296,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp280) ).
fof(f296_nnf,plain,
q21 = queue_85,
inference(nnf_transformation,[status(thm)],[f296]) ).
cnf(c296,plain,
q21 = queue_85,
inference(cnf_transformation,[status(esa)],[f296_nnf]) ).
cnf(f277,hypothesis,
queue_85 = rstore_tail(queue_83,index_84),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp261) ).
fof(f277_nnf,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(nnf_transformation,[status(thm)],[f277]) ).
cnf(c277,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(cnf_transformation,[status(esa)],[f277_nnf]) ).
cnf(p1150,plain,
rselect_head(queue_85) = rselect_head(queue_83),
inference(superposition,[status(thm)],[c277,c7]) ).
cnf(p3109,plain,
rselect_head(q21) = rselect_head(q20),
inference(superposition,[status(thm)],[c296,p1150]) ).
cnf(f278,hypothesis,
queue_89 = rstore_seq(q21,earray_88),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp262) ).
fof(f278_nnf,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(nnf_transformation,[status(thm)],[f278]) ).
cnf(c278,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(cnf_transformation,[status(esa)],[f278_nnf]) ).
cnf(p1161,plain,
rselect_head(queue_89) = rselect_head(q21),
inference(superposition,[status(thm)],[c278,c8]) ).
cnf(p3110,plain,
rselect_head(queue_89) = rselect_head(q20),
inference(demodulation,[status(thm)],[p3109,p1161]) ).
cnf(p3250,plain,
index_261 = rselect_head(q20),
inference(demodulation,[status(thm)],[p3248,p3110]) ).
cnf(p3256,plain,
rselect_head(q20) = index_261,
inference(superposition,[status(thm)],[p3250,c7]) ).
cnf(f295,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp279) ).
fof(f295_nnf,plain,
q20 = queue_79,
inference(nnf_transformation,[status(thm)],[f295]) ).
cnf(c295,plain,
q20 = queue_79,
inference(cnf_transformation,[status(esa)],[f295_nnf]) ).
cnf(f275,hypothesis,
queue_79 = rstore_tail(queue_77,index_78),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp259) ).
fof(f275_nnf,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(nnf_transformation,[status(thm)],[f275]) ).
cnf(c275,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(cnf_transformation,[status(esa)],[f275_nnf]) ).
cnf(p1134,plain,
rselect_head(queue_79) = rselect_head(queue_77),
inference(superposition,[status(thm)],[c275,c7]) ).
cnf(p3101,plain,
rselect_head(q20) = rselect_head(queue_77),
inference(superposition,[status(thm)],[c295,p1134]) ).
cnf(p3258,plain,
index_261 = rselect_head(queue_77),
inference(demodulation,[status(thm)],[p3256,p3101]) ).
cnf(p3262,plain,
rselect_head(queue_77) = index_261,
inference(superposition,[status(thm)],[p3258,c7]) ).
cnf(f293,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp277) ).
fof(f293_nnf,plain,
q19 = queue_67,
inference(nnf_transformation,[status(thm)],[f293]) ).
cnf(c293,plain,
q19 = queue_67,
inference(cnf_transformation,[status(esa)],[f293_nnf]) ).
cnf(f270,hypothesis,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp254) ).
fof(f270_nnf,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(nnf_transformation,[status(thm)],[f270]) ).
cnf(c270,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(cnf_transformation,[status(esa)],[f270_nnf]) ).
cnf(p1098,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(superposition,[status(thm)],[c270,c7]) ).
cnf(p3023,plain,
rselect_head(q19) = rselect_head(q18),
inference(superposition,[status(thm)],[c293,p1098]) ).
cnf(f274,hypothesis,
queue_77 = rstore_seq(q19,earray_76),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp258) ).
fof(f274_nnf,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(nnf_transformation,[status(thm)],[f274]) ).
cnf(c274,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(cnf_transformation,[status(esa)],[f274_nnf]) ).
cnf(p1129,plain,
rselect_head(queue_77) = rselect_head(q19),
inference(superposition,[status(thm)],[c274,c8]) ).
cnf(p3024,plain,
rselect_head(queue_77) = rselect_head(q18),
inference(demodulation,[status(thm)],[p3023,p1129]) ).
cnf(p3264,plain,
index_261 = rselect_head(q18),
inference(demodulation,[status(thm)],[p3262,p3024]) ).
cnf(p3265,plain,
rselect_head(q18) = index_261,
inference(superposition,[status(thm)],[p3264,c7]) ).
cnf(f292,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp276) ).
fof(f292_nnf,plain,
q18 = queue_61,
inference(nnf_transformation,[status(thm)],[f292]) ).
cnf(c292,plain,
q18 = queue_61,
inference(cnf_transformation,[status(esa)],[f292_nnf]) ).
cnf(f268,hypothesis,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp252) ).
fof(f268_nnf,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(nnf_transformation,[status(thm)],[f268]) ).
cnf(c268,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(cnf_transformation,[status(esa)],[f268_nnf]) ).
cnf(p1082,plain,
rselect_head(queue_61) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c268,c7]) ).
cnf(p3017,plain,
rselect_head(q18) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c292,p1082]) ).
cnf(p3267,plain,
index_261 = rselect_head(queue_59),
inference(demodulation,[status(thm)],[p3265,p3017]) ).
cnf(p3272,plain,
rselect_head(queue_59) = index_261,
inference(superposition,[status(thm)],[p3267,c7]) ).
cnf(f291,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp275) ).
fof(f291_nnf,plain,
q17 = queue_55,
inference(nnf_transformation,[status(thm)],[f291]) ).
cnf(c291,plain,
q17 = queue_55,
inference(cnf_transformation,[status(esa)],[f291_nnf]) ).
cnf(f266,hypothesis,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp250) ).
fof(f266_nnf,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(nnf_transformation,[status(thm)],[f266]) ).
cnf(c266,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(cnf_transformation,[status(esa)],[f266_nnf]) ).
cnf(p1066,plain,
rselect_head(queue_55) = rselect_head(queue_53),
inference(superposition,[status(thm)],[c266,c7]) ).
cnf(p3010,plain,
rselect_head(q17) = rselect_head(q16),
inference(superposition,[status(thm)],[c291,p1066]) ).
cnf(f267,hypothesis,
queue_59 = rstore_seq(q17,earray_58),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp251) ).
fof(f267_nnf,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(nnf_transformation,[status(thm)],[f267]) ).
cnf(c267,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(cnf_transformation,[status(esa)],[f267_nnf]) ).
cnf(p1077,plain,
rselect_head(queue_59) = rselect_head(q17),
inference(superposition,[status(thm)],[c267,c8]) ).
cnf(p3011,plain,
rselect_head(queue_59) = rselect_head(q16),
inference(demodulation,[status(thm)],[p3010,p1077]) ).
cnf(p3274,plain,
index_261 = rselect_head(q16),
inference(demodulation,[status(thm)],[p3272,p3011]) ).
cnf(p3275,plain,
rselect_head(q16) = index_261,
inference(superposition,[status(thm)],[p3274,c7]) ).
cnf(f290,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp274) ).
fof(f290_nnf,plain,
q16 = queue_49,
inference(nnf_transformation,[status(thm)],[f290]) ).
cnf(c290,plain,
q16 = queue_49,
inference(cnf_transformation,[status(esa)],[f290_nnf]) ).
cnf(f263,hypothesis,
queue_49 = rstore_tail(queue_47,index_48),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp247) ).
fof(f263_nnf,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(nnf_transformation,[status(thm)],[f263]) ).
cnf(c263,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(cnf_transformation,[status(esa)],[f263_nnf]) ).
cnf(p1047,plain,
rselect_head(queue_49) = rselect_head(queue_47),
inference(superposition,[status(thm)],[c263,c7]) ).
cnf(p3000,plain,
rselect_head(q16) = rselect_head(queue_47),
inference(superposition,[status(thm)],[c290,p1047]) ).
cnf(p3277,plain,
index_261 = rselect_head(queue_47),
inference(demodulation,[status(thm)],[p3275,p3000]) ).
cnf(p3279,plain,
rselect_head(queue_47) = index_261,
inference(superposition,[status(thm)],[p3277,c7]) ).
cnf(f289,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp273) ).
fof(f289_nnf,plain,
q15 = queue_43,
inference(nnf_transformation,[status(thm)],[f289]) ).
cnf(c289,plain,
q15 = queue_43,
inference(cnf_transformation,[status(esa)],[f289_nnf]) ).
cnf(f261,hypothesis,
queue_43 = rstore_tail(queue_41,index_42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp245) ).
fof(f261_nnf,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(nnf_transformation,[status(thm)],[f261]) ).
cnf(c261,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(cnf_transformation,[status(esa)],[f261_nnf]) ).
cnf(p1031,plain,
rselect_head(queue_43) = rselect_head(queue_41),
inference(superposition,[status(thm)],[c261,c7]) ).
cnf(p2992,plain,
rselect_head(q15) = rselect_head(q14),
inference(superposition,[status(thm)],[c289,p1031]) ).
cnf(f262,hypothesis,
queue_47 = rstore_seq(q15,earray_46),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp246) ).
fof(f262_nnf,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(nnf_transformation,[status(thm)],[f262]) ).
cnf(c262,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(cnf_transformation,[status(esa)],[f262_nnf]) ).
cnf(p1042,plain,
rselect_head(queue_47) = rselect_head(q15),
inference(superposition,[status(thm)],[c262,c8]) ).
cnf(p2993,plain,
rselect_head(queue_47) = rselect_head(q14),
inference(demodulation,[status(thm)],[p2992,p1042]) ).
cnf(p3280,plain,
index_261 = rselect_head(q14),
inference(demodulation,[status(thm)],[p3279,p2993]) ).
cnf(p3281,plain,
rselect_head(q14) = index_261,
inference(superposition,[status(thm)],[p3280,c7]) ).
cnf(f288,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp272) ).
fof(f288_nnf,plain,
q14 = queue_37,
inference(nnf_transformation,[status(thm)],[f288]) ).
cnf(c288,plain,
q14 = queue_37,
inference(cnf_transformation,[status(esa)],[f288_nnf]) ).
cnf(f259,hypothesis,
queue_37 = rstore_tail(queue_35,index_36),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp243) ).
fof(f259_nnf,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(nnf_transformation,[status(thm)],[f259]) ).
cnf(c259,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(cnf_transformation,[status(esa)],[f259_nnf]) ).
cnf(p1024,plain,
rselect_head(queue_37) = rselect_head(queue_35),
inference(superposition,[status(thm)],[c259,c7]) ).
cnf(p2986,plain,
rselect_head(q14) = rselect_head(queue_35),
inference(superposition,[status(thm)],[c288,p1024]) ).
cnf(p3283,plain,
index_261 = rselect_head(queue_35),
inference(demodulation,[status(thm)],[p3281,p2986]) ).
cnf(p3285,plain,
rselect_head(queue_35) = index_261,
inference(superposition,[status(thm)],[p3283,c7]) ).
cnf(f287,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp271) ).
fof(f287_nnf,plain,
q13 = queue_31,
inference(nnf_transformation,[status(thm)],[f287]) ).
cnf(c287,plain,
q13 = queue_31,
inference(cnf_transformation,[status(esa)],[f287_nnf]) ).
cnf(f257,hypothesis,
queue_31 = rstore_tail(queue_29,index_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp241) ).
fof(f257_nnf,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(nnf_transformation,[status(thm)],[f257]) ).
cnf(c257,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(cnf_transformation,[status(esa)],[f257_nnf]) ).
cnf(p1008,plain,
rselect_head(queue_31) = rselect_head(queue_29),
inference(superposition,[status(thm)],[c257,c7]) ).
cnf(p2979,plain,
rselect_head(q13) = rselect_head(q12),
inference(superposition,[status(thm)],[c287,p1008]) ).
cnf(f258,hypothesis,
queue_35 = rstore_seq(q13,earray_34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp242) ).
fof(f258_nnf,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(nnf_transformation,[status(thm)],[f258]) ).
cnf(c258,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(cnf_transformation,[status(esa)],[f258_nnf]) ).
cnf(p1010,plain,
rselect_head(queue_35) = rselect_head(q13),
inference(superposition,[status(thm)],[c258,c8]) ).
cnf(p2980,plain,
rselect_head(queue_35) = rselect_head(q12),
inference(demodulation,[status(thm)],[p2979,p1010]) ).
cnf(p3287,plain,
index_261 = rselect_head(q12),
inference(demodulation,[status(thm)],[p3285,p2980]) ).
cnf(p3291,plain,
rselect_head(q12) = index_261,
inference(superposition,[status(thm)],[p3287,c7]) ).
cnf(f286,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp270) ).
fof(f286_nnf,plain,
q12 = queue_25,
inference(nnf_transformation,[status(thm)],[f286]) ).
cnf(c286,plain,
q12 = queue_25,
inference(cnf_transformation,[status(esa)],[f286_nnf]) ).
cnf(f251,hypothesis,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp235) ).
fof(f251_nnf,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(nnf_transformation,[status(thm)],[f251]) ).
cnf(c251,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(cnf_transformation,[status(esa)],[f251_nnf]) ).
cnf(p960,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c251,c7]) ).
cnf(p2839,plain,
rselect_head(q12) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c286,p960]) ).
cnf(p3293,plain,
index_261 = rselect_head(queue_23),
inference(demodulation,[status(thm)],[p3291,p2839]) ).
cnf(p3297,plain,
rselect_head(queue_23) = index_261,
inference(superposition,[status(thm)],[p3293,c7]) ).
cnf(f285,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp269) ).
fof(f285_nnf,plain,
q11 = queue_19,
inference(nnf_transformation,[status(thm)],[f285]) ).
cnf(c285,plain,
q11 = queue_19,
inference(cnf_transformation,[status(esa)],[f285_nnf]) ).
cnf(f229,hypothesis,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp213) ).
fof(f229_nnf,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(nnf_transformation,[status(thm)],[f229]) ).
cnf(c229,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(cnf_transformation,[status(esa)],[f229_nnf]) ).
cnf(p794,plain,
rselect_head(queue_19) = rselect_head(queue_17),
inference(superposition,[status(thm)],[c229,c7]) ).
cnf(p2524,plain,
rselect_head(q11) = rselect_head(q10),
inference(superposition,[status(thm)],[c285,p794]) ).
cnf(f244,hypothesis,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp228) ).
fof(f244_nnf,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(nnf_transformation,[status(thm)],[f244]) ).
cnf(c244,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(cnf_transformation,[status(esa)],[f244_nnf]) ).
cnf(p907,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(superposition,[status(thm)],[c244,c8]) ).
cnf(p2525,plain,
rselect_head(queue_23) = rselect_head(q10),
inference(demodulation,[status(thm)],[p2524,p907]) ).
cnf(p3298,plain,
index_261 = rselect_head(q10),
inference(demodulation,[status(thm)],[p3297,p2525]) ).
cnf(p3300,plain,
rselect_head(q10) = index_261,
inference(superposition,[status(thm)],[p3298,c7]) ).
cnf(f325,hypothesis,
q9 = queue_259,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp309) ).
fof(f325_nnf,plain,
q9 = queue_259,
inference(nnf_transformation,[status(thm)],[f325]) ).
cnf(c325,plain,
q9 = queue_259,
inference(cnf_transformation,[status(esa)],[f325_nnf]) ).
cnf(f255,hypothesis,
queue_259 = rstore_tail(queue_257,index_258),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp239) ).
fof(f255_nnf,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(nnf_transformation,[status(thm)],[f255]) ).
cnf(c255,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(cnf_transformation,[status(esa)],[f255_nnf]) ).
cnf(p991,plain,
rselect_head(queue_259) = rselect_head(queue_257),
inference(superposition,[status(thm)],[c255,c7]) ).
cnf(p2961,plain,
rselect_head(q9) = rselect_head(q8),
inference(superposition,[status(thm)],[c325,p991]) ).
cnf(f284,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp268) ).
fof(f284_nnf,plain,
q10 = queue_13,
inference(nnf_transformation,[status(thm)],[f284]) ).
cnf(c284,plain,
q10 = queue_13,
inference(cnf_transformation,[status(esa)],[f284_nnf]) ).
cnf(f207,hypothesis,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp191) ).
fof(f207_nnf,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(nnf_transformation,[status(thm)],[f207]) ).
cnf(c207,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(cnf_transformation,[status(esa)],[f207_nnf]) ).
cnf(p662,plain,
rselect_head(queue_13) = rselect_head(queue_11),
inference(superposition,[status(thm)],[c207,c7]) ).
cnf(p2170,plain,
rselect_head(q10) = rselect_head(q9),
inference(superposition,[status(thm)],[c284,p662]) ).
cnf(p2963,plain,
rselect_head(q10) = rselect_head(q8),
inference(demodulation,[status(thm)],[p2961,p2170]) ).
cnf(p3303,plain,
index_261 = rselect_head(q8),
inference(demodulation,[status(thm)],[p3300,p2963]) ).
cnf(p3304,plain,
rselect_head(q8) = index_261,
inference(superposition,[status(thm)],[p3303,c7]) ).
cnf(f324,hypothesis,
q8 = queue_253,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp308) ).
fof(f324_nnf,plain,
q8 = queue_253,
inference(nnf_transformation,[status(thm)],[f324]) ).
cnf(c324,plain,
q8 = queue_253,
inference(cnf_transformation,[status(esa)],[f324_nnf]) ).
cnf(f253,hypothesis,
queue_253 = rstore_tail(queue_251,index_252),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp237) ).
fof(f253_nnf,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(nnf_transformation,[status(thm)],[f253]) ).
cnf(c253,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(cnf_transformation,[status(esa)],[f253_nnf]) ).
cnf(p975,plain,
rselect_head(queue_253) = rselect_head(queue_251),
inference(superposition,[status(thm)],[c253,c7]) ).
cnf(p2959,plain,
rselect_head(q8) = rselect_head(queue_251),
inference(superposition,[status(thm)],[c324,p975]) ).
cnf(p3306,plain,
index_261 = rselect_head(queue_251),
inference(demodulation,[status(thm)],[p3304,p2959]) ).
cnf(p3309,plain,
rselect_head(queue_251) = index_261,
inference(superposition,[status(thm)],[p3306,c7]) ).
cnf(f323,hypothesis,
q7 = queue_247,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp307) ).
fof(f323_nnf,plain,
q7 = queue_247,
inference(nnf_transformation,[status(thm)],[f323]) ).
cnf(c323,plain,
q7 = queue_247,
inference(cnf_transformation,[status(esa)],[f323_nnf]) ).
cnf(f250,hypothesis,
queue_247 = rstore_tail(queue_245,index_246),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp234) ).
fof(f250_nnf,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(nnf_transformation,[status(thm)],[f250]) ).
cnf(c250,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(cnf_transformation,[status(esa)],[f250_nnf]) ).
cnf(p955,plain,
rselect_head(queue_247) = rselect_head(queue_245),
inference(superposition,[status(thm)],[c250,c7]) ).
cnf(p2819,plain,
rselect_head(q7) = rselect_head(q6),
inference(superposition,[status(thm)],[c323,p955]) ).
cnf(f252,hypothesis,
queue_251 = rstore_seq(q7,earray_250),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp236) ).
fof(f252_nnf,plain,
queue_251 = rstore_seq(q7,earray_250),
inference(nnf_transformation,[status(thm)],[f252]) ).
cnf(c252,plain,
queue_251 = rstore_seq(q7,earray_250),
inference(cnf_transformation,[status(esa)],[f252_nnf]) ).
cnf(p971,plain,
rselect_head(queue_251) = rselect_head(q7),
inference(superposition,[status(thm)],[c252,c8]) ).
cnf(p2820,plain,
rselect_head(queue_251) = rselect_head(q6),
inference(demodulation,[status(thm)],[p2819,p971]) ).
cnf(p3311,plain,
index_261 = rselect_head(q6),
inference(demodulation,[status(thm)],[p3309,p2820]) ).
cnf(p3313,plain,
rselect_head(q6) = index_261,
inference(superposition,[status(thm)],[p3311,c7]) ).
cnf(f322,hypothesis,
q6 = queue_241,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp306) ).
fof(f322_nnf,plain,
q6 = queue_241,
inference(nnf_transformation,[status(thm)],[f322]) ).
cnf(c322,plain,
q6 = queue_241,
inference(cnf_transformation,[status(esa)],[f322_nnf]) ).
cnf(f248,hypothesis,
queue_241 = rstore_tail(queue_239,index_240),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp232) ).
fof(f248_nnf,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(nnf_transformation,[status(thm)],[f248]) ).
cnf(c248,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(cnf_transformation,[status(esa)],[f248_nnf]) ).
cnf(p939,plain,
rselect_head(queue_241) = rselect_head(queue_239),
inference(superposition,[status(thm)],[c248,c7]) ).
cnf(p2798,plain,
rselect_head(q6) = rselect_head(queue_239),
inference(superposition,[status(thm)],[c322,p939]) ).
cnf(p3315,plain,
index_261 = rselect_head(queue_239),
inference(demodulation,[status(thm)],[p3313,p2798]) ).
cnf(p3317,plain,
rselect_head(queue_239) = index_261,
inference(superposition,[status(thm)],[p3315,c7]) ).
cnf(f321,hypothesis,
q5 = queue_235,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp305) ).
fof(f321_nnf,plain,
q5 = queue_235,
inference(nnf_transformation,[status(thm)],[f321]) ).
cnf(c321,plain,
q5 = queue_235,
inference(cnf_transformation,[status(esa)],[f321_nnf]) ).
cnf(f246,hypothesis,
queue_235 = rstore_tail(queue_233,index_234),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp230) ).
fof(f246_nnf,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(nnf_transformation,[status(thm)],[f246]) ).
cnf(c246,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(cnf_transformation,[status(esa)],[f246_nnf]) ).
cnf(p923,plain,
rselect_head(queue_235) = rselect_head(queue_233),
inference(superposition,[status(thm)],[c246,c7]) ).
cnf(p2788,plain,
rselect_head(q5) = rselect_head(q4),
inference(superposition,[status(thm)],[c321,p923]) ).
cnf(f247,hypothesis,
queue_239 = rstore_seq(q5,earray_238),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp231) ).
fof(f247_nnf,plain,
queue_239 = rstore_seq(q5,earray_238),
inference(nnf_transformation,[status(thm)],[f247]) ).
cnf(c247,plain,
queue_239 = rstore_seq(q5,earray_238),
inference(cnf_transformation,[status(esa)],[f247_nnf]) ).
cnf(p935,plain,
rselect_head(queue_239) = rselect_head(q5),
inference(superposition,[status(thm)],[c247,c8]) ).
cnf(p2789,plain,
rselect_head(queue_239) = rselect_head(q4),
inference(demodulation,[status(thm)],[p2788,p935]) ).
cnf(p3319,plain,
index_261 = rselect_head(q4),
inference(demodulation,[status(thm)],[p3317,p2789]) ).
cnf(p3323,plain,
rselect_head(q4) = index_261,
inference(superposition,[status(thm)],[p3319,c7]) ).
cnf(f316,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp300) ).
fof(f316_nnf,plain,
q4 = queue_205,
inference(nnf_transformation,[status(thm)],[f316]) ).
cnf(c316,plain,
q4 = queue_205,
inference(cnf_transformation,[status(esa)],[f316_nnf]) ).
cnf(f235,hypothesis,
queue_205 = rstore_tail(queue_203,index_204),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp219) ).
fof(f235_nnf,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(nnf_transformation,[status(thm)],[f235]) ).
cnf(c235,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(cnf_transformation,[status(esa)],[f235_nnf]) ).
cnf(p830,plain,
rselect_head(queue_205) = rselect_head(queue_203),
inference(superposition,[status(thm)],[c235,c7]) ).
cnf(p2591,plain,
rselect_head(q4) = rselect_head(queue_203),
inference(superposition,[status(thm)],[c316,p830]) ).
cnf(p3325,plain,
index_261 = rselect_head(queue_203),
inference(demodulation,[status(thm)],[p3323,p2591]) ).
cnf(p3327,plain,
rselect_head(queue_203) = index_261,
inference(superposition,[status(thm)],[p3325,c7]) ).
cnf(f305,hypothesis,
q3 = queue_139,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp289) ).
fof(f305_nnf,plain,
q3 = queue_139,
inference(nnf_transformation,[status(thm)],[f305]) ).
cnf(c305,plain,
q3 = queue_139,
inference(cnf_transformation,[status(esa)],[f305_nnf]) ).
cnf(f211,hypothesis,
queue_139 = rstore_tail(queue_137,index_138),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp195) ).
fof(f211_nnf,plain,
queue_139 = rstore_tail(queue_137,index_138),
inference(nnf_transformation,[status(thm)],[f211]) ).
cnf(c211,plain,
queue_139 = rstore_tail(queue_137,index_138),
inference(cnf_transformation,[status(esa)],[f211_nnf]) ).
cnf(p686,plain,
rselect_head(queue_139) = rselect_head(queue_137),
inference(superposition,[status(thm)],[c211,c7]) ).
cnf(p2218,plain,
rselect_head(q3) = rselect_head(q2),
inference(superposition,[status(thm)],[c305,p686]) ).
cnf(f234,hypothesis,
queue_203 = rstore_seq(q3,earray_202),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp218) ).
fof(f234_nnf,plain,
queue_203 = rstore_seq(q3,earray_202),
inference(nnf_transformation,[status(thm)],[f234]) ).
cnf(c234,plain,
queue_203 = rstore_seq(q3,earray_202),
inference(cnf_transformation,[status(esa)],[f234_nnf]) ).
cnf(p824,plain,
rselect_head(queue_203) = rselect_head(q3),
inference(superposition,[status(thm)],[c234,c8]) ).
cnf(p2219,plain,
rselect_head(queue_203) = rselect_head(q2),
inference(demodulation,[status(thm)],[p2218,p824]) ).
cnf(p3329,plain,
index_261 = rselect_head(q2),
inference(demodulation,[status(thm)],[p3327,p2219]) ).
cnf(p3331,plain,
rselect_head(q2) = index_261,
inference(superposition,[status(thm)],[p3329,c7]) ).
cnf(f294,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp278) ).
fof(f294_nnf,plain,
q2 = queue_73,
inference(nnf_transformation,[status(thm)],[f294]) ).
cnf(c294,plain,
q2 = queue_73,
inference(cnf_transformation,[status(esa)],[f294_nnf]) ).
cnf(f273,hypothesis,
queue_73 = rstore_tail(queue_71,index_72),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp257) ).
fof(f273_nnf,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(nnf_transformation,[status(thm)],[f273]) ).
cnf(c273,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(cnf_transformation,[status(esa)],[f273_nnf]) ).
cnf(p1119,plain,
rselect_head(queue_73) = rselect_head(queue_71),
inference(superposition,[status(thm)],[c273,c7]) ).
cnf(p3095,plain,
rselect_head(q2) = rselect_head(queue_71),
inference(superposition,[status(thm)],[c294,p1119]) ).
cnf(p3334,plain,
index_261 = rselect_head(queue_71),
inference(demodulation,[status(thm)],[p3331,p3095]) ).
cnf(f283,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp267) ).
fof(f283_nnf,plain,
q1 = queue_7,
inference(nnf_transformation,[status(thm)],[f283]) ).
cnf(c283,plain,
q1 = queue_7,
inference(cnf_transformation,[status(esa)],[f283_nnf]) ).
cnf(f271,hypothesis,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp255) ).
fof(f271_nnf,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(nnf_transformation,[status(thm)],[f271]) ).
cnf(c271,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(cnf_transformation,[status(esa)],[f271_nnf]) ).
cnf(p1111,plain,
rselect_head(queue_7) = rselect_head(queue_5),
inference(superposition,[status(thm)],[c271,c7]) ).
cnf(p3030,plain,
rselect_head(q1) = index_9,
inference(superposition,[status(thm)],[c283,p1111]) ).
cnf(f272,hypothesis,
queue_71 = rstore_seq(q1,earray_70),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp256) ).
fof(f272_nnf,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(nnf_transformation,[status(thm)],[f272]) ).
cnf(c272,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(cnf_transformation,[status(esa)],[f272_nnf]) ).
cnf(p1113,plain,
rselect_head(queue_71) = rselect_head(q1),
inference(superposition,[status(thm)],[c272,c8]) ).
cnf(p3031,plain,
rselect_head(queue_71) = index_9,
inference(demodulation,[status(thm)],[p3030,p1113]) ).
cnf(p3336,plain,
index_261 = index_9,
inference(superposition,[status(thm)],[p3334,p3031]) ).
cnf(f6,axiom,
rselect_seq(rstore_tail(A,E)) = rselect_seq(A),
file('/export/starexec/sandbox/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(p903,plain,
rselect_seq(queue_229) = rselect_seq(queue_227),
inference(superposition,[status(thm)],[c243,c6]) ).
cnf(p2675,plain,
earray_260 = earray_226,
inference(superposition,[status(thm)],[c320,p903]) ).
cnf(f103,hypothesis,
elem_262 = select(earray_260,index_261),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp87) ).
fof(f103_nnf,plain,
elem_262 = select(earray_260,index_261),
inference(nnf_transformation,[status(thm)],[f103]) ).
cnf(c103,plain,
elem_262 = select(earray_260,index_261),
inference(cnf_transformation,[status(esa)],[f103_nnf]) ).
cnf(p2676,plain,
elem_262 = select(earray_226,index_261),
inference(demodulation,[status(thm)],[p2675,c103]) ).
cnf(p3338,plain,
elem_262 = select(earray_226,index_9),
inference(demodulation,[status(thm)],[p3336,p2676]) ).
cnf(f4,axiom,
rselect_tail(rstore_tail(A,E)) = E,
file('/export/starexec/sandbox/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(p1164,plain,
rselect_tail(queue_91) = index_90,
inference(superposition,[status(thm)],[c279,c4]) ).
cnf(p1760,plain,
index_93 = index_90,
inference(superposition,[status(thm)],[c297,p1164]) ).
cnf(f191,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp175) ).
fof(f191_nnf,plain,
index_90 = s(index_87),
inference(nnf_transformation,[status(thm)],[f191]) ).
cnf(c191,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(esa)],[f191_nnf]) ).
cnf(f11,axiom,
p(s(X)) = X,
file('/export/starexec/sandbox/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(p585,plain,
p(index_90) = index_87,
inference(superposition,[status(thm)],[c191,c11]) ).
cnf(p1762,plain,
p(index_93) = index_87,
inference(superposition,[status(thm)],[p1760,p585]) ).
cnf(f12,axiom,
s(p(X)) = X,
file('/export/starexec/sandbox/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(f15,axiom,
s(s(s(X))) = X,
file('/export/starexec/sandbox/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(p346,plain,
s(s(X0)) = p(X0),
inference(superposition,[status(thm)],[c12,c15]) ).
cnf(p2356,plain,
index_105 = index_9,
inference(superposition,[status(thm)],[p1762,p346]) ).
cnf(p609,plain,
rselect_tail(queue_103) = index_102,
inference(superposition,[status(thm)],[c197,c4]) ).
cnf(p833,plain,
index_105 = index_102,
inference(superposition,[status(thm)],[c299,p609]) ).
cnf(f106,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp90) ).
fof(f106_nnf,plain,
index_102 = s(index_99),
inference(nnf_transformation,[status(thm)],[f106]) ).
cnf(c106,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(esa)],[f106_nnf]) ).
cnf(p394,plain,
p(index_102) = index_99,
inference(superposition,[status(thm)],[c106,c11]) ).
cnf(p839,plain,
p(index_105) = index_99,
inference(superposition,[status(thm)],[p833,p394]) ).
cnf(p1315,plain,
s(index_111) = index_99,
inference(superposition,[status(thm)],[p839,p346]) ).
cnf(p627,plain,
rselect_tail(queue_115) = index_114,
inference(superposition,[status(thm)],[c202,c4]) ).
cnf(p865,plain,
index_117 = index_114,
inference(superposition,[status(thm)],[c301,p627]) ).
cnf(p870,plain,
index_114 = index_117,
inference(superposition,[status(thm)],[p865,p627]) ).
cnf(f110,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp94) ).
fof(f110_nnf,plain,
index_114 = s(index_111),
inference(nnf_transformation,[status(thm)],[f110]) ).
cnf(c110,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(esa)],[f110_nnf]) ).
cnf(p404,plain,
p(index_114) = index_111,
inference(superposition,[status(thm)],[c110,c11]) ).
cnf(p636,plain,
s(index_111) = index_114,
inference(superposition,[status(thm)],[p404,c12]) ).
cnf(p873,plain,
s(index_111) = index_117,
inference(demodulation,[status(thm)],[p870,p636]) ).
cnf(p1316,plain,
index_99 = index_117,
inference(demodulation,[status(thm)],[p1315,p873]) ).
cnf(f111,hypothesis,
index_117 = rselect_tail(q26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp95) ).
fof(f111_nnf,plain,
index_117 = rselect_tail(q26),
inference(nnf_transformation,[status(thm)],[f111]) ).
cnf(c111,plain,
index_117 = rselect_tail(q26),
inference(cnf_transformation,[status(esa)],[f111_nnf]) ).
cnf(f9,axiom,
rselect_tail(rstore_seq(A,E)) = rselect_tail(A),
file('/export/starexec/sandbox/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(p405,plain,
rselect_tail(q26) = index_117,
inference(superposition,[status(thm)],[c111,c9]) ).
cnf(p1319,plain,
index_117 = index_99,
inference(superposition,[status(thm)],[p1316,p405]) ).
cnf(p638,plain,
rselect_tail(queue_121) = index_120,
inference(superposition,[status(thm)],[c204,c4]) ).
cnf(p877,plain,
index_123 = index_120,
inference(superposition,[status(thm)],[c302,p638]) ).
cnf(f113,hypothesis,
index_120 = s(index_117),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp97) ).
fof(f113_nnf,plain,
index_120 = s(index_117),
inference(nnf_transformation,[status(thm)],[f113]) ).
cnf(c113,plain,
index_120 = s(index_117),
inference(cnf_transformation,[status(esa)],[f113_nnf]) ).
cnf(p411,plain,
p(index_120) = index_117,
inference(superposition,[status(thm)],[c113,c11]) ).
cnf(p880,plain,
p(index_123) = index_117,
inference(superposition,[status(thm)],[p877,p411]) ).
cnf(p1330,plain,
p(index_123) = index_99,
inference(demodulation,[status(thm)],[p1319,p880]) ).
cnf(p1826,plain,
index_105 = index_123,
inference(superposition,[status(thm)],[p1330,c12]) ).
cnf(f114,hypothesis,
index_123 = rselect_tail(q27),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp98) ).
fof(f114_nnf,plain,
index_123 = rselect_tail(q27),
inference(nnf_transformation,[status(thm)],[f114]) ).
cnf(c114,plain,
index_123 = rselect_tail(q27),
inference(cnf_transformation,[status(esa)],[f114_nnf]) ).
cnf(p414,plain,
rselect_tail(q27) = index_123,
inference(superposition,[status(thm)],[c114,c9]) ).
cnf(p1829,plain,
index_123 = index_105,
inference(superposition,[status(thm)],[p1826,p414]) ).
cnf(p670,plain,
rselect_tail(queue_133) = index_132,
inference(superposition,[status(thm)],[c209,c4]) ).
cnf(p925,plain,
index_141 = index_132,
inference(superposition,[status(thm)],[c304,p670]) ).
cnf(f117,hypothesis,
index_132 = s(index_129),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp101) ).
fof(f117_nnf,plain,
index_132 = s(index_129),
inference(nnf_transformation,[status(thm)],[f117]) ).
cnf(c117,plain,
index_132 = s(index_129),
inference(cnf_transformation,[status(esa)],[f117_nnf]) ).
cnf(p421,plain,
p(index_132) = index_129,
inference(superposition,[status(thm)],[c117,c11]) ).
cnf(p655,plain,
s(index_129) = index_132,
inference(superposition,[status(thm)],[p421,c12]) ).
cnf(p930,plain,
index_132 = index_141,
inference(superposition,[status(thm)],[p925,p655]) ).
cnf(p931,plain,
s(index_129) = index_141,
inference(demodulation,[status(thm)],[p930,p655]) ).
cnf(p1384,plain,
s(index_141) = index_123,
inference(superposition,[status(thm)],[p931,p346]) ).
cnf(p696,plain,
rselect_tail(queue_145) = index_144,
inference(superposition,[status(thm)],[c213,c4]) ).
cnf(p961,plain,
index_147 = index_144,
inference(superposition,[status(thm)],[c306,p696]) ).
cnf(f121,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp105) ).
fof(f121_nnf,plain,
index_144 = s(index_141),
inference(nnf_transformation,[status(thm)],[f121]) ).
cnf(c121,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(esa)],[f121_nnf]) ).
cnf(p429,plain,
p(index_144) = index_141,
inference(superposition,[status(thm)],[c121,c11]) ).
cnf(p663,plain,
s(index_141) = index_144,
inference(superposition,[status(thm)],[p429,c12]) ).
cnf(p966,plain,
index_144 = index_147,
inference(superposition,[status(thm)],[p961,p663]) ).
cnf(p967,plain,
s(index_141) = index_147,
inference(demodulation,[status(thm)],[p966,p663]) ).
cnf(p1385,plain,
index_123 = index_147,
inference(demodulation,[status(thm)],[p1384,p967]) ).
cnf(f122,hypothesis,
index_147 = rselect_tail(q30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp106) ).
fof(f122_nnf,plain,
index_147 = rselect_tail(q30),
inference(nnf_transformation,[status(thm)],[f122]) ).
cnf(c122,plain,
index_147 = rselect_tail(q30),
inference(cnf_transformation,[status(esa)],[f122_nnf]) ).
cnf(p432,plain,
rselect_tail(q30) = index_147,
inference(superposition,[status(thm)],[c122,c9]) ).
cnf(p1387,plain,
index_147 = index_123,
inference(superposition,[status(thm)],[p1385,p432]) ).
cnf(p707,plain,
rselect_tail(queue_151) = index_150,
inference(superposition,[status(thm)],[c215,c4]) ).
cnf(p977,plain,
index_153 = index_150,
inference(superposition,[status(thm)],[c307,p707]) ).
cnf(f124,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp108) ).
fof(f124_nnf,plain,
index_150 = s(index_147),
inference(nnf_transformation,[status(thm)],[f124]) ).
cnf(c124,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(esa)],[f124_nnf]) ).
cnf(p435,plain,
p(index_150) = index_147,
inference(superposition,[status(thm)],[c124,c11]) ).
cnf(p982,plain,
p(index_153) = index_147,
inference(superposition,[status(thm)],[p977,p435]) ).
cnf(p1399,plain,
p(index_153) = index_123,
inference(demodulation,[status(thm)],[p1387,p982]) ).
cnf(p1861,plain,
p(index_153) = index_105,
inference(demodulation,[status(thm)],[p1829,p1399]) ).
cnf(p2396,plain,
p(index_153) = index_9,
inference(demodulation,[status(thm)],[p2356,p1861]) ).
cnf(p2842,plain,
index_165 = index_9,
inference(superposition,[status(thm)],[p2396,p346]) ).
cnf(p731,plain,
rselect_tail(queue_163) = index_162,
inference(superposition,[status(thm)],[c219,c4]) ).
cnf(p1012,plain,
index_165 = index_162,
inference(superposition,[status(thm)],[c309,p731]) ).
cnf(f128,hypothesis,
index_162 = s(index_159),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp112) ).
fof(f128_nnf,plain,
index_162 = s(index_159),
inference(nnf_transformation,[status(thm)],[f128]) ).
cnf(c128,plain,
index_162 = s(index_159),
inference(cnf_transformation,[status(esa)],[f128_nnf]) ).
cnf(p445,plain,
p(index_162) = index_159,
inference(superposition,[status(thm)],[c128,c11]) ).
cnf(p679,plain,
s(index_159) = index_162,
inference(superposition,[status(thm)],[p445,c12]) ).
cnf(p1017,plain,
index_162 = index_165,
inference(superposition,[status(thm)],[p1012,p679]) ).
cnf(p1018,plain,
s(index_159) = index_165,
inference(demodulation,[status(thm)],[p1017,p679]) ).
cnf(p1503,plain,
s(index_165) = index_153,
inference(superposition,[status(thm)],[p1018,p346]) ).
cnf(p744,plain,
rselect_tail(queue_169) = index_168,
inference(superposition,[status(thm)],[c221,c4]) ).
cnf(p1032,plain,
index_171 = index_168,
inference(superposition,[status(thm)],[c310,p744]) ).
cnf(f130,hypothesis,
index_168 = s(index_165),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp114) ).
fof(f130_nnf,plain,
index_168 = s(index_165),
inference(nnf_transformation,[status(thm)],[f130]) ).
cnf(c130,plain,
index_168 = s(index_165),
inference(cnf_transformation,[status(esa)],[f130_nnf]) ).
cnf(p448,plain,
p(index_168) = index_165,
inference(superposition,[status(thm)],[c130,c11]) ).
cnf(p681,plain,
s(index_165) = index_168,
inference(superposition,[status(thm)],[p448,c12]) ).
cnf(p1037,plain,
index_168 = index_171,
inference(superposition,[status(thm)],[p1032,p681]) ).
cnf(p1038,plain,
s(index_165) = index_171,
inference(demodulation,[status(thm)],[p1037,p681]) ).
cnf(p1504,plain,
index_153 = index_171,
inference(demodulation,[status(thm)],[p1503,p1038]) ).
cnf(f131,hypothesis,
index_171 = rselect_tail(q34),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp115) ).
fof(f131_nnf,plain,
index_171 = rselect_tail(q34),
inference(nnf_transformation,[status(thm)],[f131]) ).
cnf(c131,plain,
index_171 = rselect_tail(q34),
inference(cnf_transformation,[status(esa)],[f131_nnf]) ).
cnf(p451,plain,
rselect_tail(q34) = index_171,
inference(superposition,[status(thm)],[c131,c9]) ).
cnf(p1507,plain,
index_171 = index_153,
inference(superposition,[status(thm)],[p1504,p451]) ).
cnf(p762,plain,
rselect_tail(queue_175) = index_174,
inference(superposition,[status(thm)],[c224,c4]) ).
cnf(p1051,plain,
index_177 = index_174,
inference(superposition,[status(thm)],[c311,p762]) ).
cnf(f132,hypothesis,
index_174 = s(index_171),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp116) ).
fof(f132_nnf,plain,
index_174 = s(index_171),
inference(nnf_transformation,[status(thm)],[f132]) ).
cnf(c132,plain,
index_174 = s(index_171),
inference(cnf_transformation,[status(esa)],[f132_nnf]) ).
cnf(p453,plain,
p(index_174) = index_171,
inference(superposition,[status(thm)],[c132,c11]) ).
cnf(p1053,plain,
p(index_177) = index_171,
inference(superposition,[status(thm)],[p1051,p453]) ).
cnf(p1519,plain,
p(index_177) = index_153,
inference(demodulation,[status(thm)],[p1507,p1053]) ).
cnf(p2000,plain,
index_159 = index_177,
inference(superposition,[status(thm)],[p1519,c12]) ).
cnf(f133,hypothesis,
index_177 = rselect_tail(q35),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp117) ).
fof(f133_nnf,plain,
index_177 = rselect_tail(q35),
inference(nnf_transformation,[status(thm)],[f133]) ).
cnf(c133,plain,
index_177 = rselect_tail(q35),
inference(cnf_transformation,[status(esa)],[f133_nnf]) ).
cnf(p456,plain,
rselect_tail(q35) = index_177,
inference(superposition,[status(thm)],[c133,c9]) ).
cnf(p2003,plain,
index_177 = index_159,
inference(superposition,[status(thm)],[p2000,p456]) ).
cnf(p785,plain,
rselect_tail(queue_187) = index_186,
inference(superposition,[status(thm)],[c228,c4]) ).
cnf(p1083,plain,
index_189 = index_186,
inference(superposition,[status(thm)],[c313,p785]) ).
cnf(f137,hypothesis,
index_186 = s(index_183),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp121) ).
fof(f137_nnf,plain,
index_186 = s(index_183),
inference(nnf_transformation,[status(thm)],[f137]) ).
cnf(c137,plain,
index_186 = s(index_183),
inference(cnf_transformation,[status(esa)],[f137_nnf]) ).
cnf(p465,plain,
p(index_186) = index_183,
inference(superposition,[status(thm)],[c137,c11]) ).
cnf(p700,plain,
s(index_183) = index_186,
inference(superposition,[status(thm)],[p465,c12]) ).
cnf(p1091,plain,
index_186 = index_189,
inference(superposition,[status(thm)],[p1083,p700]) ).
cnf(p1092,plain,
s(index_183) = index_189,
inference(demodulation,[status(thm)],[p1091,p700]) ).
cnf(p1606,plain,
s(index_189) = index_177,
inference(superposition,[status(thm)],[p1092,p346]) ).
cnf(p804,plain,
rselect_tail(queue_193) = index_192,
inference(superposition,[status(thm)],[c231,c4]) ).
cnf(p1115,plain,
index_195 = index_192,
inference(superposition,[status(thm)],[c314,p804]) ).
cnf(f139,hypothesis,
index_192 = s(index_189),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp123) ).
fof(f139_nnf,plain,
index_192 = s(index_189),
inference(nnf_transformation,[status(thm)],[f139]) ).
cnf(c139,plain,
index_192 = s(index_189),
inference(cnf_transformation,[status(esa)],[f139_nnf]) ).
cnf(p470,plain,
p(index_192) = index_189,
inference(superposition,[status(thm)],[c139,c11]) ).
cnf(p705,plain,
s(index_189) = index_192,
inference(superposition,[status(thm)],[p470,c12]) ).
cnf(p1124,plain,
index_192 = index_195,
inference(superposition,[status(thm)],[p1115,p705]) ).
cnf(p1125,plain,
s(index_189) = index_195,
inference(demodulation,[status(thm)],[p1124,p705]) ).
cnf(p1607,plain,
index_177 = index_195,
inference(demodulation,[status(thm)],[p1606,p1125]) ).
cnf(f140,hypothesis,
index_195 = rselect_tail(q38),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp124) ).
fof(f140_nnf,plain,
index_195 = rselect_tail(q38),
inference(nnf_transformation,[status(thm)],[f140]) ).
cnf(c140,plain,
index_195 = rselect_tail(q38),
inference(cnf_transformation,[status(esa)],[f140_nnf]) ).
cnf(p471,plain,
rselect_tail(q38) = index_195,
inference(superposition,[status(thm)],[c140,c9]) ).
cnf(p1609,plain,
index_195 = index_177,
inference(superposition,[status(thm)],[p1607,p471]) ).
cnf(p817,plain,
rselect_tail(queue_199) = index_198,
inference(superposition,[status(thm)],[c233,c4]) ).
cnf(p1135,plain,
index_207 = index_198,
inference(superposition,[status(thm)],[c315,p817]) ).
cnf(f141,hypothesis,
index_198 = s(index_195),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp125) ).
fof(f141_nnf,plain,
index_198 = s(index_195),
inference(nnf_transformation,[status(thm)],[f141]) ).
cnf(c141,plain,
index_198 = s(index_195),
inference(cnf_transformation,[status(esa)],[f141_nnf]) ).
cnf(p475,plain,
p(index_198) = index_195,
inference(superposition,[status(thm)],[c141,c11]) ).
cnf(p1137,plain,
p(index_207) = index_195,
inference(superposition,[status(thm)],[p1135,p475]) ).
cnf(p1621,plain,
p(index_207) = index_177,
inference(demodulation,[status(thm)],[p1609,p1137]) ).
cnf(p2036,plain,
p(index_207) = index_159,
inference(demodulation,[status(thm)],[p2003,p1621]) ).
cnf(p2597,plain,
index_165 = index_207,
inference(superposition,[status(thm)],[p2036,c12]) ).
cnf(f144,hypothesis,
index_207 = rselect_tail(q39),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp128) ).
fof(f144_nnf,plain,
index_207 = rselect_tail(q39),
inference(nnf_transformation,[status(thm)],[f144]) ).
cnf(c144,plain,
index_207 = rselect_tail(q39),
inference(cnf_transformation,[status(esa)],[f144_nnf]) ).
cnf(p481,plain,
rselect_tail(q39) = index_207,
inference(superposition,[status(thm)],[c144,c9]) ).
cnf(p2619,plain,
index_207 = index_165,
inference(superposition,[status(thm)],[p2597,p481]) ).
cnf(p861,plain,
rselect_tail(queue_217) = index_216,
inference(superposition,[status(thm)],[c239,c4]) ).
cnf(p1227,plain,
index_219 = index_216,
inference(superposition,[status(thm)],[c318,p861]) ).
cnf(f148,hypothesis,
index_216 = s(index_213),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp132) ).
fof(f148_nnf,plain,
index_216 = s(index_213),
inference(nnf_transformation,[status(thm)],[f148]) ).
cnf(c148,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(esa)],[f148_nnf]) ).
cnf(p489,plain,
p(index_216) = index_213,
inference(superposition,[status(thm)],[c148,c11]) ).
cnf(p724,plain,
s(index_213) = index_216,
inference(superposition,[status(thm)],[p489,c12]) ).
cnf(p1284,plain,
index_216 = index_219,
inference(superposition,[status(thm)],[p1227,p724]) ).
cnf(p1285,plain,
s(index_213) = index_219,
inference(demodulation,[status(thm)],[p1284,p724]) ).
cnf(p1801,plain,
s(index_219) = index_207,
inference(superposition,[status(thm)],[p1285,p346]) ).
cnf(p886,plain,
rselect_tail(queue_223) = index_222,
inference(superposition,[status(thm)],[c241,c4]) ).
cnf(p1335,plain,
index_225 = index_222,
inference(superposition,[status(thm)],[c319,p886]) ).
cnf(f150,hypothesis,
index_222 = s(index_219),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp134) ).
fof(f150_nnf,plain,
index_222 = s(index_219),
inference(nnf_transformation,[status(thm)],[f150]) ).
cnf(c150,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(esa)],[f150_nnf]) ).
cnf(p494,plain,
p(index_222) = index_219,
inference(superposition,[status(thm)],[c150,c11]) ).
cnf(p729,plain,
s(index_219) = index_222,
inference(superposition,[status(thm)],[p494,c12]) ).
cnf(p1342,plain,
index_222 = index_225,
inference(superposition,[status(thm)],[p1335,p729]) ).
cnf(p1343,plain,
s(index_219) = index_225,
inference(demodulation,[status(thm)],[p1342,p729]) ).
cnf(p1802,plain,
index_207 = index_225,
inference(demodulation,[status(thm)],[p1801,p1343]) ).
cnf(f151,hypothesis,
index_225 = rselect_tail(q42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp135) ).
fof(f151_nnf,plain,
index_225 = rselect_tail(q42),
inference(nnf_transformation,[status(thm)],[f151]) ).
cnf(c151,plain,
index_225 = rselect_tail(q42),
inference(cnf_transformation,[status(esa)],[f151_nnf]) ).
cnf(p495,plain,
rselect_tail(q42) = index_225,
inference(superposition,[status(thm)],[c151,c9]) ).
cnf(p1805,plain,
index_225 = index_207,
inference(superposition,[status(thm)],[p1802,p495]) ).
cnf(f64,hypothesis,
earray_226 = store(earray_224,index_225,e42),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp48) ).
fof(f64_nnf,plain,
earray_226 = store(earray_224,index_225,e42),
inference(nnf_transformation,[status(thm)],[f64]) ).
cnf(c64,plain,
earray_226 = store(earray_224,index_225,e42),
inference(cnf_transformation,[status(esa)],[f64_nnf]) ).
cnf(f0,axiom,
select(store(A,I,E),I) = E,
file('/export/starexec/sandbox/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(p496,plain,
select(earray_226,index_225) = e42,
inference(superposition,[status(thm)],[c64,c0]) ).
cnf(p1807,plain,
select(earray_226,index_207) = e42,
inference(demodulation,[status(thm)],[p1805,p496]) ).
cnf(p2638,plain,
select(earray_226,index_165) = e42,
inference(demodulation,[status(thm)],[p2619,p1807]) ).
cnf(p2891,plain,
select(earray_226,index_9) = e42,
inference(demodulation,[status(thm)],[p2842,p2638]) ).
cnf(p3593,plain,
elem_262 = e42,
inference(superposition,[status(thm)],[p3338,p2891]) ).
cnf(p1337,plain,
p(index_225) = index_219,
inference(superposition,[status(thm)],[p1335,p494]) ).
cnf(f152,hypothesis,
index_228 = s(index_225),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp136) ).
fof(f152_nnf,plain,
index_228 = s(index_225),
inference(nnf_transformation,[status(thm)],[f152]) ).
cnf(c152,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(esa)],[f152_nnf]) ).
cnf(p499,plain,
p(index_228) = index_225,
inference(superposition,[status(thm)],[c152,c11]) ).
cnf(p735,plain,
s(index_225) = index_228,
inference(superposition,[status(thm)],[p499,c12]) ).
cnf(p1295,plain,
s(index_228) = p(index_225),
inference(superposition,[status(thm)],[p735,p346]) ).
cnf(p1339,plain,
s(index_228) = index_219,
inference(demodulation,[status(thm)],[p1337,p1295]) ).
cnf(p1868,plain,
index_213 = index_228,
inference(superposition,[status(thm)],[p1339,c11]) ).
cnf(p902,plain,
rselect_tail(queue_229) = index_228,
inference(superposition,[status(thm)],[c243,c4]) ).
cnf(p1872,plain,
index_228 = index_213,
inference(superposition,[status(thm)],[p1868,p902]) ).
cnf(p1353,plain,
index_263 = index_228,
inference(superposition,[status(thm)],[c320,p902]) ).
cnf(f166,hypothesis,
s(index_264) = index_263,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp150) ).
fof(f166_nnf,plain,
s(index_264) = index_263,
inference(nnf_transformation,[status(thm)],[f166]) ).
cnf(c166,plain,
s(index_264) = index_263,
inference(cnf_transformation,[status(esa)],[f166_nnf]) ).
cnf(p1354,plain,
s(index_264) = index_228,
inference(demodulation,[status(thm)],[p1353,c166]) ).
cnf(p1876,plain,
s(index_264) = index_213,
inference(demodulation,[status(thm)],[p1872,p1354]) ).
cnf(p2526,plain,
index_207 = index_264,
inference(superposition,[status(thm)],[p1876,c11]) ).
cnf(f104,hypothesis,
elem_265 = select(earray_260,index_264),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp88) ).
fof(f104_nnf,plain,
elem_265 = select(earray_260,index_264),
inference(nnf_transformation,[status(thm)],[f104]) ).
cnf(c104,plain,
elem_265 = select(earray_260,index_264),
inference(cnf_transformation,[status(esa)],[f104_nnf]) ).
cnf(p2528,plain,
elem_265 = select(earray_260,index_207),
inference(superposition,[status(thm)],[p2526,c104]) ).
cnf(p2647,plain,
elem_265 = select(earray_260,index_165),
inference(demodulation,[status(thm)],[p2619,p2528]) ).
cnf(p2681,plain,
elem_265 = select(earray_226,index_165),
inference(demodulation,[status(thm)],[p2675,p2647]) ).
cnf(p2906,plain,
elem_265 = select(earray_226,index_9),
inference(demodulation,[status(thm)],[p2842,p2681]) ).
cnf(p3540,plain,
elem_265 = e42,
inference(superposition,[status(thm)],[p2906,p2891]) ).
cnf(f326,negated_conjecture,
elem_262 != elem_265,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f326_nnf,plain,
elem_262 != elem_265,
inference(nnf_transformation,[status(thm)],[f326]) ).
fof(f326_sk,plain,
elem_262 != elem_265,
inference(skolemisation,[status(esa)],[f326_nnf]) ).
cnf(c326,plain,
elem_262 != elem_265,
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
cnf(p3541,plain,
elem_262 != e42,
inference(demodulation,[status(thm)],[p3540,c326]) ).
cnf(p3594,plain,
e42 != e42,
inference(demodulation,[status(thm)],[p3593,p3541]) ).
cnf(p3595,plain,
$false,
inference(equality_resolution,[status(thm)],[p3594]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV570-1.043 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 20:38:04 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 31.15/4.39 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.15/4.39 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------