%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.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 36.76s 5.10s
% Output : Proof 36.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 96
% Number of leaves : 158
% Syntax : Number of formulae : 889 ( 889 unt; 0 def)
% Number of atoms : 889 ( 888 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 : 257 ( 257 usr; 247 con; 0-3 aty)
% Number of variables : 81 ( 16 sgn 40 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f341,hypothesis,
q46 = queue_247,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp325) ).
fof(f341_nnf,plain,
q46 = queue_247,
inference(nnf_transformation,[status(thm)],[f341]) ).
cnf(c341,plain,
q46 = queue_247,
inference(cnf_transformation,[status(esa)],[f341_nnf]) ).
cnf(f262,hypothesis,
queue_247 = rstore_tail(queue_245,index_246),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp246) ).
fof(f262_nnf,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(nnf_transformation,[status(thm)],[f262]) ).
cnf(c262,plain,
queue_247 = rstore_tail(queue_245,index_246),
inference(cnf_transformation,[status(esa)],[f262_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(p991,plain,
rselect_head(queue_247) = rselect_head(queue_245),
inference(superposition,[status(thm)],[c262,c7]) ).
cnf(p2901,plain,
index_279 = rselect_head(queue_245),
inference(superposition,[status(thm)],[c341,p991]) ).
cnf(p3316,plain,
rselect_head(queue_245) = index_279,
inference(superposition,[status(thm)],[p2901,c7]) ).
cnf(f340,hypothesis,
q45 = queue_241,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp324) ).
fof(f340_nnf,plain,
q45 = queue_241,
inference(nnf_transformation,[status(thm)],[f340]) ).
cnf(c340,plain,
q45 = queue_241,
inference(cnf_transformation,[status(esa)],[f340_nnf]) ).
cnf(f260,hypothesis,
queue_241 = rstore_tail(queue_239,index_240),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp244) ).
fof(f260_nnf,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(nnf_transformation,[status(thm)],[f260]) ).
cnf(c260,plain,
queue_241 = rstore_tail(queue_239,index_240),
inference(cnf_transformation,[status(esa)],[f260_nnf]) ).
cnf(p975,plain,
rselect_head(queue_241) = rselect_head(queue_239),
inference(superposition,[status(thm)],[c260,c7]) ).
cnf(p2886,plain,
rselect_head(q45) = rselect_head(q44),
inference(superposition,[status(thm)],[c340,p975]) ).
cnf(f261,hypothesis,
queue_245 = rstore_seq(q45,earray_244),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp245) ).
fof(f261_nnf,plain,
queue_245 = rstore_seq(q45,earray_244),
inference(nnf_transformation,[status(thm)],[f261]) ).
cnf(c261,plain,
queue_245 = rstore_seq(q45,earray_244),
inference(cnf_transformation,[status(esa)],[f261_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(p978,plain,
rselect_head(queue_245) = rselect_head(q45),
inference(superposition,[status(thm)],[c261,c8]) ).
cnf(p2887,plain,
rselect_head(queue_245) = rselect_head(q44),
inference(demodulation,[status(thm)],[p2886,p978]) ).
cnf(p3318,plain,
index_279 = rselect_head(q44),
inference(demodulation,[status(thm)],[p3316,p2887]) ).
cnf(p3388,plain,
rselect_head(q44) = index_279,
inference(superposition,[status(thm)],[p3318,c7]) ).
cnf(f339,hypothesis,
q44 = queue_235,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp323) ).
fof(f339_nnf,plain,
q44 = queue_235,
inference(nnf_transformation,[status(thm)],[f339]) ).
cnf(c339,plain,
q44 = queue_235,
inference(cnf_transformation,[status(esa)],[f339_nnf]) ).
cnf(f258,hypothesis,
queue_235 = rstore_tail(queue_233,index_234),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp242) ).
fof(f258_nnf,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(nnf_transformation,[status(thm)],[f258]) ).
cnf(c258,plain,
queue_235 = rstore_tail(queue_233,index_234),
inference(cnf_transformation,[status(esa)],[f258_nnf]) ).
cnf(p950,plain,
rselect_head(queue_235) = rselect_head(queue_233),
inference(superposition,[status(thm)],[c258,c7]) ).
cnf(p2877,plain,
rselect_head(q44) = rselect_head(queue_233),
inference(superposition,[status(thm)],[c339,p950]) ).
cnf(p3390,plain,
index_279 = rselect_head(queue_233),
inference(demodulation,[status(thm)],[p3388,p2877]) ).
cnf(p3392,plain,
rselect_head(queue_233) = index_279,
inference(superposition,[status(thm)],[p3390,c7]) ).
cnf(f338,hypothesis,
q43 = queue_229,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp322) ).
fof(f338_nnf,plain,
q43 = queue_229,
inference(nnf_transformation,[status(thm)],[f338]) ).
cnf(c338,plain,
q43 = queue_229,
inference(cnf_transformation,[status(esa)],[f338_nnf]) ).
cnf(f255,hypothesis,
queue_229 = rstore_tail(queue_227,index_228),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp239) ).
fof(f255_nnf,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(nnf_transformation,[status(thm)],[f255]) ).
cnf(c255,plain,
queue_229 = rstore_tail(queue_227,index_228),
inference(cnf_transformation,[status(esa)],[f255_nnf]) ).
cnf(p923,plain,
rselect_head(queue_229) = rselect_head(queue_227),
inference(superposition,[status(thm)],[c255,c7]) ).
cnf(p2869,plain,
rselect_head(q43) = rselect_head(q42),
inference(superposition,[status(thm)],[c338,p923]) ).
cnf(f257,hypothesis,
queue_233 = rstore_seq(q43,earray_232),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp241) ).
fof(f257_nnf,plain,
queue_233 = rstore_seq(q43,earray_232),
inference(nnf_transformation,[status(thm)],[f257]) ).
cnf(c257,plain,
queue_233 = rstore_seq(q43,earray_232),
inference(cnf_transformation,[status(esa)],[f257_nnf]) ).
cnf(p946,plain,
rselect_head(queue_233) = rselect_head(q43),
inference(superposition,[status(thm)],[c257,c8]) ).
cnf(p2870,plain,
rselect_head(queue_233) = rselect_head(q42),
inference(demodulation,[status(thm)],[p2869,p946]) ).
cnf(p3394,plain,
index_279 = rselect_head(q42),
inference(demodulation,[status(thm)],[p3392,p2870]) ).
cnf(p3395,plain,
rselect_head(q42) = index_279,
inference(superposition,[status(thm)],[p3394,c7]) ).
cnf(f337,hypothesis,
q42 = queue_223,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp321) ).
fof(f337_nnf,plain,
q42 = queue_223,
inference(nnf_transformation,[status(thm)],[f337]) ).
cnf(c337,plain,
q42 = queue_223,
inference(cnf_transformation,[status(esa)],[f337_nnf]) ).
cnf(f253,hypothesis,
queue_223 = rstore_tail(queue_221,index_222),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp237) ).
fof(f253_nnf,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(nnf_transformation,[status(thm)],[f253]) ).
cnf(c253,plain,
queue_223 = rstore_tail(queue_221,index_222),
inference(cnf_transformation,[status(esa)],[f253_nnf]) ).
cnf(p906,plain,
rselect_head(queue_223) = rselect_head(queue_221),
inference(superposition,[status(thm)],[c253,c7]) ).
cnf(p2858,plain,
rselect_head(q42) = rselect_head(queue_221),
inference(superposition,[status(thm)],[c337,p906]) ).
cnf(p3397,plain,
index_279 = rselect_head(queue_221),
inference(demodulation,[status(thm)],[p3395,p2858]) ).
cnf(p3399,plain,
rselect_head(queue_221) = index_279,
inference(superposition,[status(thm)],[p3397,c7]) ).
cnf(f336,hypothesis,
q41 = queue_217,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp320) ).
fof(f336_nnf,plain,
q41 = queue_217,
inference(nnf_transformation,[status(thm)],[f336]) ).
cnf(c336,plain,
q41 = queue_217,
inference(cnf_transformation,[status(esa)],[f336_nnf]) ).
cnf(f251,hypothesis,
queue_217 = rstore_tail(queue_215,index_216),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp235) ).
fof(f251_nnf,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(nnf_transformation,[status(thm)],[f251]) ).
cnf(c251,plain,
queue_217 = rstore_tail(queue_215,index_216),
inference(cnf_transformation,[status(esa)],[f251_nnf]) ).
cnf(p889,plain,
rselect_head(queue_217) = rselect_head(queue_215),
inference(superposition,[status(thm)],[c251,c7]) ).
cnf(p2851,plain,
rselect_head(q41) = rselect_head(q40),
inference(superposition,[status(thm)],[c336,p889]) ).
cnf(f252,hypothesis,
queue_221 = rstore_seq(q41,earray_220),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp236) ).
fof(f252_nnf,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(nnf_transformation,[status(thm)],[f252]) ).
cnf(c252,plain,
queue_221 = rstore_seq(q41,earray_220),
inference(cnf_transformation,[status(esa)],[f252_nnf]) ).
cnf(p902,plain,
rselect_head(queue_221) = rselect_head(q41),
inference(superposition,[status(thm)],[c252,c8]) ).
cnf(p2852,plain,
rselect_head(queue_221) = rselect_head(q40),
inference(demodulation,[status(thm)],[p2851,p902]) ).
cnf(p3401,plain,
index_279 = rselect_head(q40),
inference(demodulation,[status(thm)],[p3399,p2852]) ).
cnf(p3402,plain,
rselect_head(q40) = index_279,
inference(superposition,[status(thm)],[p3401,c7]) ).
cnf(f335,hypothesis,
q40 = queue_211,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp319) ).
fof(f335_nnf,plain,
q40 = queue_211,
inference(nnf_transformation,[status(thm)],[f335]) ).
cnf(c335,plain,
q40 = queue_211,
inference(cnf_transformation,[status(esa)],[f335_nnf]) ).
cnf(f249,hypothesis,
queue_211 = rstore_tail(queue_209,index_210),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp233) ).
fof(f249_nnf,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(nnf_transformation,[status(thm)],[f249]) ).
cnf(c249,plain,
queue_211 = rstore_tail(queue_209,index_210),
inference(cnf_transformation,[status(esa)],[f249_nnf]) ).
cnf(p878,plain,
rselect_head(queue_211) = rselect_head(queue_209),
inference(superposition,[status(thm)],[c249,c7]) ).
cnf(p2814,plain,
rselect_head(q40) = rselect_head(queue_209),
inference(superposition,[status(thm)],[c335,p878]) ).
cnf(p3404,plain,
index_279 = rselect_head(queue_209),
inference(demodulation,[status(thm)],[p3402,p2814]) ).
cnf(p3408,plain,
rselect_head(queue_209) = index_279,
inference(superposition,[status(thm)],[p3404,c7]) ).
cnf(f333,hypothesis,
q39 = queue_199,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp317) ).
fof(f333_nnf,plain,
q39 = queue_199,
inference(nnf_transformation,[status(thm)],[f333]) ).
cnf(c333,plain,
q39 = queue_199,
inference(cnf_transformation,[status(esa)],[f333_nnf]) ).
cnf(f245,hypothesis,
queue_199 = rstore_tail(queue_197,index_198),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp229) ).
fof(f245_nnf,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(nnf_transformation,[status(thm)],[f245]) ).
cnf(c245,plain,
queue_199 = rstore_tail(queue_197,index_198),
inference(cnf_transformation,[status(esa)],[f245_nnf]) ).
cnf(p854,plain,
rselect_head(queue_199) = rselect_head(queue_197),
inference(superposition,[status(thm)],[c245,c7]) ).
cnf(p2801,plain,
rselect_head(q39) = rselect_head(q38),
inference(superposition,[status(thm)],[c333,p854]) ).
cnf(f248,hypothesis,
queue_209 = rstore_seq(q39,earray_208),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp232) ).
fof(f248_nnf,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(nnf_transformation,[status(thm)],[f248]) ).
cnf(c248,plain,
queue_209 = rstore_seq(q39,earray_208),
inference(cnf_transformation,[status(esa)],[f248_nnf]) ).
cnf(p872,plain,
rselect_head(queue_209) = rselect_head(q39),
inference(superposition,[status(thm)],[c248,c8]) ).
cnf(p2802,plain,
rselect_head(queue_209) = rselect_head(q38),
inference(demodulation,[status(thm)],[p2801,p872]) ).
cnf(p3410,plain,
index_279 = rselect_head(q38),
inference(demodulation,[status(thm)],[p3408,p2802]) ).
cnf(p3412,plain,
rselect_head(q38) = index_279,
inference(superposition,[status(thm)],[p3410,c7]) ).
cnf(f332,hypothesis,
q38 = queue_193,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp316) ).
fof(f332_nnf,plain,
q38 = queue_193,
inference(nnf_transformation,[status(thm)],[f332]) ).
cnf(c332,plain,
q38 = queue_193,
inference(cnf_transformation,[status(esa)],[f332_nnf]) ).
cnf(f243,hypothesis,
queue_193 = rstore_tail(queue_191,index_192),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp227) ).
fof(f243_nnf,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(nnf_transformation,[status(thm)],[f243]) ).
cnf(c243,plain,
queue_193 = rstore_tail(queue_191,index_192),
inference(cnf_transformation,[status(esa)],[f243_nnf]) ).
cnf(p841,plain,
rselect_head(queue_193) = rselect_head(queue_191),
inference(superposition,[status(thm)],[c243,c7]) ).
cnf(p2718,plain,
rselect_head(q38) = rselect_head(queue_191),
inference(superposition,[status(thm)],[c332,p841]) ).
cnf(p3414,plain,
index_279 = rselect_head(queue_191),
inference(demodulation,[status(thm)],[p3412,p2718]) ).
cnf(p3419,plain,
rselect_head(queue_191) = index_279,
inference(superposition,[status(thm)],[p3414,c7]) ).
cnf(f331,hypothesis,
q37 = queue_187,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp315) ).
fof(f331_nnf,plain,
q37 = queue_187,
inference(nnf_transformation,[status(thm)],[f331]) ).
cnf(c331,plain,
q37 = queue_187,
inference(cnf_transformation,[status(esa)],[f331_nnf]) ).
cnf(f240,hypothesis,
queue_187 = rstore_tail(queue_185,index_186),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp224) ).
fof(f240_nnf,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(nnf_transformation,[status(thm)],[f240]) ).
cnf(c240,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(cnf_transformation,[status(esa)],[f240_nnf]) ).
cnf(p824,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(superposition,[status(thm)],[c240,c7]) ).
cnf(p2704,plain,
rselect_head(q37) = rselect_head(q36),
inference(superposition,[status(thm)],[c331,p824]) ).
cnf(f242,hypothesis,
queue_191 = rstore_seq(q37,earray_190),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp226) ).
fof(f242_nnf,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(nnf_transformation,[status(thm)],[f242]) ).
cnf(c242,plain,
queue_191 = rstore_seq(q37,earray_190),
inference(cnf_transformation,[status(esa)],[f242_nnf]) ).
cnf(p835,plain,
rselect_head(queue_191) = rselect_head(q37),
inference(superposition,[status(thm)],[c242,c8]) ).
cnf(p2705,plain,
rselect_head(queue_191) = rselect_head(q36),
inference(demodulation,[status(thm)],[p2704,p835]) ).
cnf(p3421,plain,
index_279 = rselect_head(q36),
inference(demodulation,[status(thm)],[p3419,p2705]) ).
cnf(p3424,plain,
rselect_head(q36) = index_279,
inference(superposition,[status(thm)],[p3421,c7]) ).
cnf(f330,hypothesis,
q36 = queue_181,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp314) ).
fof(f330_nnf,plain,
q36 = queue_181,
inference(nnf_transformation,[status(thm)],[f330]) ).
cnf(c330,plain,
q36 = queue_181,
inference(cnf_transformation,[status(esa)],[f330_nnf]) ).
cnf(f238,hypothesis,
queue_181 = rstore_tail(queue_179,index_180),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp222) ).
fof(f238_nnf,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(nnf_transformation,[status(thm)],[f238]) ).
cnf(c238,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(cnf_transformation,[status(esa)],[f238_nnf]) ).
cnf(p813,plain,
rselect_head(queue_181) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c238,c7]) ).
cnf(p2698,plain,
rselect_head(q36) = rselect_head(queue_179),
inference(superposition,[status(thm)],[c330,p813]) ).
cnf(p3426,plain,
index_279 = rselect_head(queue_179),
inference(demodulation,[status(thm)],[p3424,p2698]) ).
cnf(p3431,plain,
rselect_head(queue_179) = index_279,
inference(superposition,[status(thm)],[p3426,c7]) ).
cnf(f329,hypothesis,
q35 = queue_175,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp313) ).
fof(f329_nnf,plain,
q35 = queue_175,
inference(nnf_transformation,[status(thm)],[f329]) ).
cnf(c329,plain,
q35 = queue_175,
inference(cnf_transformation,[status(esa)],[f329_nnf]) ).
cnf(f236,hypothesis,
queue_175 = rstore_tail(queue_173,index_174),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp220) ).
fof(f236_nnf,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(nnf_transformation,[status(thm)],[f236]) ).
cnf(c236,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(cnf_transformation,[status(esa)],[f236_nnf]) ).
cnf(p800,plain,
rselect_head(queue_175) = rselect_head(queue_173),
inference(superposition,[status(thm)],[c236,c7]) ).
cnf(p2568,plain,
rselect_head(q35) = rselect_head(q34),
inference(superposition,[status(thm)],[c329,p800]) ).
cnf(f237,hypothesis,
queue_179 = rstore_seq(q35,earray_178),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp221) ).
fof(f237_nnf,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(nnf_transformation,[status(thm)],[f237]) ).
cnf(c237,plain,
queue_179 = rstore_seq(q35,earray_178),
inference(cnf_transformation,[status(esa)],[f237_nnf]) ).
cnf(p806,plain,
rselect_head(queue_179) = rselect_head(q35),
inference(superposition,[status(thm)],[c237,c8]) ).
cnf(p2569,plain,
rselect_head(queue_179) = rselect_head(q34),
inference(demodulation,[status(thm)],[p2568,p806]) ).
cnf(p3433,plain,
index_279 = rselect_head(q34),
inference(demodulation,[status(thm)],[p3431,p2569]) ).
cnf(p3437,plain,
rselect_head(q34) = index_279,
inference(superposition,[status(thm)],[p3433,c7]) ).
cnf(f328,hypothesis,
q34 = queue_169,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp312) ).
fof(f328_nnf,plain,
q34 = queue_169,
inference(nnf_transformation,[status(thm)],[f328]) ).
cnf(c328,plain,
q34 = queue_169,
inference(cnf_transformation,[status(esa)],[f328_nnf]) ).
cnf(f233,hypothesis,
queue_169 = rstore_tail(queue_167,index_168),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp217) ).
fof(f233_nnf,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(nnf_transformation,[status(thm)],[f233]) ).
cnf(c233,plain,
queue_169 = rstore_tail(queue_167,index_168),
inference(cnf_transformation,[status(esa)],[f233_nnf]) ).
cnf(p782,plain,
rselect_head(queue_169) = rselect_head(queue_167),
inference(superposition,[status(thm)],[c233,c7]) ).
cnf(p2511,plain,
rselect_head(q34) = rselect_head(queue_167),
inference(superposition,[status(thm)],[c328,p782]) ).
cnf(p3439,plain,
index_279 = rselect_head(queue_167),
inference(demodulation,[status(thm)],[p3437,p2511]) ).
cnf(p3443,plain,
rselect_head(queue_167) = index_279,
inference(superposition,[status(thm)],[p3439,c7]) ).
cnf(f327,hypothesis,
q33 = queue_163,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp311) ).
fof(f327_nnf,plain,
q33 = queue_163,
inference(nnf_transformation,[status(thm)],[f327]) ).
cnf(c327,plain,
q33 = queue_163,
inference(cnf_transformation,[status(esa)],[f327_nnf]) ).
cnf(f231,hypothesis,
queue_163 = rstore_tail(queue_161,index_162),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp215) ).
fof(f231_nnf,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(nnf_transformation,[status(thm)],[f231]) ).
cnf(c231,plain,
queue_163 = rstore_tail(queue_161,index_162),
inference(cnf_transformation,[status(esa)],[f231_nnf]) ).
cnf(p769,plain,
rselect_head(queue_163) = rselect_head(queue_161),
inference(superposition,[status(thm)],[c231,c7]) ).
cnf(p2504,plain,
rselect_head(q33) = rselect_head(q32),
inference(superposition,[status(thm)],[c327,p769]) ).
cnf(f232,hypothesis,
queue_167 = rstore_seq(q33,earray_166),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp216) ).
fof(f232_nnf,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(nnf_transformation,[status(thm)],[f232]) ).
cnf(c232,plain,
queue_167 = rstore_seq(q33,earray_166),
inference(cnf_transformation,[status(esa)],[f232_nnf]) ).
cnf(p775,plain,
rselect_head(queue_167) = rselect_head(q33),
inference(superposition,[status(thm)],[c232,c8]) ).
cnf(p2505,plain,
rselect_head(queue_167) = rselect_head(q32),
inference(demodulation,[status(thm)],[p2504,p775]) ).
cnf(p3445,plain,
index_279 = rselect_head(q32),
inference(demodulation,[status(thm)],[p3443,p2505]) ).
cnf(p3448,plain,
rselect_head(q32) = index_279,
inference(superposition,[status(thm)],[p3445,c7]) ).
cnf(f326,hypothesis,
q32 = queue_157,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp310) ).
fof(f326_nnf,plain,
q32 = queue_157,
inference(nnf_transformation,[status(thm)],[f326]) ).
cnf(c326,plain,
q32 = queue_157,
inference(cnf_transformation,[status(esa)],[f326_nnf]) ).
cnf(f229,hypothesis,
queue_157 = rstore_tail(queue_155,index_156),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp213) ).
fof(f229_nnf,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(nnf_transformation,[status(thm)],[f229]) ).
cnf(c229,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(cnf_transformation,[status(esa)],[f229_nnf]) ).
cnf(p758,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c229,c7]) ).
cnf(p2496,plain,
rselect_head(q32) = rselect_head(queue_155),
inference(superposition,[status(thm)],[c326,p758]) ).
cnf(p3450,plain,
index_279 = rselect_head(queue_155),
inference(demodulation,[status(thm)],[p3448,p2496]) ).
cnf(p3454,plain,
rselect_head(queue_155) = index_279,
inference(superposition,[status(thm)],[p3450,c7]) ).
cnf(f325,hypothesis,
q31 = queue_151,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp309) ).
fof(f325_nnf,plain,
q31 = queue_151,
inference(nnf_transformation,[status(thm)],[f325]) ).
cnf(c325,plain,
q31 = queue_151,
inference(cnf_transformation,[status(esa)],[f325_nnf]) ).
cnf(f227,hypothesis,
queue_151 = rstore_tail(queue_149,index_150),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp211) ).
fof(f227_nnf,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(nnf_transformation,[status(thm)],[f227]) ).
cnf(c227,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(cnf_transformation,[status(esa)],[f227_nnf]) ).
cnf(p745,plain,
rselect_head(queue_151) = rselect_head(queue_149),
inference(superposition,[status(thm)],[c227,c7]) ).
cnf(p2459,plain,
rselect_head(q31) = rselect_head(q30),
inference(superposition,[status(thm)],[c325,p745]) ).
cnf(f228,hypothesis,
queue_155 = rstore_seq(q31,earray_154),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp212) ).
fof(f228_nnf,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(nnf_transformation,[status(thm)],[f228]) ).
cnf(c228,plain,
queue_155 = rstore_seq(q31,earray_154),
inference(cnf_transformation,[status(esa)],[f228_nnf]) ).
cnf(p751,plain,
rselect_head(queue_155) = rselect_head(q31),
inference(superposition,[status(thm)],[c228,c8]) ).
cnf(p2460,plain,
rselect_head(queue_155) = rselect_head(q30),
inference(demodulation,[status(thm)],[p2459,p751]) ).
cnf(p3455,plain,
index_279 = rselect_head(q30),
inference(demodulation,[status(thm)],[p3454,p2460]) ).
cnf(p3459,plain,
rselect_head(q30) = index_279,
inference(superposition,[status(thm)],[p3455,c7]) ).
cnf(f324,hypothesis,
q30 = queue_145,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp308) ).
fof(f324_nnf,plain,
q30 = queue_145,
inference(nnf_transformation,[status(thm)],[f324]) ).
cnf(c324,plain,
q30 = queue_145,
inference(cnf_transformation,[status(esa)],[f324_nnf]) ).
cnf(f225,hypothesis,
queue_145 = rstore_tail(queue_143,index_144),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp209) ).
fof(f225_nnf,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(nnf_transformation,[status(thm)],[f225]) ).
cnf(c225,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(cnf_transformation,[status(esa)],[f225_nnf]) ).
cnf(p732,plain,
rselect_head(queue_145) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c225,c7]) ).
cnf(p2428,plain,
rselect_head(q30) = rselect_head(queue_143),
inference(superposition,[status(thm)],[c324,p732]) ).
cnf(p3461,plain,
index_279 = rselect_head(queue_143),
inference(demodulation,[status(thm)],[p3459,p2428]) ).
cnf(p3463,plain,
rselect_head(queue_143) = index_279,
inference(superposition,[status(thm)],[p3461,c7]) ).
cnf(f322,hypothesis,
q29 = queue_133,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp306) ).
fof(f322_nnf,plain,
q29 = queue_133,
inference(nnf_transformation,[status(thm)],[f322]) ).
cnf(c322,plain,
q29 = queue_133,
inference(cnf_transformation,[status(esa)],[f322_nnf]) ).
cnf(f221,hypothesis,
queue_133 = rstore_tail(queue_131,index_132),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp205) ).
fof(f221_nnf,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(nnf_transformation,[status(thm)],[f221]) ).
cnf(c221,plain,
queue_133 = rstore_tail(queue_131,index_132),
inference(cnf_transformation,[status(esa)],[f221_nnf]) ).
cnf(p708,plain,
rselect_head(queue_133) = rselect_head(queue_131),
inference(superposition,[status(thm)],[c221,c7]) ).
cnf(p2393,plain,
rselect_head(q29) = rselect_head(q28),
inference(superposition,[status(thm)],[c322,p708]) ).
cnf(f224,hypothesis,
queue_143 = rstore_seq(q29,earray_142),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp208) ).
fof(f224_nnf,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(nnf_transformation,[status(thm)],[f224]) ).
cnf(c224,plain,
queue_143 = rstore_seq(q29,earray_142),
inference(cnf_transformation,[status(esa)],[f224_nnf]) ).
cnf(p725,plain,
rselect_head(queue_143) = rselect_head(q29),
inference(superposition,[status(thm)],[c224,c8]) ).
cnf(p2394,plain,
rselect_head(queue_143) = rselect_head(q28),
inference(demodulation,[status(thm)],[p2393,p725]) ).
cnf(p3465,plain,
index_279 = rselect_head(q28),
inference(demodulation,[status(thm)],[p3463,p2394]) ).
cnf(p3469,plain,
rselect_head(q28) = index_279,
inference(superposition,[status(thm)],[p3465,c7]) ).
cnf(f321,hypothesis,
q28 = queue_127,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp305) ).
fof(f321_nnf,plain,
q28 = queue_127,
inference(nnf_transformation,[status(thm)],[f321]) ).
cnf(c321,plain,
q28 = queue_127,
inference(cnf_transformation,[status(esa)],[f321_nnf]) ).
cnf(f218,hypothesis,
queue_127 = rstore_tail(queue_125,index_126),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp202) ).
fof(f218_nnf,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(nnf_transformation,[status(thm)],[f218]) ).
cnf(c218,plain,
queue_127 = rstore_tail(queue_125,index_126),
inference(cnf_transformation,[status(esa)],[f218_nnf]) ).
cnf(p689,plain,
rselect_head(queue_127) = rselect_head(queue_125),
inference(superposition,[status(thm)],[c218,c7]) ).
cnf(p2331,plain,
rselect_head(q28) = rselect_head(queue_125),
inference(superposition,[status(thm)],[c321,p689]) ).
cnf(p3471,plain,
index_279 = rselect_head(queue_125),
inference(demodulation,[status(thm)],[p3469,p2331]) ).
cnf(p3475,plain,
rselect_head(queue_125) = index_279,
inference(superposition,[status(thm)],[p3471,c7]) ).
cnf(f320,hypothesis,
q27 = queue_121,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp304) ).
fof(f320_nnf,plain,
q27 = queue_121,
inference(nnf_transformation,[status(thm)],[f320]) ).
cnf(c320,plain,
q27 = queue_121,
inference(cnf_transformation,[status(esa)],[f320_nnf]) ).
cnf(f216,hypothesis,
queue_121 = rstore_tail(queue_119,index_120),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp200) ).
fof(f216_nnf,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(nnf_transformation,[status(thm)],[f216]) ).
cnf(c216,plain,
queue_121 = rstore_tail(queue_119,index_120),
inference(cnf_transformation,[status(esa)],[f216_nnf]) ).
cnf(p676,plain,
rselect_head(queue_121) = rselect_head(queue_119),
inference(superposition,[status(thm)],[c216,c7]) ).
cnf(p2299,plain,
rselect_head(q27) = rselect_head(q26),
inference(superposition,[status(thm)],[c320,p676]) ).
cnf(f217,hypothesis,
queue_125 = rstore_seq(q27,earray_124),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp201) ).
fof(f217_nnf,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(nnf_transformation,[status(thm)],[f217]) ).
cnf(c217,plain,
queue_125 = rstore_seq(q27,earray_124),
inference(cnf_transformation,[status(esa)],[f217_nnf]) ).
cnf(p682,plain,
rselect_head(queue_125) = rselect_head(q27),
inference(superposition,[status(thm)],[c217,c8]) ).
cnf(p2300,plain,
rselect_head(queue_125) = rselect_head(q26),
inference(demodulation,[status(thm)],[p2299,p682]) ).
cnf(p3476,plain,
index_279 = rselect_head(q26),
inference(demodulation,[status(thm)],[p3475,p2300]) ).
cnf(p3477,plain,
rselect_head(q26) = index_279,
inference(superposition,[status(thm)],[p3476,c7]) ).
cnf(f319,hypothesis,
q26 = queue_115,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp303) ).
fof(f319_nnf,plain,
q26 = queue_115,
inference(nnf_transformation,[status(thm)],[f319]) ).
cnf(c319,plain,
q26 = queue_115,
inference(cnf_transformation,[status(esa)],[f319_nnf]) ).
cnf(f214,hypothesis,
queue_115 = rstore_tail(queue_113,index_114),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp198) ).
fof(f214_nnf,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(nnf_transformation,[status(thm)],[f214]) ).
cnf(c214,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(cnf_transformation,[status(esa)],[f214_nnf]) ).
cnf(p667,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c214,c7]) ).
cnf(p2252,plain,
rselect_head(q26) = rselect_head(queue_113),
inference(superposition,[status(thm)],[c319,p667]) ).
cnf(p3479,plain,
index_279 = rselect_head(queue_113),
inference(demodulation,[status(thm)],[p3477,p2252]) ).
cnf(p3483,plain,
rselect_head(queue_113) = index_279,
inference(superposition,[status(thm)],[p3479,c7]) ).
cnf(f318,hypothesis,
q25 = queue_109,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp302) ).
fof(f318_nnf,plain,
q25 = queue_109,
inference(nnf_transformation,[status(thm)],[f318]) ).
cnf(c318,plain,
q25 = queue_109,
inference(cnf_transformation,[status(esa)],[f318_nnf]) ).
cnf(f211,hypothesis,
queue_109 = rstore_tail(queue_107,index_108),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp195) ).
fof(f211_nnf,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(nnf_transformation,[status(thm)],[f211]) ).
cnf(c211,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(cnf_transformation,[status(esa)],[f211_nnf]) ).
cnf(p657,plain,
rselect_head(queue_109) = rselect_head(queue_107),
inference(superposition,[status(thm)],[c211,c7]) ).
cnf(p2218,plain,
rselect_head(q25) = rselect_head(q24),
inference(superposition,[status(thm)],[c318,p657]) ).
cnf(f213,hypothesis,
queue_113 = rstore_seq(q25,earray_112),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp197) ).
fof(f213_nnf,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(nnf_transformation,[status(thm)],[f213]) ).
cnf(c213,plain,
queue_113 = rstore_seq(q25,earray_112),
inference(cnf_transformation,[status(esa)],[f213_nnf]) ).
cnf(p662,plain,
rselect_head(queue_113) = rselect_head(q25),
inference(superposition,[status(thm)],[c213,c8]) ).
cnf(p2219,plain,
rselect_head(queue_113) = rselect_head(q24),
inference(demodulation,[status(thm)],[p2218,p662]) ).
cnf(p3484,plain,
index_279 = rselect_head(q24),
inference(demodulation,[status(thm)],[p3483,p2219]) ).
cnf(p3485,plain,
rselect_head(q24) = index_279,
inference(superposition,[status(thm)],[p3484,c7]) ).
cnf(f316,hypothesis,
q23 = queue_97,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp300) ).
fof(f316_nnf,plain,
q23 = queue_97,
inference(nnf_transformation,[status(thm)],[f316]) ).
cnf(c316,plain,
q23 = queue_97,
inference(cnf_transformation,[status(esa)],[f316_nnf]) ).
cnf(f299,hypothesis,
queue_97 = rstore_tail(queue_95,index_96),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp283) ).
fof(f299_nnf,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(nnf_transformation,[status(thm)],[f299]) ).
cnf(c299,plain,
queue_97 = rstore_tail(queue_95,index_96),
inference(cnf_transformation,[status(esa)],[f299_nnf]) ).
cnf(p1257,plain,
rselect_head(queue_97) = rselect_head(queue_95),
inference(superposition,[status(thm)],[c299,c7]) ).
cnf(p3369,plain,
rselect_head(q23) = rselect_head(q22),
inference(superposition,[status(thm)],[c316,p1257]) ).
cnf(f317,hypothesis,
q24 = queue_103,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp301) ).
fof(f317_nnf,plain,
q24 = queue_103,
inference(nnf_transformation,[status(thm)],[f317]) ).
cnf(c317,plain,
q24 = queue_103,
inference(cnf_transformation,[status(esa)],[f317_nnf]) ).
cnf(f209,hypothesis,
queue_103 = rstore_tail(queue_101,index_102),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp193) ).
fof(f209_nnf,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(nnf_transformation,[status(thm)],[f209]) ).
cnf(c209,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(cnf_transformation,[status(esa)],[f209_nnf]) ).
cnf(p650,plain,
rselect_head(queue_103) = rselect_head(queue_101),
inference(superposition,[status(thm)],[c209,c7]) ).
cnf(p2175,plain,
rselect_head(q24) = rselect_head(q23),
inference(superposition,[status(thm)],[c317,p650]) ).
cnf(p3371,plain,
rselect_head(q24) = rselect_head(q22),
inference(demodulation,[status(thm)],[p3369,p2175]) ).
cnf(p3488,plain,
index_279 = rselect_head(q22),
inference(demodulation,[status(thm)],[p3485,p3371]) ).
cnf(p3490,plain,
rselect_head(q22) = index_279,
inference(superposition,[status(thm)],[p3488,c7]) ).
cnf(f315,hypothesis,
q22 = queue_91,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp299) ).
fof(f315_nnf,plain,
q22 = queue_91,
inference(nnf_transformation,[status(thm)],[f315]) ).
cnf(c315,plain,
q22 = queue_91,
inference(cnf_transformation,[status(esa)],[f315_nnf]) ).
cnf(f297,hypothesis,
queue_91 = rstore_tail(queue_89,index_90),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp281) ).
fof(f297_nnf,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(nnf_transformation,[status(thm)],[f297]) ).
cnf(c297,plain,
queue_91 = rstore_tail(queue_89,index_90),
inference(cnf_transformation,[status(esa)],[f297_nnf]) ).
cnf(p1241,plain,
rselect_head(queue_91) = rselect_head(queue_89),
inference(superposition,[status(thm)],[c297,c7]) ).
cnf(p3356,plain,
rselect_head(q22) = rselect_head(queue_89),
inference(superposition,[status(thm)],[c315,p1241]) ).
cnf(p3492,plain,
index_279 = rselect_head(queue_89),
inference(demodulation,[status(thm)],[p3490,p3356]) ).
cnf(p3495,plain,
rselect_head(queue_89) = index_279,
inference(superposition,[status(thm)],[p3492,c7]) ).
cnf(f314,hypothesis,
q21 = queue_85,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp298) ).
fof(f314_nnf,plain,
q21 = queue_85,
inference(nnf_transformation,[status(thm)],[f314]) ).
cnf(c314,plain,
q21 = queue_85,
inference(cnf_transformation,[status(esa)],[f314_nnf]) ).
cnf(f295,hypothesis,
queue_85 = rstore_tail(queue_83,index_84),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp279) ).
fof(f295_nnf,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(nnf_transformation,[status(thm)],[f295]) ).
cnf(c295,plain,
queue_85 = rstore_tail(queue_83,index_84),
inference(cnf_transformation,[status(esa)],[f295_nnf]) ).
cnf(p1225,plain,
rselect_head(queue_85) = rselect_head(queue_83),
inference(superposition,[status(thm)],[c295,c7]) ).
cnf(p3348,plain,
rselect_head(q21) = rselect_head(q20),
inference(superposition,[status(thm)],[c314,p1225]) ).
cnf(f296,hypothesis,
queue_89 = rstore_seq(q21,earray_88),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp280) ).
fof(f296_nnf,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(nnf_transformation,[status(thm)],[f296]) ).
cnf(c296,plain,
queue_89 = rstore_seq(q21,earray_88),
inference(cnf_transformation,[status(esa)],[f296_nnf]) ).
cnf(p1236,plain,
rselect_head(queue_89) = rselect_head(q21),
inference(superposition,[status(thm)],[c296,c8]) ).
cnf(p3349,plain,
rselect_head(queue_89) = rselect_head(q20),
inference(demodulation,[status(thm)],[p3348,p1236]) ).
cnf(p3497,plain,
index_279 = rselect_head(q20),
inference(demodulation,[status(thm)],[p3495,p3349]) ).
cnf(p3500,plain,
rselect_head(q20) = index_279,
inference(superposition,[status(thm)],[p3497,c7]) ).
cnf(f313,hypothesis,
q20 = queue_79,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp297) ).
fof(f313_nnf,plain,
q20 = queue_79,
inference(nnf_transformation,[status(thm)],[f313]) ).
cnf(c313,plain,
q20 = queue_79,
inference(cnf_transformation,[status(esa)],[f313_nnf]) ).
cnf(f293,hypothesis,
queue_79 = rstore_tail(queue_77,index_78),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp277) ).
fof(f293_nnf,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(nnf_transformation,[status(thm)],[f293]) ).
cnf(c293,plain,
queue_79 = rstore_tail(queue_77,index_78),
inference(cnf_transformation,[status(esa)],[f293_nnf]) ).
cnf(p1210,plain,
rselect_head(queue_79) = rselect_head(queue_77),
inference(superposition,[status(thm)],[c293,c7]) ).
cnf(p3341,plain,
rselect_head(q20) = rselect_head(queue_77),
inference(superposition,[status(thm)],[c313,p1210]) ).
cnf(p3502,plain,
index_279 = rselect_head(queue_77),
inference(demodulation,[status(thm)],[p3500,p3341]) ).
cnf(p3506,plain,
rselect_head(queue_77) = index_279,
inference(superposition,[status(thm)],[p3502,c7]) ).
cnf(f311,hypothesis,
q19 = queue_67,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp295) ).
fof(f311_nnf,plain,
q19 = queue_67,
inference(nnf_transformation,[status(thm)],[f311]) ).
cnf(c311,plain,
q19 = queue_67,
inference(cnf_transformation,[status(esa)],[f311_nnf]) ).
cnf(f288,hypothesis,
queue_67 = rstore_tail(queue_65,index_66),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp272) ).
fof(f288_nnf,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(nnf_transformation,[status(thm)],[f288]) ).
cnf(c288,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(cnf_transformation,[status(esa)],[f288_nnf]) ).
cnf(p1174,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(superposition,[status(thm)],[c288,c7]) ).
cnf(p3314,plain,
rselect_head(q19) = rselect_head(q18),
inference(superposition,[status(thm)],[c311,p1174]) ).
cnf(f292,hypothesis,
queue_77 = rstore_seq(q19,earray_76),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp276) ).
fof(f292_nnf,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(nnf_transformation,[status(thm)],[f292]) ).
cnf(c292,plain,
queue_77 = rstore_seq(q19,earray_76),
inference(cnf_transformation,[status(esa)],[f292_nnf]) ).
cnf(p1204,plain,
rselect_head(queue_77) = rselect_head(q19),
inference(superposition,[status(thm)],[c292,c8]) ).
cnf(p3315,plain,
rselect_head(queue_77) = rselect_head(q18),
inference(demodulation,[status(thm)],[p3314,p1204]) ).
cnf(p3508,plain,
index_279 = rselect_head(q18),
inference(demodulation,[status(thm)],[p3506,p3315]) ).
cnf(p3512,plain,
rselect_head(q18) = index_279,
inference(superposition,[status(thm)],[p3508,c7]) ).
cnf(f310,hypothesis,
q18 = queue_61,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp294) ).
fof(f310_nnf,plain,
q18 = queue_61,
inference(nnf_transformation,[status(thm)],[f310]) ).
cnf(c310,plain,
q18 = queue_61,
inference(cnf_transformation,[status(esa)],[f310_nnf]) ).
cnf(f286,hypothesis,
queue_61 = rstore_tail(queue_59,index_60),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp270) ).
fof(f286_nnf,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(nnf_transformation,[status(thm)],[f286]) ).
cnf(c286,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(cnf_transformation,[status(esa)],[f286_nnf]) ).
cnf(p1166,plain,
rselect_head(queue_61) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c286,c7]) ).
cnf(p3308,plain,
rselect_head(q18) = rselect_head(queue_59),
inference(superposition,[status(thm)],[c310,p1166]) ).
cnf(p3514,plain,
index_279 = rselect_head(queue_59),
inference(demodulation,[status(thm)],[p3512,p3308]) ).
cnf(p3518,plain,
rselect_head(queue_59) = index_279,
inference(superposition,[status(thm)],[p3514,c7]) ).
cnf(f309,hypothesis,
q17 = queue_55,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp293) ).
fof(f309_nnf,plain,
q17 = queue_55,
inference(nnf_transformation,[status(thm)],[f309]) ).
cnf(c309,plain,
q17 = queue_55,
inference(cnf_transformation,[status(esa)],[f309_nnf]) ).
cnf(f284,hypothesis,
queue_55 = rstore_tail(queue_53,index_54),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp268) ).
fof(f284_nnf,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(nnf_transformation,[status(thm)],[f284]) ).
cnf(c284,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(cnf_transformation,[status(esa)],[f284_nnf]) ).
cnf(p1141,plain,
rselect_head(queue_55) = rselect_head(queue_53),
inference(superposition,[status(thm)],[c284,c7]) ).
cnf(p3301,plain,
rselect_head(q17) = rselect_head(q16),
inference(superposition,[status(thm)],[c309,p1141]) ).
cnf(f285,hypothesis,
queue_59 = rstore_seq(q17,earray_58),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp269) ).
fof(f285_nnf,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(nnf_transformation,[status(thm)],[f285]) ).
cnf(c285,plain,
queue_59 = rstore_seq(q17,earray_58),
inference(cnf_transformation,[status(esa)],[f285_nnf]) ).
cnf(p1152,plain,
rselect_head(queue_59) = rselect_head(q17),
inference(superposition,[status(thm)],[c285,c8]) ).
cnf(p3302,plain,
rselect_head(queue_59) = rselect_head(q16),
inference(demodulation,[status(thm)],[p3301,p1152]) ).
cnf(p3520,plain,
index_279 = rselect_head(q16),
inference(demodulation,[status(thm)],[p3518,p3302]) ).
cnf(p3523,plain,
rselect_head(q16) = index_279,
inference(superposition,[status(thm)],[p3520,c7]) ).
cnf(f308,hypothesis,
q16 = queue_49,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp292) ).
fof(f308_nnf,plain,
q16 = queue_49,
inference(nnf_transformation,[status(thm)],[f308]) ).
cnf(c308,plain,
q16 = queue_49,
inference(cnf_transformation,[status(esa)],[f308_nnf]) ).
cnf(f281,hypothesis,
queue_49 = rstore_tail(queue_47,index_48),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp265) ).
fof(f281_nnf,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(nnf_transformation,[status(thm)],[f281]) ).
cnf(c281,plain,
queue_49 = rstore_tail(queue_47,index_48),
inference(cnf_transformation,[status(esa)],[f281_nnf]) ).
cnf(p1122,plain,
rselect_head(queue_49) = rselect_head(queue_47),
inference(superposition,[status(thm)],[c281,c7]) ).
cnf(p3295,plain,
rselect_head(q16) = rselect_head(queue_47),
inference(superposition,[status(thm)],[c308,p1122]) ).
cnf(p3525,plain,
index_279 = rselect_head(queue_47),
inference(demodulation,[status(thm)],[p3523,p3295]) ).
cnf(p3527,plain,
rselect_head(queue_47) = index_279,
inference(superposition,[status(thm)],[p3525,c7]) ).
cnf(f307,hypothesis,
q15 = queue_43,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp291) ).
fof(f307_nnf,plain,
q15 = queue_43,
inference(nnf_transformation,[status(thm)],[f307]) ).
cnf(c307,plain,
q15 = queue_43,
inference(cnf_transformation,[status(esa)],[f307_nnf]) ).
cnf(f279,hypothesis,
queue_43 = rstore_tail(queue_41,index_42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp263) ).
fof(f279_nnf,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(nnf_transformation,[status(thm)],[f279]) ).
cnf(c279,plain,
queue_43 = rstore_tail(queue_41,index_42),
inference(cnf_transformation,[status(esa)],[f279_nnf]) ).
cnf(p1106,plain,
rselect_head(queue_43) = rselect_head(queue_41),
inference(superposition,[status(thm)],[c279,c7]) ).
cnf(p3287,plain,
rselect_head(q15) = rselect_head(q14),
inference(superposition,[status(thm)],[c307,p1106]) ).
cnf(f280,hypothesis,
queue_47 = rstore_seq(q15,earray_46),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp264) ).
fof(f280_nnf,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(nnf_transformation,[status(thm)],[f280]) ).
cnf(c280,plain,
queue_47 = rstore_seq(q15,earray_46),
inference(cnf_transformation,[status(esa)],[f280_nnf]) ).
cnf(p1117,plain,
rselect_head(queue_47) = rselect_head(q15),
inference(superposition,[status(thm)],[c280,c8]) ).
cnf(p3288,plain,
rselect_head(queue_47) = rselect_head(q14),
inference(demodulation,[status(thm)],[p3287,p1117]) ).
cnf(p3528,plain,
index_279 = rselect_head(q14),
inference(demodulation,[status(thm)],[p3527,p3288]) ).
cnf(p3532,plain,
rselect_head(q14) = index_279,
inference(superposition,[status(thm)],[p3528,c7]) ).
cnf(f306,hypothesis,
q14 = queue_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp290) ).
fof(f306_nnf,plain,
q14 = queue_37,
inference(nnf_transformation,[status(thm)],[f306]) ).
cnf(c306,plain,
q14 = queue_37,
inference(cnf_transformation,[status(esa)],[f306_nnf]) ).
cnf(f277,hypothesis,
queue_37 = rstore_tail(queue_35,index_36),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp261) ).
fof(f277_nnf,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(nnf_transformation,[status(thm)],[f277]) ).
cnf(c277,plain,
queue_37 = rstore_tail(queue_35,index_36),
inference(cnf_transformation,[status(esa)],[f277_nnf]) ).
cnf(p1099,plain,
rselect_head(queue_37) = rselect_head(queue_35),
inference(superposition,[status(thm)],[c277,c7]) ).
cnf(p3219,plain,
rselect_head(q14) = rselect_head(queue_35),
inference(superposition,[status(thm)],[c306,p1099]) ).
cnf(p3534,plain,
index_279 = rselect_head(queue_35),
inference(demodulation,[status(thm)],[p3532,p3219]) ).
cnf(p3538,plain,
rselect_head(queue_35) = index_279,
inference(superposition,[status(thm)],[p3534,c7]) ).
cnf(f305,hypothesis,
q13 = queue_31,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp289) ).
fof(f305_nnf,plain,
q13 = queue_31,
inference(nnf_transformation,[status(thm)],[f305]) ).
cnf(c305,plain,
q13 = queue_31,
inference(cnf_transformation,[status(esa)],[f305_nnf]) ).
cnf(f275,hypothesis,
queue_31 = rstore_tail(queue_29,index_30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp259) ).
fof(f275_nnf,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(nnf_transformation,[status(thm)],[f275]) ).
cnf(c275,plain,
queue_31 = rstore_tail(queue_29,index_30),
inference(cnf_transformation,[status(esa)],[f275_nnf]) ).
cnf(p1083,plain,
rselect_head(queue_31) = rselect_head(queue_29),
inference(superposition,[status(thm)],[c275,c7]) ).
cnf(p3212,plain,
rselect_head(q13) = rselect_head(q12),
inference(superposition,[status(thm)],[c305,p1083]) ).
cnf(f276,hypothesis,
queue_35 = rstore_seq(q13,earray_34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp260) ).
fof(f276_nnf,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(nnf_transformation,[status(thm)],[f276]) ).
cnf(c276,plain,
queue_35 = rstore_seq(q13,earray_34),
inference(cnf_transformation,[status(esa)],[f276_nnf]) ).
cnf(p1085,plain,
rselect_head(queue_35) = rselect_head(q13),
inference(superposition,[status(thm)],[c276,c8]) ).
cnf(p3213,plain,
rselect_head(queue_35) = rselect_head(q12),
inference(demodulation,[status(thm)],[p3212,p1085]) ).
cnf(p3540,plain,
index_279 = rselect_head(q12),
inference(demodulation,[status(thm)],[p3538,p3213]) ).
cnf(p3544,plain,
rselect_head(q12) = index_279,
inference(superposition,[status(thm)],[p3540,c7]) ).
cnf(f304,hypothesis,
q12 = queue_25,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp288) ).
fof(f304_nnf,plain,
q12 = queue_25,
inference(nnf_transformation,[status(thm)],[f304]) ).
cnf(c304,plain,
q12 = queue_25,
inference(cnf_transformation,[status(esa)],[f304_nnf]) ).
cnf(f263,hypothesis,
queue_25 = rstore_tail(queue_23,index_24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp247) ).
fof(f263_nnf,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(nnf_transformation,[status(thm)],[f263]) ).
cnf(c263,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(cnf_transformation,[status(esa)],[f263_nnf]) ).
cnf(p996,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c263,c7]) ).
cnf(p2906,plain,
rselect_head(q12) = rselect_head(queue_23),
inference(superposition,[status(thm)],[c304,p996]) ).
cnf(p3546,plain,
index_279 = rselect_head(queue_23),
inference(demodulation,[status(thm)],[p3544,p2906]) ).
cnf(p3548,plain,
rselect_head(queue_23) = index_279,
inference(superposition,[status(thm)],[p3546,c7]) ).
cnf(f303,hypothesis,
q11 = queue_19,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp287) ).
fof(f303_nnf,plain,
q11 = queue_19,
inference(nnf_transformation,[status(thm)],[f303]) ).
cnf(c303,plain,
q11 = queue_19,
inference(cnf_transformation,[status(esa)],[f303_nnf]) ).
cnf(f241,hypothesis,
queue_19 = rstore_tail(queue_17,index_18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp225) ).
fof(f241_nnf,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(nnf_transformation,[status(thm)],[f241]) ).
cnf(c241,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(cnf_transformation,[status(esa)],[f241_nnf]) ).
cnf(p829,plain,
rselect_head(queue_19) = rselect_head(queue_17),
inference(superposition,[status(thm)],[c241,c7]) ).
cnf(p2711,plain,
rselect_head(q11) = rselect_head(q10),
inference(superposition,[status(thm)],[c303,p829]) ).
cnf(f256,hypothesis,
queue_23 = rstore_seq(q11,earray_22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp240) ).
fof(f256_nnf,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(nnf_transformation,[status(thm)],[f256]) ).
cnf(c256,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(cnf_transformation,[status(esa)],[f256_nnf]) ).
cnf(p934,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(superposition,[status(thm)],[c256,c8]) ).
cnf(p2712,plain,
rselect_head(queue_23) = rselect_head(q10),
inference(demodulation,[status(thm)],[p2711,p934]) ).
cnf(p3549,plain,
index_279 = rselect_head(q10),
inference(demodulation,[status(thm)],[p3548,p2712]) ).
cnf(p3550,plain,
rselect_head(q10) = index_279,
inference(superposition,[status(thm)],[p3549,c7]) ).
cnf(f346,hypothesis,
q9 = queue_277,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp330) ).
fof(f346_nnf,plain,
q9 = queue_277,
inference(nnf_transformation,[status(thm)],[f346]) ).
cnf(c346,plain,
q9 = queue_277,
inference(cnf_transformation,[status(esa)],[f346_nnf]) ).
cnf(f273,hypothesis,
queue_277 = rstore_tail(queue_275,index_276),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp257) ).
fof(f273_nnf,plain,
queue_277 = rstore_tail(queue_275,index_276),
inference(nnf_transformation,[status(thm)],[f273]) ).
cnf(c273,plain,
queue_277 = rstore_tail(queue_275,index_276),
inference(cnf_transformation,[status(esa)],[f273_nnf]) ).
cnf(p1066,plain,
rselect_head(queue_277) = rselect_head(queue_275),
inference(superposition,[status(thm)],[c273,c7]) ).
cnf(p3203,plain,
rselect_head(q9) = rselect_head(q8),
inference(superposition,[status(thm)],[c346,p1066]) ).
cnf(f302,hypothesis,
q10 = queue_13,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp286) ).
fof(f302_nnf,plain,
q10 = queue_13,
inference(nnf_transformation,[status(thm)],[f302]) ).
cnf(c302,plain,
q10 = queue_13,
inference(cnf_transformation,[status(esa)],[f302_nnf]) ).
cnf(f219,hypothesis,
queue_13 = rstore_tail(queue_11,index_12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp203) ).
fof(f219_nnf,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(nnf_transformation,[status(thm)],[f219]) ).
cnf(c219,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(cnf_transformation,[status(esa)],[f219_nnf]) ).
cnf(p697,plain,
rselect_head(queue_13) = rselect_head(queue_11),
inference(superposition,[status(thm)],[c219,c7]) ).
cnf(p2340,plain,
rselect_head(q10) = rselect_head(q9),
inference(superposition,[status(thm)],[c302,p697]) ).
cnf(p3205,plain,
rselect_head(q10) = rselect_head(q8),
inference(demodulation,[status(thm)],[p3203,p2340]) ).
cnf(p3553,plain,
index_279 = rselect_head(q8),
inference(demodulation,[status(thm)],[p3550,p3205]) ).
cnf(p3554,plain,
rselect_head(q8) = index_279,
inference(superposition,[status(thm)],[p3553,c7]) ).
cnf(f345,hypothesis,
q8 = queue_271,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp329) ).
fof(f345_nnf,plain,
q8 = queue_271,
inference(nnf_transformation,[status(thm)],[f345]) ).
cnf(c345,plain,
q8 = queue_271,
inference(cnf_transformation,[status(esa)],[f345_nnf]) ).
cnf(f271,hypothesis,
queue_271 = rstore_tail(queue_269,index_270),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp255) ).
fof(f271_nnf,plain,
queue_271 = rstore_tail(queue_269,index_270),
inference(nnf_transformation,[status(thm)],[f271]) ).
cnf(c271,plain,
queue_271 = rstore_tail(queue_269,index_270),
inference(cnf_transformation,[status(esa)],[f271_nnf]) ).
cnf(p1050,plain,
rselect_head(queue_271) = rselect_head(queue_269),
inference(superposition,[status(thm)],[c271,c7]) ).
cnf(p3047,plain,
rselect_head(q8) = rselect_head(queue_269),
inference(superposition,[status(thm)],[c345,p1050]) ).
cnf(p3556,plain,
index_279 = rselect_head(queue_269),
inference(demodulation,[status(thm)],[p3554,p3047]) ).
cnf(p3562,plain,
rselect_head(queue_269) = index_279,
inference(superposition,[status(thm)],[p3556,c7]) ).
cnf(f344,hypothesis,
q7 = queue_265,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp328) ).
fof(f344_nnf,plain,
q7 = queue_265,
inference(nnf_transformation,[status(thm)],[f344]) ).
cnf(c344,plain,
q7 = queue_265,
inference(cnf_transformation,[status(esa)],[f344_nnf]) ).
cnf(f269,hypothesis,
queue_265 = rstore_tail(queue_263,index_264),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp253) ).
fof(f269_nnf,plain,
queue_265 = rstore_tail(queue_263,index_264),
inference(nnf_transformation,[status(thm)],[f269]) ).
cnf(c269,plain,
queue_265 = rstore_tail(queue_263,index_264),
inference(cnf_transformation,[status(esa)],[f269_nnf]) ).
cnf(p1035,plain,
rselect_head(queue_265) = rselect_head(queue_263),
inference(superposition,[status(thm)],[c269,c7]) ).
cnf(p3022,plain,
rselect_head(q7) = rselect_head(q6),
inference(superposition,[status(thm)],[c344,p1035]) ).
cnf(f270,hypothesis,
queue_269 = rstore_seq(q7,earray_268),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp254) ).
fof(f270_nnf,plain,
queue_269 = rstore_seq(q7,earray_268),
inference(nnf_transformation,[status(thm)],[f270]) ).
cnf(c270,plain,
queue_269 = rstore_seq(q7,earray_268),
inference(cnf_transformation,[status(esa)],[f270_nnf]) ).
cnf(p1046,plain,
rselect_head(queue_269) = rselect_head(q7),
inference(superposition,[status(thm)],[c270,c8]) ).
cnf(p3023,plain,
rselect_head(queue_269) = rselect_head(q6),
inference(demodulation,[status(thm)],[p3022,p1046]) ).
cnf(p3564,plain,
index_279 = rselect_head(q6),
inference(demodulation,[status(thm)],[p3562,p3023]) ).
cnf(p3567,plain,
rselect_head(q6) = index_279,
inference(superposition,[status(thm)],[p3564,c7]) ).
cnf(f343,hypothesis,
q6 = queue_259,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp327) ).
fof(f343_nnf,plain,
q6 = queue_259,
inference(nnf_transformation,[status(thm)],[f343]) ).
cnf(c343,plain,
q6 = queue_259,
inference(cnf_transformation,[status(esa)],[f343_nnf]) ).
cnf(f267,hypothesis,
queue_259 = rstore_tail(queue_257,index_258),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp251) ).
fof(f267_nnf,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(nnf_transformation,[status(thm)],[f267]) ).
cnf(c267,plain,
queue_259 = rstore_tail(queue_257,index_258),
inference(cnf_transformation,[status(esa)],[f267_nnf]) ).
cnf(p1027,plain,
rselect_head(queue_259) = rselect_head(queue_257),
inference(superposition,[status(thm)],[c267,c7]) ).
cnf(p3016,plain,
rselect_head(q6) = rselect_head(queue_257),
inference(superposition,[status(thm)],[c343,p1027]) ).
cnf(p3569,plain,
index_279 = rselect_head(queue_257),
inference(demodulation,[status(thm)],[p3567,p3016]) ).
cnf(p3572,plain,
rselect_head(queue_257) = index_279,
inference(superposition,[status(thm)],[p3569,c7]) ).
cnf(f342,hypothesis,
q5 = queue_253,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp326) ).
fof(f342_nnf,plain,
q5 = queue_253,
inference(nnf_transformation,[status(thm)],[f342]) ).
cnf(c342,plain,
q5 = queue_253,
inference(cnf_transformation,[status(esa)],[f342_nnf]) ).
cnf(f265,hypothesis,
queue_253 = rstore_tail(queue_251,index_252),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp249) ).
fof(f265_nnf,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(nnf_transformation,[status(thm)],[f265]) ).
cnf(c265,plain,
queue_253 = rstore_tail(queue_251,index_252),
inference(cnf_transformation,[status(esa)],[f265_nnf]) ).
cnf(p1011,plain,
rselect_head(queue_253) = rselect_head(queue_251),
inference(superposition,[status(thm)],[c265,c7]) ).
cnf(p3009,plain,
rselect_head(q5) = rselect_head(q4),
inference(superposition,[status(thm)],[c342,p1011]) ).
cnf(f266,hypothesis,
queue_257 = rstore_seq(q5,earray_256),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp250) ).
fof(f266_nnf,plain,
queue_257 = rstore_seq(q5,earray_256),
inference(nnf_transformation,[status(thm)],[f266]) ).
cnf(c266,plain,
queue_257 = rstore_seq(q5,earray_256),
inference(cnf_transformation,[status(esa)],[f266_nnf]) ).
cnf(p1014,plain,
rselect_head(queue_257) = rselect_head(q5),
inference(superposition,[status(thm)],[c266,c8]) ).
cnf(p3010,plain,
rselect_head(queue_257) = rselect_head(q4),
inference(demodulation,[status(thm)],[p3009,p1014]) ).
cnf(p3574,plain,
index_279 = rselect_head(q4),
inference(demodulation,[status(thm)],[p3572,p3010]) ).
cnf(p3575,plain,
rselect_head(q4) = index_279,
inference(superposition,[status(thm)],[p3574,c7]) ).
cnf(f334,hypothesis,
q4 = queue_205,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp318) ).
fof(f334_nnf,plain,
q4 = queue_205,
inference(nnf_transformation,[status(thm)],[f334]) ).
cnf(c334,plain,
q4 = queue_205,
inference(cnf_transformation,[status(esa)],[f334_nnf]) ).
cnf(f247,hypothesis,
queue_205 = rstore_tail(queue_203,index_204),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp231) ).
fof(f247_nnf,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(nnf_transformation,[status(thm)],[f247]) ).
cnf(c247,plain,
queue_205 = rstore_tail(queue_203,index_204),
inference(cnf_transformation,[status(esa)],[f247_nnf]) ).
cnf(p867,plain,
rselect_head(queue_205) = rselect_head(queue_203),
inference(superposition,[status(thm)],[c247,c7]) ).
cnf(p2808,plain,
rselect_head(q4) = rselect_head(queue_203),
inference(superposition,[status(thm)],[c334,p867]) ).
cnf(p3577,plain,
index_279 = rselect_head(queue_203),
inference(demodulation,[status(thm)],[p3575,p2808]) ).
cnf(p3579,plain,
rselect_head(queue_203) = index_279,
inference(superposition,[status(thm)],[p3577,c7]) ).
cnf(f323,hypothesis,
q3 = queue_139,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp307) ).
fof(f323_nnf,plain,
q3 = queue_139,
inference(nnf_transformation,[status(thm)],[f323]) ).
cnf(c323,plain,
q3 = queue_139,
inference(cnf_transformation,[status(esa)],[f323_nnf]) ).
cnf(f223,hypothesis,
queue_139 = rstore_tail(queue_137,index_138),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp207) ).
fof(f223_nnf,plain,
queue_139 = rstore_tail(queue_137,index_138),
inference(nnf_transformation,[status(thm)],[f223]) ).
cnf(c223,plain,
queue_139 = rstore_tail(queue_137,index_138),
inference(cnf_transformation,[status(esa)],[f223_nnf]) ).
cnf(p721,plain,
rselect_head(queue_139) = rselect_head(queue_137),
inference(superposition,[status(thm)],[c223,c7]) ).
cnf(p2422,plain,
rselect_head(q3) = rselect_head(q2),
inference(superposition,[status(thm)],[c323,p721]) ).
cnf(f246,hypothesis,
queue_203 = rstore_seq(q3,earray_202),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp230) ).
fof(f246_nnf,plain,
queue_203 = rstore_seq(q3,earray_202),
inference(nnf_transformation,[status(thm)],[f246]) ).
cnf(c246,plain,
queue_203 = rstore_seq(q3,earray_202),
inference(cnf_transformation,[status(esa)],[f246_nnf]) ).
cnf(p859,plain,
rselect_head(queue_203) = rselect_head(q3),
inference(superposition,[status(thm)],[c246,c8]) ).
cnf(p2423,plain,
rselect_head(queue_203) = rselect_head(q2),
inference(demodulation,[status(thm)],[p2422,p859]) ).
cnf(p3581,plain,
index_279 = rselect_head(q2),
inference(demodulation,[status(thm)],[p3579,p2423]) ).
cnf(p3583,plain,
rselect_head(q2) = index_279,
inference(superposition,[status(thm)],[p3581,c7]) ).
cnf(f312,hypothesis,
q2 = queue_73,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp296) ).
fof(f312_nnf,plain,
q2 = queue_73,
inference(nnf_transformation,[status(thm)],[f312]) ).
cnf(c312,plain,
q2 = queue_73,
inference(cnf_transformation,[status(esa)],[f312_nnf]) ).
cnf(f291,hypothesis,
queue_73 = rstore_tail(queue_71,index_72),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp275) ).
fof(f291_nnf,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(nnf_transformation,[status(thm)],[f291]) ).
cnf(c291,plain,
queue_73 = rstore_tail(queue_71,index_72),
inference(cnf_transformation,[status(esa)],[f291_nnf]) ).
cnf(p1202,plain,
rselect_head(queue_73) = rselect_head(queue_71),
inference(superposition,[status(thm)],[c291,c7]) ).
cnf(p3335,plain,
rselect_head(q2) = rselect_head(queue_71),
inference(superposition,[status(thm)],[c312,p1202]) ).
cnf(p3586,plain,
index_279 = rselect_head(queue_71),
inference(demodulation,[status(thm)],[p3583,p3335]) ).
cnf(p3587,plain,
rselect_head(queue_71) = index_279,
inference(superposition,[status(thm)],[p3586,c7]) ).
cnf(f301,hypothesis,
q1 = queue_7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp285) ).
fof(f301_nnf,plain,
q1 = queue_7,
inference(nnf_transformation,[status(thm)],[f301]) ).
cnf(c301,plain,
q1 = queue_7,
inference(cnf_transformation,[status(esa)],[f301_nnf]) ).
cnf(f289,hypothesis,
queue_7 = rstore_tail(queue_5,index_6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp273) ).
fof(f289_nnf,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(nnf_transformation,[status(thm)],[f289]) ).
cnf(c289,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(cnf_transformation,[status(esa)],[f289_nnf]) ).
cnf(p1186,plain,
rselect_head(queue_7) = rselect_head(queue_5),
inference(superposition,[status(thm)],[c289,c7]) ).
cnf(p3324,plain,
rselect_head(q1) = rselect_head(q0),
inference(superposition,[status(thm)],[c301,p1186]) ).
cnf(f290,hypothesis,
queue_71 = rstore_seq(q1,earray_70),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp274) ).
fof(f290_nnf,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(nnf_transformation,[status(thm)],[f290]) ).
cnf(c290,plain,
queue_71 = rstore_seq(q1,earray_70),
inference(cnf_transformation,[status(esa)],[f290_nnf]) ).
cnf(p1188,plain,
rselect_head(queue_71) = rselect_head(q1),
inference(superposition,[status(thm)],[c290,c8]) ).
cnf(p3325,plain,
rselect_head(queue_71) = rselect_head(q0),
inference(demodulation,[status(thm)],[p3324,p1188]) ).
cnf(p3589,plain,
index_279 = rselect_head(q0),
inference(demodulation,[status(thm)],[p3587,p3325]) ).
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(p1239,plain,
rselect_tail(queue_91) = index_90,
inference(superposition,[status(thm)],[c297,c4]) ).
cnf(p1874,plain,
index_93 = index_90,
inference(superposition,[status(thm)],[c315,p1239]) ).
cnf(f203,hypothesis,
index_90 = s(index_87),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp187) ).
fof(f203_nnf,plain,
index_90 = s(index_87),
inference(nnf_transformation,[status(thm)],[f203]) ).
cnf(c203,plain,
index_90 = s(index_87),
inference(cnf_transformation,[status(esa)],[f203_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(p625,plain,
p(index_90) = index_87,
inference(superposition,[status(thm)],[c203,c11]) ).
cnf(p1876,plain,
p(index_93) = index_87,
inference(superposition,[status(thm)],[p1874,p625]) ).
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(p2575,plain,
index_15 = index_111,
inference(superposition,[status(thm)],[p1876,c12]) ).
cnf(p1064,plain,
rselect_tail(queue_277) = index_276,
inference(superposition,[status(thm)],[c273,c4]) ).
cnf(p1581,plain,
index_9 = index_276,
inference(superposition,[status(thm)],[c346,p1064]) ).
cnf(f176,hypothesis,
index_276 = s(index_273),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp160) ).
fof(f176_nnf,plain,
index_276 = s(index_273),
inference(nnf_transformation,[status(thm)],[f176]) ).
cnf(c176,plain,
index_276 = s(index_273),
inference(cnf_transformation,[status(esa)],[f176_nnf]) ).
cnf(p565,plain,
p(index_276) = index_273,
inference(superposition,[status(thm)],[c176,c11]) ).
cnf(p1583,plain,
p(index_9) = index_273,
inference(superposition,[status(thm)],[p1581,p565]) ).
cnf(p695,plain,
rselect_tail(queue_13) = index_12,
inference(superposition,[status(thm)],[c219,c4]) ).
cnf(p964,plain,
index_15 = index_12,
inference(superposition,[status(thm)],[c302,p695]) ).
cnf(f118,hypothesis,
index_12 = s(index_9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp102) ).
fof(f118_nnf,plain,
index_12 = s(index_9),
inference(nnf_transformation,[status(thm)],[f118]) ).
cnf(c118,plain,
index_12 = s(index_9),
inference(cnf_transformation,[status(esa)],[f118_nnf]) ).
cnf(p434,plain,
p(index_12) = index_9,
inference(superposition,[status(thm)],[c118,c11]) ).
cnf(p684,plain,
s(index_9) = index_12,
inference(superposition,[status(thm)],[p434,c12]) ).
cnf(p969,plain,
index_12 = index_15,
inference(superposition,[status(thm)],[p964,p684]) ).
cnf(p970,plain,
s(index_9) = index_15,
inference(demodulation,[status(thm)],[p969,p684]) ).
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(p364,plain,
s(s(X0)) = p(X0),
inference(superposition,[status(thm)],[c12,c15]) ).
cnf(p1451,plain,
s(index_15) = p(index_9),
inference(superposition,[status(thm)],[p970,p364]) ).
cnf(p1585,plain,
s(index_15) = index_273,
inference(demodulation,[status(thm)],[p1583,p1451]) ).
cnf(p2253,plain,
index_267 = index_15,
inference(superposition,[status(thm)],[p1585,c11]) ).
cnf(p865,plain,
rselect_tail(queue_205) = index_204,
inference(superposition,[status(thm)],[c247,c4]) ).
cnf(p1206,plain,
index_249 = index_204,
inference(superposition,[status(thm)],[c334,p865]) ).
cnf(f149,hypothesis,
index_204 = s(index_201),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp133) ).
fof(f149_nnf,plain,
index_204 = s(index_201),
inference(nnf_transformation,[status(thm)],[f149]) ).
cnf(c149,plain,
index_204 = s(index_201),
inference(cnf_transformation,[status(esa)],[f149_nnf]) ).
cnf(p505,plain,
p(index_204) = index_201,
inference(superposition,[status(thm)],[c149,c11]) ).
cnf(p759,plain,
s(index_201) = index_204,
inference(superposition,[status(thm)],[p505,c12]) ).
cnf(p1215,plain,
index_204 = index_249,
inference(superposition,[status(thm)],[p1206,p759]) ).
cnf(p1216,plain,
s(index_201) = index_249,
inference(demodulation,[status(thm)],[p1215,p759]) ).
cnf(p1828,plain,
s(index_249) = index_135,
inference(superposition,[status(thm)],[p1216,p364]) ).
cnf(p1009,plain,
rselect_tail(queue_253) = index_252,
inference(superposition,[status(thm)],[c265,c4]) ).
cnf(p1517,plain,
index_255 = index_252,
inference(superposition,[status(thm)],[c342,p1009]) ).
cnf(f167,hypothesis,
index_252 = s(index_249),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp151) ).
fof(f167_nnf,plain,
index_252 = s(index_249),
inference(nnf_transformation,[status(thm)],[f167]) ).
cnf(c167,plain,
index_252 = s(index_249),
inference(cnf_transformation,[status(esa)],[f167_nnf]) ).
cnf(p546,plain,
p(index_252) = index_249,
inference(superposition,[status(thm)],[c167,c11]) ).
cnf(p801,plain,
s(index_249) = index_252,
inference(superposition,[status(thm)],[p546,c12]) ).
cnf(p1524,plain,
index_252 = index_255,
inference(superposition,[status(thm)],[p1517,p801]) ).
cnf(p1525,plain,
s(index_249) = index_255,
inference(demodulation,[status(thm)],[p1524,p801]) ).
cnf(p1829,plain,
index_135 = index_255,
inference(demodulation,[status(thm)],[p1828,p1525]) ).
cnf(f168,hypothesis,
index_255 = rselect_tail(q5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp152) ).
fof(f168_nnf,plain,
index_255 = rselect_tail(q5),
inference(nnf_transformation,[status(thm)],[f168]) ).
cnf(c168,plain,
index_255 = rselect_tail(q5),
inference(cnf_transformation,[status(esa)],[f168_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(p548,plain,
rselect_tail(q5) = index_255,
inference(superposition,[status(thm)],[c168,c9]) ).
cnf(p1831,plain,
index_255 = index_135,
inference(superposition,[status(thm)],[p1829,p548]) ).
cnf(p1033,plain,
rselect_tail(queue_265) = index_264,
inference(superposition,[status(thm)],[c269,c4]) ).
cnf(p1547,plain,
index_267 = index_264,
inference(superposition,[status(thm)],[c344,p1033]) ).
cnf(f171,hypothesis,
index_264 = s(index_261),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp155) ).
fof(f171_nnf,plain,
index_264 = s(index_261),
inference(nnf_transformation,[status(thm)],[f171]) ).
cnf(c171,plain,
index_264 = s(index_261),
inference(cnf_transformation,[status(esa)],[f171_nnf]) ).
cnf(p554,plain,
p(index_264) = index_261,
inference(superposition,[status(thm)],[c171,c11]) ).
cnf(p808,plain,
s(index_261) = index_264,
inference(superposition,[status(thm)],[p554,c12]) ).
cnf(p1554,plain,
index_264 = index_267,
inference(superposition,[status(thm)],[p1547,p808]) ).
cnf(p1025,plain,
rselect_tail(queue_259) = index_258,
inference(superposition,[status(thm)],[c267,c4]) ).
cnf(p1532,plain,
index_261 = index_258,
inference(superposition,[status(thm)],[c343,p1025]) ).
cnf(f169,hypothesis,
index_258 = s(index_255),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp153) ).
fof(f169_nnf,plain,
index_258 = s(index_255),
inference(nnf_transformation,[status(thm)],[f169]) ).
cnf(c169,plain,
index_258 = s(index_255),
inference(cnf_transformation,[status(esa)],[f169_nnf]) ).
cnf(p549,plain,
p(index_258) = index_255,
inference(superposition,[status(thm)],[c169,c11]) ).
cnf(p1534,plain,
p(index_261) = index_255,
inference(superposition,[status(thm)],[p1532,p549]) ).
cnf(p1379,plain,
s(index_264) = p(index_261),
inference(superposition,[status(thm)],[p808,p364]) ).
cnf(p1536,plain,
s(index_264) = index_255,
inference(demodulation,[status(thm)],[p1534,p1379]) ).
cnf(p1560,plain,
s(index_267) = index_255,
inference(demodulation,[status(thm)],[p1554,p1536]) ).
cnf(p1852,plain,
s(index_267) = index_135,
inference(demodulation,[status(thm)],[p1831,p1560]) ).
cnf(p2269,plain,
s(index_15) = index_135,
inference(demodulation,[status(thm)],[p2253,p1852]) ).
cnf(p2603,plain,
s(index_111) = index_135,
inference(demodulation,[status(thm)],[p2575,p2269]) ).
cnf(p2939,plain,
index_201 = index_9,
inference(superposition,[status(thm)],[p2603,p364]) ).
cnf(p1200,plain,
rselect_tail(queue_73) = index_72,
inference(superposition,[status(thm)],[c291,c4]) ).
cnf(p1796,plain,
index_135 = index_72,
inference(superposition,[status(thm)],[c312,p1200]) ).
cnf(f196,hypothesis,
index_72 = s(index_69),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp180) ).
fof(f196_nnf,plain,
index_72 = s(index_69),
inference(nnf_transformation,[status(thm)],[f196]) ).
cnf(c196,plain,
index_72 = s(index_69),
inference(cnf_transformation,[status(esa)],[f196_nnf]) ).
cnf(p609,plain,
p(index_72) = index_69,
inference(superposition,[status(thm)],[c196,c11]) ).
cnf(p1798,plain,
p(index_135) = index_69,
inference(superposition,[status(thm)],[p1796,p609]) ).
cnf(p718,plain,
rselect_tail(queue_139) = index_138,
inference(superposition,[status(thm)],[c223,c4]) ).
cnf(p1000,plain,
index_201 = index_138,
inference(superposition,[status(thm)],[c323,p718]) ).
cnf(f125,hypothesis,
index_138 = s(index_135),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp109) ).
fof(f125_nnf,plain,
index_138 = s(index_135),
inference(nnf_transformation,[status(thm)],[f125]) ).
cnf(c125,plain,
index_138 = s(index_135),
inference(cnf_transformation,[status(esa)],[f125_nnf]) ).
cnf(p451,plain,
p(index_138) = index_135,
inference(superposition,[status(thm)],[c125,c11]) ).
cnf(p703,plain,
s(index_135) = index_138,
inference(superposition,[status(thm)],[p451,c12]) ).
cnf(p1005,plain,
index_138 = index_201,
inference(superposition,[status(thm)],[p1000,p703]) ).
cnf(p1006,plain,
s(index_135) = index_201,
inference(demodulation,[status(thm)],[p1005,p703]) ).
cnf(p1516,plain,
s(index_201) = p(index_135),
inference(superposition,[status(thm)],[p1006,p364]) ).
cnf(p1800,plain,
s(index_201) = index_69,
inference(demodulation,[status(thm)],[p1798,p1516]) ).
cnf(p2466,plain,
index_3 = index_201,
inference(superposition,[status(thm)],[p1800,c11]) ).
cnf(f300,hypothesis,
q0 = queue_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp284) ).
fof(f300_nnf,plain,
q0 = queue_1,
inference(nnf_transformation,[status(thm)],[f300]) ).
cnf(c300,plain,
q0 = queue_1,
inference(cnf_transformation,[status(esa)],[f300_nnf]) ).
cnf(f207,hypothesis,
queue_1 = rstore_head(q,index_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp191) ).
fof(f207_nnf,plain,
queue_1 = rstore_head(q,index_0),
inference(nnf_transformation,[status(thm)],[f207]) ).
cnf(c207,plain,
queue_1 = rstore_head(q,index_0),
inference(cnf_transformation,[status(esa)],[f207_nnf]) ).
cnf(p640,plain,
q0 = rstore_head(q,index_0),
inference(superposition,[status(thm)],[c300,c207]) ).
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(p2162,plain,
index_3 = index_0,
inference(superposition,[status(thm)],[p640,c10]) ).
cnf(f111,hypothesis,
index_0 = rselect_tail(q),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp95) ).
fof(f111_nnf,plain,
index_0 = rselect_tail(q),
inference(nnf_transformation,[status(thm)],[f111]) ).
cnf(c111,plain,
index_0 = rselect_tail(q),
inference(cnf_transformation,[status(esa)],[f111_nnf]) ).
cnf(p420,plain,
rselect_tail(q) = index_0,
inference(superposition,[status(thm)],[c111,c9]) ).
cnf(p2171,plain,
index_0 = index_3,
inference(superposition,[status(thm)],[p2162,p420]) ).
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(p641,plain,
rselect_head(queue_1) = index_0,
inference(superposition,[status(thm)],[c207,c3]) ).
cnf(p891,plain,
rselect_head(q0) = index_0,
inference(superposition,[status(thm)],[c300,p641]) ).
cnf(p2174,plain,
rselect_head(q0) = index_3,
inference(demodulation,[status(thm)],[p2171,p891]) ).
cnf(p2482,plain,
rselect_head(q0) = index_201,
inference(demodulation,[status(thm)],[p2466,p2174]) ).
cnf(p2978,plain,
rselect_head(q0) = index_9,
inference(demodulation,[status(thm)],[p2939,p2482]) ).
cnf(p3594,plain,
index_279 = index_9,
inference(superposition,[status(thm)],[p3589,p2978]) ).
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(p990,plain,
rselect_seq(queue_247) = rselect_seq(queue_245),
inference(superposition,[status(thm)],[c262,c6]) ).
cnf(p2891,plain,
earray_278 = earray_244,
inference(superposition,[status(thm)],[c341,p990]) ).
cnf(f109,hypothesis,
elem_280 = select(earray_278,index_279),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp93) ).
fof(f109_nnf,plain,
elem_280 = select(earray_278,index_279),
inference(nnf_transformation,[status(thm)],[f109]) ).
cnf(c109,plain,
elem_280 = select(earray_278,index_279),
inference(cnf_transformation,[status(esa)],[f109_nnf]) ).
cnf(p2892,plain,
elem_280 = select(earray_244,index_279),
inference(demodulation,[status(thm)],[p2891,c109]) ).
cnf(p3596,plain,
elem_280 = select(earray_244,index_9),
inference(demodulation,[status(thm)],[p3594,p2892]) ).
cnf(p2645,plain,
index_105 = index_9,
inference(superposition,[status(thm)],[p1876,p364]) ).
cnf(p648,plain,
rselect_tail(queue_103) = index_102,
inference(superposition,[status(thm)],[c209,c4]) ).
cnf(p892,plain,
index_105 = index_102,
inference(superposition,[status(thm)],[c317,p648]) ).
cnf(f112,hypothesis,
index_102 = s(index_99),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp96) ).
fof(f112_nnf,plain,
index_102 = s(index_99),
inference(nnf_transformation,[status(thm)],[f112]) ).
cnf(c112,plain,
index_102 = s(index_99),
inference(cnf_transformation,[status(esa)],[f112_nnf]) ).
cnf(p421,plain,
p(index_102) = index_99,
inference(superposition,[status(thm)],[c112,c11]) ).
cnf(p895,plain,
p(index_105) = index_99,
inference(superposition,[status(thm)],[p892,p421]) ).
cnf(p1395,plain,
s(index_111) = index_99,
inference(superposition,[status(thm)],[p895,p364]) ).
cnf(p665,plain,
rselect_tail(queue_115) = index_114,
inference(superposition,[status(thm)],[c214,c4]) ).
cnf(p920,plain,
index_117 = index_114,
inference(superposition,[status(thm)],[c319,p665]) ).
cnf(p929,plain,
index_114 = index_117,
inference(superposition,[status(thm)],[p920,p665]) ).
cnf(f116,hypothesis,
index_114 = s(index_111),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp100) ).
fof(f116_nnf,plain,
index_114 = s(index_111),
inference(nnf_transformation,[status(thm)],[f116]) ).
cnf(c116,plain,
index_114 = s(index_111),
inference(cnf_transformation,[status(esa)],[f116_nnf]) ).
cnf(p429,plain,
p(index_114) = index_111,
inference(superposition,[status(thm)],[c116,c11]) ).
cnf(p679,plain,
s(index_111) = index_114,
inference(superposition,[status(thm)],[p429,c12]) ).
cnf(p932,plain,
s(index_111) = index_117,
inference(demodulation,[status(thm)],[p929,p679]) ).
cnf(p1396,plain,
index_99 = index_117,
inference(demodulation,[status(thm)],[p1395,p932]) ).
cnf(f117,hypothesis,
index_117 = rselect_tail(q26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp101) ).
fof(f117_nnf,plain,
index_117 = rselect_tail(q26),
inference(nnf_transformation,[status(thm)],[f117]) ).
cnf(c117,plain,
index_117 = rselect_tail(q26),
inference(cnf_transformation,[status(esa)],[f117_nnf]) ).
cnf(p433,plain,
rselect_tail(q26) = index_117,
inference(superposition,[status(thm)],[c117,c9]) ).
cnf(p1399,plain,
index_117 = index_99,
inference(superposition,[status(thm)],[p1396,p433]) ).
cnf(p673,plain,
rselect_tail(queue_121) = index_120,
inference(superposition,[status(thm)],[c216,c4]) ).
cnf(p936,plain,
index_123 = index_120,
inference(superposition,[status(thm)],[c320,p673]) ).
cnf(f119,hypothesis,
index_120 = s(index_117),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp103) ).
fof(f119_nnf,plain,
index_120 = s(index_117),
inference(nnf_transformation,[status(thm)],[f119]) ).
cnf(c119,plain,
index_120 = s(index_117),
inference(cnf_transformation,[status(esa)],[f119_nnf]) ).
cnf(p438,plain,
p(index_120) = index_117,
inference(superposition,[status(thm)],[c119,c11]) ).
cnf(p939,plain,
p(index_123) = index_117,
inference(superposition,[status(thm)],[p936,p438]) ).
cnf(p1410,plain,
p(index_123) = index_99,
inference(demodulation,[status(thm)],[p1399,p939]) ).
cnf(p1939,plain,
index_105 = index_123,
inference(superposition,[status(thm)],[p1410,c12]) ).
cnf(f120,hypothesis,
index_123 = rselect_tail(q27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp104) ).
fof(f120_nnf,plain,
index_123 = rselect_tail(q27),
inference(nnf_transformation,[status(thm)],[f120]) ).
cnf(c120,plain,
index_123 = rselect_tail(q27),
inference(cnf_transformation,[status(esa)],[f120_nnf]) ).
cnf(p440,plain,
rselect_tail(q27) = index_123,
inference(superposition,[status(thm)],[c120,c9]) ).
cnf(p1942,plain,
index_123 = index_105,
inference(superposition,[status(thm)],[p1939,p440]) ).
cnf(p705,plain,
rselect_tail(queue_133) = index_132,
inference(superposition,[status(thm)],[c221,c4]) ).
cnf(p980,plain,
index_141 = index_132,
inference(superposition,[status(thm)],[c322,p705]) ).
cnf(f123,hypothesis,
index_132 = s(index_129),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp107) ).
fof(f123_nnf,plain,
index_132 = s(index_129),
inference(nnf_transformation,[status(thm)],[f123]) ).
cnf(c123,plain,
index_132 = s(index_129),
inference(cnf_transformation,[status(esa)],[f123_nnf]) ).
cnf(p446,plain,
p(index_132) = index_129,
inference(superposition,[status(thm)],[c123,c11]) ).
cnf(p698,plain,
s(index_129) = index_132,
inference(superposition,[status(thm)],[p446,c12]) ).
cnf(p985,plain,
index_132 = index_141,
inference(superposition,[status(thm)],[p980,p698]) ).
cnf(p986,plain,
s(index_129) = index_141,
inference(demodulation,[status(thm)],[p985,p698]) ).
cnf(p1469,plain,
s(index_141) = index_123,
inference(superposition,[status(thm)],[p986,p364]) ).
cnf(p729,plain,
rselect_tail(queue_145) = index_144,
inference(superposition,[status(thm)],[c225,c4]) ).
cnf(p1016,plain,
index_147 = index_144,
inference(superposition,[status(thm)],[c324,p729]) ).
cnf(f127,hypothesis,
index_144 = s(index_141),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp111) ).
fof(f127_nnf,plain,
index_144 = s(index_141),
inference(nnf_transformation,[status(thm)],[f127]) ).
cnf(c127,plain,
index_144 = s(index_141),
inference(cnf_transformation,[status(esa)],[f127_nnf]) ).
cnf(p456,plain,
p(index_144) = index_141,
inference(superposition,[status(thm)],[c127,c11]) ).
cnf(p709,plain,
s(index_141) = index_144,
inference(superposition,[status(thm)],[p456,c12]) ).
cnf(p1021,plain,
index_144 = index_147,
inference(superposition,[status(thm)],[p1016,p709]) ).
cnf(p1022,plain,
s(index_141) = index_147,
inference(demodulation,[status(thm)],[p1021,p709]) ).
cnf(p1470,plain,
index_123 = index_147,
inference(demodulation,[status(thm)],[p1469,p1022]) ).
cnf(f128,hypothesis,
index_147 = rselect_tail(q30),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp112) ).
fof(f128_nnf,plain,
index_147 = rselect_tail(q30),
inference(nnf_transformation,[status(thm)],[f128]) ).
cnf(c128,plain,
index_147 = rselect_tail(q30),
inference(cnf_transformation,[status(esa)],[f128_nnf]) ).
cnf(p458,plain,
rselect_tail(q30) = index_147,
inference(superposition,[status(thm)],[c128,c9]) ).
cnf(p1472,plain,
index_147 = index_123,
inference(superposition,[status(thm)],[p1470,p458]) ).
cnf(p742,plain,
rselect_tail(queue_151) = index_150,
inference(superposition,[status(thm)],[c227,c4]) ).
cnf(p1032,plain,
index_153 = index_150,
inference(superposition,[status(thm)],[c325,p742]) ).
cnf(f130,hypothesis,
index_150 = s(index_147),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp114) ).
fof(f130_nnf,plain,
index_150 = s(index_147),
inference(nnf_transformation,[status(thm)],[f130]) ).
cnf(c130,plain,
index_150 = s(index_147),
inference(cnf_transformation,[status(esa)],[f130_nnf]) ).
cnf(p462,plain,
p(index_150) = index_147,
inference(superposition,[status(thm)],[c130,c11]) ).
cnf(p1038,plain,
p(index_153) = index_147,
inference(superposition,[status(thm)],[p1032,p462]) ).
cnf(p1484,plain,
p(index_153) = index_123,
inference(demodulation,[status(thm)],[p1472,p1038]) ).
cnf(p1974,plain,
p(index_153) = index_105,
inference(demodulation,[status(thm)],[p1942,p1484]) ).
cnf(p2686,plain,
p(index_153) = index_9,
inference(demodulation,[status(thm)],[p2645,p1974]) ).
cnf(p3064,plain,
index_165 = index_9,
inference(superposition,[status(thm)],[p2686,p364]) ).
cnf(p973,plain,
rselect_tail(queue_241) = index_240,
inference(superposition,[status(thm)],[c260,c4]) ).
cnf(p1452,plain,
index_243 = index_240,
inference(superposition,[status(thm)],[c340,p973]) ).
cnf(f163,hypothesis,
index_240 = s(index_237),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp147) ).
fof(f163_nnf,plain,
index_240 = s(index_237),
inference(nnf_transformation,[status(thm)],[f163]) ).
cnf(c163,plain,
index_240 = s(index_237),
inference(cnf_transformation,[status(esa)],[f163_nnf]) ).
cnf(p536,plain,
p(index_240) = index_237,
inference(superposition,[status(thm)],[c163,c11]) ).
cnf(p1454,plain,
p(index_243) = index_237,
inference(superposition,[status(thm)],[p1452,p536]) ).
cnf(f165,hypothesis,
index_246 = s(index_243),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp149) ).
fof(f165_nnf,plain,
index_246 = s(index_243),
inference(nnf_transformation,[status(thm)],[f165]) ).
cnf(c165,plain,
index_246 = s(index_243),
inference(cnf_transformation,[status(esa)],[f165_nnf]) ).
cnf(p541,plain,
p(index_246) = index_243,
inference(superposition,[status(thm)],[c165,c11]) ).
cnf(p795,plain,
s(index_243) = index_246,
inference(superposition,[status(thm)],[p541,c12]) ).
cnf(p1376,plain,
s(index_246) = p(index_243),
inference(superposition,[status(thm)],[p795,p364]) ).
cnf(p1456,plain,
s(index_246) = index_237,
inference(demodulation,[status(thm)],[p1454,p1376]) ).
cnf(p1983,plain,
index_231 = index_246,
inference(superposition,[status(thm)],[p1456,c11]) ).
cnf(p1986,plain,
p(index_231) = index_243,
inference(superposition,[status(thm)],[p1983,p541]) ).
cnf(p887,plain,
rselect_tail(queue_217) = index_216,
inference(superposition,[status(thm)],[c251,c4]) ).
cnf(p1242,plain,
index_219 = index_216,
inference(superposition,[status(thm)],[c336,p887]) ).
cnf(f154,hypothesis,
index_216 = s(index_213),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp138) ).
fof(f154_nnf,plain,
index_216 = s(index_213),
inference(nnf_transformation,[status(thm)],[f154]) ).
cnf(c154,plain,
index_216 = s(index_213),
inference(cnf_transformation,[status(esa)],[f154_nnf]) ).
cnf(p516,plain,
p(index_216) = index_213,
inference(superposition,[status(thm)],[c154,c11]) ).
cnf(p770,plain,
s(index_213) = index_216,
inference(superposition,[status(thm)],[p516,c12]) ).
cnf(p1247,plain,
index_216 = index_219,
inference(superposition,[status(thm)],[p1242,p770]) ).
cnf(p1248,plain,
s(index_213) = index_219,
inference(demodulation,[status(thm)],[p1247,p770]) ).
cnf(p1891,plain,
s(index_219) = index_207,
inference(superposition,[status(thm)],[p1248,p364]) ).
cnf(p904,plain,
rselect_tail(queue_223) = index_222,
inference(superposition,[status(thm)],[c253,c4]) ).
cnf(p1305,plain,
index_225 = index_222,
inference(superposition,[status(thm)],[c337,p904]) ).
cnf(f156,hypothesis,
index_222 = s(index_219),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp140) ).
fof(f156_nnf,plain,
index_222 = s(index_219),
inference(nnf_transformation,[status(thm)],[f156]) ).
cnf(c156,plain,
index_222 = s(index_219),
inference(cnf_transformation,[status(esa)],[f156_nnf]) ).
cnf(p519,plain,
p(index_222) = index_219,
inference(superposition,[status(thm)],[c156,c11]) ).
cnf(p772,plain,
s(index_219) = index_222,
inference(superposition,[status(thm)],[p519,c12]) ).
cnf(p1310,plain,
index_222 = index_225,
inference(superposition,[status(thm)],[p1305,p772]) ).
cnf(p1311,plain,
s(index_219) = index_225,
inference(demodulation,[status(thm)],[p1310,p772]) ).
cnf(p1892,plain,
index_207 = index_225,
inference(demodulation,[status(thm)],[p1891,p1311]) ).
cnf(f157,hypothesis,
index_225 = rselect_tail(q42),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp141) ).
fof(f157_nnf,plain,
index_225 = rselect_tail(q42),
inference(nnf_transformation,[status(thm)],[f157]) ).
cnf(c157,plain,
index_225 = rselect_tail(q42),
inference(cnf_transformation,[status(esa)],[f157_nnf]) ).
cnf(p523,plain,
rselect_tail(q42) = index_225,
inference(superposition,[status(thm)],[c157,c9]) ).
cnf(p1894,plain,
index_225 = index_207,
inference(superposition,[status(thm)],[p1892,p523]) ).
cnf(p921,plain,
rselect_tail(queue_229) = index_228,
inference(superposition,[status(thm)],[c255,c4]) ).
cnf(p1415,plain,
index_231 = index_228,
inference(superposition,[status(thm)],[c338,p921]) ).
cnf(f158,hypothesis,
index_228 = s(index_225),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp142) ).
fof(f158_nnf,plain,
index_228 = s(index_225),
inference(nnf_transformation,[status(thm)],[f158]) ).
cnf(c158,plain,
index_228 = s(index_225),
inference(cnf_transformation,[status(esa)],[f158_nnf]) ).
cnf(p524,plain,
p(index_228) = index_225,
inference(superposition,[status(thm)],[c158,c11]) ).
cnf(p1417,plain,
p(index_231) = index_225,
inference(superposition,[status(thm)],[p1415,p524]) ).
cnf(p1907,plain,
p(index_231) = index_207,
inference(demodulation,[status(thm)],[p1894,p1417]) ).
cnf(p1987,plain,
index_243 = index_207,
inference(demodulation,[status(thm)],[p1986,p1907]) ).
cnf(p790,plain,
s(index_237) = index_240,
inference(superposition,[status(thm)],[p536,c12]) ).
cnf(p1459,plain,
index_240 = index_243,
inference(superposition,[status(thm)],[p1452,p790]) ).
cnf(p1460,plain,
s(index_237) = index_243,
inference(demodulation,[status(thm)],[p1459,p790]) ).
cnf(p2176,plain,
index_165 = index_207,
inference(superposition,[status(thm)],[p1987,p1460]) ).
cnf(f150,hypothesis,
index_207 = rselect_tail(q39),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp134) ).
fof(f150_nnf,plain,
index_207 = rselect_tail(q39),
inference(nnf_transformation,[status(thm)],[f150]) ).
cnf(c150,plain,
index_207 = rselect_tail(q39),
inference(cnf_transformation,[status(esa)],[f150_nnf]) ).
cnf(p507,plain,
rselect_tail(q39) = index_207,
inference(superposition,[status(thm)],[c150,c9]) ).
cnf(p2178,plain,
index_207 = index_165,
inference(superposition,[status(thm)],[p2176,p507]) ).
cnf(f70,hypothesis,
earray_244 = store(earray_242,index_243,e45),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp54) ).
fof(f70_nnf,plain,
earray_244 = store(earray_242,index_243,e45),
inference(nnf_transformation,[status(thm)],[f70]) ).
cnf(c70,plain,
earray_244 = store(earray_242,index_243,e45),
inference(cnf_transformation,[status(esa)],[f70_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(p532,plain,
select(earray_244,index_243) = e45,
inference(superposition,[status(thm)],[c70,c0]) ).
cnf(p2004,plain,
select(earray_244,index_207) = e45,
inference(superposition,[status(thm)],[p1987,p532]) ).
cnf(p2210,plain,
select(earray_244,index_165) = e45,
inference(demodulation,[status(thm)],[p2178,p2004]) ).
cnf(p3102,plain,
select(earray_244,index_9) = e45,
inference(demodulation,[status(thm)],[p3064,p2210]) ).
cnf(p3870,plain,
elem_280 = e45,
inference(superposition,[status(thm)],[p3596,p3102]) ).
cnf(p1989,plain,
index_246 = index_231,
inference(superposition,[status(thm)],[p1983,p795]) ).
cnf(p989,plain,
rselect_tail(queue_247) = index_246,
inference(superposition,[status(thm)],[c262,c4]) ).
cnf(p1489,plain,
index_281 = index_246,
inference(superposition,[status(thm)],[c341,p989]) ).
cnf(f179,hypothesis,
s(index_282) = index_281,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp163) ).
fof(f179_nnf,plain,
s(index_282) = index_281,
inference(nnf_transformation,[status(thm)],[f179]) ).
cnf(c179,plain,
s(index_282) = index_281,
inference(cnf_transformation,[status(esa)],[f179_nnf]) ).
cnf(p1490,plain,
s(index_282) = index_246,
inference(demodulation,[status(thm)],[p1489,c179]) ).
cnf(p1994,plain,
s(index_282) = index_231,
inference(demodulation,[status(thm)],[p1989,p1490]) ).
cnf(p2816,plain,
index_165 = index_282,
inference(superposition,[status(thm)],[p1994,c11]) ).
cnf(f110,hypothesis,
elem_283 = select(earray_278,index_282),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp94) ).
fof(f110_nnf,plain,
elem_283 = select(earray_278,index_282),
inference(nnf_transformation,[status(thm)],[f110]) ).
cnf(c110,plain,
elem_283 = select(earray_278,index_282),
inference(cnf_transformation,[status(esa)],[f110_nnf]) ).
cnf(p2819,plain,
elem_283 = select(earray_278,index_165),
inference(superposition,[status(thm)],[p2816,c110]) ).
cnf(p2897,plain,
elem_283 = select(earray_244,index_165),
inference(demodulation,[status(thm)],[p2891,p2819]) ).
cnf(p3134,plain,
elem_283 = select(earray_244,index_9),
inference(demodulation,[status(thm)],[p3064,p2897]) ).
cnf(p3814,plain,
elem_283 = e45,
inference(superposition,[status(thm)],[p3134,p3102]) ).
cnf(f347,negated_conjecture,
elem_280 != elem_283,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f347_nnf,plain,
elem_280 != elem_283,
inference(nnf_transformation,[status(thm)],[f347]) ).
fof(f347_sk,plain,
elem_280 != elem_283,
inference(skolemisation,[status(esa)],[f347_nnf]) ).
cnf(c347,plain,
elem_280 != elem_283,
inference(cnf_transformation,[status(esa)],[f347_sk]) ).
cnf(p3815,plain,
elem_280 != e45,
inference(demodulation,[status(thm)],[p3814,c347]) ).
cnf(p3871,plain,
e45 != e45,
inference(demodulation,[status(thm)],[p3870,p3815]) ).
cnf(p3872,plain,
$false,
inference(equality_resolution,[status(thm)],[p3871]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV570-1.046 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 20:39:04 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 36.76/5.10 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 36.76/5.10 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------