%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:08:41 AM UTC 2026
% Result : Unsatisfiable 15.15s 2.33s
% Output : CNFRefutation 15.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 254
% Syntax : Number of formulae : 1529 (1455 unt; 0 def)
% Number of atoms : 1603 (1602 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 356 ( 282 ~; 74 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 20 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 266 ( 266 usr; 257 con; 0-3 aty)
% Number of variables : 123 ( 10 sgn 42 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(a1,axiom,
! [VAR_0,VAR_1,VAR_2] : select(store(VAR_0,VAR_1,VAR_2),VAR_1) = VAR_2,
file('theBenchmark.p',a1) ).
cnf(c_1,plain,
select(store(A,B,C),B) = C,
inference(clausify,[status(thm)],[a1]) ).
fof(a2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( select(store(VAR_2,VAR_0,VAR_3),VAR_1) = select(VAR_2,VAR_1)
| VAR_0 = VAR_1 ),
file('theBenchmark.p',a2) ).
cnf(c_2,plain,
( select(store(C,A,D),B) = select(C,B)
| A = B ),
inference(clausify,[status(thm)],[a2]) ).
fof(a1_seq,axiom,
! [VAR_0,VAR_1] : rselect_seq(rstore_seq(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',a1_seq) ).
cnf(c_3,plain,
rselect_seq(rstore_seq(A,B)) = B,
inference(clausify,[status(thm)],[a1_seq]) ).
fof(a1_head,axiom,
! [VAR_0,VAR_1] : rselect_head(rstore_head(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',a1_head) ).
cnf(c_4,plain,
rselect_head(rstore_head(A,B)) = B,
inference(clausify,[status(thm)],[a1_head]) ).
fof(a1_tail,axiom,
! [VAR_0,VAR_1] : rselect_tail(rstore_tail(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',a1_tail) ).
cnf(c_5,plain,
rselect_tail(rstore_tail(A,B)) = B,
inference(clausify,[status(thm)],[a1_tail]) ).
fof(a2_seq_head,axiom,
! [VAR_0,VAR_1] : rselect_seq(rstore_head(VAR_0,VAR_1)) = rselect_seq(VAR_0),
file('theBenchmark.p',a2_seq_head) ).
cnf(c_6,plain,
rselect_seq(rstore_head(A,B)) = rselect_seq(A),
inference(clausify,[status(thm)],[a2_seq_head]) ).
fof(a2_seq_tail,axiom,
! [VAR_0,VAR_1] : rselect_seq(rstore_tail(VAR_0,VAR_1)) = rselect_seq(VAR_0),
file('theBenchmark.p',a2_seq_tail) ).
cnf(c_7,plain,
rselect_seq(rstore_tail(A,B)) = rselect_seq(A),
inference(clausify,[status(thm)],[a2_seq_tail]) ).
fof(a2_head_tail,axiom,
! [VAR_0,VAR_1] : rselect_head(rstore_tail(VAR_0,VAR_1)) = rselect_head(VAR_0),
file('theBenchmark.p',a2_head_tail) ).
cnf(c_8,plain,
rselect_head(rstore_tail(A,B)) = rselect_head(A),
inference(clausify,[status(thm)],[a2_head_tail]) ).
fof(a2_head_seq,axiom,
! [VAR_0,VAR_1] : rselect_head(rstore_seq(VAR_0,VAR_1)) = rselect_head(VAR_0),
file('theBenchmark.p',a2_head_seq) ).
cnf(c_9,plain,
rselect_head(rstore_seq(A,B)) = rselect_head(A),
inference(clausify,[status(thm)],[a2_head_seq]) ).
fof(a2_tail_head,axiom,
! [VAR_0,VAR_1] : rselect_tail(rstore_head(VAR_0,VAR_1)) = rselect_tail(VAR_0),
file('theBenchmark.p',a2_tail_head) ).
cnf(c_11,plain,
rselect_tail(rstore_head(A,B)) = rselect_tail(A),
inference(clausify,[status(thm)],[a2_tail_head]) ).
fof(as19,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(VAR_0))))))))))))))))))) != VAR_0,
file('theBenchmark.p',as19) ).
cnf(c_43,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))))) != A,
inference(clausify,[status(thm)],[as19]) ).
fof(as18,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(VAR_0)))))))))))))))))) != VAR_0,
file('theBenchmark.p',as18) ).
cnf(c_44,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))))) != A,
inference(clausify,[status(thm)],[as18]) ).
fof(as17,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(VAR_0))))))))))))))))) != VAR_0,
file('theBenchmark.p',as17) ).
cnf(c_45,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))))) != A,
inference(clausify,[status(thm)],[as17]) ).
fof(as16,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(VAR_0)))))))))))))))) != VAR_0,
file('theBenchmark.p',as16) ).
cnf(c_46,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))))) != A,
inference(clausify,[status(thm)],[as16]) ).
fof(as15,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(VAR_0))))))))))))))) != VAR_0,
file('theBenchmark.p',as15) ).
cnf(c_47,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))))) != A,
inference(clausify,[status(thm)],[as15]) ).
fof(as14,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(s(s(VAR_0)))))))))))))) != VAR_0,
file('theBenchmark.p',as14) ).
cnf(c_48,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))))) != A,
inference(clausify,[status(thm)],[as14]) ).
fof(as13,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(s(VAR_0))))))))))))) != VAR_0,
file('theBenchmark.p',as13) ).
cnf(c_49,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(A))))))))))))) != A,
inference(clausify,[status(thm)],[as13]) ).
fof(as12,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(s(VAR_0)))))))))))) != VAR_0,
file('theBenchmark.p',as12) ).
cnf(c_50,plain,
s(s(s(s(s(s(s(s(s(s(s(s(A)))))))))))) != A,
inference(clausify,[status(thm)],[as12]) ).
fof(as11,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(s(VAR_0))))))))))) != VAR_0,
file('theBenchmark.p',as11) ).
cnf(c_51,plain,
s(s(s(s(s(s(s(s(s(s(s(A))))))))))) != A,
inference(clausify,[status(thm)],[as11]) ).
fof(as10,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(s(VAR_0)))))))))) != VAR_0,
file('theBenchmark.p',as10) ).
cnf(c_52,plain,
s(s(s(s(s(s(s(s(s(s(A)))))))))) != A,
inference(clausify,[status(thm)],[as10]) ).
fof(as9,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(s(VAR_0))))))))) != VAR_0,
file('theBenchmark.p',as9) ).
cnf(c_53,plain,
s(s(s(s(s(s(s(s(s(A))))))))) != A,
inference(clausify,[status(thm)],[as9]) ).
fof(as8,axiom,
! [VAR_0] : s(s(s(s(s(s(s(s(VAR_0)))))))) != VAR_0,
file('theBenchmark.p',as8) ).
cnf(c_54,plain,
s(s(s(s(s(s(s(s(A)))))))) != A,
inference(clausify,[status(thm)],[as8]) ).
fof(as7,axiom,
! [VAR_0] : s(s(s(s(s(s(s(VAR_0))))))) != VAR_0,
file('theBenchmark.p',as7) ).
cnf(c_55,plain,
s(s(s(s(s(s(s(A))))))) != A,
inference(clausify,[status(thm)],[as7]) ).
fof(as6,axiom,
! [VAR_0] : s(s(s(s(s(s(VAR_0)))))) != VAR_0,
file('theBenchmark.p',as6) ).
cnf(c_56,plain,
s(s(s(s(s(s(A)))))) != A,
inference(clausify,[status(thm)],[as6]) ).
fof(as5,axiom,
! [VAR_0] : s(s(s(s(s(VAR_0))))) != VAR_0,
file('theBenchmark.p',as5) ).
cnf(c_57,plain,
s(s(s(s(s(A))))) != A,
inference(clausify,[status(thm)],[as5]) ).
fof(as4,axiom,
! [VAR_0] : s(s(s(s(VAR_0)))) != VAR_0,
file('theBenchmark.p',as4) ).
cnf(c_58,plain,
s(s(s(s(A)))) != A,
inference(clausify,[status(thm)],[as4]) ).
fof(as3,axiom,
! [VAR_0] : s(s(s(VAR_0))) != VAR_0,
file('theBenchmark.p',as3) ).
cnf(c_59,plain,
s(s(s(A))) != A,
inference(clausify,[status(thm)],[as3]) ).
fof(as2,axiom,
! [VAR_0] : s(s(VAR_0)) != VAR_0,
file('theBenchmark.p',as2) ).
cnf(c_60,plain,
s(s(A)) != A,
inference(clausify,[status(thm)],[as2]) ).
fof(as1,axiom,
! [VAR_0] : s(VAR_0) != VAR_0,
file('theBenchmark.p',as1) ).
cnf(c_61,plain,
s(A) != A,
inference(clausify,[status(thm)],[as1]) ).
fof(hyp1,axiom,
earray_100 = store(earray_98,index_99,e21),
file('theBenchmark.p',hyp1) ).
cnf(c_64,plain,
earray_100 = store(earray_98,index_99,e21),
inference(clausify,[status(thm)],[hyp1]) ).
cnf(c_65,plain,
store(earray_98,index_99,e21) = earray_100,
inference(copy,[status(thm)],[c_64]) ).
fof(hyp2,axiom,
earray_104 = rselect_seq(q22),
file('theBenchmark.p',hyp2) ).
cnf(c_66,plain,
earray_104 = rselect_seq(q22),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_67,plain,
rselect_seq(q22) = earray_104,
inference(copy,[status(thm)],[c_66]) ).
fof(hyp3,axiom,
earray_106 = store(earray_104,index_105,e22),
file('theBenchmark.p',hyp3) ).
cnf(c_68,plain,
earray_106 = store(earray_104,index_105,e22),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_69,plain,
store(earray_104,index_105,e22) = earray_106,
inference(copy,[status(thm)],[c_68]) ).
fof(hyp4,axiom,
earray_110 = rselect_seq(q23),
file('theBenchmark.p',hyp4) ).
cnf(c_70,plain,
earray_110 = rselect_seq(q23),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_71,plain,
rselect_seq(q23) = earray_110,
inference(copy,[status(thm)],[c_70]) ).
fof(hyp5,axiom,
earray_112 = store(earray_110,index_111,e23),
file('theBenchmark.p',hyp5) ).
cnf(c_72,plain,
earray_112 = store(earray_110,index_111,e23),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_73,plain,
store(earray_110,index_111,e23) = earray_112,
inference(copy,[status(thm)],[c_72]) ).
fof(hyp6,axiom,
earray_119 = rselect_seq(q24),
file('theBenchmark.p',hyp6) ).
cnf(c_74,plain,
earray_119 = rselect_seq(q24),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_75,plain,
rselect_seq(q24) = earray_119,
inference(copy,[status(thm)],[c_74]) ).
fof(hyp7,axiom,
earray_121 = store(earray_119,index_120,e24),
file('theBenchmark.p',hyp7) ).
cnf(c_76,plain,
earray_121 = store(earray_119,index_120,e24),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_77,plain,
store(earray_119,index_120,e24) = earray_121,
inference(copy,[status(thm)],[c_76]) ).
fof(hyp8,axiom,
earray_125 = rselect_seq(q25),
file('theBenchmark.p',hyp8) ).
cnf(c_78,plain,
earray_125 = rselect_seq(q25),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_79,plain,
rselect_seq(q25) = earray_125,
inference(copy,[status(thm)],[c_78]) ).
fof(hyp9,axiom,
earray_127 = store(earray_125,index_126,e25),
file('theBenchmark.p',hyp9) ).
cnf(c_80,plain,
earray_127 = store(earray_125,index_126,e25),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_81,plain,
store(earray_125,index_126,e25) = earray_127,
inference(copy,[status(thm)],[c_80]) ).
fof(hyp10,axiom,
earray_131 = rselect_seq(q26),
file('theBenchmark.p',hyp10) ).
cnf(c_82,plain,
earray_131 = rselect_seq(q26),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_83,plain,
rselect_seq(q26) = earray_131,
inference(copy,[status(thm)],[c_82]) ).
fof(hyp11,axiom,
earray_133 = store(earray_131,index_132,e26),
file('theBenchmark.p',hyp11) ).
cnf(c_84,plain,
earray_133 = store(earray_131,index_132,e26),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_85,plain,
store(earray_131,index_132,e26) = earray_133,
inference(copy,[status(thm)],[c_84]) ).
fof(hyp13,axiom,
earray_140 = rselect_seq(q27),
file('theBenchmark.p',hyp13) ).
cnf(c_88,plain,
earray_140 = rselect_seq(q27),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_89,plain,
rselect_seq(q27) = earray_140,
inference(copy,[status(thm)],[c_88]) ).
fof(hyp14,axiom,
earray_142 = store(earray_140,index_141,e27),
file('theBenchmark.p',hyp14) ).
cnf(c_90,plain,
earray_142 = store(earray_140,index_141,e27),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_91,plain,
store(earray_140,index_141,e27) = earray_142,
inference(copy,[status(thm)],[c_90]) ).
fof(hyp15,axiom,
earray_146 = rselect_seq(q28),
file('theBenchmark.p',hyp15) ).
cnf(c_92,plain,
earray_146 = rselect_seq(q28),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_93,plain,
rselect_seq(q28) = earray_146,
inference(copy,[status(thm)],[c_92]) ).
fof(hyp16,axiom,
earray_148 = store(earray_146,index_147,e28),
file('theBenchmark.p',hyp16) ).
cnf(c_94,plain,
earray_148 = store(earray_146,index_147,e28),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_95,plain,
store(earray_146,index_147,e28) = earray_148,
inference(copy,[status(thm)],[c_94]) ).
fof(hyp19,axiom,
earray_16 = store(earray_14,index_15,e10),
file('theBenchmark.p',hyp19) ).
cnf(c_100,plain,
earray_16 = store(earray_14,index_15,e10),
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_101,plain,
store(earray_14,index_15,e10) = earray_16,
inference(copy,[status(thm)],[c_100]) ).
fof(hyp20,axiom,
earray_161 = rselect_seq(q29),
file('theBenchmark.p',hyp20) ).
cnf(c_102,plain,
earray_161 = rselect_seq(q29),
inference(clausify,[status(thm)],[hyp20]) ).
cnf(c_103,plain,
rselect_seq(q29) = earray_161,
inference(copy,[status(thm)],[c_102]) ).
fof(hyp21,axiom,
earray_163 = store(earray_161,index_162,e29),
file('theBenchmark.p',hyp21) ).
cnf(c_104,plain,
earray_163 = store(earray_161,index_162,e29),
inference(clausify,[status(thm)],[hyp21]) ).
cnf(c_105,plain,
store(earray_161,index_162,e29) = earray_163,
inference(copy,[status(thm)],[c_104]) ).
fof(hyp33,axiom,
earray_20 = rselect_seq(q11),
file('theBenchmark.p',hyp33) ).
cnf(c_128,plain,
earray_20 = rselect_seq(q11),
inference(clausify,[status(thm)],[hyp33]) ).
cnf(c_129,plain,
rselect_seq(q11) = earray_20,
inference(copy,[status(thm)],[c_128]) ).
fof(hyp36,axiom,
earray_212 = rselect_seq(q30),
file('theBenchmark.p',hyp36) ).
cnf(c_134,plain,
earray_212 = rselect_seq(q30),
inference(clausify,[status(thm)],[hyp36]) ).
cnf(c_135,plain,
rselect_seq(q30) = earray_212,
inference(copy,[status(thm)],[c_134]) ).
fof(hyp37,axiom,
earray_22 = store(earray_20,index_21,e11),
file('theBenchmark.p',hyp37) ).
cnf(c_136,plain,
earray_22 = store(earray_20,index_21,e11),
inference(clausify,[status(thm)],[hyp37]) ).
cnf(c_137,plain,
store(earray_20,index_21,e11) = earray_22,
inference(copy,[status(thm)],[c_136]) ).
fof(hyp38,axiom,
earray_29 = rselect_seq(q12),
file('theBenchmark.p',hyp38) ).
cnf(c_138,plain,
earray_29 = rselect_seq(q12),
inference(clausify,[status(thm)],[hyp38]) ).
cnf(c_139,plain,
rselect_seq(q12) = earray_29,
inference(copy,[status(thm)],[c_138]) ).
fof(hyp39,axiom,
earray_31 = store(earray_29,index_30,e12),
file('theBenchmark.p',hyp39) ).
cnf(c_140,plain,
earray_31 = store(earray_29,index_30,e12),
inference(clausify,[status(thm)],[hyp39]) ).
cnf(c_141,plain,
store(earray_29,index_30,e12) = earray_31,
inference(copy,[status(thm)],[c_140]) ).
fof(hyp40,axiom,
earray_35 = rselect_seq(q13),
file('theBenchmark.p',hyp40) ).
cnf(c_142,plain,
earray_35 = rselect_seq(q13),
inference(clausify,[status(thm)],[hyp40]) ).
cnf(c_143,plain,
rselect_seq(q13) = earray_35,
inference(copy,[status(thm)],[c_142]) ).
fof(hyp41,axiom,
earray_37 = store(earray_35,index_36,e13),
file('theBenchmark.p',hyp41) ).
cnf(c_144,plain,
earray_37 = store(earray_35,index_36,e13),
inference(clausify,[status(thm)],[hyp41]) ).
cnf(c_145,plain,
store(earray_35,index_36,e13) = earray_37,
inference(copy,[status(thm)],[c_144]) ).
fof(hyp43,axiom,
earray_41 = rselect_seq(q14),
file('theBenchmark.p',hyp43) ).
cnf(c_148,plain,
earray_41 = rselect_seq(q14),
inference(clausify,[status(thm)],[hyp43]) ).
cnf(c_149,plain,
rselect_seq(q14) = earray_41,
inference(copy,[status(thm)],[c_148]) ).
fof(hyp44,axiom,
earray_43 = store(earray_41,index_42,e14),
file('theBenchmark.p',hyp44) ).
cnf(c_150,plain,
earray_43 = store(earray_41,index_42,e14),
inference(clausify,[status(thm)],[hyp44]) ).
cnf(c_151,plain,
store(earray_41,index_42,e14) = earray_43,
inference(copy,[status(thm)],[c_150]) ).
fof(hyp45,axiom,
earray_50 = rselect_seq(q15),
file('theBenchmark.p',hyp45) ).
cnf(c_152,plain,
earray_50 = rselect_seq(q15),
inference(clausify,[status(thm)],[hyp45]) ).
cnf(c_153,plain,
rselect_seq(q15) = earray_50,
inference(copy,[status(thm)],[c_152]) ).
fof(hyp46,axiom,
earray_52 = store(earray_50,index_51,e15),
file('theBenchmark.p',hyp46) ).
cnf(c_154,plain,
earray_52 = store(earray_50,index_51,e15),
inference(clausify,[status(thm)],[hyp46]) ).
cnf(c_155,plain,
store(earray_50,index_51,e15) = earray_52,
inference(copy,[status(thm)],[c_154]) ).
fof(hyp47,axiom,
earray_56 = rselect_seq(q16),
file('theBenchmark.p',hyp47) ).
cnf(c_156,plain,
earray_56 = rselect_seq(q16),
inference(clausify,[status(thm)],[hyp47]) ).
cnf(c_157,plain,
rselect_seq(q16) = earray_56,
inference(copy,[status(thm)],[c_156]) ).
fof(hyp48,axiom,
earray_58 = store(earray_56,index_57,e16),
file('theBenchmark.p',hyp48) ).
cnf(c_158,plain,
earray_58 = store(earray_56,index_57,e16),
inference(clausify,[status(thm)],[hyp48]) ).
cnf(c_159,plain,
store(earray_56,index_57,e16) = earray_58,
inference(copy,[status(thm)],[c_158]) ).
fof(hyp49,axiom,
earray_62 = rselect_seq(q17),
file('theBenchmark.p',hyp49) ).
cnf(c_160,plain,
earray_62 = rselect_seq(q17),
inference(clausify,[status(thm)],[hyp49]) ).
cnf(c_161,plain,
rselect_seq(q17) = earray_62,
inference(copy,[status(thm)],[c_160]) ).
fof(hyp50,axiom,
earray_64 = store(earray_62,index_63,e17),
file('theBenchmark.p',hyp50) ).
cnf(c_162,plain,
earray_64 = store(earray_62,index_63,e17),
inference(clausify,[status(thm)],[hyp50]) ).
cnf(c_163,plain,
store(earray_62,index_63,e17) = earray_64,
inference(copy,[status(thm)],[c_162]) ).
fof(hyp51,axiom,
earray_71 = rselect_seq(q18),
file('theBenchmark.p',hyp51) ).
cnf(c_164,plain,
earray_71 = rselect_seq(q18),
inference(clausify,[status(thm)],[hyp51]) ).
cnf(c_165,plain,
rselect_seq(q18) = earray_71,
inference(copy,[status(thm)],[c_164]) ).
fof(hyp52,axiom,
earray_73 = store(earray_71,index_72,e18),
file('theBenchmark.p',hyp52) ).
cnf(c_166,plain,
earray_73 = store(earray_71,index_72,e18),
inference(clausify,[status(thm)],[hyp52]) ).
cnf(c_167,plain,
store(earray_71,index_72,e18) = earray_73,
inference(copy,[status(thm)],[c_166]) ).
fof(hyp56,axiom,
earray_83 = rselect_seq(q19),
file('theBenchmark.p',hyp56) ).
cnf(c_174,plain,
earray_83 = rselect_seq(q19),
inference(clausify,[status(thm)],[hyp56]) ).
cnf(c_175,plain,
rselect_seq(q19) = earray_83,
inference(copy,[status(thm)],[c_174]) ).
fof(hyp57,axiom,
earray_85 = store(earray_83,index_84,e19),
file('theBenchmark.p',hyp57) ).
cnf(c_176,plain,
earray_85 = store(earray_83,index_84,e19),
inference(clausify,[status(thm)],[hyp57]) ).
cnf(c_177,plain,
store(earray_83,index_84,e19) = earray_85,
inference(copy,[status(thm)],[c_176]) ).
fof(hyp58,axiom,
earray_89 = rselect_seq(q20),
file('theBenchmark.p',hyp58) ).
cnf(c_178,plain,
earray_89 = rselect_seq(q20),
inference(clausify,[status(thm)],[hyp58]) ).
cnf(c_179,plain,
rselect_seq(q20) = earray_89,
inference(copy,[status(thm)],[c_178]) ).
fof(hyp59,axiom,
earray_91 = store(earray_89,index_90,e20),
file('theBenchmark.p',hyp59) ).
cnf(c_180,plain,
earray_91 = store(earray_89,index_90,e20),
inference(clausify,[status(thm)],[hyp59]) ).
cnf(c_181,plain,
store(earray_89,index_90,e20) = earray_91,
inference(copy,[status(thm)],[c_180]) ).
fof(hyp60,axiom,
earray_98 = rselect_seq(q21),
file('theBenchmark.p',hyp60) ).
cnf(c_182,plain,
earray_98 = rselect_seq(q21),
inference(clausify,[status(thm)],[hyp60]) ).
cnf(c_183,plain,
rselect_seq(q21) = earray_98,
inference(copy,[status(thm)],[c_182]) ).
fof(hyp61,axiom,
elem_214 = select(earray_212,index_213),
file('theBenchmark.p',hyp61) ).
cnf(c_184,plain,
elem_214 = select(earray_212,index_213),
inference(clausify,[status(thm)],[hyp61]) ).
cnf(c_185,plain,
select(earray_212,index_213) = elem_214,
inference(copy,[status(thm)],[c_184]) ).
fof(hyp62,axiom,
index_0 = rselect_tail(q),
file('theBenchmark.p',hyp62) ).
cnf(c_186,plain,
index_0 = rselect_tail(q),
inference(clausify,[status(thm)],[hyp62]) ).
cnf(c_187,plain,
rselect_tail(q) = index_0,
inference(copy,[status(thm)],[c_186]) ).
fof(hyp63,axiom,
index_102 = s(index_99),
file('theBenchmark.p',hyp63) ).
cnf(c_188,plain,
index_102 = s(index_99),
inference(clausify,[status(thm)],[hyp63]) ).
cnf(c_189,plain,
s(index_99) = index_102,
inference(copy,[status(thm)],[c_188]) ).
fof(hyp64,axiom,
index_105 = rselect_tail(q22),
file('theBenchmark.p',hyp64) ).
cnf(c_190,plain,
index_105 = rselect_tail(q22),
inference(clausify,[status(thm)],[hyp64]) ).
cnf(c_191,plain,
rselect_tail(q22) = index_105,
inference(copy,[status(thm)],[c_190]) ).
fof(hyp65,axiom,
index_108 = s(index_105),
file('theBenchmark.p',hyp65) ).
cnf(c_192,plain,
index_108 = s(index_105),
inference(clausify,[status(thm)],[hyp65]) ).
cnf(c_193,plain,
s(index_105) = index_108,
inference(copy,[status(thm)],[c_192]) ).
fof(hyp66,axiom,
index_111 = rselect_tail(q23),
file('theBenchmark.p',hyp66) ).
cnf(c_194,plain,
index_111 = rselect_tail(q23),
inference(clausify,[status(thm)],[hyp66]) ).
cnf(c_195,plain,
rselect_tail(q23) = index_111,
inference(copy,[status(thm)],[c_194]) ).
fof(hyp67,axiom,
index_114 = s(index_111),
file('theBenchmark.p',hyp67) ).
cnf(c_196,plain,
index_114 = s(index_111),
inference(clausify,[status(thm)],[hyp67]) ).
cnf(c_197,plain,
s(index_111) = index_114,
inference(copy,[status(thm)],[c_196]) ).
fof(hyp68,axiom,
index_116 = rselect_head(queue_115),
file('theBenchmark.p',hyp68) ).
cnf(c_198,plain,
index_116 = rselect_head(queue_115),
inference(clausify,[status(thm)],[hyp68]) ).
cnf(c_199,plain,
rselect_head(queue_115) = index_116,
inference(copy,[status(thm)],[c_198]) ).
fof(hyp69,axiom,
index_117 = s(index_116),
file('theBenchmark.p',hyp69) ).
cnf(c_200,plain,
index_117 = s(index_116),
inference(clausify,[status(thm)],[hyp69]) ).
cnf(c_201,plain,
s(index_116) = index_117,
inference(copy,[status(thm)],[c_200]) ).
fof(hyp70,axiom,
index_12 = s(index_9),
file('theBenchmark.p',hyp70) ).
cnf(c_202,plain,
index_12 = s(index_9),
inference(clausify,[status(thm)],[hyp70]) ).
cnf(c_203,plain,
s(index_9) = index_12,
inference(copy,[status(thm)],[c_202]) ).
fof(hyp71,axiom,
index_120 = rselect_tail(q24),
file('theBenchmark.p',hyp71) ).
cnf(c_204,plain,
index_120 = rselect_tail(q24),
inference(clausify,[status(thm)],[hyp71]) ).
cnf(c_205,plain,
rselect_tail(q24) = index_120,
inference(copy,[status(thm)],[c_204]) ).
fof(hyp72,axiom,
index_123 = s(index_120),
file('theBenchmark.p',hyp72) ).
cnf(c_206,plain,
index_123 = s(index_120),
inference(clausify,[status(thm)],[hyp72]) ).
cnf(c_207,plain,
s(index_120) = index_123,
inference(copy,[status(thm)],[c_206]) ).
fof(hyp73,axiom,
index_126 = rselect_tail(q25),
file('theBenchmark.p',hyp73) ).
cnf(c_208,plain,
index_126 = rselect_tail(q25),
inference(clausify,[status(thm)],[hyp73]) ).
cnf(c_209,plain,
rselect_tail(q25) = index_126,
inference(copy,[status(thm)],[c_208]) ).
fof(hyp74,axiom,
index_129 = s(index_126),
file('theBenchmark.p',hyp74) ).
cnf(c_210,plain,
index_129 = s(index_126),
inference(clausify,[status(thm)],[hyp74]) ).
cnf(c_211,plain,
s(index_126) = index_129,
inference(copy,[status(thm)],[c_210]) ).
fof(hyp75,axiom,
index_132 = rselect_tail(q26),
file('theBenchmark.p',hyp75) ).
cnf(c_212,plain,
index_132 = rselect_tail(q26),
inference(clausify,[status(thm)],[hyp75]) ).
cnf(c_213,plain,
rselect_tail(q26) = index_132,
inference(copy,[status(thm)],[c_212]) ).
fof(hyp76,axiom,
index_135 = s(index_132),
file('theBenchmark.p',hyp76) ).
cnf(c_214,plain,
index_135 = s(index_132),
inference(clausify,[status(thm)],[hyp76]) ).
cnf(c_215,plain,
s(index_132) = index_135,
inference(copy,[status(thm)],[c_214]) ).
fof(hyp77,axiom,
index_137 = rselect_head(queue_136),
file('theBenchmark.p',hyp77) ).
cnf(c_216,plain,
index_137 = rselect_head(queue_136),
inference(clausify,[status(thm)],[hyp77]) ).
cnf(c_217,plain,
rselect_head(queue_136) = index_137,
inference(copy,[status(thm)],[c_216]) ).
fof(hyp78,axiom,
index_138 = s(index_137),
file('theBenchmark.p',hyp78) ).
cnf(c_218,plain,
index_138 = s(index_137),
inference(clausify,[status(thm)],[hyp78]) ).
cnf(c_219,plain,
s(index_137) = index_138,
inference(copy,[status(thm)],[c_218]) ).
fof(hyp79,axiom,
index_141 = rselect_tail(q27),
file('theBenchmark.p',hyp79) ).
cnf(c_220,plain,
index_141 = rselect_tail(q27),
inference(clausify,[status(thm)],[hyp79]) ).
cnf(c_221,plain,
rselect_tail(q27) = index_141,
inference(copy,[status(thm)],[c_220]) ).
fof(hyp80,axiom,
index_144 = s(index_141),
file('theBenchmark.p',hyp80) ).
cnf(c_222,plain,
index_144 = s(index_141),
inference(clausify,[status(thm)],[hyp80]) ).
cnf(c_223,plain,
s(index_141) = index_144,
inference(copy,[status(thm)],[c_222]) ).
fof(hyp81,axiom,
index_147 = rselect_tail(q28),
file('theBenchmark.p',hyp81) ).
cnf(c_224,plain,
index_147 = rselect_tail(q28),
inference(clausify,[status(thm)],[hyp81]) ).
cnf(c_225,plain,
rselect_tail(q28) = index_147,
inference(copy,[status(thm)],[c_224]) ).
fof(hyp82,axiom,
index_15 = rselect_tail(q10),
file('theBenchmark.p',hyp82) ).
cnf(c_226,plain,
index_15 = rselect_tail(q10),
inference(clausify,[status(thm)],[hyp82]) ).
cnf(c_227,plain,
rselect_tail(q10) = index_15,
inference(copy,[status(thm)],[c_226]) ).
fof(hyp83,axiom,
index_150 = s(index_147),
file('theBenchmark.p',hyp83) ).
cnf(c_228,plain,
index_150 = s(index_147),
inference(clausify,[status(thm)],[hyp83]) ).
cnf(c_229,plain,
s(index_147) = index_150,
inference(copy,[status(thm)],[c_228]) ).
fof(hyp84,axiom,
index_153 = rselect_tail(q2),
file('theBenchmark.p',hyp84) ).
cnf(c_230,plain,
index_153 = rselect_tail(q2),
inference(clausify,[status(thm)],[hyp84]) ).
cnf(c_231,plain,
rselect_tail(q2) = index_153,
inference(copy,[status(thm)],[c_230]) ).
fof(hyp85,axiom,
index_156 = s(index_153),
file('theBenchmark.p',hyp85) ).
cnf(c_232,plain,
index_156 = s(index_153),
inference(clausify,[status(thm)],[hyp85]) ).
cnf(c_233,plain,
s(index_153) = index_156,
inference(copy,[status(thm)],[c_232]) ).
fof(hyp86,axiom,
index_158 = rselect_head(queue_157),
file('theBenchmark.p',hyp86) ).
cnf(c_234,plain,
index_158 = rselect_head(queue_157),
inference(clausify,[status(thm)],[hyp86]) ).
cnf(c_235,plain,
rselect_head(queue_157) = index_158,
inference(copy,[status(thm)],[c_234]) ).
fof(hyp87,axiom,
index_159 = s(index_158),
file('theBenchmark.p',hyp87) ).
cnf(c_236,plain,
index_159 = s(index_158),
inference(clausify,[status(thm)],[hyp87]) ).
cnf(c_237,plain,
s(index_158) = index_159,
inference(copy,[status(thm)],[c_236]) ).
fof(hyp88,axiom,
index_162 = rselect_tail(q29),
file('theBenchmark.p',hyp88) ).
cnf(c_238,plain,
index_162 = rselect_tail(q29),
inference(clausify,[status(thm)],[hyp88]) ).
cnf(c_239,plain,
rselect_tail(q29) = index_162,
inference(copy,[status(thm)],[c_238]) ).
fof(hyp90,axiom,
index_167 = rselect_head(queue_166),
file('theBenchmark.p',hyp90) ).
cnf(c_242,plain,
index_167 = rselect_head(queue_166),
inference(clausify,[status(thm)],[hyp90]) ).
cnf(c_243,plain,
rselect_head(queue_166) = index_167,
inference(copy,[status(thm)],[c_242]) ).
fof(hyp91,axiom,
index_168 = s(index_167),
file('theBenchmark.p',hyp91) ).
cnf(c_244,plain,
index_168 = s(index_167),
inference(clausify,[status(thm)],[hyp91]) ).
cnf(c_245,plain,
s(index_167) = index_168,
inference(copy,[status(thm)],[c_244]) ).
fof(hyp92,axiom,
index_171 = rselect_tail(q3),
file('theBenchmark.p',hyp92) ).
cnf(c_246,plain,
index_171 = rselect_tail(q3),
inference(clausify,[status(thm)],[hyp92]) ).
cnf(c_247,plain,
rselect_tail(q3) = index_171,
inference(copy,[status(thm)],[c_246]) ).
fof(hyp93,axiom,
index_174 = s(index_171),
file('theBenchmark.p',hyp93) ).
cnf(c_248,plain,
index_174 = s(index_171),
inference(clausify,[status(thm)],[hyp93]) ).
cnf(c_249,plain,
s(index_171) = index_174,
inference(copy,[status(thm)],[c_248]) ).
fof(hyp94,axiom,
index_177 = rselect_tail(q4),
file('theBenchmark.p',hyp94) ).
cnf(c_250,plain,
index_177 = rselect_tail(q4),
inference(clausify,[status(thm)],[hyp94]) ).
cnf(c_251,plain,
rselect_tail(q4) = index_177,
inference(copy,[status(thm)],[c_250]) ).
fof(hyp95,axiom,
index_18 = s(index_15),
file('theBenchmark.p',hyp95) ).
cnf(c_252,plain,
index_18 = s(index_15),
inference(clausify,[status(thm)],[hyp95]) ).
cnf(c_253,plain,
s(index_15) = index_18,
inference(copy,[status(thm)],[c_252]) ).
fof(hyp96,axiom,
index_180 = s(index_177),
file('theBenchmark.p',hyp96) ).
cnf(c_254,plain,
index_180 = s(index_177),
inference(clausify,[status(thm)],[hyp96]) ).
cnf(c_255,plain,
s(index_177) = index_180,
inference(copy,[status(thm)],[c_254]) ).
fof(hyp97,axiom,
index_183 = rselect_tail(q5),
file('theBenchmark.p',hyp97) ).
cnf(c_256,plain,
index_183 = rselect_tail(q5),
inference(clausify,[status(thm)],[hyp97]) ).
cnf(c_257,plain,
rselect_tail(q5) = index_183,
inference(copy,[status(thm)],[c_256]) ).
fof(hyp98,axiom,
index_186 = s(index_183),
file('theBenchmark.p',hyp98) ).
cnf(c_258,plain,
index_186 = s(index_183),
inference(clausify,[status(thm)],[hyp98]) ).
cnf(c_259,plain,
s(index_183) = index_186,
inference(copy,[status(thm)],[c_258]) ).
fof(hyp99,axiom,
index_188 = rselect_head(queue_187),
file('theBenchmark.p',hyp99) ).
cnf(c_260,plain,
index_188 = rselect_head(queue_187),
inference(clausify,[status(thm)],[hyp99]) ).
cnf(c_261,plain,
rselect_head(queue_187) = index_188,
inference(copy,[status(thm)],[c_260]) ).
fof(hyp100,axiom,
index_189 = s(index_188),
file('theBenchmark.p',hyp100) ).
cnf(c_262,plain,
index_189 = s(index_188),
inference(clausify,[status(thm)],[hyp100]) ).
cnf(c_263,plain,
s(index_188) = index_189,
inference(copy,[status(thm)],[c_262]) ).
fof(hyp101,axiom,
index_192 = rselect_tail(q6),
file('theBenchmark.p',hyp101) ).
cnf(c_264,plain,
index_192 = rselect_tail(q6),
inference(clausify,[status(thm)],[hyp101]) ).
cnf(c_265,plain,
rselect_tail(q6) = index_192,
inference(copy,[status(thm)],[c_264]) ).
fof(hyp102,axiom,
index_195 = s(index_192),
file('theBenchmark.p',hyp102) ).
cnf(c_266,plain,
index_195 = s(index_192),
inference(clausify,[status(thm)],[hyp102]) ).
cnf(c_267,plain,
s(index_192) = index_195,
inference(copy,[status(thm)],[c_266]) ).
fof(hyp103,axiom,
index_198 = rselect_tail(q7),
file('theBenchmark.p',hyp103) ).
cnf(c_268,plain,
index_198 = rselect_tail(q7),
inference(clausify,[status(thm)],[hyp103]) ).
cnf(c_269,plain,
rselect_tail(q7) = index_198,
inference(copy,[status(thm)],[c_268]) ).
fof(hyp104,axiom,
index_201 = s(index_198),
file('theBenchmark.p',hyp104) ).
cnf(c_270,plain,
index_201 = s(index_198),
inference(clausify,[status(thm)],[hyp104]) ).
cnf(c_271,plain,
s(index_198) = index_201,
inference(copy,[status(thm)],[c_270]) ).
fof(hyp105,axiom,
index_204 = rselect_tail(q8),
file('theBenchmark.p',hyp105) ).
cnf(c_272,plain,
index_204 = rselect_tail(q8),
inference(clausify,[status(thm)],[hyp105]) ).
cnf(c_273,plain,
rselect_tail(q8) = index_204,
inference(copy,[status(thm)],[c_272]) ).
fof(hyp106,axiom,
index_207 = s(index_204),
file('theBenchmark.p',hyp106) ).
cnf(c_274,plain,
index_207 = s(index_204),
inference(clausify,[status(thm)],[hyp106]) ).
cnf(c_275,plain,
s(index_204) = index_207,
inference(copy,[status(thm)],[c_274]) ).
fof(hyp107,axiom,
index_209 = rselect_head(queue_208),
file('theBenchmark.p',hyp107) ).
cnf(c_276,plain,
index_209 = rselect_head(queue_208),
inference(clausify,[status(thm)],[hyp107]) ).
cnf(c_277,plain,
rselect_head(queue_208) = index_209,
inference(copy,[status(thm)],[c_276]) ).
fof(hyp108,axiom,
index_21 = rselect_tail(q11),
file('theBenchmark.p',hyp108) ).
cnf(c_278,plain,
index_21 = rselect_tail(q11),
inference(clausify,[status(thm)],[hyp108]) ).
cnf(c_279,plain,
rselect_tail(q11) = index_21,
inference(copy,[status(thm)],[c_278]) ).
fof(hyp109,axiom,
index_210 = s(index_209),
file('theBenchmark.p',hyp109) ).
cnf(c_280,plain,
index_210 = s(index_209),
inference(clausify,[status(thm)],[hyp109]) ).
cnf(c_281,plain,
s(index_209) = index_210,
inference(copy,[status(thm)],[c_280]) ).
fof(hyp110,axiom,
index_213 = rselect_head(q30),
file('theBenchmark.p',hyp110) ).
cnf(c_282,plain,
index_213 = rselect_head(q30),
inference(clausify,[status(thm)],[hyp110]) ).
cnf(c_283,plain,
rselect_head(q30) = index_213,
inference(copy,[status(thm)],[c_282]) ).
fof(hyp111,axiom,
index_24 = s(index_21),
file('theBenchmark.p',hyp111) ).
cnf(c_284,plain,
index_24 = s(index_21),
inference(clausify,[status(thm)],[hyp111]) ).
cnf(c_285,plain,
s(index_21) = index_24,
inference(copy,[status(thm)],[c_284]) ).
fof(hyp112,axiom,
index_26 = rselect_head(queue_25),
file('theBenchmark.p',hyp112) ).
cnf(c_286,plain,
index_26 = rselect_head(queue_25),
inference(clausify,[status(thm)],[hyp112]) ).
cnf(c_287,plain,
rselect_head(queue_25) = index_26,
inference(copy,[status(thm)],[c_286]) ).
fof(hyp113,axiom,
index_27 = s(index_26),
file('theBenchmark.p',hyp113) ).
cnf(c_288,plain,
index_27 = s(index_26),
inference(clausify,[status(thm)],[hyp113]) ).
cnf(c_289,plain,
s(index_26) = index_27,
inference(copy,[status(thm)],[c_288]) ).
fof(hyp114,axiom,
index_3 = rselect_tail(q0),
file('theBenchmark.p',hyp114) ).
cnf(c_290,plain,
index_3 = rselect_tail(q0),
inference(clausify,[status(thm)],[hyp114]) ).
cnf(c_291,plain,
rselect_tail(q0) = index_3,
inference(copy,[status(thm)],[c_290]) ).
fof(hyp115,axiom,
index_30 = rselect_tail(q12),
file('theBenchmark.p',hyp115) ).
cnf(c_292,plain,
index_30 = rselect_tail(q12),
inference(clausify,[status(thm)],[hyp115]) ).
cnf(c_293,plain,
rselect_tail(q12) = index_30,
inference(copy,[status(thm)],[c_292]) ).
fof(hyp116,axiom,
index_33 = s(index_30),
file('theBenchmark.p',hyp116) ).
cnf(c_294,plain,
index_33 = s(index_30),
inference(clausify,[status(thm)],[hyp116]) ).
cnf(c_295,plain,
s(index_30) = index_33,
inference(copy,[status(thm)],[c_294]) ).
fof(hyp117,axiom,
index_36 = rselect_tail(q13),
file('theBenchmark.p',hyp117) ).
cnf(c_296,plain,
index_36 = rselect_tail(q13),
inference(clausify,[status(thm)],[hyp117]) ).
cnf(c_297,plain,
rselect_tail(q13) = index_36,
inference(copy,[status(thm)],[c_296]) ).
fof(hyp118,axiom,
index_39 = s(index_36),
file('theBenchmark.p',hyp118) ).
cnf(c_298,plain,
index_39 = s(index_36),
inference(clausify,[status(thm)],[hyp118]) ).
cnf(c_299,plain,
s(index_36) = index_39,
inference(copy,[status(thm)],[c_298]) ).
fof(hyp119,axiom,
index_42 = rselect_tail(q14),
file('theBenchmark.p',hyp119) ).
cnf(c_300,plain,
index_42 = rselect_tail(q14),
inference(clausify,[status(thm)],[hyp119]) ).
cnf(c_301,plain,
rselect_tail(q14) = index_42,
inference(copy,[status(thm)],[c_300]) ).
fof(hyp120,axiom,
index_45 = s(index_42),
file('theBenchmark.p',hyp120) ).
cnf(c_302,plain,
index_45 = s(index_42),
inference(clausify,[status(thm)],[hyp120]) ).
cnf(c_303,plain,
s(index_42) = index_45,
inference(copy,[status(thm)],[c_302]) ).
fof(hyp121,axiom,
index_47 = rselect_head(queue_46),
file('theBenchmark.p',hyp121) ).
cnf(c_304,plain,
index_47 = rselect_head(queue_46),
inference(clausify,[status(thm)],[hyp121]) ).
cnf(c_305,plain,
rselect_head(queue_46) = index_47,
inference(copy,[status(thm)],[c_304]) ).
fof(hyp122,axiom,
index_48 = s(index_47),
file('theBenchmark.p',hyp122) ).
cnf(c_306,plain,
index_48 = s(index_47),
inference(clausify,[status(thm)],[hyp122]) ).
cnf(c_307,plain,
s(index_47) = index_48,
inference(copy,[status(thm)],[c_306]) ).
fof(hyp123,axiom,
index_51 = rselect_tail(q15),
file('theBenchmark.p',hyp123) ).
cnf(c_308,plain,
index_51 = rselect_tail(q15),
inference(clausify,[status(thm)],[hyp123]) ).
cnf(c_309,plain,
rselect_tail(q15) = index_51,
inference(copy,[status(thm)],[c_308]) ).
fof(hyp124,axiom,
index_54 = s(index_51),
file('theBenchmark.p',hyp124) ).
cnf(c_310,plain,
index_54 = s(index_51),
inference(clausify,[status(thm)],[hyp124]) ).
cnf(c_311,plain,
s(index_51) = index_54,
inference(copy,[status(thm)],[c_310]) ).
fof(hyp125,axiom,
index_57 = rselect_tail(q16),
file('theBenchmark.p',hyp125) ).
cnf(c_312,plain,
index_57 = rselect_tail(q16),
inference(clausify,[status(thm)],[hyp125]) ).
cnf(c_313,plain,
rselect_tail(q16) = index_57,
inference(copy,[status(thm)],[c_312]) ).
fof(hyp126,axiom,
index_6 = s(index_3),
file('theBenchmark.p',hyp126) ).
cnf(c_314,plain,
index_6 = s(index_3),
inference(clausify,[status(thm)],[hyp126]) ).
cnf(c_315,plain,
s(index_3) = index_6,
inference(copy,[status(thm)],[c_314]) ).
fof(hyp127,axiom,
index_60 = s(index_57),
file('theBenchmark.p',hyp127) ).
cnf(c_316,plain,
index_60 = s(index_57),
inference(clausify,[status(thm)],[hyp127]) ).
cnf(c_317,plain,
s(index_57) = index_60,
inference(copy,[status(thm)],[c_316]) ).
fof(hyp128,axiom,
index_63 = rselect_tail(q17),
file('theBenchmark.p',hyp128) ).
cnf(c_318,plain,
index_63 = rselect_tail(q17),
inference(clausify,[status(thm)],[hyp128]) ).
cnf(c_319,plain,
rselect_tail(q17) = index_63,
inference(copy,[status(thm)],[c_318]) ).
fof(hyp129,axiom,
index_66 = s(index_63),
file('theBenchmark.p',hyp129) ).
cnf(c_320,plain,
index_66 = s(index_63),
inference(clausify,[status(thm)],[hyp129]) ).
cnf(c_321,plain,
s(index_63) = index_66,
inference(copy,[status(thm)],[c_320]) ).
fof(hyp130,axiom,
index_68 = rselect_head(queue_67),
file('theBenchmark.p',hyp130) ).
cnf(c_322,plain,
index_68 = rselect_head(queue_67),
inference(clausify,[status(thm)],[hyp130]) ).
cnf(c_323,plain,
rselect_head(queue_67) = index_68,
inference(copy,[status(thm)],[c_322]) ).
fof(hyp131,axiom,
index_69 = s(index_68),
file('theBenchmark.p',hyp131) ).
cnf(c_324,plain,
index_69 = s(index_68),
inference(clausify,[status(thm)],[hyp131]) ).
cnf(c_325,plain,
s(index_68) = index_69,
inference(copy,[status(thm)],[c_324]) ).
fof(hyp132,axiom,
index_72 = rselect_tail(q18),
file('theBenchmark.p',hyp132) ).
cnf(c_326,plain,
index_72 = rselect_tail(q18),
inference(clausify,[status(thm)],[hyp132]) ).
cnf(c_327,plain,
rselect_tail(q18) = index_72,
inference(copy,[status(thm)],[c_326]) ).
fof(hyp133,axiom,
index_75 = s(index_72),
file('theBenchmark.p',hyp133) ).
cnf(c_328,plain,
index_75 = s(index_72),
inference(clausify,[status(thm)],[hyp133]) ).
cnf(c_329,plain,
s(index_72) = index_75,
inference(copy,[status(thm)],[c_328]) ).
fof(hyp134,axiom,
index_78 = rselect_tail(q1),
file('theBenchmark.p',hyp134) ).
cnf(c_330,plain,
index_78 = rselect_tail(q1),
inference(clausify,[status(thm)],[hyp134]) ).
cnf(c_331,plain,
rselect_tail(q1) = index_78,
inference(copy,[status(thm)],[c_330]) ).
fof(hyp135,axiom,
index_81 = s(index_78),
file('theBenchmark.p',hyp135) ).
cnf(c_332,plain,
index_81 = s(index_78),
inference(clausify,[status(thm)],[hyp135]) ).
cnf(c_333,plain,
s(index_78) = index_81,
inference(copy,[status(thm)],[c_332]) ).
fof(hyp136,axiom,
index_84 = rselect_tail(q19),
file('theBenchmark.p',hyp136) ).
cnf(c_334,plain,
index_84 = rselect_tail(q19),
inference(clausify,[status(thm)],[hyp136]) ).
cnf(c_335,plain,
rselect_tail(q19) = index_84,
inference(copy,[status(thm)],[c_334]) ).
fof(hyp137,axiom,
index_87 = s(index_84),
file('theBenchmark.p',hyp137) ).
cnf(c_336,plain,
index_87 = s(index_84),
inference(clausify,[status(thm)],[hyp137]) ).
cnf(c_337,plain,
s(index_84) = index_87,
inference(copy,[status(thm)],[c_336]) ).
fof(hyp138,axiom,
index_9 = rselect_tail(q9),
file('theBenchmark.p',hyp138) ).
cnf(c_338,plain,
index_9 = rselect_tail(q9),
inference(clausify,[status(thm)],[hyp138]) ).
cnf(c_339,plain,
rselect_tail(q9) = index_9,
inference(copy,[status(thm)],[c_338]) ).
fof(hyp139,axiom,
index_90 = rselect_tail(q20),
file('theBenchmark.p',hyp139) ).
cnf(c_340,plain,
index_90 = rselect_tail(q20),
inference(clausify,[status(thm)],[hyp139]) ).
cnf(c_341,plain,
rselect_tail(q20) = index_90,
inference(copy,[status(thm)],[c_340]) ).
fof(hyp140,axiom,
index_93 = s(index_90),
file('theBenchmark.p',hyp140) ).
cnf(c_342,plain,
index_93 = s(index_90),
inference(clausify,[status(thm)],[hyp140]) ).
cnf(c_343,plain,
s(index_90) = index_93,
inference(copy,[status(thm)],[c_342]) ).
fof(hyp141,axiom,
index_95 = rselect_head(queue_94),
file('theBenchmark.p',hyp141) ).
cnf(c_344,plain,
index_95 = rselect_head(queue_94),
inference(clausify,[status(thm)],[hyp141]) ).
cnf(c_345,plain,
rselect_head(queue_94) = index_95,
inference(copy,[status(thm)],[c_344]) ).
fof(hyp142,axiom,
index_96 = s(index_95),
file('theBenchmark.p',hyp142) ).
cnf(c_346,plain,
index_96 = s(index_95),
inference(clausify,[status(thm)],[hyp142]) ).
cnf(c_347,plain,
s(index_95) = index_96,
inference(copy,[status(thm)],[c_346]) ).
fof(hyp143,axiom,
index_99 = rselect_tail(q21),
file('theBenchmark.p',hyp143) ).
cnf(c_348,plain,
index_99 = rselect_tail(q21),
inference(clausify,[status(thm)],[hyp143]) ).
cnf(c_349,plain,
rselect_tail(q21) = index_99,
inference(copy,[status(thm)],[c_348]) ).
fof(hyp144,axiom,
queue_1 = rstore_head(q,index_0),
file('theBenchmark.p',hyp144) ).
cnf(c_350,plain,
queue_1 = rstore_head(q,index_0),
inference(clausify,[status(thm)],[hyp144]) ).
cnf(c_351,plain,
rstore_head(q,index_0) = queue_1,
inference(copy,[status(thm)],[c_350]) ).
fof(hyp145,axiom,
queue_101 = rstore_seq(q21,earray_100),
file('theBenchmark.p',hyp145) ).
cnf(c_352,plain,
queue_101 = rstore_seq(q21,earray_100),
inference(clausify,[status(thm)],[hyp145]) ).
cnf(c_353,plain,
rstore_seq(q21,earray_100) = queue_101,
inference(copy,[status(thm)],[c_352]) ).
fof(hyp146,axiom,
queue_103 = rstore_tail(queue_101,index_102),
file('theBenchmark.p',hyp146) ).
cnf(c_354,plain,
queue_103 = rstore_tail(queue_101,index_102),
inference(clausify,[status(thm)],[hyp146]) ).
cnf(c_355,plain,
rstore_tail(queue_101,index_102) = queue_103,
inference(copy,[status(thm)],[c_354]) ).
fof(hyp147,axiom,
queue_107 = rstore_seq(q22,earray_106),
file('theBenchmark.p',hyp147) ).
cnf(c_356,plain,
queue_107 = rstore_seq(q22,earray_106),
inference(clausify,[status(thm)],[hyp147]) ).
cnf(c_357,plain,
rstore_seq(q22,earray_106) = queue_107,
inference(copy,[status(thm)],[c_356]) ).
fof(hyp148,axiom,
queue_109 = rstore_tail(queue_107,index_108),
file('theBenchmark.p',hyp148) ).
cnf(c_358,plain,
queue_109 = rstore_tail(queue_107,index_108),
inference(clausify,[status(thm)],[hyp148]) ).
cnf(c_359,plain,
rstore_tail(queue_107,index_108) = queue_109,
inference(copy,[status(thm)],[c_358]) ).
fof(hyp149,axiom,
queue_11 = rstore_seq(q9,earray_10),
file('theBenchmark.p',hyp149) ).
cnf(c_360,plain,
queue_11 = rstore_seq(q9,earray_10),
inference(clausify,[status(thm)],[hyp149]) ).
cnf(c_361,plain,
rstore_seq(q9,earray_10) = queue_11,
inference(copy,[status(thm)],[c_360]) ).
fof(hyp150,axiom,
queue_113 = rstore_seq(q23,earray_112),
file('theBenchmark.p',hyp150) ).
cnf(c_362,plain,
queue_113 = rstore_seq(q23,earray_112),
inference(clausify,[status(thm)],[hyp150]) ).
cnf(c_363,plain,
rstore_seq(q23,earray_112) = queue_113,
inference(copy,[status(thm)],[c_362]) ).
fof(hyp151,axiom,
queue_115 = rstore_tail(queue_113,index_114),
file('theBenchmark.p',hyp151) ).
cnf(c_364,plain,
queue_115 = rstore_tail(queue_113,index_114),
inference(clausify,[status(thm)],[hyp151]) ).
cnf(c_365,plain,
rstore_tail(queue_113,index_114) = queue_115,
inference(copy,[status(thm)],[c_364]) ).
fof(hyp152,axiom,
queue_118 = rstore_head(queue_115,index_117),
file('theBenchmark.p',hyp152) ).
cnf(c_366,plain,
queue_118 = rstore_head(queue_115,index_117),
inference(clausify,[status(thm)],[hyp152]) ).
cnf(c_367,plain,
rstore_head(queue_115,index_117) = queue_118,
inference(copy,[status(thm)],[c_366]) ).
fof(hyp153,axiom,
queue_122 = rstore_seq(q24,earray_121),
file('theBenchmark.p',hyp153) ).
cnf(c_368,plain,
queue_122 = rstore_seq(q24,earray_121),
inference(clausify,[status(thm)],[hyp153]) ).
cnf(c_369,plain,
rstore_seq(q24,earray_121) = queue_122,
inference(copy,[status(thm)],[c_368]) ).
fof(hyp154,axiom,
queue_124 = rstore_tail(queue_122,index_123),
file('theBenchmark.p',hyp154) ).
cnf(c_370,plain,
queue_124 = rstore_tail(queue_122,index_123),
inference(clausify,[status(thm)],[hyp154]) ).
cnf(c_371,plain,
rstore_tail(queue_122,index_123) = queue_124,
inference(copy,[status(thm)],[c_370]) ).
fof(hyp155,axiom,
queue_128 = rstore_seq(q25,earray_127),
file('theBenchmark.p',hyp155) ).
cnf(c_372,plain,
queue_128 = rstore_seq(q25,earray_127),
inference(clausify,[status(thm)],[hyp155]) ).
cnf(c_373,plain,
rstore_seq(q25,earray_127) = queue_128,
inference(copy,[status(thm)],[c_372]) ).
fof(hyp156,axiom,
queue_13 = rstore_tail(queue_11,index_12),
file('theBenchmark.p',hyp156) ).
cnf(c_374,plain,
queue_13 = rstore_tail(queue_11,index_12),
inference(clausify,[status(thm)],[hyp156]) ).
cnf(c_375,plain,
rstore_tail(queue_11,index_12) = queue_13,
inference(copy,[status(thm)],[c_374]) ).
fof(hyp157,axiom,
queue_130 = rstore_tail(queue_128,index_129),
file('theBenchmark.p',hyp157) ).
cnf(c_376,plain,
queue_130 = rstore_tail(queue_128,index_129),
inference(clausify,[status(thm)],[hyp157]) ).
cnf(c_377,plain,
rstore_tail(queue_128,index_129) = queue_130,
inference(copy,[status(thm)],[c_376]) ).
fof(hyp158,axiom,
queue_134 = rstore_seq(q26,earray_133),
file('theBenchmark.p',hyp158) ).
cnf(c_378,plain,
queue_134 = rstore_seq(q26,earray_133),
inference(clausify,[status(thm)],[hyp158]) ).
cnf(c_379,plain,
rstore_seq(q26,earray_133) = queue_134,
inference(copy,[status(thm)],[c_378]) ).
fof(hyp159,axiom,
queue_136 = rstore_tail(queue_134,index_135),
file('theBenchmark.p',hyp159) ).
cnf(c_380,plain,
queue_136 = rstore_tail(queue_134,index_135),
inference(clausify,[status(thm)],[hyp159]) ).
cnf(c_381,plain,
rstore_tail(queue_134,index_135) = queue_136,
inference(copy,[status(thm)],[c_380]) ).
fof(hyp160,axiom,
queue_139 = rstore_head(queue_136,index_138),
file('theBenchmark.p',hyp160) ).
cnf(c_382,plain,
queue_139 = rstore_head(queue_136,index_138),
inference(clausify,[status(thm)],[hyp160]) ).
cnf(c_383,plain,
rstore_head(queue_136,index_138) = queue_139,
inference(copy,[status(thm)],[c_382]) ).
fof(hyp161,axiom,
queue_143 = rstore_seq(q27,earray_142),
file('theBenchmark.p',hyp161) ).
cnf(c_384,plain,
queue_143 = rstore_seq(q27,earray_142),
inference(clausify,[status(thm)],[hyp161]) ).
cnf(c_385,plain,
rstore_seq(q27,earray_142) = queue_143,
inference(copy,[status(thm)],[c_384]) ).
fof(hyp162,axiom,
queue_145 = rstore_tail(queue_143,index_144),
file('theBenchmark.p',hyp162) ).
cnf(c_386,plain,
queue_145 = rstore_tail(queue_143,index_144),
inference(clausify,[status(thm)],[hyp162]) ).
cnf(c_387,plain,
rstore_tail(queue_143,index_144) = queue_145,
inference(copy,[status(thm)],[c_386]) ).
fof(hyp163,axiom,
queue_149 = rstore_seq(q28,earray_148),
file('theBenchmark.p',hyp163) ).
cnf(c_388,plain,
queue_149 = rstore_seq(q28,earray_148),
inference(clausify,[status(thm)],[hyp163]) ).
cnf(c_389,plain,
rstore_seq(q28,earray_148) = queue_149,
inference(copy,[status(thm)],[c_388]) ).
fof(hyp164,axiom,
queue_151 = rstore_tail(queue_149,index_150),
file('theBenchmark.p',hyp164) ).
cnf(c_390,plain,
queue_151 = rstore_tail(queue_149,index_150),
inference(clausify,[status(thm)],[hyp164]) ).
cnf(c_391,plain,
rstore_tail(queue_149,index_150) = queue_151,
inference(copy,[status(thm)],[c_390]) ).
fof(hyp165,axiom,
queue_155 = rstore_seq(q2,earray_154),
file('theBenchmark.p',hyp165) ).
cnf(c_392,plain,
queue_155 = rstore_seq(q2,earray_154),
inference(clausify,[status(thm)],[hyp165]) ).
cnf(c_393,plain,
rstore_seq(q2,earray_154) = queue_155,
inference(copy,[status(thm)],[c_392]) ).
fof(hyp166,axiom,
queue_157 = rstore_tail(queue_155,index_156),
file('theBenchmark.p',hyp166) ).
cnf(c_394,plain,
queue_157 = rstore_tail(queue_155,index_156),
inference(clausify,[status(thm)],[hyp166]) ).
cnf(c_395,plain,
rstore_tail(queue_155,index_156) = queue_157,
inference(copy,[status(thm)],[c_394]) ).
fof(hyp167,axiom,
queue_160 = rstore_head(queue_157,index_159),
file('theBenchmark.p',hyp167) ).
cnf(c_396,plain,
queue_160 = rstore_head(queue_157,index_159),
inference(clausify,[status(thm)],[hyp167]) ).
cnf(c_397,plain,
rstore_head(queue_157,index_159) = queue_160,
inference(copy,[status(thm)],[c_396]) ).
fof(hyp168,axiom,
queue_164 = rstore_seq(q29,earray_163),
file('theBenchmark.p',hyp168) ).
cnf(c_398,plain,
queue_164 = rstore_seq(q29,earray_163),
inference(clausify,[status(thm)],[hyp168]) ).
cnf(c_399,plain,
rstore_seq(q29,earray_163) = queue_164,
inference(copy,[status(thm)],[c_398]) ).
fof(hyp169,axiom,
queue_166 = rstore_tail(queue_164,index_165),
file('theBenchmark.p',hyp169) ).
cnf(c_400,plain,
queue_166 = rstore_tail(queue_164,index_165),
inference(clausify,[status(thm)],[hyp169]) ).
cnf(c_401,plain,
rstore_tail(queue_164,index_165) = queue_166,
inference(copy,[status(thm)],[c_400]) ).
fof(hyp170,axiom,
queue_169 = rstore_head(queue_166,index_168),
file('theBenchmark.p',hyp170) ).
cnf(c_402,plain,
queue_169 = rstore_head(queue_166,index_168),
inference(clausify,[status(thm)],[hyp170]) ).
cnf(c_403,plain,
rstore_head(queue_166,index_168) = queue_169,
inference(copy,[status(thm)],[c_402]) ).
fof(hyp171,axiom,
queue_17 = rstore_seq(q10,earray_16),
file('theBenchmark.p',hyp171) ).
cnf(c_404,plain,
queue_17 = rstore_seq(q10,earray_16),
inference(clausify,[status(thm)],[hyp171]) ).
cnf(c_405,plain,
rstore_seq(q10,earray_16) = queue_17,
inference(copy,[status(thm)],[c_404]) ).
fof(hyp172,axiom,
queue_173 = rstore_seq(q3,earray_172),
file('theBenchmark.p',hyp172) ).
cnf(c_406,plain,
queue_173 = rstore_seq(q3,earray_172),
inference(clausify,[status(thm)],[hyp172]) ).
cnf(c_407,plain,
rstore_seq(q3,earray_172) = queue_173,
inference(copy,[status(thm)],[c_406]) ).
fof(hyp173,axiom,
queue_175 = rstore_tail(queue_173,index_174),
file('theBenchmark.p',hyp173) ).
cnf(c_408,plain,
queue_175 = rstore_tail(queue_173,index_174),
inference(clausify,[status(thm)],[hyp173]) ).
cnf(c_409,plain,
rstore_tail(queue_173,index_174) = queue_175,
inference(copy,[status(thm)],[c_408]) ).
fof(hyp174,axiom,
queue_179 = rstore_seq(q4,earray_178),
file('theBenchmark.p',hyp174) ).
cnf(c_410,plain,
queue_179 = rstore_seq(q4,earray_178),
inference(clausify,[status(thm)],[hyp174]) ).
cnf(c_411,plain,
rstore_seq(q4,earray_178) = queue_179,
inference(copy,[status(thm)],[c_410]) ).
fof(hyp175,axiom,
queue_181 = rstore_tail(queue_179,index_180),
file('theBenchmark.p',hyp175) ).
cnf(c_412,plain,
queue_181 = rstore_tail(queue_179,index_180),
inference(clausify,[status(thm)],[hyp175]) ).
cnf(c_413,plain,
rstore_tail(queue_179,index_180) = queue_181,
inference(copy,[status(thm)],[c_412]) ).
fof(hyp176,axiom,
queue_185 = rstore_seq(q5,earray_184),
file('theBenchmark.p',hyp176) ).
cnf(c_414,plain,
queue_185 = rstore_seq(q5,earray_184),
inference(clausify,[status(thm)],[hyp176]) ).
cnf(c_415,plain,
rstore_seq(q5,earray_184) = queue_185,
inference(copy,[status(thm)],[c_414]) ).
fof(hyp177,axiom,
queue_187 = rstore_tail(queue_185,index_186),
file('theBenchmark.p',hyp177) ).
cnf(c_416,plain,
queue_187 = rstore_tail(queue_185,index_186),
inference(clausify,[status(thm)],[hyp177]) ).
cnf(c_417,plain,
rstore_tail(queue_185,index_186) = queue_187,
inference(copy,[status(thm)],[c_416]) ).
fof(hyp178,axiom,
queue_19 = rstore_tail(queue_17,index_18),
file('theBenchmark.p',hyp178) ).
cnf(c_418,plain,
queue_19 = rstore_tail(queue_17,index_18),
inference(clausify,[status(thm)],[hyp178]) ).
cnf(c_419,plain,
rstore_tail(queue_17,index_18) = queue_19,
inference(copy,[status(thm)],[c_418]) ).
fof(hyp179,axiom,
queue_190 = rstore_head(queue_187,index_189),
file('theBenchmark.p',hyp179) ).
cnf(c_420,plain,
queue_190 = rstore_head(queue_187,index_189),
inference(clausify,[status(thm)],[hyp179]) ).
cnf(c_421,plain,
rstore_head(queue_187,index_189) = queue_190,
inference(copy,[status(thm)],[c_420]) ).
fof(hyp180,axiom,
queue_194 = rstore_seq(q6,earray_193),
file('theBenchmark.p',hyp180) ).
cnf(c_422,plain,
queue_194 = rstore_seq(q6,earray_193),
inference(clausify,[status(thm)],[hyp180]) ).
cnf(c_423,plain,
rstore_seq(q6,earray_193) = queue_194,
inference(copy,[status(thm)],[c_422]) ).
fof(hyp181,axiom,
queue_196 = rstore_tail(queue_194,index_195),
file('theBenchmark.p',hyp181) ).
cnf(c_424,plain,
queue_196 = rstore_tail(queue_194,index_195),
inference(clausify,[status(thm)],[hyp181]) ).
cnf(c_425,plain,
rstore_tail(queue_194,index_195) = queue_196,
inference(copy,[status(thm)],[c_424]) ).
fof(hyp182,axiom,
queue_200 = rstore_seq(q7,earray_199),
file('theBenchmark.p',hyp182) ).
cnf(c_426,plain,
queue_200 = rstore_seq(q7,earray_199),
inference(clausify,[status(thm)],[hyp182]) ).
cnf(c_427,plain,
rstore_seq(q7,earray_199) = queue_200,
inference(copy,[status(thm)],[c_426]) ).
fof(hyp183,axiom,
queue_202 = rstore_tail(queue_200,index_201),
file('theBenchmark.p',hyp183) ).
cnf(c_428,plain,
queue_202 = rstore_tail(queue_200,index_201),
inference(clausify,[status(thm)],[hyp183]) ).
cnf(c_429,plain,
rstore_tail(queue_200,index_201) = queue_202,
inference(copy,[status(thm)],[c_428]) ).
fof(hyp184,axiom,
queue_206 = rstore_seq(q8,earray_205),
file('theBenchmark.p',hyp184) ).
cnf(c_430,plain,
queue_206 = rstore_seq(q8,earray_205),
inference(clausify,[status(thm)],[hyp184]) ).
cnf(c_431,plain,
rstore_seq(q8,earray_205) = queue_206,
inference(copy,[status(thm)],[c_430]) ).
fof(hyp185,axiom,
queue_208 = rstore_tail(queue_206,index_207),
file('theBenchmark.p',hyp185) ).
cnf(c_432,plain,
queue_208 = rstore_tail(queue_206,index_207),
inference(clausify,[status(thm)],[hyp185]) ).
cnf(c_433,plain,
rstore_tail(queue_206,index_207) = queue_208,
inference(copy,[status(thm)],[c_432]) ).
fof(hyp186,axiom,
queue_211 = rstore_head(queue_208,index_210),
file('theBenchmark.p',hyp186) ).
cnf(c_434,plain,
queue_211 = rstore_head(queue_208,index_210),
inference(clausify,[status(thm)],[hyp186]) ).
cnf(c_435,plain,
rstore_head(queue_208,index_210) = queue_211,
inference(copy,[status(thm)],[c_434]) ).
fof(hyp187,axiom,
queue_23 = rstore_seq(q11,earray_22),
file('theBenchmark.p',hyp187) ).
cnf(c_436,plain,
queue_23 = rstore_seq(q11,earray_22),
inference(clausify,[status(thm)],[hyp187]) ).
cnf(c_437,plain,
rstore_seq(q11,earray_22) = queue_23,
inference(copy,[status(thm)],[c_436]) ).
fof(hyp188,axiom,
queue_25 = rstore_tail(queue_23,index_24),
file('theBenchmark.p',hyp188) ).
cnf(c_438,plain,
queue_25 = rstore_tail(queue_23,index_24),
inference(clausify,[status(thm)],[hyp188]) ).
cnf(c_439,plain,
rstore_tail(queue_23,index_24) = queue_25,
inference(copy,[status(thm)],[c_438]) ).
fof(hyp189,axiom,
queue_28 = rstore_head(queue_25,index_27),
file('theBenchmark.p',hyp189) ).
cnf(c_440,plain,
queue_28 = rstore_head(queue_25,index_27),
inference(clausify,[status(thm)],[hyp189]) ).
cnf(c_441,plain,
rstore_head(queue_25,index_27) = queue_28,
inference(copy,[status(thm)],[c_440]) ).
fof(hyp190,axiom,
queue_32 = rstore_seq(q12,earray_31),
file('theBenchmark.p',hyp190) ).
cnf(c_442,plain,
queue_32 = rstore_seq(q12,earray_31),
inference(clausify,[status(thm)],[hyp190]) ).
cnf(c_443,plain,
rstore_seq(q12,earray_31) = queue_32,
inference(copy,[status(thm)],[c_442]) ).
fof(hyp191,axiom,
queue_34 = rstore_tail(queue_32,index_33),
file('theBenchmark.p',hyp191) ).
cnf(c_444,plain,
queue_34 = rstore_tail(queue_32,index_33),
inference(clausify,[status(thm)],[hyp191]) ).
cnf(c_445,plain,
rstore_tail(queue_32,index_33) = queue_34,
inference(copy,[status(thm)],[c_444]) ).
fof(hyp192,axiom,
queue_38 = rstore_seq(q13,earray_37),
file('theBenchmark.p',hyp192) ).
cnf(c_446,plain,
queue_38 = rstore_seq(q13,earray_37),
inference(clausify,[status(thm)],[hyp192]) ).
cnf(c_447,plain,
rstore_seq(q13,earray_37) = queue_38,
inference(copy,[status(thm)],[c_446]) ).
fof(hyp193,axiom,
queue_40 = rstore_tail(queue_38,index_39),
file('theBenchmark.p',hyp193) ).
cnf(c_448,plain,
queue_40 = rstore_tail(queue_38,index_39),
inference(clausify,[status(thm)],[hyp193]) ).
cnf(c_449,plain,
rstore_tail(queue_38,index_39) = queue_40,
inference(copy,[status(thm)],[c_448]) ).
fof(hyp194,axiom,
queue_44 = rstore_seq(q14,earray_43),
file('theBenchmark.p',hyp194) ).
cnf(c_450,plain,
queue_44 = rstore_seq(q14,earray_43),
inference(clausify,[status(thm)],[hyp194]) ).
cnf(c_451,plain,
rstore_seq(q14,earray_43) = queue_44,
inference(copy,[status(thm)],[c_450]) ).
fof(hyp195,axiom,
queue_46 = rstore_tail(queue_44,index_45),
file('theBenchmark.p',hyp195) ).
cnf(c_452,plain,
queue_46 = rstore_tail(queue_44,index_45),
inference(clausify,[status(thm)],[hyp195]) ).
cnf(c_453,plain,
rstore_tail(queue_44,index_45) = queue_46,
inference(copy,[status(thm)],[c_452]) ).
fof(hyp196,axiom,
queue_49 = rstore_head(queue_46,index_48),
file('theBenchmark.p',hyp196) ).
cnf(c_454,plain,
queue_49 = rstore_head(queue_46,index_48),
inference(clausify,[status(thm)],[hyp196]) ).
cnf(c_455,plain,
rstore_head(queue_46,index_48) = queue_49,
inference(copy,[status(thm)],[c_454]) ).
fof(hyp197,axiom,
queue_5 = rstore_seq(q0,earray_4),
file('theBenchmark.p',hyp197) ).
cnf(c_456,plain,
queue_5 = rstore_seq(q0,earray_4),
inference(clausify,[status(thm)],[hyp197]) ).
cnf(c_457,plain,
rstore_seq(q0,earray_4) = queue_5,
inference(copy,[status(thm)],[c_456]) ).
fof(hyp198,axiom,
queue_53 = rstore_seq(q15,earray_52),
file('theBenchmark.p',hyp198) ).
cnf(c_458,plain,
queue_53 = rstore_seq(q15,earray_52),
inference(clausify,[status(thm)],[hyp198]) ).
cnf(c_459,plain,
rstore_seq(q15,earray_52) = queue_53,
inference(copy,[status(thm)],[c_458]) ).
fof(hyp199,axiom,
queue_55 = rstore_tail(queue_53,index_54),
file('theBenchmark.p',hyp199) ).
cnf(c_460,plain,
queue_55 = rstore_tail(queue_53,index_54),
inference(clausify,[status(thm)],[hyp199]) ).
cnf(c_461,plain,
rstore_tail(queue_53,index_54) = queue_55,
inference(copy,[status(thm)],[c_460]) ).
fof(hyp200,axiom,
queue_59 = rstore_seq(q16,earray_58),
file('theBenchmark.p',hyp200) ).
cnf(c_462,plain,
queue_59 = rstore_seq(q16,earray_58),
inference(clausify,[status(thm)],[hyp200]) ).
cnf(c_463,plain,
rstore_seq(q16,earray_58) = queue_59,
inference(copy,[status(thm)],[c_462]) ).
fof(hyp201,axiom,
queue_61 = rstore_tail(queue_59,index_60),
file('theBenchmark.p',hyp201) ).
cnf(c_464,plain,
queue_61 = rstore_tail(queue_59,index_60),
inference(clausify,[status(thm)],[hyp201]) ).
cnf(c_465,plain,
rstore_tail(queue_59,index_60) = queue_61,
inference(copy,[status(thm)],[c_464]) ).
fof(hyp202,axiom,
queue_65 = rstore_seq(q17,earray_64),
file('theBenchmark.p',hyp202) ).
cnf(c_466,plain,
queue_65 = rstore_seq(q17,earray_64),
inference(clausify,[status(thm)],[hyp202]) ).
cnf(c_467,plain,
rstore_seq(q17,earray_64) = queue_65,
inference(copy,[status(thm)],[c_466]) ).
fof(hyp203,axiom,
queue_67 = rstore_tail(queue_65,index_66),
file('theBenchmark.p',hyp203) ).
cnf(c_468,plain,
queue_67 = rstore_tail(queue_65,index_66),
inference(clausify,[status(thm)],[hyp203]) ).
cnf(c_469,plain,
rstore_tail(queue_65,index_66) = queue_67,
inference(copy,[status(thm)],[c_468]) ).
fof(hyp204,axiom,
queue_7 = rstore_tail(queue_5,index_6),
file('theBenchmark.p',hyp204) ).
cnf(c_470,plain,
queue_7 = rstore_tail(queue_5,index_6),
inference(clausify,[status(thm)],[hyp204]) ).
cnf(c_471,plain,
rstore_tail(queue_5,index_6) = queue_7,
inference(copy,[status(thm)],[c_470]) ).
fof(hyp205,axiom,
queue_70 = rstore_head(queue_67,index_69),
file('theBenchmark.p',hyp205) ).
cnf(c_472,plain,
queue_70 = rstore_head(queue_67,index_69),
inference(clausify,[status(thm)],[hyp205]) ).
cnf(c_473,plain,
rstore_head(queue_67,index_69) = queue_70,
inference(copy,[status(thm)],[c_472]) ).
fof(hyp206,axiom,
queue_74 = rstore_seq(q18,earray_73),
file('theBenchmark.p',hyp206) ).
cnf(c_474,plain,
queue_74 = rstore_seq(q18,earray_73),
inference(clausify,[status(thm)],[hyp206]) ).
cnf(c_475,plain,
rstore_seq(q18,earray_73) = queue_74,
inference(copy,[status(thm)],[c_474]) ).
fof(hyp207,axiom,
queue_76 = rstore_tail(queue_74,index_75),
file('theBenchmark.p',hyp207) ).
cnf(c_476,plain,
queue_76 = rstore_tail(queue_74,index_75),
inference(clausify,[status(thm)],[hyp207]) ).
cnf(c_477,plain,
rstore_tail(queue_74,index_75) = queue_76,
inference(copy,[status(thm)],[c_476]) ).
fof(hyp208,axiom,
queue_80 = rstore_seq(q1,earray_79),
file('theBenchmark.p',hyp208) ).
cnf(c_478,plain,
queue_80 = rstore_seq(q1,earray_79),
inference(clausify,[status(thm)],[hyp208]) ).
cnf(c_479,plain,
rstore_seq(q1,earray_79) = queue_80,
inference(copy,[status(thm)],[c_478]) ).
fof(hyp209,axiom,
queue_82 = rstore_tail(queue_80,index_81),
file('theBenchmark.p',hyp209) ).
cnf(c_480,plain,
queue_82 = rstore_tail(queue_80,index_81),
inference(clausify,[status(thm)],[hyp209]) ).
cnf(c_481,plain,
rstore_tail(queue_80,index_81) = queue_82,
inference(copy,[status(thm)],[c_480]) ).
fof(hyp210,axiom,
queue_86 = rstore_seq(q19,earray_85),
file('theBenchmark.p',hyp210) ).
cnf(c_482,plain,
queue_86 = rstore_seq(q19,earray_85),
inference(clausify,[status(thm)],[hyp210]) ).
cnf(c_483,plain,
rstore_seq(q19,earray_85) = queue_86,
inference(copy,[status(thm)],[c_482]) ).
fof(hyp211,axiom,
queue_88 = rstore_tail(queue_86,index_87),
file('theBenchmark.p',hyp211) ).
cnf(c_484,plain,
queue_88 = rstore_tail(queue_86,index_87),
inference(clausify,[status(thm)],[hyp211]) ).
cnf(c_485,plain,
rstore_tail(queue_86,index_87) = queue_88,
inference(copy,[status(thm)],[c_484]) ).
fof(hyp212,axiom,
queue_92 = rstore_seq(q20,earray_91),
file('theBenchmark.p',hyp212) ).
cnf(c_486,plain,
queue_92 = rstore_seq(q20,earray_91),
inference(clausify,[status(thm)],[hyp212]) ).
cnf(c_487,plain,
rstore_seq(q20,earray_91) = queue_92,
inference(copy,[status(thm)],[c_486]) ).
fof(hyp213,axiom,
queue_94 = rstore_tail(queue_92,index_93),
file('theBenchmark.p',hyp213) ).
cnf(c_488,plain,
queue_94 = rstore_tail(queue_92,index_93),
inference(clausify,[status(thm)],[hyp213]) ).
cnf(c_489,plain,
rstore_tail(queue_92,index_93) = queue_94,
inference(copy,[status(thm)],[c_488]) ).
fof(hyp214,axiom,
queue_97 = rstore_head(queue_94,index_96),
file('theBenchmark.p',hyp214) ).
cnf(c_490,plain,
queue_97 = rstore_head(queue_94,index_96),
inference(clausify,[status(thm)],[hyp214]) ).
cnf(c_491,plain,
rstore_head(queue_94,index_96) = queue_97,
inference(copy,[status(thm)],[c_490]) ).
fof(hyp215,axiom,
q0 = queue_1,
file('theBenchmark.p',hyp215) ).
cnf(c_492,plain,
q0 = queue_1,
inference(clausify,[status(thm)],[hyp215]) ).
cnf(c_493,plain,
queue_1 = q0,
inference(copy,[status(thm)],[c_492]) ).
fof(hyp216,axiom,
q1 = queue_7,
file('theBenchmark.p',hyp216) ).
cnf(c_494,plain,
q1 = queue_7,
inference(clausify,[status(thm)],[hyp216]) ).
cnf(c_495,plain,
queue_7 = q1,
inference(copy,[status(thm)],[c_494]) ).
fof(hyp217,axiom,
q10 = queue_13,
file('theBenchmark.p',hyp217) ).
cnf(c_496,plain,
q10 = queue_13,
inference(clausify,[status(thm)],[hyp217]) ).
cnf(c_497,plain,
queue_13 = q10,
inference(copy,[status(thm)],[c_496]) ).
fof(hyp218,axiom,
q11 = queue_19,
file('theBenchmark.p',hyp218) ).
cnf(c_498,plain,
q11 = queue_19,
inference(clausify,[status(thm)],[hyp218]) ).
cnf(c_499,plain,
queue_19 = q11,
inference(copy,[status(thm)],[c_498]) ).
fof(hyp219,axiom,
q12 = queue_28,
file('theBenchmark.p',hyp219) ).
cnf(c_500,plain,
q12 = queue_28,
inference(clausify,[status(thm)],[hyp219]) ).
cnf(c_501,plain,
queue_28 = q12,
inference(copy,[status(thm)],[c_500]) ).
fof(hyp220,axiom,
q13 = queue_34,
file('theBenchmark.p',hyp220) ).
cnf(c_502,plain,
q13 = queue_34,
inference(clausify,[status(thm)],[hyp220]) ).
cnf(c_503,plain,
queue_34 = q13,
inference(copy,[status(thm)],[c_502]) ).
fof(hyp221,axiom,
q14 = queue_40,
file('theBenchmark.p',hyp221) ).
cnf(c_504,plain,
q14 = queue_40,
inference(clausify,[status(thm)],[hyp221]) ).
cnf(c_505,plain,
queue_40 = q14,
inference(copy,[status(thm)],[c_504]) ).
fof(hyp222,axiom,
q15 = queue_49,
file('theBenchmark.p',hyp222) ).
cnf(c_506,plain,
q15 = queue_49,
inference(clausify,[status(thm)],[hyp222]) ).
cnf(c_507,plain,
queue_49 = q15,
inference(copy,[status(thm)],[c_506]) ).
fof(hyp223,axiom,
q16 = queue_55,
file('theBenchmark.p',hyp223) ).
cnf(c_508,plain,
q16 = queue_55,
inference(clausify,[status(thm)],[hyp223]) ).
cnf(c_509,plain,
queue_55 = q16,
inference(copy,[status(thm)],[c_508]) ).
fof(hyp224,axiom,
q17 = queue_61,
file('theBenchmark.p',hyp224) ).
cnf(c_510,plain,
q17 = queue_61,
inference(clausify,[status(thm)],[hyp224]) ).
cnf(c_511,plain,
queue_61 = q17,
inference(copy,[status(thm)],[c_510]) ).
fof(hyp225,axiom,
q18 = queue_70,
file('theBenchmark.p',hyp225) ).
cnf(c_512,plain,
q18 = queue_70,
inference(clausify,[status(thm)],[hyp225]) ).
cnf(c_513,plain,
queue_70 = q18,
inference(copy,[status(thm)],[c_512]) ).
fof(hyp226,axiom,
q19 = queue_76,
file('theBenchmark.p',hyp226) ).
cnf(c_514,plain,
q19 = queue_76,
inference(clausify,[status(thm)],[hyp226]) ).
cnf(c_515,plain,
queue_76 = q19,
inference(copy,[status(thm)],[c_514]) ).
fof(hyp227,axiom,
q2 = queue_82,
file('theBenchmark.p',hyp227) ).
cnf(c_516,plain,
q2 = queue_82,
inference(clausify,[status(thm)],[hyp227]) ).
cnf(c_517,plain,
queue_82 = q2,
inference(copy,[status(thm)],[c_516]) ).
fof(hyp228,axiom,
q20 = queue_88,
file('theBenchmark.p',hyp228) ).
cnf(c_518,plain,
q20 = queue_88,
inference(clausify,[status(thm)],[hyp228]) ).
cnf(c_519,plain,
queue_88 = q20,
inference(copy,[status(thm)],[c_518]) ).
fof(hyp229,axiom,
q21 = queue_97,
file('theBenchmark.p',hyp229) ).
cnf(c_520,plain,
q21 = queue_97,
inference(clausify,[status(thm)],[hyp229]) ).
cnf(c_521,plain,
queue_97 = q21,
inference(copy,[status(thm)],[c_520]) ).
fof(hyp230,axiom,
q22 = queue_103,
file('theBenchmark.p',hyp230) ).
cnf(c_522,plain,
q22 = queue_103,
inference(clausify,[status(thm)],[hyp230]) ).
cnf(c_523,plain,
queue_103 = q22,
inference(copy,[status(thm)],[c_522]) ).
fof(hyp231,axiom,
q23 = queue_109,
file('theBenchmark.p',hyp231) ).
cnf(c_524,plain,
q23 = queue_109,
inference(clausify,[status(thm)],[hyp231]) ).
cnf(c_525,plain,
queue_109 = q23,
inference(copy,[status(thm)],[c_524]) ).
fof(hyp232,axiom,
q24 = queue_118,
file('theBenchmark.p',hyp232) ).
cnf(c_526,plain,
q24 = queue_118,
inference(clausify,[status(thm)],[hyp232]) ).
cnf(c_527,plain,
queue_118 = q24,
inference(copy,[status(thm)],[c_526]) ).
fof(hyp233,axiom,
q25 = queue_124,
file('theBenchmark.p',hyp233) ).
cnf(c_528,plain,
q25 = queue_124,
inference(clausify,[status(thm)],[hyp233]) ).
cnf(c_529,plain,
queue_124 = q25,
inference(copy,[status(thm)],[c_528]) ).
fof(hyp234,axiom,
q26 = queue_130,
file('theBenchmark.p',hyp234) ).
cnf(c_530,plain,
q26 = queue_130,
inference(clausify,[status(thm)],[hyp234]) ).
cnf(c_531,plain,
queue_130 = q26,
inference(copy,[status(thm)],[c_530]) ).
fof(hyp235,axiom,
q27 = queue_139,
file('theBenchmark.p',hyp235) ).
cnf(c_532,plain,
q27 = queue_139,
inference(clausify,[status(thm)],[hyp235]) ).
cnf(c_533,plain,
queue_139 = q27,
inference(copy,[status(thm)],[c_532]) ).
fof(hyp236,axiom,
q28 = queue_145,
file('theBenchmark.p',hyp236) ).
cnf(c_534,plain,
q28 = queue_145,
inference(clausify,[status(thm)],[hyp236]) ).
cnf(c_535,plain,
queue_145 = q28,
inference(copy,[status(thm)],[c_534]) ).
fof(hyp237,axiom,
q29 = queue_151,
file('theBenchmark.p',hyp237) ).
cnf(c_536,plain,
q29 = queue_151,
inference(clausify,[status(thm)],[hyp237]) ).
cnf(c_537,plain,
queue_151 = q29,
inference(copy,[status(thm)],[c_536]) ).
fof(hyp238,axiom,
q3 = queue_160,
file('theBenchmark.p',hyp238) ).
cnf(c_538,plain,
q3 = queue_160,
inference(clausify,[status(thm)],[hyp238]) ).
cnf(c_539,plain,
queue_160 = q3,
inference(copy,[status(thm)],[c_538]) ).
fof(hyp239,axiom,
q30 = queue_169,
file('theBenchmark.p',hyp239) ).
cnf(c_540,plain,
q30 = queue_169,
inference(clausify,[status(thm)],[hyp239]) ).
cnf(c_541,plain,
queue_169 = q30,
inference(copy,[status(thm)],[c_540]) ).
fof(hyp240,axiom,
q4 = queue_175,
file('theBenchmark.p',hyp240) ).
cnf(c_542,plain,
q4 = queue_175,
inference(clausify,[status(thm)],[hyp240]) ).
cnf(c_543,plain,
queue_175 = q4,
inference(copy,[status(thm)],[c_542]) ).
fof(hyp241,axiom,
q5 = queue_181,
file('theBenchmark.p',hyp241) ).
cnf(c_544,plain,
q5 = queue_181,
inference(clausify,[status(thm)],[hyp241]) ).
cnf(c_545,plain,
queue_181 = q5,
inference(copy,[status(thm)],[c_544]) ).
fof(hyp242,axiom,
q6 = queue_190,
file('theBenchmark.p',hyp242) ).
cnf(c_546,plain,
q6 = queue_190,
inference(clausify,[status(thm)],[hyp242]) ).
cnf(c_547,plain,
queue_190 = q6,
inference(copy,[status(thm)],[c_546]) ).
fof(hyp243,axiom,
q7 = queue_196,
file('theBenchmark.p',hyp243) ).
cnf(c_548,plain,
q7 = queue_196,
inference(clausify,[status(thm)],[hyp243]) ).
cnf(c_549,plain,
queue_196 = q7,
inference(copy,[status(thm)],[c_548]) ).
fof(hyp244,axiom,
q8 = queue_202,
file('theBenchmark.p',hyp244) ).
cnf(c_550,plain,
q8 = queue_202,
inference(clausify,[status(thm)],[hyp244]) ).
cnf(c_551,plain,
queue_202 = q8,
inference(copy,[status(thm)],[c_550]) ).
fof(hyp245,axiom,
q9 = queue_211,
file('theBenchmark.p',hyp245) ).
cnf(c_552,plain,
q9 = queue_211,
inference(clausify,[status(thm)],[hyp245]) ).
cnf(c_553,plain,
queue_211 = q9,
inference(copy,[status(thm)],[c_552]) ).
fof(goal,axiom,
elem_214 != e10,
file('theBenchmark.p',goal) ).
cnf(c_554,plain,
elem_214 != e10,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_555,plain,
rstore_head(q,index_0) = q0,
inference(paramod,[status(thm)],[c_493,c_351]) ).
cnf(c_556,plain,
rstore_tail(queue_5,index_6) = q1,
inference(paramod,[status(thm)],[c_495,c_471]) ).
cnf(c_557,plain,
rstore_tail(queue_11,index_12) = q10,
inference(paramod,[status(thm)],[c_497,c_375]) ).
cnf(c_558,plain,
rstore_tail(queue_17,index_18) = q11,
inference(paramod,[status(thm)],[c_499,c_419]) ).
cnf(c_559,plain,
rstore_head(queue_25,index_27) = q12,
inference(paramod,[status(thm)],[c_501,c_441]) ).
cnf(c_560,plain,
rstore_tail(queue_32,index_33) = q13,
inference(paramod,[status(thm)],[c_503,c_445]) ).
cnf(c_561,plain,
rstore_tail(queue_38,index_39) = q14,
inference(paramod,[status(thm)],[c_505,c_449]) ).
cnf(c_562,plain,
rstore_head(queue_46,index_48) = q15,
inference(paramod,[status(thm)],[c_507,c_455]) ).
cnf(c_563,plain,
rstore_tail(queue_53,index_54) = q16,
inference(paramod,[status(thm)],[c_509,c_461]) ).
cnf(c_564,plain,
rstore_tail(queue_59,index_60) = q17,
inference(paramod,[status(thm)],[c_511,c_465]) ).
cnf(c_565,plain,
rstore_head(queue_67,index_69) = q18,
inference(paramod,[status(thm)],[c_513,c_473]) ).
cnf(c_566,plain,
rstore_tail(queue_74,index_75) = q19,
inference(paramod,[status(thm)],[c_515,c_477]) ).
cnf(c_567,plain,
rstore_tail(queue_80,index_81) = q2,
inference(paramod,[status(thm)],[c_517,c_481]) ).
cnf(c_568,plain,
rstore_tail(queue_86,index_87) = q20,
inference(paramod,[status(thm)],[c_519,c_485]) ).
cnf(c_569,plain,
rstore_head(queue_94,index_96) = q21,
inference(paramod,[status(thm)],[c_521,c_491]) ).
cnf(c_570,plain,
rstore_tail(queue_101,index_102) = q22,
inference(paramod,[status(thm)],[c_523,c_355]) ).
cnf(c_571,plain,
rstore_tail(queue_107,index_108) = q23,
inference(paramod,[status(thm)],[c_525,c_359]) ).
cnf(c_572,plain,
rstore_head(queue_115,index_117) = q24,
inference(paramod,[status(thm)],[c_527,c_367]) ).
cnf(c_573,plain,
rstore_tail(queue_122,index_123) = q25,
inference(paramod,[status(thm)],[c_529,c_371]) ).
cnf(c_574,plain,
rstore_tail(queue_128,index_129) = q26,
inference(paramod,[status(thm)],[c_531,c_377]) ).
cnf(c_575,plain,
rstore_head(queue_136,index_138) = q27,
inference(paramod,[status(thm)],[c_533,c_383]) ).
cnf(c_576,plain,
rstore_tail(queue_143,index_144) = q28,
inference(paramod,[status(thm)],[c_535,c_387]) ).
cnf(c_577,plain,
rstore_tail(queue_149,index_150) = q29,
inference(paramod,[status(thm)],[c_537,c_391]) ).
cnf(c_578,plain,
rstore_head(queue_157,index_159) = q3,
inference(paramod,[status(thm)],[c_539,c_397]) ).
cnf(c_579,plain,
rstore_head(queue_166,index_168) = q30,
inference(paramod,[status(thm)],[c_541,c_403]) ).
cnf(c_580,plain,
rstore_tail(queue_173,index_174) = q4,
inference(paramod,[status(thm)],[c_543,c_409]) ).
cnf(c_581,plain,
rstore_tail(queue_179,index_180) = q5,
inference(paramod,[status(thm)],[c_545,c_413]) ).
cnf(c_582,plain,
rstore_head(queue_187,index_189) = q6,
inference(paramod,[status(thm)],[c_547,c_421]) ).
cnf(c_583,plain,
rstore_tail(queue_194,index_195) = q7,
inference(paramod,[status(thm)],[c_549,c_425]) ).
cnf(c_584,plain,
rstore_tail(queue_200,index_201) = q8,
inference(paramod,[status(thm)],[c_551,c_429]) ).
cnf(c_585,plain,
rstore_head(queue_208,index_210) = q9,
inference(paramod,[status(thm)],[c_553,c_435]) ).
cnf(c_4456,plain,
( select(earray_100,A) = select(earray_98,A)
| index_99 = A ),
inference(paramod,[status(thm)],[c_65,c_2]) ).
cnf(c_592,plain,
( select(earray_98,A) = select(earray_100,A)
| index_99 = A ),
inference(copy,[status(thm)],[c_4456]) ).
cnf(c_594,plain,
( select(earray_106,A) = select(earray_104,A)
| index_105 = A ),
inference(paramod,[status(thm)],[c_69,c_2]) ).
cnf(c_596,plain,
( select(earray_112,A) = select(earray_110,A)
| index_111 = A ),
inference(paramod,[status(thm)],[c_73,c_2]) ).
cnf(c_598,plain,
( select(earray_121,A) = select(earray_119,A)
| index_120 = A ),
inference(paramod,[status(thm)],[c_77,c_2]) ).
cnf(c_600,plain,
( select(earray_127,A) = select(earray_125,A)
| index_126 = A ),
inference(paramod,[status(thm)],[c_81,c_2]) ).
cnf(c_602,plain,
( select(earray_133,A) = select(earray_131,A)
| index_132 = A ),
inference(paramod,[status(thm)],[c_85,c_2]) ).
cnf(c_604,plain,
( select(earray_142,A) = select(earray_140,A)
| index_141 = A ),
inference(paramod,[status(thm)],[c_91,c_2]) ).
cnf(c_606,plain,
( select(earray_148,A) = select(earray_146,A)
| index_147 = A ),
inference(paramod,[status(thm)],[c_95,c_2]) ).
cnf(c_609,plain,
select(earray_16,index_15) = e10,
inference(paramod,[status(thm)],[c_101,c_1]) ).
cnf(c_612,plain,
( select(earray_163,A) = select(earray_161,A)
| index_162 = A ),
inference(paramod,[status(thm)],[c_105,c_2]) ).
cnf(c_626,plain,
( select(earray_22,A) = select(earray_20,A)
| index_21 = A ),
inference(paramod,[status(thm)],[c_137,c_2]) ).
cnf(c_628,plain,
( select(earray_31,A) = select(earray_29,A)
| index_30 = A ),
inference(paramod,[status(thm)],[c_141,c_2]) ).
cnf(c_630,plain,
( select(earray_37,A) = select(earray_35,A)
| index_36 = A ),
inference(paramod,[status(thm)],[c_145,c_2]) ).
cnf(c_634,plain,
( select(earray_43,A) = select(earray_41,A)
| index_42 = A ),
inference(paramod,[status(thm)],[c_151,c_2]) ).
cnf(c_636,plain,
( select(earray_52,A) = select(earray_50,A)
| index_51 = A ),
inference(paramod,[status(thm)],[c_155,c_2]) ).
cnf(c_638,plain,
( select(earray_58,A) = select(earray_56,A)
| index_57 = A ),
inference(paramod,[status(thm)],[c_159,c_2]) ).
cnf(c_640,plain,
( select(earray_64,A) = select(earray_62,A)
| index_63 = A ),
inference(paramod,[status(thm)],[c_163,c_2]) ).
cnf(c_642,plain,
( select(earray_73,A) = select(earray_71,A)
| index_72 = A ),
inference(paramod,[status(thm)],[c_167,c_2]) ).
cnf(c_646,plain,
( select(earray_85,A) = select(earray_83,A)
| index_84 = A ),
inference(paramod,[status(thm)],[c_177,c_2]) ).
cnf(c_648,plain,
( select(earray_91,A) = select(earray_89,A)
| index_90 = A ),
inference(paramod,[status(thm)],[c_181,c_2]) ).
cnf(c_794,plain,
s(s(s(s(s(s(s(s(index_18)))))))) != index_15,
inference(paramod,[status(thm)],[c_253,c_53]) ).
cnf(c_795,plain,
s(s(s(s(s(s(s(index_18))))))) != index_15,
inference(paramod,[status(thm)],[c_253,c_54]) ).
cnf(c_796,plain,
s(s(s(s(s(s(index_18)))))) != index_15,
inference(paramod,[status(thm)],[c_253,c_55]) ).
cnf(c_797,plain,
s(s(s(s(s(index_18))))) != index_15,
inference(paramod,[status(thm)],[c_253,c_56]) ).
cnf(c_798,plain,
s(s(s(s(index_18)))) != index_15,
inference(paramod,[status(thm)],[c_253,c_57]) ).
cnf(c_799,plain,
s(s(s(index_18))) != index_15,
inference(paramod,[status(thm)],[c_253,c_58]) ).
cnf(c_800,plain,
s(s(index_18)) != index_15,
inference(paramod,[status(thm)],[c_253,c_59]) ).
cnf(c_801,plain,
s(index_18) != index_15,
inference(paramod,[status(thm)],[c_253,c_60]) ).
cnf(c_802,plain,
index_18 != index_15,
inference(paramod,[status(thm)],[c_253,c_61]) ).
cnf(c_1010,plain,
rselect_seq(queue_101) = earray_100,
inference(paramod,[status(thm)],[c_353,c_3]) ).
cnf(c_1011,plain,
rselect_head(queue_101) = rselect_head(q21),
inference(paramod,[status(thm)],[c_353,c_9]) ).
cnf(c_1013,plain,
rselect_seq(queue_107) = earray_106,
inference(paramod,[status(thm)],[c_357,c_3]) ).
cnf(c_1014,plain,
rselect_head(queue_107) = rselect_head(q22),
inference(paramod,[status(thm)],[c_357,c_9]) ).
cnf(c_1017,plain,
rselect_head(queue_11) = rselect_head(q9),
inference(paramod,[status(thm)],[c_361,c_9]) ).
cnf(c_1019,plain,
rselect_seq(queue_113) = earray_112,
inference(paramod,[status(thm)],[c_363,c_3]) ).
cnf(c_1020,plain,
rselect_head(queue_113) = rselect_head(q23),
inference(paramod,[status(thm)],[c_363,c_9]) ).
cnf(c_1022,plain,
rselect_tail(queue_115) = index_114,
inference(paramod,[status(thm)],[c_365,c_5]) ).
cnf(c_4457,plain,
rselect_seq(queue_115) = rselect_seq(queue_113),
inference(paramod,[status(thm)],[c_365,c_7]) ).
cnf(c_1023,plain,
rselect_seq(queue_115) = earray_112,
inference(paramod,[status(thm)],[c_1019,c_4457]) ).
cnf(c_4458,plain,
rselect_head(queue_115) = rselect_head(queue_113),
inference(paramod,[status(thm)],[c_365,c_8]) ).
cnf(c_4459,plain,
index_116 = rselect_head(queue_113),
inference(paramod,[status(thm)],[c_199,c_4458]) ).
cnf(c_4460,plain,
index_116 = rselect_head(q23),
inference(paramod,[status(thm)],[c_1020,c_4459]) ).
cnf(c_1024,plain,
rselect_head(q23) = index_116,
inference(copy,[status(thm)],[c_4460]) ).
cnf(c_1026,plain,
rselect_seq(queue_122) = earray_121,
inference(paramod,[status(thm)],[c_369,c_3]) ).
cnf(c_1027,plain,
rselect_head(queue_122) = rselect_head(q24),
inference(paramod,[status(thm)],[c_369,c_9]) ).
cnf(c_1029,plain,
rselect_seq(queue_128) = earray_127,
inference(paramod,[status(thm)],[c_373,c_3]) ).
cnf(c_1030,plain,
rselect_head(queue_128) = rselect_head(q25),
inference(paramod,[status(thm)],[c_373,c_9]) ).
cnf(c_1032,plain,
rselect_seq(queue_134) = earray_133,
inference(paramod,[status(thm)],[c_379,c_3]) ).
cnf(c_1033,plain,
rselect_head(queue_134) = rselect_head(q26),
inference(paramod,[status(thm)],[c_379,c_9]) ).
cnf(c_1035,plain,
rselect_tail(queue_136) = index_135,
inference(paramod,[status(thm)],[c_381,c_5]) ).
cnf(c_4461,plain,
rselect_seq(queue_136) = rselect_seq(queue_134),
inference(paramod,[status(thm)],[c_381,c_7]) ).
cnf(c_1036,plain,
rselect_seq(queue_136) = earray_133,
inference(paramod,[status(thm)],[c_1032,c_4461]) ).
cnf(c_4462,plain,
rselect_head(queue_136) = rselect_head(queue_134),
inference(paramod,[status(thm)],[c_381,c_8]) ).
cnf(c_4463,plain,
index_137 = rselect_head(queue_134),
inference(paramod,[status(thm)],[c_217,c_4462]) ).
cnf(c_4464,plain,
index_137 = rselect_head(q26),
inference(paramod,[status(thm)],[c_1033,c_4463]) ).
cnf(c_1037,plain,
rselect_head(q26) = index_137,
inference(copy,[status(thm)],[c_4464]) ).
cnf(c_1039,plain,
rselect_seq(queue_143) = earray_142,
inference(paramod,[status(thm)],[c_385,c_3]) ).
cnf(c_1040,plain,
rselect_head(queue_143) = rselect_head(q27),
inference(paramod,[status(thm)],[c_385,c_9]) ).
cnf(c_1042,plain,
rselect_seq(queue_149) = earray_148,
inference(paramod,[status(thm)],[c_389,c_3]) ).
cnf(c_1043,plain,
rselect_head(queue_149) = rselect_head(q28),
inference(paramod,[status(thm)],[c_389,c_9]) ).
cnf(c_1046,plain,
rselect_head(queue_155) = rselect_head(q2),
inference(paramod,[status(thm)],[c_393,c_9]) ).
cnf(c_1048,plain,
rselect_tail(queue_157) = index_156,
inference(paramod,[status(thm)],[c_395,c_5]) ).
cnf(c_4465,plain,
rselect_head(queue_157) = rselect_head(queue_155),
inference(paramod,[status(thm)],[c_395,c_8]) ).
cnf(c_4466,plain,
index_158 = rselect_head(queue_155),
inference(paramod,[status(thm)],[c_235,c_4465]) ).
cnf(c_4467,plain,
index_158 = rselect_head(q2),
inference(paramod,[status(thm)],[c_1046,c_4466]) ).
cnf(c_1050,plain,
rselect_head(q2) = index_158,
inference(copy,[status(thm)],[c_4467]) ).
cnf(c_1052,plain,
rselect_seq(queue_164) = earray_163,
inference(paramod,[status(thm)],[c_399,c_3]) ).
cnf(c_1053,plain,
rselect_head(queue_164) = rselect_head(q29),
inference(paramod,[status(thm)],[c_399,c_9]) ).
cnf(c_4468,plain,
rselect_seq(queue_166) = rselect_seq(queue_164),
inference(paramod,[status(thm)],[c_401,c_7]) ).
cnf(c_1056,plain,
rselect_seq(queue_166) = earray_163,
inference(paramod,[status(thm)],[c_1052,c_4468]) ).
cnf(c_4469,plain,
rselect_head(queue_166) = rselect_head(queue_164),
inference(paramod,[status(thm)],[c_401,c_8]) ).
cnf(c_4470,plain,
index_167 = rselect_head(queue_164),
inference(paramod,[status(thm)],[c_243,c_4469]) ).
cnf(c_4471,plain,
index_167 = rselect_head(q29),
inference(paramod,[status(thm)],[c_1053,c_4470]) ).
cnf(c_1057,plain,
rselect_head(q29) = index_167,
inference(copy,[status(thm)],[c_4471]) ).
cnf(c_1059,plain,
rselect_seq(queue_17) = earray_16,
inference(paramod,[status(thm)],[c_405,c_3]) ).
cnf(c_1060,plain,
rselect_head(queue_17) = rselect_head(q10),
inference(paramod,[status(thm)],[c_405,c_9]) ).
cnf(c_1063,plain,
rselect_head(queue_173) = rselect_head(q3),
inference(paramod,[status(thm)],[c_407,c_9]) ).
cnf(c_1066,plain,
rselect_head(queue_179) = rselect_head(q4),
inference(paramod,[status(thm)],[c_411,c_9]) ).
cnf(c_1069,plain,
rselect_head(queue_185) = rselect_head(q5),
inference(paramod,[status(thm)],[c_415,c_9]) ).
cnf(c_1071,plain,
rselect_tail(queue_187) = index_186,
inference(paramod,[status(thm)],[c_417,c_5]) ).
cnf(c_4472,plain,
rselect_head(queue_187) = rselect_head(queue_185),
inference(paramod,[status(thm)],[c_417,c_8]) ).
cnf(c_4473,plain,
index_188 = rselect_head(queue_185),
inference(paramod,[status(thm)],[c_261,c_4472]) ).
cnf(c_4474,plain,
index_188 = rselect_head(q5),
inference(paramod,[status(thm)],[c_1069,c_4473]) ).
cnf(c_1073,plain,
rselect_head(q5) = index_188,
inference(copy,[status(thm)],[c_4474]) ).
cnf(c_1076,plain,
rselect_head(queue_194) = rselect_head(q6),
inference(paramod,[status(thm)],[c_423,c_9]) ).
cnf(c_1079,plain,
rselect_head(queue_200) = rselect_head(q7),
inference(paramod,[status(thm)],[c_427,c_9]) ).
cnf(c_1082,plain,
rselect_head(queue_206) = rselect_head(q8),
inference(paramod,[status(thm)],[c_431,c_9]) ).
cnf(c_1084,plain,
rselect_tail(queue_208) = index_207,
inference(paramod,[status(thm)],[c_433,c_5]) ).
cnf(c_4475,plain,
rselect_head(queue_208) = rselect_head(queue_206),
inference(paramod,[status(thm)],[c_433,c_8]) ).
cnf(c_4476,plain,
index_209 = rselect_head(queue_206),
inference(paramod,[status(thm)],[c_277,c_4475]) ).
cnf(c_4477,plain,
index_209 = rselect_head(q8),
inference(paramod,[status(thm)],[c_1082,c_4476]) ).
cnf(c_1086,plain,
rselect_head(q8) = index_209,
inference(copy,[status(thm)],[c_4477]) ).
cnf(c_1088,plain,
rselect_seq(queue_23) = earray_22,
inference(paramod,[status(thm)],[c_437,c_3]) ).
cnf(c_1089,plain,
rselect_head(queue_23) = rselect_head(q11),
inference(paramod,[status(thm)],[c_437,c_9]) ).
cnf(c_1091,plain,
rselect_tail(queue_25) = index_24,
inference(paramod,[status(thm)],[c_439,c_5]) ).
cnf(c_4478,plain,
rselect_seq(queue_25) = rselect_seq(queue_23),
inference(paramod,[status(thm)],[c_439,c_7]) ).
cnf(c_1092,plain,
rselect_seq(queue_25) = earray_22,
inference(paramod,[status(thm)],[c_1088,c_4478]) ).
cnf(c_4479,plain,
rselect_head(queue_25) = rselect_head(queue_23),
inference(paramod,[status(thm)],[c_439,c_8]) ).
cnf(c_4480,plain,
index_26 = rselect_head(queue_23),
inference(paramod,[status(thm)],[c_287,c_4479]) ).
cnf(c_4481,plain,
index_26 = rselect_head(q11),
inference(paramod,[status(thm)],[c_1089,c_4480]) ).
cnf(c_1093,plain,
rselect_head(q11) = index_26,
inference(copy,[status(thm)],[c_4481]) ).
cnf(c_1095,plain,
rselect_seq(queue_32) = earray_31,
inference(paramod,[status(thm)],[c_443,c_3]) ).
cnf(c_1096,plain,
rselect_head(queue_32) = rselect_head(q12),
inference(paramod,[status(thm)],[c_443,c_9]) ).
cnf(c_1098,plain,
rselect_seq(queue_38) = earray_37,
inference(paramod,[status(thm)],[c_447,c_3]) ).
cnf(c_1099,plain,
rselect_head(queue_38) = rselect_head(q13),
inference(paramod,[status(thm)],[c_447,c_9]) ).
cnf(c_1101,plain,
rselect_seq(queue_44) = earray_43,
inference(paramod,[status(thm)],[c_451,c_3]) ).
cnf(c_1102,plain,
rselect_head(queue_44) = rselect_head(q14),
inference(paramod,[status(thm)],[c_451,c_9]) ).
cnf(c_1104,plain,
rselect_tail(queue_46) = index_45,
inference(paramod,[status(thm)],[c_453,c_5]) ).
cnf(c_4482,plain,
rselect_seq(queue_46) = rselect_seq(queue_44),
inference(paramod,[status(thm)],[c_453,c_7]) ).
cnf(c_1105,plain,
rselect_seq(queue_46) = earray_43,
inference(paramod,[status(thm)],[c_1101,c_4482]) ).
cnf(c_4483,plain,
rselect_head(queue_46) = rselect_head(queue_44),
inference(paramod,[status(thm)],[c_453,c_8]) ).
cnf(c_4484,plain,
index_47 = rselect_head(queue_44),
inference(paramod,[status(thm)],[c_305,c_4483]) ).
cnf(c_4485,plain,
index_47 = rselect_head(q14),
inference(paramod,[status(thm)],[c_1102,c_4484]) ).
cnf(c_1106,plain,
rselect_head(q14) = index_47,
inference(copy,[status(thm)],[c_4485]) ).
cnf(c_1109,plain,
rselect_head(queue_5) = rselect_head(q0),
inference(paramod,[status(thm)],[c_457,c_9]) ).
cnf(c_1111,plain,
rselect_seq(queue_53) = earray_52,
inference(paramod,[status(thm)],[c_459,c_3]) ).
cnf(c_1112,plain,
rselect_head(queue_53) = rselect_head(q15),
inference(paramod,[status(thm)],[c_459,c_9]) ).
cnf(c_1114,plain,
rselect_seq(queue_59) = earray_58,
inference(paramod,[status(thm)],[c_463,c_3]) ).
cnf(c_1115,plain,
rselect_head(queue_59) = rselect_head(q16),
inference(paramod,[status(thm)],[c_463,c_9]) ).
cnf(c_1117,plain,
rselect_seq(queue_65) = earray_64,
inference(paramod,[status(thm)],[c_467,c_3]) ).
cnf(c_1118,plain,
rselect_head(queue_65) = rselect_head(q17),
inference(paramod,[status(thm)],[c_467,c_9]) ).
cnf(c_1120,plain,
rselect_tail(queue_67) = index_66,
inference(paramod,[status(thm)],[c_469,c_5]) ).
cnf(c_4486,plain,
rselect_seq(queue_67) = rselect_seq(queue_65),
inference(paramod,[status(thm)],[c_469,c_7]) ).
cnf(c_1121,plain,
rselect_seq(queue_67) = earray_64,
inference(paramod,[status(thm)],[c_1117,c_4486]) ).
cnf(c_4487,plain,
rselect_head(queue_67) = rselect_head(queue_65),
inference(paramod,[status(thm)],[c_469,c_8]) ).
cnf(c_4488,plain,
index_68 = rselect_head(queue_65),
inference(paramod,[status(thm)],[c_323,c_4487]) ).
cnf(c_4489,plain,
index_68 = rselect_head(q17),
inference(paramod,[status(thm)],[c_1118,c_4488]) ).
cnf(c_1122,plain,
rselect_head(q17) = index_68,
inference(copy,[status(thm)],[c_4489]) ).
cnf(c_1124,plain,
rselect_seq(queue_74) = earray_73,
inference(paramod,[status(thm)],[c_475,c_3]) ).
cnf(c_1125,plain,
rselect_head(queue_74) = rselect_head(q18),
inference(paramod,[status(thm)],[c_475,c_9]) ).
cnf(c_1128,plain,
rselect_head(queue_80) = rselect_head(q1),
inference(paramod,[status(thm)],[c_479,c_9]) ).
cnf(c_1130,plain,
rselect_seq(queue_86) = earray_85,
inference(paramod,[status(thm)],[c_483,c_3]) ).
cnf(c_1131,plain,
rselect_head(queue_86) = rselect_head(q19),
inference(paramod,[status(thm)],[c_483,c_9]) ).
cnf(c_1133,plain,
rselect_seq(queue_92) = earray_91,
inference(paramod,[status(thm)],[c_487,c_3]) ).
cnf(c_1134,plain,
rselect_head(queue_92) = rselect_head(q20),
inference(paramod,[status(thm)],[c_487,c_9]) ).
cnf(c_1136,plain,
rselect_tail(queue_94) = index_93,
inference(paramod,[status(thm)],[c_489,c_5]) ).
cnf(c_4490,plain,
rselect_seq(queue_94) = rselect_seq(queue_92),
inference(paramod,[status(thm)],[c_489,c_7]) ).
cnf(c_1137,plain,
rselect_seq(queue_94) = earray_91,
inference(paramod,[status(thm)],[c_1133,c_4490]) ).
cnf(c_4491,plain,
rselect_head(queue_94) = rselect_head(queue_92),
inference(paramod,[status(thm)],[c_489,c_8]) ).
cnf(c_4492,plain,
index_95 = rselect_head(queue_92),
inference(paramod,[status(thm)],[c_345,c_4491]) ).
cnf(c_4493,plain,
index_95 = rselect_head(q20),
inference(paramod,[status(thm)],[c_1134,c_4492]) ).
cnf(c_1138,plain,
rselect_head(q20) = index_95,
inference(copy,[status(thm)],[c_4493]) ).
cnf(c_1140,plain,
rselect_head(q0) = index_0,
inference(paramod,[status(thm)],[c_555,c_4]) ).
cnf(c_4494,plain,
rselect_tail(q0) = rselect_tail(q),
inference(paramod,[status(thm)],[c_555,c_11]) ).
cnf(c_4495,plain,
index_3 = rselect_tail(q),
inference(paramod,[status(thm)],[c_291,c_4494]) ).
cnf(c_4496,plain,
index_3 = index_0,
inference(paramod,[status(thm)],[c_187,c_4495]) ).
cnf(c_1142,plain,
index_0 = index_3,
inference(copy,[status(thm)],[c_4496]) ).
cnf(c_4497,plain,
rselect_head(queue_5) = index_0,
inference(paramod,[status(thm)],[c_1140,c_1109]) ).
cnf(c_1143,plain,
rselect_head(queue_5) = index_3,
inference(paramod,[status(thm)],[c_1142,c_4497]) ).
cnf(c_4498,plain,
rselect_tail(q1) = index_6,
inference(paramod,[status(thm)],[c_556,c_5]) ).
cnf(c_4499,plain,
index_78 = index_6,
inference(paramod,[status(thm)],[c_331,c_4498]) ).
cnf(c_1147,plain,
index_6 = index_78,
inference(copy,[status(thm)],[c_4499]) ).
cnf(c_4500,plain,
rselect_head(q1) = rselect_head(queue_5),
inference(paramod,[status(thm)],[c_556,c_8]) ).
cnf(c_1149,plain,
rselect_head(q1) = index_3,
inference(paramod,[status(thm)],[c_1143,c_4500]) ).
cnf(c_1160,plain,
s(index_3) = index_78,
inference(paramod,[status(thm)],[c_1147,c_315]) ).
cnf(c_1164,plain,
rselect_head(queue_80) = index_3,
inference(paramod,[status(thm)],[c_1149,c_1128]) ).
cnf(c_4501,plain,
rselect_tail(q10) = index_12,
inference(paramod,[status(thm)],[c_557,c_5]) ).
cnf(c_4502,plain,
index_15 = index_12,
inference(paramod,[status(thm)],[c_227,c_4501]) ).
cnf(c_1165,plain,
index_12 = index_15,
inference(copy,[status(thm)],[c_4502]) ).
cnf(c_4503,plain,
rselect_head(q10) = rselect_head(queue_11),
inference(paramod,[status(thm)],[c_557,c_8]) ).
cnf(c_4504,plain,
rselect_head(q10) = rselect_head(q9),
inference(paramod,[status(thm)],[c_1017,c_4503]) ).
cnf(c_1167,plain,
rselect_head(q9) = rselect_head(q10),
inference(copy,[status(thm)],[c_4504]) ).
cnf(c_1178,plain,
s(index_9) = index_15,
inference(paramod,[status(thm)],[c_1165,c_203]) ).
cnf(c_4505,plain,
rselect_tail(q11) = index_18,
inference(paramod,[status(thm)],[c_558,c_5]) ).
cnf(c_4506,plain,
index_21 = index_18,
inference(paramod,[status(thm)],[c_279,c_4505]) ).
cnf(c_1183,plain,
index_18 = index_21,
inference(copy,[status(thm)],[c_4506]) ).
cnf(c_4507,plain,
rselect_seq(q11) = rselect_seq(queue_17),
inference(paramod,[status(thm)],[c_558,c_7]) ).
cnf(c_4508,plain,
earray_20 = rselect_seq(queue_17),
inference(paramod,[status(thm)],[c_129,c_4507]) ).
cnf(c_1184,plain,
earray_20 = earray_16,
inference(paramod,[status(thm)],[c_1059,c_4508]) ).
cnf(c_4509,plain,
rselect_head(q11) = rselect_head(queue_17),
inference(paramod,[status(thm)],[c_558,c_8]) ).
cnf(c_4510,plain,
index_26 = rselect_head(queue_17),
inference(paramod,[status(thm)],[c_1093,c_4509]) ).
cnf(c_4511,plain,
index_26 = rselect_head(q10),
inference(paramod,[status(thm)],[c_1060,c_4510]) ).
cnf(c_1185,plain,
rselect_head(q10) = index_26,
inference(copy,[status(thm)],[c_4511]) ).
cnf(c_1194,plain,
index_21 != index_15,
inference(paramod,[status(thm)],[c_1183,c_802]) ).
cnf(c_4512,plain,
s(index_21) != index_15,
inference(paramod,[status(thm)],[c_1183,c_801]) ).
cnf(c_1195,plain,
index_24 != index_15,
inference(paramod,[status(thm)],[c_285,c_4512]) ).
cnf(c_4513,plain,
s(s(index_21)) != index_15,
inference(paramod,[status(thm)],[c_1183,c_800]) ).
cnf(c_1196,plain,
s(index_24) != index_15,
inference(paramod,[status(thm)],[c_285,c_4513]) ).
cnf(c_4514,plain,
s(s(s(index_21))) != index_15,
inference(paramod,[status(thm)],[c_1183,c_799]) ).
cnf(c_1197,plain,
s(s(index_24)) != index_15,
inference(paramod,[status(thm)],[c_285,c_4514]) ).
cnf(c_4515,plain,
s(s(s(s(index_21)))) != index_15,
inference(paramod,[status(thm)],[c_1183,c_798]) ).
cnf(c_1198,plain,
s(s(s(index_24))) != index_15,
inference(paramod,[status(thm)],[c_285,c_4515]) ).
cnf(c_4516,plain,
s(s(s(s(s(index_21))))) != index_15,
inference(paramod,[status(thm)],[c_1183,c_797]) ).
cnf(c_1199,plain,
s(s(s(s(index_24)))) != index_15,
inference(paramod,[status(thm)],[c_285,c_4516]) ).
cnf(c_4517,plain,
s(s(s(s(s(s(index_21)))))) != index_15,
inference(paramod,[status(thm)],[c_1183,c_796]) ).
cnf(c_1200,plain,
s(s(s(s(s(index_24))))) != index_15,
inference(paramod,[status(thm)],[c_285,c_4517]) ).
cnf(c_4518,plain,
s(s(s(s(s(s(s(index_21))))))) != index_15,
inference(paramod,[status(thm)],[c_1183,c_795]) ).
cnf(c_1201,plain,
s(s(s(s(s(s(index_24)))))) != index_15,
inference(paramod,[status(thm)],[c_285,c_4518]) ).
cnf(c_4519,plain,
s(s(s(s(s(s(s(s(index_21)))))))) != index_15,
inference(paramod,[status(thm)],[c_1183,c_794]) ).
cnf(c_1202,plain,
s(s(s(s(s(s(s(index_24))))))) != index_15,
inference(paramod,[status(thm)],[c_285,c_4519]) ).
cnf(c_1204,plain,
s(index_15) = index_21,
inference(paramod,[status(thm)],[c_1183,c_253]) ).
cnf(c_1205,plain,
( select(earray_22,A) = select(earray_16,A)
| index_21 = A ),
inference(paramod,[status(thm)],[c_1184,c_626]) ).
cnf(c_1209,plain,
rselect_head(q9) = index_26,
inference(paramod,[status(thm)],[c_1185,c_1167]) ).
cnf(c_1211,plain,
rselect_head(q12) = index_27,
inference(paramod,[status(thm)],[c_559,c_4]) ).
cnf(c_4520,plain,
rselect_seq(q12) = rselect_seq(queue_25),
inference(paramod,[status(thm)],[c_559,c_6]) ).
cnf(c_4521,plain,
earray_29 = rselect_seq(queue_25),
inference(paramod,[status(thm)],[c_139,c_4520]) ).
cnf(c_1212,plain,
earray_29 = earray_22,
inference(paramod,[status(thm)],[c_1092,c_4521]) ).
cnf(c_4522,plain,
rselect_tail(q12) = rselect_tail(queue_25),
inference(paramod,[status(thm)],[c_559,c_11]) ).
cnf(c_4523,plain,
index_30 = rselect_tail(queue_25),
inference(paramod,[status(thm)],[c_293,c_4522]) ).
cnf(c_4524,plain,
index_30 = index_24,
inference(paramod,[status(thm)],[c_1091,c_4523]) ).
cnf(c_1213,plain,
index_24 = index_30,
inference(copy,[status(thm)],[c_4524]) ).
cnf(c_1214,plain,
rselect_head(queue_32) = index_27,
inference(paramod,[status(thm)],[c_1211,c_1096]) ).
cnf(c_1215,plain,
( select(earray_31,A) = select(earray_22,A)
| index_30 = A ),
inference(paramod,[status(thm)],[c_1212,c_628]) ).
cnf(c_4525,plain,
s(s(s(s(s(s(s(index_30))))))) != index_15,
inference(paramod,[status(thm)],[c_1213,c_1202]) ).
cnf(c_1218,plain,
s(s(s(s(s(s(index_33)))))) != index_15,
inference(paramod,[status(thm)],[c_295,c_4525]) ).
cnf(c_4526,plain,
s(s(s(s(s(s(index_30)))))) != index_15,
inference(paramod,[status(thm)],[c_1213,c_1201]) ).
cnf(c_1219,plain,
s(s(s(s(s(index_33))))) != index_15,
inference(paramod,[status(thm)],[c_295,c_4526]) ).
cnf(c_4527,plain,
s(s(s(s(s(index_30))))) != index_15,
inference(paramod,[status(thm)],[c_1213,c_1200]) ).
cnf(c_1220,plain,
s(s(s(s(index_33)))) != index_15,
inference(paramod,[status(thm)],[c_295,c_4527]) ).
cnf(c_4528,plain,
s(s(s(s(index_30)))) != index_15,
inference(paramod,[status(thm)],[c_1213,c_1199]) ).
cnf(c_1221,plain,
s(s(s(index_33))) != index_15,
inference(paramod,[status(thm)],[c_295,c_4528]) ).
cnf(c_4529,plain,
s(s(s(index_30))) != index_15,
inference(paramod,[status(thm)],[c_1213,c_1198]) ).
cnf(c_1222,plain,
s(s(index_33)) != index_15,
inference(paramod,[status(thm)],[c_295,c_4529]) ).
cnf(c_4530,plain,
s(s(index_30)) != index_15,
inference(paramod,[status(thm)],[c_1213,c_1197]) ).
cnf(c_1223,plain,
s(index_33) != index_15,
inference(paramod,[status(thm)],[c_295,c_4530]) ).
cnf(c_4531,plain,
s(index_30) != index_15,
inference(paramod,[status(thm)],[c_1213,c_1196]) ).
cnf(c_1224,plain,
index_33 != index_15,
inference(paramod,[status(thm)],[c_295,c_4531]) ).
cnf(c_1225,plain,
index_30 != index_15,
inference(paramod,[status(thm)],[c_1213,c_1195]) ).
cnf(c_1244,plain,
s(index_21) = index_30,
inference(paramod,[status(thm)],[c_1213,c_285]) ).
cnf(c_4532,plain,
rselect_tail(q13) = index_33,
inference(paramod,[status(thm)],[c_560,c_5]) ).
cnf(c_4533,plain,
index_36 = index_33,
inference(paramod,[status(thm)],[c_297,c_4532]) ).
cnf(c_1245,plain,
index_33 = index_36,
inference(copy,[status(thm)],[c_4533]) ).
cnf(c_4534,plain,
rselect_seq(q13) = rselect_seq(queue_32),
inference(paramod,[status(thm)],[c_560,c_7]) ).
cnf(c_4535,plain,
earray_35 = rselect_seq(queue_32),
inference(paramod,[status(thm)],[c_143,c_4534]) ).
cnf(c_1246,plain,
earray_35 = earray_31,
inference(paramod,[status(thm)],[c_1095,c_4535]) ).
cnf(c_4536,plain,
rselect_head(q13) = rselect_head(queue_32),
inference(paramod,[status(thm)],[c_560,c_8]) ).
cnf(c_1247,plain,
rselect_head(q13) = index_27,
inference(paramod,[status(thm)],[c_1214,c_4536]) ).
cnf(c_1262,plain,
index_36 != index_15,
inference(paramod,[status(thm)],[c_1245,c_1224]) ).
cnf(c_4537,plain,
s(index_36) != index_15,
inference(paramod,[status(thm)],[c_1245,c_1223]) ).
cnf(c_1263,plain,
index_39 != index_15,
inference(paramod,[status(thm)],[c_299,c_4537]) ).
cnf(c_4538,plain,
s(s(index_36)) != index_15,
inference(paramod,[status(thm)],[c_1245,c_1222]) ).
cnf(c_1264,plain,
s(index_39) != index_15,
inference(paramod,[status(thm)],[c_299,c_4538]) ).
cnf(c_4539,plain,
s(s(s(index_36))) != index_15,
inference(paramod,[status(thm)],[c_1245,c_1221]) ).
cnf(c_1265,plain,
s(s(index_39)) != index_15,
inference(paramod,[status(thm)],[c_299,c_4539]) ).
cnf(c_4540,plain,
s(s(s(s(index_36)))) != index_15,
inference(paramod,[status(thm)],[c_1245,c_1220]) ).
cnf(c_1266,plain,
s(s(s(index_39))) != index_15,
inference(paramod,[status(thm)],[c_299,c_4540]) ).
cnf(c_4541,plain,
s(s(s(s(s(index_36))))) != index_15,
inference(paramod,[status(thm)],[c_1245,c_1219]) ).
cnf(c_1267,plain,
s(s(s(s(index_39)))) != index_15,
inference(paramod,[status(thm)],[c_299,c_4541]) ).
cnf(c_4542,plain,
s(s(s(s(s(s(index_36)))))) != index_15,
inference(paramod,[status(thm)],[c_1245,c_1218]) ).
cnf(c_1268,plain,
s(s(s(s(s(index_39))))) != index_15,
inference(paramod,[status(thm)],[c_299,c_4542]) ).
cnf(c_1279,plain,
s(index_30) = index_36,
inference(paramod,[status(thm)],[c_1245,c_295]) ).
cnf(c_1280,plain,
( select(earray_37,A) = select(earray_31,A)
| index_36 = A ),
inference(paramod,[status(thm)],[c_1246,c_630]) ).
cnf(c_1283,plain,
rselect_head(queue_38) = index_27,
inference(paramod,[status(thm)],[c_1247,c_1099]) ).
cnf(c_4543,plain,
rselect_tail(q14) = index_39,
inference(paramod,[status(thm)],[c_561,c_5]) ).
cnf(c_4544,plain,
index_42 = index_39,
inference(paramod,[status(thm)],[c_301,c_4543]) ).
cnf(c_1284,plain,
index_39 = index_42,
inference(copy,[status(thm)],[c_4544]) ).
cnf(c_4545,plain,
rselect_seq(q14) = rselect_seq(queue_38),
inference(paramod,[status(thm)],[c_561,c_7]) ).
cnf(c_4546,plain,
earray_41 = rselect_seq(queue_38),
inference(paramod,[status(thm)],[c_149,c_4545]) ).
cnf(c_1285,plain,
earray_41 = earray_37,
inference(paramod,[status(thm)],[c_1098,c_4546]) ).
cnf(c_4547,plain,
rselect_head(q14) = rselect_head(queue_38),
inference(paramod,[status(thm)],[c_561,c_8]) ).
cnf(c_4548,plain,
index_47 = rselect_head(queue_38),
inference(paramod,[status(thm)],[c_1106,c_4547]) ).
cnf(c_1286,plain,
index_47 = index_27,
inference(paramod,[status(thm)],[c_1283,c_4548]) ).
cnf(c_4549,plain,
s(s(s(s(s(index_42))))) != index_15,
inference(paramod,[status(thm)],[c_1284,c_1268]) ).
cnf(c_1295,plain,
s(s(s(s(index_45)))) != index_15,
inference(paramod,[status(thm)],[c_303,c_4549]) ).
cnf(c_4550,plain,
s(s(s(s(index_42)))) != index_15,
inference(paramod,[status(thm)],[c_1284,c_1267]) ).
cnf(c_1296,plain,
s(s(s(index_45))) != index_15,
inference(paramod,[status(thm)],[c_303,c_4550]) ).
cnf(c_4551,plain,
s(s(s(index_42))) != index_15,
inference(paramod,[status(thm)],[c_1284,c_1266]) ).
cnf(c_1297,plain,
s(s(index_45)) != index_15,
inference(paramod,[status(thm)],[c_303,c_4551]) ).
cnf(c_4552,plain,
s(s(index_42)) != index_15,
inference(paramod,[status(thm)],[c_1284,c_1265]) ).
cnf(c_1298,plain,
s(index_45) != index_15,
inference(paramod,[status(thm)],[c_303,c_4552]) ).
cnf(c_4553,plain,
s(index_42) != index_15,
inference(paramod,[status(thm)],[c_1284,c_1264]) ).
cnf(c_1299,plain,
index_45 != index_15,
inference(paramod,[status(thm)],[c_303,c_4553]) ).
cnf(c_1300,plain,
index_42 != index_15,
inference(paramod,[status(thm)],[c_1284,c_1263]) ).
cnf(c_1323,plain,
s(index_36) = index_42,
inference(paramod,[status(thm)],[c_1284,c_299]) ).
cnf(c_1324,plain,
( select(earray_43,A) = select(earray_37,A)
| index_42 = A ),
inference(paramod,[status(thm)],[c_1285,c_634]) ).
cnf(c_1338,plain,
s(index_27) = index_48,
inference(paramod,[status(thm)],[c_1286,c_307]) ).
cnf(c_1348,plain,
rselect_head(q15) = index_48,
inference(paramod,[status(thm)],[c_562,c_4]) ).
cnf(c_4554,plain,
rselect_seq(q15) = rselect_seq(queue_46),
inference(paramod,[status(thm)],[c_562,c_6]) ).
cnf(c_4555,plain,
earray_50 = rselect_seq(queue_46),
inference(paramod,[status(thm)],[c_153,c_4554]) ).
cnf(c_1349,plain,
earray_50 = earray_43,
inference(paramod,[status(thm)],[c_1105,c_4555]) ).
cnf(c_4556,plain,
rselect_tail(q15) = rselect_tail(queue_46),
inference(paramod,[status(thm)],[c_562,c_11]) ).
cnf(c_4557,plain,
index_51 = rselect_tail(queue_46),
inference(paramod,[status(thm)],[c_309,c_4556]) ).
cnf(c_4558,plain,
index_51 = index_45,
inference(paramod,[status(thm)],[c_1104,c_4557]) ).
cnf(c_1350,plain,
index_45 = index_51,
inference(copy,[status(thm)],[c_4558]) ).
cnf(c_1351,plain,
rselect_head(queue_53) = index_48,
inference(paramod,[status(thm)],[c_1348,c_1112]) ).
cnf(c_1352,plain,
( select(earray_52,A) = select(earray_43,A)
| index_51 = A ),
inference(paramod,[status(thm)],[c_1349,c_636]) ).
cnf(c_1373,plain,
index_51 != index_15,
inference(paramod,[status(thm)],[c_1350,c_1299]) ).
cnf(c_4559,plain,
s(index_51) != index_15,
inference(paramod,[status(thm)],[c_1350,c_1298]) ).
cnf(c_1374,plain,
index_54 != index_15,
inference(paramod,[status(thm)],[c_311,c_4559]) ).
cnf(c_4560,plain,
s(s(index_51)) != index_15,
inference(paramod,[status(thm)],[c_1350,c_1297]) ).
cnf(c_1375,plain,
s(index_54) != index_15,
inference(paramod,[status(thm)],[c_311,c_4560]) ).
cnf(c_4561,plain,
s(s(s(index_51))) != index_15,
inference(paramod,[status(thm)],[c_1350,c_1296]) ).
cnf(c_1376,plain,
s(s(index_54)) != index_15,
inference(paramod,[status(thm)],[c_311,c_4561]) ).
cnf(c_4562,plain,
s(s(s(s(index_51)))) != index_15,
inference(paramod,[status(thm)],[c_1350,c_1295]) ).
cnf(c_1377,plain,
s(s(s(index_54))) != index_15,
inference(paramod,[status(thm)],[c_311,c_4562]) ).
cnf(c_1396,plain,
s(index_42) = index_51,
inference(paramod,[status(thm)],[c_1350,c_303]) ).
cnf(c_4563,plain,
rselect_tail(q16) = index_54,
inference(paramod,[status(thm)],[c_563,c_5]) ).
cnf(c_4564,plain,
index_57 = index_54,
inference(paramod,[status(thm)],[c_313,c_4563]) ).
cnf(c_1397,plain,
index_54 = index_57,
inference(copy,[status(thm)],[c_4564]) ).
cnf(c_4565,plain,
rselect_seq(q16) = rselect_seq(queue_53),
inference(paramod,[status(thm)],[c_563,c_7]) ).
cnf(c_4566,plain,
earray_56 = rselect_seq(queue_53),
inference(paramod,[status(thm)],[c_157,c_4565]) ).
cnf(c_1398,plain,
earray_56 = earray_52,
inference(paramod,[status(thm)],[c_1111,c_4566]) ).
cnf(c_4567,plain,
rselect_head(q16) = rselect_head(queue_53),
inference(paramod,[status(thm)],[c_563,c_8]) ).
cnf(c_1399,plain,
rselect_head(q16) = index_48,
inference(paramod,[status(thm)],[c_1351,c_4567]) ).
cnf(c_4568,plain,
s(s(s(index_57))) != index_15,
inference(paramod,[status(thm)],[c_1397,c_1377]) ).
cnf(c_1414,plain,
s(s(index_60)) != index_15,
inference(paramod,[status(thm)],[c_317,c_4568]) ).
cnf(c_4569,plain,
s(s(index_57)) != index_15,
inference(paramod,[status(thm)],[c_1397,c_1376]) ).
cnf(c_1415,plain,
s(index_60) != index_15,
inference(paramod,[status(thm)],[c_317,c_4569]) ).
cnf(c_4570,plain,
s(index_57) != index_15,
inference(paramod,[status(thm)],[c_1397,c_1375]) ).
cnf(c_1416,plain,
index_60 != index_15,
inference(paramod,[status(thm)],[c_317,c_4570]) ).
cnf(c_1417,plain,
index_57 != index_15,
inference(paramod,[status(thm)],[c_1397,c_1374]) ).
cnf(c_1443,plain,
s(index_51) = index_57,
inference(paramod,[status(thm)],[c_1397,c_311]) ).
cnf(c_1444,plain,
( select(earray_58,A) = select(earray_52,A)
| index_57 = A ),
inference(paramod,[status(thm)],[c_1398,c_638]) ).
cnf(c_1447,plain,
rselect_head(queue_59) = index_48,
inference(paramod,[status(thm)],[c_1399,c_1115]) ).
cnf(c_4571,plain,
rselect_tail(q17) = index_60,
inference(paramod,[status(thm)],[c_564,c_5]) ).
cnf(c_4572,plain,
index_63 = index_60,
inference(paramod,[status(thm)],[c_319,c_4571]) ).
cnf(c_1448,plain,
index_60 = index_63,
inference(copy,[status(thm)],[c_4572]) ).
cnf(c_4573,plain,
rselect_seq(q17) = rselect_seq(queue_59),
inference(paramod,[status(thm)],[c_564,c_7]) ).
cnf(c_4574,plain,
earray_62 = rselect_seq(queue_59),
inference(paramod,[status(thm)],[c_161,c_4573]) ).
cnf(c_1449,plain,
earray_62 = earray_58,
inference(paramod,[status(thm)],[c_1114,c_4574]) ).
cnf(c_4575,plain,
rselect_head(q17) = rselect_head(queue_59),
inference(paramod,[status(thm)],[c_564,c_8]) ).
cnf(c_4576,plain,
index_68 = rselect_head(queue_59),
inference(paramod,[status(thm)],[c_1122,c_4575]) ).
cnf(c_1450,plain,
index_68 = index_48,
inference(paramod,[status(thm)],[c_1447,c_4576]) ).
cnf(c_1471,plain,
index_63 != index_15,
inference(paramod,[status(thm)],[c_1448,c_1416]) ).
cnf(c_4577,plain,
s(index_63) != index_15,
inference(paramod,[status(thm)],[c_1448,c_1415]) ).
cnf(c_1472,plain,
index_66 != index_15,
inference(paramod,[status(thm)],[c_321,c_4577]) ).
cnf(c_4578,plain,
s(s(index_63)) != index_15,
inference(paramod,[status(thm)],[c_1448,c_1414]) ).
cnf(c_1473,plain,
s(index_66) != index_15,
inference(paramod,[status(thm)],[c_321,c_4578]) ).
cnf(c_1496,plain,
s(index_57) = index_63,
inference(paramod,[status(thm)],[c_1448,c_317]) ).
cnf(c_1497,plain,
( select(earray_64,A) = select(earray_58,A)
| index_63 = A ),
inference(paramod,[status(thm)],[c_1449,c_640]) ).
cnf(c_1511,plain,
s(index_48) = index_69,
inference(paramod,[status(thm)],[c_1450,c_325]) ).
cnf(c_1528,plain,
rselect_head(q18) = index_69,
inference(paramod,[status(thm)],[c_565,c_4]) ).
cnf(c_4579,plain,
rselect_seq(q18) = rselect_seq(queue_67),
inference(paramod,[status(thm)],[c_565,c_6]) ).
cnf(c_4580,plain,
earray_71 = rselect_seq(queue_67),
inference(paramod,[status(thm)],[c_165,c_4579]) ).
cnf(c_1529,plain,
earray_71 = earray_64,
inference(paramod,[status(thm)],[c_1121,c_4580]) ).
cnf(c_4581,plain,
rselect_tail(q18) = rselect_tail(queue_67),
inference(paramod,[status(thm)],[c_565,c_11]) ).
cnf(c_4582,plain,
index_72 = rselect_tail(queue_67),
inference(paramod,[status(thm)],[c_327,c_4581]) ).
cnf(c_4583,plain,
index_72 = index_66,
inference(paramod,[status(thm)],[c_1120,c_4582]) ).
cnf(c_1530,plain,
index_66 = index_72,
inference(copy,[status(thm)],[c_4583]) ).
cnf(c_1531,plain,
rselect_head(queue_74) = index_69,
inference(paramod,[status(thm)],[c_1528,c_1125]) ).
cnf(c_1532,plain,
( select(earray_73,A) = select(earray_64,A)
| index_72 = A ),
inference(paramod,[status(thm)],[c_1529,c_642]) ).
cnf(c_4584,plain,
s(index_72) != index_15,
inference(paramod,[status(thm)],[c_1530,c_1473]) ).
cnf(c_1553,plain,
index_75 != index_15,
inference(paramod,[status(thm)],[c_329,c_4584]) ).
cnf(c_1554,plain,
index_72 != index_15,
inference(paramod,[status(thm)],[c_1530,c_1472]) ).
cnf(c_1582,plain,
s(index_63) = index_72,
inference(paramod,[status(thm)],[c_1530,c_321]) ).
cnf(c_4585,plain,
rselect_tail(q19) = index_75,
inference(paramod,[status(thm)],[c_566,c_5]) ).
cnf(c_4586,plain,
index_84 = index_75,
inference(paramod,[status(thm)],[c_335,c_4585]) ).
cnf(c_1583,plain,
index_75 = index_84,
inference(copy,[status(thm)],[c_4586]) ).
cnf(c_4587,plain,
rselect_seq(q19) = rselect_seq(queue_74),
inference(paramod,[status(thm)],[c_566,c_7]) ).
cnf(c_4588,plain,
earray_83 = rselect_seq(queue_74),
inference(paramod,[status(thm)],[c_175,c_4587]) ).
cnf(c_1584,plain,
earray_83 = earray_73,
inference(paramod,[status(thm)],[c_1124,c_4588]) ).
cnf(c_4589,plain,
rselect_head(q19) = rselect_head(queue_74),
inference(paramod,[status(thm)],[c_566,c_8]) ).
cnf(c_1585,plain,
rselect_head(q19) = index_69,
inference(paramod,[status(thm)],[c_1531,c_4589]) ).
cnf(c_1606,plain,
index_84 != index_15,
inference(paramod,[status(thm)],[c_1583,c_1553]) ).
cnf(c_1632,plain,
s(index_72) = index_84,
inference(paramod,[status(thm)],[c_1583,c_329]) ).
cnf(c_1633,plain,
( select(earray_85,A) = select(earray_73,A)
| index_84 = A ),
inference(paramod,[status(thm)],[c_1584,c_646]) ).
cnf(c_1636,plain,
rselect_head(queue_86) = index_69,
inference(paramod,[status(thm)],[c_1585,c_1131]) ).
cnf(c_4590,plain,
rselect_tail(q2) = index_81,
inference(paramod,[status(thm)],[c_567,c_5]) ).
cnf(c_4591,plain,
index_153 = index_81,
inference(paramod,[status(thm)],[c_231,c_4590]) ).
cnf(c_1637,plain,
index_81 = index_153,
inference(copy,[status(thm)],[c_4591]) ).
cnf(c_4592,plain,
rselect_head(q2) = rselect_head(queue_80),
inference(paramod,[status(thm)],[c_567,c_8]) ).
cnf(c_4593,plain,
index_158 = rselect_head(queue_80),
inference(paramod,[status(thm)],[c_1050,c_4592]) ).
cnf(c_1639,plain,
index_158 = index_3,
inference(paramod,[status(thm)],[c_1164,c_4593]) ).
cnf(c_1658,plain,
s(index_78) = index_153,
inference(paramod,[status(thm)],[c_1637,c_333]) ).
cnf(c_4594,plain,
s(index_3) = index_159,
inference(paramod,[status(thm)],[c_1639,c_237]) ).
cnf(c_4595,plain,
index_78 = index_159,
inference(paramod,[status(thm)],[c_1160,c_4594]) ).
cnf(c_1675,plain,
index_159 = index_78,
inference(copy,[status(thm)],[c_4595]) ).
cnf(c_1677,plain,
rstore_head(queue_157,index_78) = q3,
inference(paramod,[status(thm)],[c_1675,c_578]) ).
cnf(c_4596,plain,
rselect_tail(q20) = index_87,
inference(paramod,[status(thm)],[c_568,c_5]) ).
cnf(c_4597,plain,
index_90 = index_87,
inference(paramod,[status(thm)],[c_341,c_4596]) ).
cnf(c_1678,plain,
index_87 = index_90,
inference(copy,[status(thm)],[c_4597]) ).
cnf(c_4598,plain,
rselect_seq(q20) = rselect_seq(queue_86),
inference(paramod,[status(thm)],[c_568,c_7]) ).
cnf(c_4599,plain,
earray_89 = rselect_seq(queue_86),
inference(paramod,[status(thm)],[c_179,c_4598]) ).
cnf(c_1679,plain,
earray_89 = earray_85,
inference(paramod,[status(thm)],[c_1130,c_4599]) ).
cnf(c_4600,plain,
rselect_head(q20) = rselect_head(queue_86),
inference(paramod,[status(thm)],[c_568,c_8]) ).
cnf(c_4601,plain,
index_95 = rselect_head(queue_86),
inference(paramod,[status(thm)],[c_1138,c_4600]) ).
cnf(c_1680,plain,
index_95 = index_69,
inference(paramod,[status(thm)],[c_1636,c_4601]) ).
cnf(c_1727,plain,
s(index_84) = index_90,
inference(paramod,[status(thm)],[c_1678,c_337]) ).
cnf(c_1728,plain,
( select(earray_91,A) = select(earray_85,A)
| index_90 = A ),
inference(paramod,[status(thm)],[c_1679,c_648]) ).
cnf(c_1742,plain,
s(index_69) = index_96,
inference(paramod,[status(thm)],[c_1680,c_347]) ).
cnf(c_1765,plain,
rselect_head(q21) = index_96,
inference(paramod,[status(thm)],[c_569,c_4]) ).
cnf(c_4602,plain,
rselect_seq(q21) = rselect_seq(queue_94),
inference(paramod,[status(thm)],[c_569,c_6]) ).
cnf(c_4603,plain,
earray_98 = rselect_seq(queue_94),
inference(paramod,[status(thm)],[c_183,c_4602]) ).
cnf(c_1766,plain,
earray_98 = earray_91,
inference(paramod,[status(thm)],[c_1137,c_4603]) ).
cnf(c_4604,plain,
rselect_tail(q21) = rselect_tail(queue_94),
inference(paramod,[status(thm)],[c_569,c_11]) ).
cnf(c_4605,plain,
index_99 = rselect_tail(queue_94),
inference(paramod,[status(thm)],[c_349,c_4604]) ).
cnf(c_4606,plain,
index_99 = index_93,
inference(paramod,[status(thm)],[c_1136,c_4605]) ).
cnf(c_1767,plain,
index_93 = index_99,
inference(copy,[status(thm)],[c_4606]) ).
cnf(c_1768,plain,
rselect_head(queue_101) = index_96,
inference(paramod,[status(thm)],[c_1765,c_1011]) ).
cnf(c_1769,plain,
( select(earray_91,A) = select(earray_100,A)
| index_99 = A ),
inference(paramod,[status(thm)],[c_1766,c_592]) ).
cnf(c_1819,plain,
s(index_90) = index_99,
inference(paramod,[status(thm)],[c_1767,c_343]) ).
cnf(c_4607,plain,
rselect_tail(q22) = index_102,
inference(paramod,[status(thm)],[c_570,c_5]) ).
cnf(c_4608,plain,
index_105 = index_102,
inference(paramod,[status(thm)],[c_191,c_4607]) ).
cnf(c_1820,plain,
index_102 = index_105,
inference(copy,[status(thm)],[c_4608]) ).
cnf(c_4609,plain,
rselect_seq(q22) = rselect_seq(queue_101),
inference(paramod,[status(thm)],[c_570,c_7]) ).
cnf(c_4610,plain,
earray_104 = rselect_seq(queue_101),
inference(paramod,[status(thm)],[c_67,c_4609]) ).
cnf(c_1821,plain,
earray_104 = earray_100,
inference(paramod,[status(thm)],[c_1010,c_4610]) ).
cnf(c_4611,plain,
rselect_head(q22) = rselect_head(queue_101),
inference(paramod,[status(thm)],[c_570,c_8]) ).
cnf(c_1822,plain,
rselect_head(q22) = index_96,
inference(paramod,[status(thm)],[c_1768,c_4611]) ).
cnf(c_1869,plain,
s(index_99) = index_105,
inference(paramod,[status(thm)],[c_1820,c_189]) ).
cnf(c_1870,plain,
( select(earray_106,A) = select(earray_100,A)
| index_105 = A ),
inference(paramod,[status(thm)],[c_1821,c_594]) ).
cnf(c_1873,plain,
rselect_head(queue_107) = index_96,
inference(paramod,[status(thm)],[c_1822,c_1014]) ).
cnf(c_4612,plain,
rselect_tail(q23) = index_108,
inference(paramod,[status(thm)],[c_571,c_5]) ).
cnf(c_4613,plain,
index_111 = index_108,
inference(paramod,[status(thm)],[c_195,c_4612]) ).
cnf(c_1874,plain,
index_108 = index_111,
inference(copy,[status(thm)],[c_4613]) ).
cnf(c_4614,plain,
rselect_seq(q23) = rselect_seq(queue_107),
inference(paramod,[status(thm)],[c_571,c_7]) ).
cnf(c_4615,plain,
earray_110 = rselect_seq(queue_107),
inference(paramod,[status(thm)],[c_71,c_4614]) ).
cnf(c_1875,plain,
earray_110 = earray_106,
inference(paramod,[status(thm)],[c_1013,c_4615]) ).
cnf(c_4616,plain,
rselect_head(q23) = rselect_head(queue_107),
inference(paramod,[status(thm)],[c_571,c_8]) ).
cnf(c_4617,plain,
index_116 = rselect_head(queue_107),
inference(paramod,[status(thm)],[c_1024,c_4616]) ).
cnf(c_4618,plain,
index_116 = index_96,
inference(paramod,[status(thm)],[c_1873,c_4617]) ).
cnf(c_1876,plain,
index_96 = index_116,
inference(copy,[status(thm)],[c_4618]) ).
cnf(c_1923,plain,
s(index_105) = index_111,
inference(paramod,[status(thm)],[c_1874,c_193]) ).
cnf(c_1924,plain,
( select(earray_112,A) = select(earray_106,A)
| index_111 = A ),
inference(paramod,[status(thm)],[c_1875,c_596]) ).
cnf(c_1952,plain,
s(index_69) = index_116,
inference(paramod,[status(thm)],[c_1876,c_1742]) ).
cnf(c_1963,plain,
rselect_head(q24) = index_117,
inference(paramod,[status(thm)],[c_572,c_4]) ).
cnf(c_4619,plain,
rselect_seq(q24) = rselect_seq(queue_115),
inference(paramod,[status(thm)],[c_572,c_6]) ).
cnf(c_4620,plain,
earray_119 = rselect_seq(queue_115),
inference(paramod,[status(thm)],[c_75,c_4619]) ).
cnf(c_1964,plain,
earray_119 = earray_112,
inference(paramod,[status(thm)],[c_1023,c_4620]) ).
cnf(c_4621,plain,
rselect_tail(q24) = rselect_tail(queue_115),
inference(paramod,[status(thm)],[c_572,c_11]) ).
cnf(c_4622,plain,
index_120 = rselect_tail(queue_115),
inference(paramod,[status(thm)],[c_205,c_4621]) ).
cnf(c_4623,plain,
index_120 = index_114,
inference(paramod,[status(thm)],[c_1022,c_4622]) ).
cnf(c_1965,plain,
index_114 = index_120,
inference(copy,[status(thm)],[c_4623]) ).
cnf(c_1966,plain,
rselect_head(queue_122) = index_117,
inference(paramod,[status(thm)],[c_1963,c_1027]) ).
cnf(c_1967,plain,
( select(earray_121,A) = select(earray_112,A)
| index_120 = A ),
inference(paramod,[status(thm)],[c_1964,c_598]) ).
cnf(c_2017,plain,
s(index_111) = index_120,
inference(paramod,[status(thm)],[c_1965,c_197]) ).
cnf(c_4624,plain,
rselect_tail(q25) = index_123,
inference(paramod,[status(thm)],[c_573,c_5]) ).
cnf(c_4625,plain,
index_126 = index_123,
inference(paramod,[status(thm)],[c_209,c_4624]) ).
cnf(c_2018,plain,
index_123 = index_126,
inference(copy,[status(thm)],[c_4625]) ).
cnf(c_4626,plain,
rselect_seq(q25) = rselect_seq(queue_122),
inference(paramod,[status(thm)],[c_573,c_7]) ).
cnf(c_4627,plain,
earray_125 = rselect_seq(queue_122),
inference(paramod,[status(thm)],[c_79,c_4626]) ).
cnf(c_2019,plain,
earray_125 = earray_121,
inference(paramod,[status(thm)],[c_1026,c_4627]) ).
cnf(c_4628,plain,
rselect_head(q25) = rselect_head(queue_122),
inference(paramod,[status(thm)],[c_573,c_8]) ).
cnf(c_2020,plain,
rselect_head(q25) = index_117,
inference(paramod,[status(thm)],[c_1966,c_4628]) ).
cnf(c_2067,plain,
s(index_120) = index_126,
inference(paramod,[status(thm)],[c_2018,c_207]) ).
cnf(c_2068,plain,
( select(earray_127,A) = select(earray_121,A)
| index_126 = A ),
inference(paramod,[status(thm)],[c_2019,c_600]) ).
cnf(c_2071,plain,
rselect_head(queue_128) = index_117,
inference(paramod,[status(thm)],[c_2020,c_1030]) ).
cnf(c_4629,plain,
rselect_tail(q26) = index_129,
inference(paramod,[status(thm)],[c_574,c_5]) ).
cnf(c_4630,plain,
index_132 = index_129,
inference(paramod,[status(thm)],[c_213,c_4629]) ).
cnf(c_2072,plain,
index_129 = index_132,
inference(copy,[status(thm)],[c_4630]) ).
cnf(c_4631,plain,
rselect_seq(q26) = rselect_seq(queue_128),
inference(paramod,[status(thm)],[c_574,c_7]) ).
cnf(c_4632,plain,
earray_131 = rselect_seq(queue_128),
inference(paramod,[status(thm)],[c_83,c_4631]) ).
cnf(c_2073,plain,
earray_131 = earray_127,
inference(paramod,[status(thm)],[c_1029,c_4632]) ).
cnf(c_4633,plain,
rselect_head(q26) = rselect_head(queue_128),
inference(paramod,[status(thm)],[c_574,c_8]) ).
cnf(c_4634,plain,
index_137 = rselect_head(queue_128),
inference(paramod,[status(thm)],[c_1037,c_4633]) ).
cnf(c_2074,plain,
index_137 = index_117,
inference(paramod,[status(thm)],[c_2071,c_4634]) ).
cnf(c_2121,plain,
s(index_126) = index_132,
inference(paramod,[status(thm)],[c_2072,c_211]) ).
cnf(c_2122,plain,
( select(earray_133,A) = select(earray_127,A)
| index_132 = A ),
inference(paramod,[status(thm)],[c_2073,c_602]) ).
cnf(c_2136,plain,
s(index_117) = index_138,
inference(paramod,[status(thm)],[c_2074,c_219]) ).
cnf(c_2168,plain,
rselect_head(q27) = index_138,
inference(paramod,[status(thm)],[c_575,c_4]) ).
cnf(c_4635,plain,
rselect_seq(q27) = rselect_seq(queue_136),
inference(paramod,[status(thm)],[c_575,c_6]) ).
cnf(c_4636,plain,
earray_140 = rselect_seq(queue_136),
inference(paramod,[status(thm)],[c_89,c_4635]) ).
cnf(c_2169,plain,
earray_140 = earray_133,
inference(paramod,[status(thm)],[c_1036,c_4636]) ).
cnf(c_4637,plain,
rselect_tail(q27) = rselect_tail(queue_136),
inference(paramod,[status(thm)],[c_575,c_11]) ).
cnf(c_4638,plain,
index_141 = rselect_tail(queue_136),
inference(paramod,[status(thm)],[c_221,c_4637]) ).
cnf(c_4639,plain,
index_141 = index_135,
inference(paramod,[status(thm)],[c_1035,c_4638]) ).
cnf(c_2170,plain,
index_135 = index_141,
inference(copy,[status(thm)],[c_4639]) ).
cnf(c_2171,plain,
rselect_head(queue_143) = index_138,
inference(paramod,[status(thm)],[c_2168,c_1040]) ).
cnf(c_2172,plain,
( select(earray_142,A) = select(earray_133,A)
| index_141 = A ),
inference(paramod,[status(thm)],[c_2169,c_604]) ).
cnf(c_2222,plain,
s(index_132) = index_141,
inference(paramod,[status(thm)],[c_2170,c_215]) ).
cnf(c_4640,plain,
rselect_tail(q28) = index_144,
inference(paramod,[status(thm)],[c_576,c_5]) ).
cnf(c_4641,plain,
index_147 = index_144,
inference(paramod,[status(thm)],[c_225,c_4640]) ).
cnf(c_2223,plain,
index_144 = index_147,
inference(copy,[status(thm)],[c_4641]) ).
cnf(c_4642,plain,
rselect_seq(q28) = rselect_seq(queue_143),
inference(paramod,[status(thm)],[c_576,c_7]) ).
cnf(c_4643,plain,
earray_146 = rselect_seq(queue_143),
inference(paramod,[status(thm)],[c_93,c_4642]) ).
cnf(c_2224,plain,
earray_146 = earray_142,
inference(paramod,[status(thm)],[c_1039,c_4643]) ).
cnf(c_4644,plain,
rselect_head(q28) = rselect_head(queue_143),
inference(paramod,[status(thm)],[c_576,c_8]) ).
cnf(c_2225,plain,
rselect_head(q28) = index_138,
inference(paramod,[status(thm)],[c_2171,c_4644]) ).
cnf(c_2272,plain,
s(index_141) = index_147,
inference(paramod,[status(thm)],[c_2223,c_223]) ).
cnf(c_2273,plain,
( select(earray_148,A) = select(earray_142,A)
| index_147 = A ),
inference(paramod,[status(thm)],[c_2224,c_606]) ).
cnf(c_2276,plain,
rselect_head(queue_149) = index_138,
inference(paramod,[status(thm)],[c_2225,c_1043]) ).
cnf(c_4645,plain,
rselect_tail(q29) = index_150,
inference(paramod,[status(thm)],[c_577,c_5]) ).
cnf(c_4646,plain,
index_162 = index_150,
inference(paramod,[status(thm)],[c_239,c_4645]) ).
cnf(c_2277,plain,
index_150 = index_162,
inference(copy,[status(thm)],[c_4646]) ).
cnf(c_4647,plain,
rselect_seq(q29) = rselect_seq(queue_149),
inference(paramod,[status(thm)],[c_577,c_7]) ).
cnf(c_4648,plain,
earray_161 = rselect_seq(queue_149),
inference(paramod,[status(thm)],[c_103,c_4647]) ).
cnf(c_2278,plain,
earray_161 = earray_148,
inference(paramod,[status(thm)],[c_1042,c_4648]) ).
cnf(c_4649,plain,
rselect_head(q29) = rselect_head(queue_149),
inference(paramod,[status(thm)],[c_577,c_8]) ).
cnf(c_4650,plain,
index_167 = rselect_head(queue_149),
inference(paramod,[status(thm)],[c_1057,c_4649]) ).
cnf(c_2279,plain,
index_167 = index_138,
inference(paramod,[status(thm)],[c_2276,c_4650]) ).
cnf(c_2326,plain,
s(index_147) = index_162,
inference(paramod,[status(thm)],[c_2277,c_229]) ).
cnf(c_2327,plain,
( select(earray_163,A) = select(earray_148,A)
| index_162 = A ),
inference(paramod,[status(thm)],[c_2278,c_612]) ).
cnf(c_2341,plain,
s(index_138) = index_168,
inference(paramod,[status(thm)],[c_2279,c_245]) ).
cnf(c_4651,plain,
rselect_head(q30) = index_168,
inference(paramod,[status(thm)],[c_579,c_4]) ).
cnf(c_2376,plain,
index_213 = index_168,
inference(paramod,[status(thm)],[c_283,c_4651]) ).
cnf(c_4652,plain,
rselect_seq(q30) = rselect_seq(queue_166),
inference(paramod,[status(thm)],[c_579,c_6]) ).
cnf(c_4653,plain,
earray_212 = rselect_seq(queue_166),
inference(paramod,[status(thm)],[c_135,c_4652]) ).
cnf(c_2377,plain,
earray_212 = earray_163,
inference(paramod,[status(thm)],[c_1056,c_4653]) ).
cnf(c_4654,plain,
select(earray_163,index_213) = elem_214,
inference(paramod,[status(thm)],[c_2377,c_185]) ).
cnf(c_2381,plain,
select(earray_163,index_168) = elem_214,
inference(paramod,[status(thm)],[c_2376,c_4654]) ).
cnf(c_4655,plain,
rselect_tail(q4) = index_174,
inference(paramod,[status(thm)],[c_580,c_5]) ).
cnf(c_4656,plain,
index_177 = index_174,
inference(paramod,[status(thm)],[c_251,c_4655]) ).
cnf(c_2383,plain,
index_174 = index_177,
inference(copy,[status(thm)],[c_4656]) ).
cnf(c_4657,plain,
rselect_head(q4) = rselect_head(queue_173),
inference(paramod,[status(thm)],[c_580,c_8]) ).
cnf(c_2385,plain,
rselect_head(q4) = rselect_head(q3),
inference(paramod,[status(thm)],[c_1063,c_4657]) ).
cnf(c_2396,plain,
s(index_171) = index_177,
inference(paramod,[status(thm)],[c_2383,c_249]) ).
cnf(c_2400,plain,
rselect_head(queue_179) = rselect_head(q3),
inference(paramod,[status(thm)],[c_2385,c_1066]) ).
cnf(c_4658,plain,
rselect_tail(q5) = index_180,
inference(paramod,[status(thm)],[c_581,c_5]) ).
cnf(c_4659,plain,
index_183 = index_180,
inference(paramod,[status(thm)],[c_257,c_4658]) ).
cnf(c_2401,plain,
index_180 = index_183,
inference(copy,[status(thm)],[c_4659]) ).
cnf(c_4660,plain,
rselect_head(q5) = rselect_head(queue_179),
inference(paramod,[status(thm)],[c_581,c_8]) ).
cnf(c_4661,plain,
index_188 = rselect_head(queue_179),
inference(paramod,[status(thm)],[c_1073,c_4660]) ).
cnf(c_4662,plain,
index_188 = rselect_head(q3),
inference(paramod,[status(thm)],[c_2400,c_4661]) ).
cnf(c_2403,plain,
rselect_head(q3) = index_188,
inference(copy,[status(thm)],[c_4662]) ).
cnf(c_2422,plain,
s(index_177) = index_183,
inference(paramod,[status(thm)],[c_2401,c_255]) ).
cnf(c_2429,plain,
rselect_head(q6) = index_189,
inference(paramod,[status(thm)],[c_582,c_4]) ).
cnf(c_4663,plain,
rselect_tail(q6) = rselect_tail(queue_187),
inference(paramod,[status(thm)],[c_582,c_11]) ).
cnf(c_4664,plain,
index_192 = rselect_tail(queue_187),
inference(paramod,[status(thm)],[c_265,c_4663]) ).
cnf(c_4665,plain,
index_192 = index_186,
inference(paramod,[status(thm)],[c_1071,c_4664]) ).
cnf(c_2431,plain,
index_186 = index_192,
inference(copy,[status(thm)],[c_4665]) ).
cnf(c_2432,plain,
rselect_head(queue_194) = index_189,
inference(paramod,[status(thm)],[c_2429,c_1076]) ).
cnf(c_2462,plain,
s(index_183) = index_192,
inference(paramod,[status(thm)],[c_2431,c_259]) ).
cnf(c_4666,plain,
rselect_tail(q7) = index_195,
inference(paramod,[status(thm)],[c_583,c_5]) ).
cnf(c_4667,plain,
index_198 = index_195,
inference(paramod,[status(thm)],[c_269,c_4666]) ).
cnf(c_2463,plain,
index_195 = index_198,
inference(copy,[status(thm)],[c_4667]) ).
cnf(c_4668,plain,
rselect_head(q7) = rselect_head(queue_194),
inference(paramod,[status(thm)],[c_583,c_8]) ).
cnf(c_2465,plain,
rselect_head(q7) = index_189,
inference(paramod,[status(thm)],[c_2432,c_4668]) ).
cnf(c_2497,plain,
s(index_192) = index_198,
inference(paramod,[status(thm)],[c_2463,c_267]) ).
cnf(c_2501,plain,
rselect_head(queue_200) = index_189,
inference(paramod,[status(thm)],[c_2465,c_1079]) ).
cnf(c_4669,plain,
rselect_tail(q8) = index_201,
inference(paramod,[status(thm)],[c_584,c_5]) ).
cnf(c_4670,plain,
index_204 = index_201,
inference(paramod,[status(thm)],[c_273,c_4669]) ).
cnf(c_2502,plain,
index_201 = index_204,
inference(copy,[status(thm)],[c_4670]) ).
cnf(c_4671,plain,
rselect_head(q8) = rselect_head(queue_200),
inference(paramod,[status(thm)],[c_584,c_8]) ).
cnf(c_4672,plain,
index_209 = rselect_head(queue_200),
inference(paramod,[status(thm)],[c_1086,c_4671]) ).
cnf(c_2504,plain,
index_209 = index_189,
inference(paramod,[status(thm)],[c_2501,c_4672]) ).
cnf(c_2541,plain,
s(index_198) = index_204,
inference(paramod,[status(thm)],[c_2502,c_271]) ).
cnf(c_2556,plain,
s(index_189) = index_210,
inference(paramod,[status(thm)],[c_2504,c_281]) ).
cnf(c_4673,plain,
rselect_head(q9) = index_210,
inference(paramod,[status(thm)],[c_585,c_4]) ).
cnf(c_2566,plain,
index_26 = index_210,
inference(paramod,[status(thm)],[c_1209,c_4673]) ).
cnf(c_4674,plain,
rselect_tail(q9) = rselect_tail(queue_208),
inference(paramod,[status(thm)],[c_585,c_11]) ).
cnf(c_4675,plain,
index_9 = rselect_tail(queue_208),
inference(paramod,[status(thm)],[c_339,c_4674]) ).
cnf(c_4676,plain,
index_9 = index_207,
inference(paramod,[status(thm)],[c_1084,c_4675]) ).
cnf(c_2568,plain,
index_207 = index_9,
inference(copy,[status(thm)],[c_4676]) ).
cnf(c_2584,plain,
s(index_210) = index_27,
inference(paramod,[status(thm)],[c_2566,c_289]) ).
cnf(c_2630,plain,
s(index_204) = index_9,
inference(paramod,[status(thm)],[c_2568,c_275]) ).
cnf(c_4677,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_43]) ).
cnf(c_4678,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4677]) ).
cnf(c_4679,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4678]) ).
cnf(c_4680,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4679]) ).
cnf(c_4681,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4680]) ).
cnf(c_4682,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4681]) ).
cnf(c_4683,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_63)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4682]) ).
cnf(c_4684,plain,
s(s(s(s(s(s(s(s(s(s(s(index_72))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4683]) ).
cnf(c_4685,plain,
s(s(s(s(s(s(s(s(s(s(index_84)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4684]) ).
cnf(c_4686,plain,
s(s(s(s(s(s(s(s(s(index_90))))))))) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4685]) ).
cnf(c_4687,plain,
s(s(s(s(s(s(s(s(index_99)))))))) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4686]) ).
cnf(c_4688,plain,
s(s(s(s(s(s(s(index_105))))))) != index_15,
inference(paramod,[status(thm)],[c_1869,c_4687]) ).
cnf(c_4689,plain,
s(s(s(s(s(s(index_111)))))) != index_15,
inference(paramod,[status(thm)],[c_1923,c_4688]) ).
cnf(c_4690,plain,
s(s(s(s(s(index_120))))) != index_15,
inference(paramod,[status(thm)],[c_2017,c_4689]) ).
cnf(c_4691,plain,
s(s(s(s(index_126)))) != index_15,
inference(paramod,[status(thm)],[c_2067,c_4690]) ).
cnf(c_4692,plain,
s(s(s(index_132))) != index_15,
inference(paramod,[status(thm)],[c_2121,c_4691]) ).
cnf(c_4693,plain,
s(s(index_141)) != index_15,
inference(paramod,[status(thm)],[c_2222,c_4692]) ).
cnf(c_4694,plain,
s(index_147) != index_15,
inference(paramod,[status(thm)],[c_2272,c_4693]) ).
cnf(c_2812,plain,
index_162 != index_15,
inference(paramod,[status(thm)],[c_2326,c_4694]) ).
cnf(c_4695,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_44]) ).
cnf(c_4696,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4695]) ).
cnf(c_4697,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4696]) ).
cnf(c_4698,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4697]) ).
cnf(c_4699,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4698]) ).
cnf(c_4700,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4699]) ).
cnf(c_4701,plain,
s(s(s(s(s(s(s(s(s(s(s(index_63))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4700]) ).
cnf(c_4702,plain,
s(s(s(s(s(s(s(s(s(s(index_72)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4701]) ).
cnf(c_4703,plain,
s(s(s(s(s(s(s(s(s(index_84))))))))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4702]) ).
cnf(c_4704,plain,
s(s(s(s(s(s(s(s(index_90)))))))) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4703]) ).
cnf(c_4705,plain,
s(s(s(s(s(s(s(index_99))))))) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4704]) ).
cnf(c_4706,plain,
s(s(s(s(s(s(index_105)))))) != index_15,
inference(paramod,[status(thm)],[c_1869,c_4705]) ).
cnf(c_4707,plain,
s(s(s(s(s(index_111))))) != index_15,
inference(paramod,[status(thm)],[c_1923,c_4706]) ).
cnf(c_4708,plain,
s(s(s(s(index_120)))) != index_15,
inference(paramod,[status(thm)],[c_2017,c_4707]) ).
cnf(c_4709,plain,
s(s(s(index_126))) != index_15,
inference(paramod,[status(thm)],[c_2067,c_4708]) ).
cnf(c_4710,plain,
s(s(index_132)) != index_15,
inference(paramod,[status(thm)],[c_2121,c_4709]) ).
cnf(c_4711,plain,
s(index_141) != index_15,
inference(paramod,[status(thm)],[c_2222,c_4710]) ).
cnf(c_4712,plain,
index_147 != index_15,
inference(paramod,[status(thm)],[c_2272,c_4711]) ).
cnf(c_2813,plain,
index_15 != index_147,
inference(copy,[status(thm)],[c_4712]) ).
cnf(c_4713,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_45]) ).
cnf(c_4714,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4713]) ).
cnf(c_4715,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4714]) ).
cnf(c_4716,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4715]) ).
cnf(c_4717,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4716]) ).
cnf(c_4718,plain,
s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4717]) ).
cnf(c_4719,plain,
s(s(s(s(s(s(s(s(s(s(index_63)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4718]) ).
cnf(c_4720,plain,
s(s(s(s(s(s(s(s(s(index_72))))))))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4719]) ).
cnf(c_4721,plain,
s(s(s(s(s(s(s(s(index_84)))))))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4720]) ).
cnf(c_4722,plain,
s(s(s(s(s(s(s(index_90))))))) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4721]) ).
cnf(c_4723,plain,
s(s(s(s(s(s(index_99)))))) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4722]) ).
cnf(c_4724,plain,
s(s(s(s(s(index_105))))) != index_15,
inference(paramod,[status(thm)],[c_1869,c_4723]) ).
cnf(c_4725,plain,
s(s(s(s(index_111)))) != index_15,
inference(paramod,[status(thm)],[c_1923,c_4724]) ).
cnf(c_4726,plain,
s(s(s(index_120))) != index_15,
inference(paramod,[status(thm)],[c_2017,c_4725]) ).
cnf(c_4727,plain,
s(s(index_126)) != index_15,
inference(paramod,[status(thm)],[c_2067,c_4726]) ).
cnf(c_4728,plain,
s(index_132) != index_15,
inference(paramod,[status(thm)],[c_2121,c_4727]) ).
cnf(c_4729,plain,
index_141 != index_15,
inference(paramod,[status(thm)],[c_2222,c_4728]) ).
cnf(c_2814,plain,
index_15 != index_141,
inference(copy,[status(thm)],[c_4729]) ).
cnf(c_4730,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_46]) ).
cnf(c_4731,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4730]) ).
cnf(c_4732,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4731]) ).
cnf(c_4733,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4732]) ).
cnf(c_4734,plain,
s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4733]) ).
cnf(c_4735,plain,
s(s(s(s(s(s(s(s(s(s(index_57)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4734]) ).
cnf(c_4736,plain,
s(s(s(s(s(s(s(s(s(index_63))))))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4735]) ).
cnf(c_4737,plain,
s(s(s(s(s(s(s(s(index_72)))))))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4736]) ).
cnf(c_4738,plain,
s(s(s(s(s(s(s(index_84))))))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4737]) ).
cnf(c_4739,plain,
s(s(s(s(s(s(index_90)))))) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4738]) ).
cnf(c_4740,plain,
s(s(s(s(s(index_99))))) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4739]) ).
cnf(c_4741,plain,
s(s(s(s(index_105)))) != index_15,
inference(paramod,[status(thm)],[c_1869,c_4740]) ).
cnf(c_4742,plain,
s(s(s(index_111))) != index_15,
inference(paramod,[status(thm)],[c_1923,c_4741]) ).
cnf(c_4743,plain,
s(s(index_120)) != index_15,
inference(paramod,[status(thm)],[c_2017,c_4742]) ).
cnf(c_4744,plain,
s(index_126) != index_15,
inference(paramod,[status(thm)],[c_2067,c_4743]) ).
cnf(c_4745,plain,
index_132 != index_15,
inference(paramod,[status(thm)],[c_2121,c_4744]) ).
cnf(c_2815,plain,
index_15 != index_132,
inference(copy,[status(thm)],[c_4745]) ).
cnf(c_4746,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_47]) ).
cnf(c_4747,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4746]) ).
cnf(c_4748,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4747]) ).
cnf(c_4749,plain,
s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4748]) ).
cnf(c_4750,plain,
s(s(s(s(s(s(s(s(s(s(index_51)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4749]) ).
cnf(c_4751,plain,
s(s(s(s(s(s(s(s(s(index_57))))))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4750]) ).
cnf(c_4752,plain,
s(s(s(s(s(s(s(s(index_63)))))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4751]) ).
cnf(c_4753,plain,
s(s(s(s(s(s(s(index_72))))))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4752]) ).
cnf(c_4754,plain,
s(s(s(s(s(s(index_84)))))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4753]) ).
cnf(c_4755,plain,
s(s(s(s(s(index_90))))) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4754]) ).
cnf(c_4756,plain,
s(s(s(s(index_99)))) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4755]) ).
cnf(c_4757,plain,
s(s(s(index_105))) != index_15,
inference(paramod,[status(thm)],[c_1869,c_4756]) ).
cnf(c_4758,plain,
s(s(index_111)) != index_15,
inference(paramod,[status(thm)],[c_1923,c_4757]) ).
cnf(c_4759,plain,
s(index_120) != index_15,
inference(paramod,[status(thm)],[c_2017,c_4758]) ).
cnf(c_4760,plain,
index_126 != index_15,
inference(paramod,[status(thm)],[c_2067,c_4759]) ).
cnf(c_2816,plain,
index_15 != index_126,
inference(copy,[status(thm)],[c_4760]) ).
cnf(c_4761,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_48]) ).
cnf(c_4762,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4761]) ).
cnf(c_4763,plain,
s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4762]) ).
cnf(c_4764,plain,
s(s(s(s(s(s(s(s(s(s(index_42)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4763]) ).
cnf(c_4765,plain,
s(s(s(s(s(s(s(s(s(index_51))))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4764]) ).
cnf(c_4766,plain,
s(s(s(s(s(s(s(s(index_57)))))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4765]) ).
cnf(c_4767,plain,
s(s(s(s(s(s(s(index_63))))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4766]) ).
cnf(c_4768,plain,
s(s(s(s(s(s(index_72)))))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4767]) ).
cnf(c_4769,plain,
s(s(s(s(s(index_84))))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4768]) ).
cnf(c_4770,plain,
s(s(s(s(index_90)))) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4769]) ).
cnf(c_4771,plain,
s(s(s(index_99))) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4770]) ).
cnf(c_4772,plain,
s(s(index_105)) != index_15,
inference(paramod,[status(thm)],[c_1869,c_4771]) ).
cnf(c_4773,plain,
s(index_111) != index_15,
inference(paramod,[status(thm)],[c_1923,c_4772]) ).
cnf(c_4774,plain,
index_120 != index_15,
inference(paramod,[status(thm)],[c_2017,c_4773]) ).
cnf(c_2817,plain,
index_15 != index_120,
inference(copy,[status(thm)],[c_4774]) ).
cnf(c_4775,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_49]) ).
cnf(c_4776,plain,
s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4775]) ).
cnf(c_4777,plain,
s(s(s(s(s(s(s(s(s(s(index_36)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4776]) ).
cnf(c_4778,plain,
s(s(s(s(s(s(s(s(s(index_42))))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4777]) ).
cnf(c_4779,plain,
s(s(s(s(s(s(s(s(index_51)))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4778]) ).
cnf(c_4780,plain,
s(s(s(s(s(s(s(index_57))))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4779]) ).
cnf(c_4781,plain,
s(s(s(s(s(s(index_63)))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4780]) ).
cnf(c_4782,plain,
s(s(s(s(s(index_72))))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4781]) ).
cnf(c_4783,plain,
s(s(s(s(index_84)))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4782]) ).
cnf(c_4784,plain,
s(s(s(index_90))) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4783]) ).
cnf(c_4785,plain,
s(s(index_99)) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4784]) ).
cnf(c_4786,plain,
s(index_105) != index_15,
inference(paramod,[status(thm)],[c_1869,c_4785]) ).
cnf(c_4787,plain,
index_111 != index_15,
inference(paramod,[status(thm)],[c_1923,c_4786]) ).
cnf(c_2818,plain,
index_15 != index_111,
inference(copy,[status(thm)],[c_4787]) ).
cnf(c_4788,plain,
s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_50]) ).
cnf(c_4789,plain,
s(s(s(s(s(s(s(s(s(s(index_30)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4788]) ).
cnf(c_4790,plain,
s(s(s(s(s(s(s(s(s(index_36))))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4789]) ).
cnf(c_4791,plain,
s(s(s(s(s(s(s(s(index_42)))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4790]) ).
cnf(c_4792,plain,
s(s(s(s(s(s(s(index_51))))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4791]) ).
cnf(c_4793,plain,
s(s(s(s(s(s(index_57)))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4792]) ).
cnf(c_4794,plain,
s(s(s(s(s(index_63))))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4793]) ).
cnf(c_4795,plain,
s(s(s(s(index_72)))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4794]) ).
cnf(c_4796,plain,
s(s(s(index_84))) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4795]) ).
cnf(c_4797,plain,
s(s(index_90)) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4796]) ).
cnf(c_4798,plain,
s(index_99) != index_15,
inference(paramod,[status(thm)],[c_1819,c_4797]) ).
cnf(c_4799,plain,
index_105 != index_15,
inference(paramod,[status(thm)],[c_1869,c_4798]) ).
cnf(c_2819,plain,
index_15 != index_105,
inference(copy,[status(thm)],[c_4799]) ).
cnf(c_4800,plain,
s(s(s(s(s(s(s(s(s(s(index_21)))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_51]) ).
cnf(c_4801,plain,
s(s(s(s(s(s(s(s(s(index_30))))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4800]) ).
cnf(c_4802,plain,
s(s(s(s(s(s(s(s(index_36)))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4801]) ).
cnf(c_4803,plain,
s(s(s(s(s(s(s(index_42))))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4802]) ).
cnf(c_4804,plain,
s(s(s(s(s(s(index_51)))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4803]) ).
cnf(c_4805,plain,
s(s(s(s(s(index_57))))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4804]) ).
cnf(c_4806,plain,
s(s(s(s(index_63)))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4805]) ).
cnf(c_4807,plain,
s(s(s(index_72))) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4806]) ).
cnf(c_4808,plain,
s(s(index_84)) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4807]) ).
cnf(c_4809,plain,
s(index_90) != index_15,
inference(paramod,[status(thm)],[c_1727,c_4808]) ).
cnf(c_2820,plain,
index_99 != index_15,
inference(paramod,[status(thm)],[c_1819,c_4809]) ).
cnf(c_4810,plain,
s(s(s(s(s(s(s(s(s(index_21))))))))) != index_15,
inference(paramod,[status(thm)],[c_1204,c_52]) ).
cnf(c_4811,plain,
s(s(s(s(s(s(s(s(index_30)))))))) != index_15,
inference(paramod,[status(thm)],[c_1244,c_4810]) ).
cnf(c_4812,plain,
s(s(s(s(s(s(s(index_36))))))) != index_15,
inference(paramod,[status(thm)],[c_1279,c_4811]) ).
cnf(c_4813,plain,
s(s(s(s(s(s(index_42)))))) != index_15,
inference(paramod,[status(thm)],[c_1323,c_4812]) ).
cnf(c_4814,plain,
s(s(s(s(s(index_51))))) != index_15,
inference(paramod,[status(thm)],[c_1396,c_4813]) ).
cnf(c_4815,plain,
s(s(s(s(index_57)))) != index_15,
inference(paramod,[status(thm)],[c_1443,c_4814]) ).
cnf(c_4816,plain,
s(s(s(index_63))) != index_15,
inference(paramod,[status(thm)],[c_1496,c_4815]) ).
cnf(c_4817,plain,
s(s(index_72)) != index_15,
inference(paramod,[status(thm)],[c_1582,c_4816]) ).
cnf(c_4818,plain,
s(index_84) != index_15,
inference(paramod,[status(thm)],[c_1632,c_4817]) ).
cnf(c_2821,plain,
index_90 != index_15,
inference(paramod,[status(thm)],[c_1727,c_4818]) ).
cnf(c_4819,plain,
( select(earray_22,index_15) = e10
| index_21 = index_15 ),
inference(paramod,[status(thm)],[c_609,c_1205]) ).
cnf(c_3012,plain,
select(earray_22,index_15) = e10,
inference(resolve,[status(thm)],[c_1194,c_4819]) ).
cnf(c_4820,plain,
rselect_head(q3) = index_78,
inference(paramod,[status(thm)],[c_1677,c_4]) ).
cnf(c_3227,plain,
index_188 = index_78,
inference(paramod,[status(thm)],[c_2403,c_4820]) ).
cnf(c_4821,plain,
rselect_tail(q3) = rselect_tail(queue_157),
inference(paramod,[status(thm)],[c_1677,c_11]) ).
cnf(c_4822,plain,
index_171 = rselect_tail(queue_157),
inference(paramod,[status(thm)],[c_247,c_4821]) ).
cnf(c_4823,plain,
index_171 = index_156,
inference(paramod,[status(thm)],[c_1048,c_4822]) ).
cnf(c_3229,plain,
index_156 = index_171,
inference(copy,[status(thm)],[c_4823]) ).
cnf(c_4824,plain,
s(index_78) = index_189,
inference(paramod,[status(thm)],[c_3227,c_263]) ).
cnf(c_4825,plain,
index_153 = index_189,
inference(paramod,[status(thm)],[c_1658,c_4824]) ).
cnf(c_3245,plain,
index_189 = index_153,
inference(copy,[status(thm)],[c_4825]) ).
cnf(c_3286,plain,
s(index_153) = index_171,
inference(paramod,[status(thm)],[c_3229,c_233]) ).
cnf(c_4826,plain,
s(index_153) = index_210,
inference(paramod,[status(thm)],[c_3245,c_2556]) ).
cnf(c_4827,plain,
index_171 = index_210,
inference(paramod,[status(thm)],[c_3286,c_4826]) ).
cnf(c_3303,plain,
index_210 = index_171,
inference(copy,[status(thm)],[c_4827]) ).
cnf(c_4828,plain,
s(index_171) = index_27,
inference(paramod,[status(thm)],[c_3303,c_2584]) ).
cnf(c_4829,plain,
index_177 = index_27,
inference(paramod,[status(thm)],[c_2396,c_4828]) ).
cnf(c_3319,plain,
index_27 = index_177,
inference(copy,[status(thm)],[c_4829]) ).
cnf(c_4830,plain,
s(index_177) = index_48,
inference(paramod,[status(thm)],[c_3319,c_1338]) ).
cnf(c_4831,plain,
index_183 = index_48,
inference(paramod,[status(thm)],[c_2422,c_4830]) ).
cnf(c_3350,plain,
index_48 = index_183,
inference(copy,[status(thm)],[c_4831]) ).
cnf(c_4832,plain,
s(index_183) = index_69,
inference(paramod,[status(thm)],[c_3350,c_1511]) ).
cnf(c_4833,plain,
index_192 = index_69,
inference(paramod,[status(thm)],[c_2462,c_4832]) ).
cnf(c_3372,plain,
index_69 = index_192,
inference(copy,[status(thm)],[c_4833]) ).
cnf(c_4834,plain,
s(index_192) = index_116,
inference(paramod,[status(thm)],[c_3372,c_1952]) ).
cnf(c_4835,plain,
index_198 = index_116,
inference(paramod,[status(thm)],[c_2497,c_4834]) ).
cnf(c_3393,plain,
index_116 = index_198,
inference(copy,[status(thm)],[c_4835]) ).
cnf(c_4836,plain,
s(index_198) = index_117,
inference(paramod,[status(thm)],[c_3393,c_201]) ).
cnf(c_4837,plain,
index_204 = index_117,
inference(paramod,[status(thm)],[c_2541,c_4836]) ).
cnf(c_3420,plain,
index_117 = index_204,
inference(copy,[status(thm)],[c_4837]) ).
cnf(c_4838,plain,
s(index_204) = index_138,
inference(paramod,[status(thm)],[c_3420,c_2136]) ).
cnf(c_4839,plain,
index_9 = index_138,
inference(paramod,[status(thm)],[c_2630,c_4838]) ).
cnf(c_3432,plain,
index_138 = index_9,
inference(copy,[status(thm)],[c_4839]) ).
cnf(c_4840,plain,
s(index_9) = index_168,
inference(paramod,[status(thm)],[c_3432,c_2341]) ).
cnf(c_4841,plain,
index_15 = index_168,
inference(paramod,[status(thm)],[c_1178,c_4840]) ).
cnf(c_3442,plain,
index_168 = index_15,
inference(copy,[status(thm)],[c_4841]) ).
cnf(c_3458,plain,
select(earray_163,index_15) = elem_214,
inference(paramod,[status(thm)],[c_3442,c_2381]) ).
cnf(c_4842,plain,
( select(earray_31,index_15) = e10
| index_30 = index_15 ),
inference(paramod,[status(thm)],[c_3012,c_1215]) ).
cnf(c_3574,plain,
select(earray_31,index_15) = e10,
inference(resolve,[status(thm)],[c_1225,c_4842]) ).
cnf(c_4843,plain,
( select(earray_37,index_15) = e10
| index_36 = index_15 ),
inference(paramod,[status(thm)],[c_3574,c_1280]) ).
cnf(c_3661,plain,
select(earray_37,index_15) = e10,
inference(resolve,[status(thm)],[c_1262,c_4843]) ).
cnf(c_4844,plain,
( select(earray_43,index_15) = e10
| index_42 = index_15 ),
inference(paramod,[status(thm)],[c_3661,c_1324]) ).
cnf(c_3750,plain,
select(earray_43,index_15) = e10,
inference(resolve,[status(thm)],[c_1300,c_4844]) ).
cnf(c_4845,plain,
( select(earray_52,index_15) = e10
| index_51 = index_15 ),
inference(paramod,[status(thm)],[c_3750,c_1352]) ).
cnf(c_3825,plain,
select(earray_52,index_15) = e10,
inference(resolve,[status(thm)],[c_1373,c_4845]) ).
cnf(c_4846,plain,
( select(earray_58,index_15) = e10
| index_57 = index_15 ),
inference(paramod,[status(thm)],[c_3825,c_1444]) ).
cnf(c_3895,plain,
select(earray_58,index_15) = e10,
inference(resolve,[status(thm)],[c_1417,c_4846]) ).
cnf(c_4847,plain,
( select(earray_148,index_15) = elem_214
| index_162 = index_15 ),
inference(paramod,[status(thm)],[c_2327,c_3458]) ).
cnf(c_3927,plain,
select(earray_148,index_15) = elem_214,
inference(resolve,[status(thm)],[c_2812,c_4847]) ).
cnf(c_4848,plain,
( select(earray_64,index_15) = e10
| index_63 = index_15 ),
inference(paramod,[status(thm)],[c_3895,c_1497]) ).
cnf(c_3972,plain,
select(earray_64,index_15) = e10,
inference(resolve,[status(thm)],[c_1471,c_4848]) ).
cnf(c_4849,plain,
( elem_214 = select(earray_142,index_15)
| index_147 = index_15 ),
inference(paramod,[status(thm)],[c_3927,c_2273]) ).
cnf(c_4850,plain,
( elem_214 = select(earray_142,index_15)
| index_15 = index_147 ),
inference(copy,[status(thm)],[c_4849]) ).
cnf(c_4851,plain,
( select(earray_142,index_15) = elem_214
| index_15 = index_147 ),
inference(copy,[status(thm)],[c_4850]) ).
cnf(c_4011,plain,
select(earray_142,index_15) = elem_214,
inference(resolve,[status(thm)],[c_2813,c_4851]) ).
cnf(c_4852,plain,
( select(earray_73,index_15) = e10
| index_72 = index_15 ),
inference(paramod,[status(thm)],[c_3972,c_1532]) ).
cnf(c_4067,plain,
select(earray_73,index_15) = e10,
inference(resolve,[status(thm)],[c_1554,c_4852]) ).
cnf(c_4853,plain,
( elem_214 = select(earray_133,index_15)
| index_141 = index_15 ),
inference(paramod,[status(thm)],[c_4011,c_2172]) ).
cnf(c_4854,plain,
( elem_214 = select(earray_133,index_15)
| index_15 = index_141 ),
inference(copy,[status(thm)],[c_4853]) ).
cnf(c_4855,plain,
( select(earray_133,index_15) = elem_214
| index_15 = index_141 ),
inference(copy,[status(thm)],[c_4854]) ).
cnf(c_4108,plain,
select(earray_133,index_15) = elem_214,
inference(resolve,[status(thm)],[c_2814,c_4855]) ).
cnf(c_4856,plain,
( select(earray_85,index_15) = e10
| index_84 = index_15 ),
inference(paramod,[status(thm)],[c_4067,c_1633]) ).
cnf(c_4143,plain,
select(earray_85,index_15) = e10,
inference(resolve,[status(thm)],[c_1606,c_4856]) ).
cnf(c_4857,plain,
( elem_214 = select(earray_127,index_15)
| index_132 = index_15 ),
inference(paramod,[status(thm)],[c_4108,c_2122]) ).
cnf(c_4858,plain,
( elem_214 = select(earray_127,index_15)
| index_15 = index_132 ),
inference(copy,[status(thm)],[c_4857]) ).
cnf(c_4859,plain,
( select(earray_127,index_15) = elem_214
| index_15 = index_132 ),
inference(copy,[status(thm)],[c_4858]) ).
cnf(c_4188,plain,
select(earray_127,index_15) = elem_214,
inference(resolve,[status(thm)],[c_2815,c_4859]) ).
cnf(c_4860,plain,
( select(earray_91,index_15) = e10
| index_90 = index_15 ),
inference(paramod,[status(thm)],[c_4143,c_1728]) ).
cnf(c_4228,plain,
select(earray_91,index_15) = e10,
inference(resolve,[status(thm)],[c_2821,c_4860]) ).
cnf(c_4861,plain,
( elem_214 = select(earray_121,index_15)
| index_126 = index_15 ),
inference(paramod,[status(thm)],[c_4188,c_2068]) ).
cnf(c_4862,plain,
( elem_214 = select(earray_121,index_15)
| index_15 = index_126 ),
inference(copy,[status(thm)],[c_4861]) ).
cnf(c_4863,plain,
( select(earray_121,index_15) = elem_214
| index_15 = index_126 ),
inference(copy,[status(thm)],[c_4862]) ).
cnf(c_4277,plain,
select(earray_121,index_15) = elem_214,
inference(resolve,[status(thm)],[c_2816,c_4863]) ).
cnf(c_4864,plain,
( e10 = select(earray_100,index_15)
| index_99 = index_15 ),
inference(paramod,[status(thm)],[c_4228,c_1769]) ).
cnf(c_4865,plain,
( select(earray_100,index_15) = e10
| index_99 = index_15 ),
inference(copy,[status(thm)],[c_4864]) ).
cnf(c_4310,plain,
select(earray_100,index_15) = e10,
inference(resolve,[status(thm)],[c_2820,c_4865]) ).
cnf(c_4866,plain,
( elem_214 = select(earray_112,index_15)
| index_120 = index_15 ),
inference(paramod,[status(thm)],[c_4277,c_1967]) ).
cnf(c_4867,plain,
( elem_214 = select(earray_112,index_15)
| index_15 = index_120 ),
inference(copy,[status(thm)],[c_4866]) ).
cnf(c_4868,plain,
( select(earray_112,index_15) = elem_214
| index_15 = index_120 ),
inference(copy,[status(thm)],[c_4867]) ).
cnf(c_4374,plain,
select(earray_112,index_15) = elem_214,
inference(resolve,[status(thm)],[c_2817,c_4868]) ).
cnf(c_4869,plain,
( select(earray_106,index_15) = e10
| index_105 = index_15 ),
inference(paramod,[status(thm)],[c_4310,c_1870]) ).
cnf(c_4870,plain,
( select(earray_106,index_15) = e10
| index_15 = index_105 ),
inference(copy,[status(thm)],[c_4869]) ).
cnf(c_4406,plain,
select(earray_106,index_15) = e10,
inference(resolve,[status(thm)],[c_2819,c_4870]) ).
cnf(c_4871,plain,
( elem_214 = select(earray_106,index_15)
| index_111 = index_15 ),
inference(paramod,[status(thm)],[c_4374,c_1924]) ).
cnf(c_4872,plain,
( elem_214 = e10
| index_111 = index_15 ),
inference(paramod,[status(thm)],[c_4406,c_4871]) ).
cnf(c_4873,plain,
( elem_214 = e10
| index_15 = index_111 ),
inference(copy,[status(thm)],[c_4872]) ).
cnf(c_4874,plain,
elem_214 = e10,
inference(resolve,[status(thm)],[c_2818,c_4873]) ).
cnf(c_4455,plain,
$false,
inference(resolve,[status(thm)],[c_554,c_4874]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV568-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n008.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 14:30:54 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 3861501 was started by sandbox on n008,
% 0.08/0.36 % Sat Sep 26 14:30:54 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 15.15/2.33
% 15.15/2.33 % given #500 (T,wt=14): 1012 rselect_tail(queue_101) = index_99. [para(353(a,1),10(a,1,1)),rewrite([349(4)])].
% 15.15/2.33
% 15.15/2.33 % given #1000 (W,wt=8): 3054 index_63 != index_171. [para(2396(a,1),48(a,1,1,1,1,1,1,1,1,1,1,1,1,1,1)),rewrite([2422(2),2462(2),2497(2),2541(2),2630(2),1178(2),1204(2),1244(2),1279(2),1323(2),1396(2),1443(2),1496(2)])].
% 15.15/2.33
% 15.15/2.33 % given #1500 (F,wt=58): 2881 s(s(s(s(s(index_165))))) != index_42. [para(1396(a,1),41(a,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1)),rewrite([1443(2),1496(2),1582(2),1632(2),1727(2),1819(2),1869(2),1923(2),2017(2),2067(2),2121(2),2222(2),2272(2),2326(2),241(2)])].
% 15.15/2.33
% 15.15/2.33 % SZS status Unsatisfiable for theBenchmark
% 15.15/2.33
% 15.15/2.33 % Proof 1 at 1.65 (+ 0.20) seconds.
% 15.15/2.33 % Length of proof is 856.
% 15.15/2.33 % Level of proof is 27.
% 15.15/2.33 % Maximum clause weight is 212.000.
% 15.15/2.33 % Given clauses 1701.
% 15.15/2.33
% 15.15/2.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------