%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV569-1.030 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:42 AM UTC 2026
% Result : Unsatisfiable 48.78s 12.69s
% Output : CNFRefutation 56.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 83
% Number of leaves : 249
% Syntax : Number of formulae : 1732 (1313 unt; 0 def)
% Number of atoms : 2151 (2150 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 744 ( 325 ~; 419 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 263 ( 263 usr; 260 con; 0-3 aty)
% Number of variables : 205 ( 4 sgn 26 !; 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(head_distinct_from_tail,axiom,
head != tail,
file('theBenchmark.p',head_distinct_from_tail) ).
cnf(c_3,plain,
head != tail,
inference(clausify,[status(thm)],[head_distinct_from_tail]) ).
fof(head_distinct_from_seq,axiom,
head != seq,
file('theBenchmark.p',head_distinct_from_seq) ).
cnf(c_4,plain,
head != seq,
inference(clausify,[status(thm)],[head_distinct_from_seq]) ).
fof(tail_distinct_from_seq,axiom,
tail != seq,
file('theBenchmark.p',tail_distinct_from_seq) ).
cnf(c_5,plain,
tail != seq,
inference(clausify,[status(thm)],[tail_distinct_from_seq]) ).
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_37,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_38,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_39,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_40,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_41,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_42,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_43,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_44,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_45,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_46,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_47,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_48,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_49,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_50,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_51,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_52,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_53,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_54,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_55,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_58,plain,
earray_100 = store(earray_98,index_99,e21),
inference(clausify,[status(thm)],[hyp1]) ).
cnf(c_59,plain,
store(earray_98,index_99,e21) = earray_100,
inference(copy,[status(thm)],[c_58]) ).
fof(hyp2,axiom,
earray_104 = select(q22,seq),
file('theBenchmark.p',hyp2) ).
cnf(c_60,plain,
earray_104 = select(q22,seq),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_61,plain,
select(q22,seq) = earray_104,
inference(copy,[status(thm)],[c_60]) ).
fof(hyp3,axiom,
earray_106 = store(earray_104,index_105,e22),
file('theBenchmark.p',hyp3) ).
cnf(c_62,plain,
earray_106 = store(earray_104,index_105,e22),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_63,plain,
store(earray_104,index_105,e22) = earray_106,
inference(copy,[status(thm)],[c_62]) ).
fof(hyp4,axiom,
earray_110 = select(q23,seq),
file('theBenchmark.p',hyp4) ).
cnf(c_64,plain,
earray_110 = select(q23,seq),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_65,plain,
select(q23,seq) = earray_110,
inference(copy,[status(thm)],[c_64]) ).
fof(hyp5,axiom,
earray_112 = store(earray_110,index_111,e23),
file('theBenchmark.p',hyp5) ).
cnf(c_66,plain,
earray_112 = store(earray_110,index_111,e23),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_67,plain,
store(earray_110,index_111,e23) = earray_112,
inference(copy,[status(thm)],[c_66]) ).
fof(hyp6,axiom,
earray_119 = select(q24,seq),
file('theBenchmark.p',hyp6) ).
cnf(c_68,plain,
earray_119 = select(q24,seq),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_69,plain,
select(q24,seq) = earray_119,
inference(copy,[status(thm)],[c_68]) ).
fof(hyp7,axiom,
earray_121 = store(earray_119,index_120,e24),
file('theBenchmark.p',hyp7) ).
cnf(c_70,plain,
earray_121 = store(earray_119,index_120,e24),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_71,plain,
store(earray_119,index_120,e24) = earray_121,
inference(copy,[status(thm)],[c_70]) ).
fof(hyp8,axiom,
earray_125 = select(q25,seq),
file('theBenchmark.p',hyp8) ).
cnf(c_72,plain,
earray_125 = select(q25,seq),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_73,plain,
select(q25,seq) = earray_125,
inference(copy,[status(thm)],[c_72]) ).
fof(hyp9,axiom,
earray_127 = store(earray_125,index_126,e25),
file('theBenchmark.p',hyp9) ).
cnf(c_74,plain,
earray_127 = store(earray_125,index_126,e25),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_75,plain,
store(earray_125,index_126,e25) = earray_127,
inference(copy,[status(thm)],[c_74]) ).
fof(hyp10,axiom,
earray_131 = select(q26,seq),
file('theBenchmark.p',hyp10) ).
cnf(c_76,plain,
earray_131 = select(q26,seq),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_77,plain,
select(q26,seq) = earray_131,
inference(copy,[status(thm)],[c_76]) ).
fof(hyp11,axiom,
earray_133 = store(earray_131,index_132,e26),
file('theBenchmark.p',hyp11) ).
cnf(c_78,plain,
earray_133 = store(earray_131,index_132,e26),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_79,plain,
store(earray_131,index_132,e26) = earray_133,
inference(copy,[status(thm)],[c_78]) ).
fof(hyp13,axiom,
earray_140 = select(q27,seq),
file('theBenchmark.p',hyp13) ).
cnf(c_82,plain,
earray_140 = select(q27,seq),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_83,plain,
select(q27,seq) = earray_140,
inference(copy,[status(thm)],[c_82]) ).
fof(hyp14,axiom,
earray_142 = store(earray_140,index_141,e27),
file('theBenchmark.p',hyp14) ).
cnf(c_84,plain,
earray_142 = store(earray_140,index_141,e27),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_85,plain,
store(earray_140,index_141,e27) = earray_142,
inference(copy,[status(thm)],[c_84]) ).
fof(hyp15,axiom,
earray_146 = select(q28,seq),
file('theBenchmark.p',hyp15) ).
cnf(c_86,plain,
earray_146 = select(q28,seq),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_87,plain,
select(q28,seq) = earray_146,
inference(copy,[status(thm)],[c_86]) ).
fof(hyp16,axiom,
earray_148 = store(earray_146,index_147,e28),
file('theBenchmark.p',hyp16) ).
cnf(c_88,plain,
earray_148 = store(earray_146,index_147,e28),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_89,plain,
store(earray_146,index_147,e28) = earray_148,
inference(copy,[status(thm)],[c_88]) ).
fof(hyp19,axiom,
earray_16 = store(earray_14,index_15,e10),
file('theBenchmark.p',hyp19) ).
cnf(c_94,plain,
earray_16 = store(earray_14,index_15,e10),
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_95,plain,
store(earray_14,index_15,e10) = earray_16,
inference(copy,[status(thm)],[c_94]) ).
fof(hyp20,axiom,
earray_161 = select(q29,seq),
file('theBenchmark.p',hyp20) ).
cnf(c_96,plain,
earray_161 = select(q29,seq),
inference(clausify,[status(thm)],[hyp20]) ).
cnf(c_97,plain,
select(q29,seq) = earray_161,
inference(copy,[status(thm)],[c_96]) ).
fof(hyp21,axiom,
earray_163 = store(earray_161,index_162,e29),
file('theBenchmark.p',hyp21) ).
cnf(c_98,plain,
earray_163 = store(earray_161,index_162,e29),
inference(clausify,[status(thm)],[hyp21]) ).
cnf(c_99,plain,
store(earray_161,index_162,e29) = earray_163,
inference(copy,[status(thm)],[c_98]) ).
fof(hyp33,axiom,
earray_20 = select(q11,seq),
file('theBenchmark.p',hyp33) ).
cnf(c_122,plain,
earray_20 = select(q11,seq),
inference(clausify,[status(thm)],[hyp33]) ).
cnf(c_123,plain,
select(q11,seq) = earray_20,
inference(copy,[status(thm)],[c_122]) ).
fof(hyp36,axiom,
earray_212 = select(q30,seq),
file('theBenchmark.p',hyp36) ).
cnf(c_128,plain,
earray_212 = select(q30,seq),
inference(clausify,[status(thm)],[hyp36]) ).
cnf(c_129,plain,
select(q30,seq) = earray_212,
inference(copy,[status(thm)],[c_128]) ).
fof(hyp37,axiom,
earray_22 = store(earray_20,index_21,e11),
file('theBenchmark.p',hyp37) ).
cnf(c_130,plain,
earray_22 = store(earray_20,index_21,e11),
inference(clausify,[status(thm)],[hyp37]) ).
cnf(c_131,plain,
store(earray_20,index_21,e11) = earray_22,
inference(copy,[status(thm)],[c_130]) ).
fof(hyp38,axiom,
earray_29 = select(q12,seq),
file('theBenchmark.p',hyp38) ).
cnf(c_132,plain,
earray_29 = select(q12,seq),
inference(clausify,[status(thm)],[hyp38]) ).
cnf(c_133,plain,
select(q12,seq) = earray_29,
inference(copy,[status(thm)],[c_132]) ).
fof(hyp39,axiom,
earray_31 = store(earray_29,index_30,e12),
file('theBenchmark.p',hyp39) ).
cnf(c_134,plain,
earray_31 = store(earray_29,index_30,e12),
inference(clausify,[status(thm)],[hyp39]) ).
cnf(c_135,plain,
store(earray_29,index_30,e12) = earray_31,
inference(copy,[status(thm)],[c_134]) ).
fof(hyp40,axiom,
earray_35 = select(q13,seq),
file('theBenchmark.p',hyp40) ).
cnf(c_136,plain,
earray_35 = select(q13,seq),
inference(clausify,[status(thm)],[hyp40]) ).
cnf(c_137,plain,
select(q13,seq) = earray_35,
inference(copy,[status(thm)],[c_136]) ).
fof(hyp41,axiom,
earray_37 = store(earray_35,index_36,e13),
file('theBenchmark.p',hyp41) ).
cnf(c_138,plain,
earray_37 = store(earray_35,index_36,e13),
inference(clausify,[status(thm)],[hyp41]) ).
cnf(c_139,plain,
store(earray_35,index_36,e13) = earray_37,
inference(copy,[status(thm)],[c_138]) ).
fof(hyp43,axiom,
earray_41 = select(q14,seq),
file('theBenchmark.p',hyp43) ).
cnf(c_142,plain,
earray_41 = select(q14,seq),
inference(clausify,[status(thm)],[hyp43]) ).
cnf(c_143,plain,
select(q14,seq) = earray_41,
inference(copy,[status(thm)],[c_142]) ).
fof(hyp44,axiom,
earray_43 = store(earray_41,index_42,e14),
file('theBenchmark.p',hyp44) ).
cnf(c_144,plain,
earray_43 = store(earray_41,index_42,e14),
inference(clausify,[status(thm)],[hyp44]) ).
cnf(c_145,plain,
store(earray_41,index_42,e14) = earray_43,
inference(copy,[status(thm)],[c_144]) ).
fof(hyp45,axiom,
earray_50 = select(q15,seq),
file('theBenchmark.p',hyp45) ).
cnf(c_146,plain,
earray_50 = select(q15,seq),
inference(clausify,[status(thm)],[hyp45]) ).
cnf(c_147,plain,
select(q15,seq) = earray_50,
inference(copy,[status(thm)],[c_146]) ).
fof(hyp46,axiom,
earray_52 = store(earray_50,index_51,e15),
file('theBenchmark.p',hyp46) ).
cnf(c_148,plain,
earray_52 = store(earray_50,index_51,e15),
inference(clausify,[status(thm)],[hyp46]) ).
cnf(c_149,plain,
store(earray_50,index_51,e15) = earray_52,
inference(copy,[status(thm)],[c_148]) ).
fof(hyp47,axiom,
earray_56 = select(q16,seq),
file('theBenchmark.p',hyp47) ).
cnf(c_150,plain,
earray_56 = select(q16,seq),
inference(clausify,[status(thm)],[hyp47]) ).
cnf(c_151,plain,
select(q16,seq) = earray_56,
inference(copy,[status(thm)],[c_150]) ).
fof(hyp48,axiom,
earray_58 = store(earray_56,index_57,e16),
file('theBenchmark.p',hyp48) ).
cnf(c_152,plain,
earray_58 = store(earray_56,index_57,e16),
inference(clausify,[status(thm)],[hyp48]) ).
cnf(c_153,plain,
store(earray_56,index_57,e16) = earray_58,
inference(copy,[status(thm)],[c_152]) ).
fof(hyp49,axiom,
earray_62 = select(q17,seq),
file('theBenchmark.p',hyp49) ).
cnf(c_154,plain,
earray_62 = select(q17,seq),
inference(clausify,[status(thm)],[hyp49]) ).
cnf(c_155,plain,
select(q17,seq) = earray_62,
inference(copy,[status(thm)],[c_154]) ).
fof(hyp50,axiom,
earray_64 = store(earray_62,index_63,e17),
file('theBenchmark.p',hyp50) ).
cnf(c_156,plain,
earray_64 = store(earray_62,index_63,e17),
inference(clausify,[status(thm)],[hyp50]) ).
cnf(c_157,plain,
store(earray_62,index_63,e17) = earray_64,
inference(copy,[status(thm)],[c_156]) ).
fof(hyp51,axiom,
earray_71 = select(q18,seq),
file('theBenchmark.p',hyp51) ).
cnf(c_158,plain,
earray_71 = select(q18,seq),
inference(clausify,[status(thm)],[hyp51]) ).
cnf(c_159,plain,
select(q18,seq) = earray_71,
inference(copy,[status(thm)],[c_158]) ).
fof(hyp52,axiom,
earray_73 = store(earray_71,index_72,e18),
file('theBenchmark.p',hyp52) ).
cnf(c_160,plain,
earray_73 = store(earray_71,index_72,e18),
inference(clausify,[status(thm)],[hyp52]) ).
cnf(c_161,plain,
store(earray_71,index_72,e18) = earray_73,
inference(copy,[status(thm)],[c_160]) ).
fof(hyp56,axiom,
earray_83 = select(q19,seq),
file('theBenchmark.p',hyp56) ).
cnf(c_168,plain,
earray_83 = select(q19,seq),
inference(clausify,[status(thm)],[hyp56]) ).
cnf(c_169,plain,
select(q19,seq) = earray_83,
inference(copy,[status(thm)],[c_168]) ).
fof(hyp57,axiom,
earray_85 = store(earray_83,index_84,e19),
file('theBenchmark.p',hyp57) ).
cnf(c_170,plain,
earray_85 = store(earray_83,index_84,e19),
inference(clausify,[status(thm)],[hyp57]) ).
cnf(c_171,plain,
store(earray_83,index_84,e19) = earray_85,
inference(copy,[status(thm)],[c_170]) ).
fof(hyp58,axiom,
earray_89 = select(q20,seq),
file('theBenchmark.p',hyp58) ).
cnf(c_172,plain,
earray_89 = select(q20,seq),
inference(clausify,[status(thm)],[hyp58]) ).
cnf(c_173,plain,
select(q20,seq) = earray_89,
inference(copy,[status(thm)],[c_172]) ).
fof(hyp59,axiom,
earray_91 = store(earray_89,index_90,e20),
file('theBenchmark.p',hyp59) ).
cnf(c_174,plain,
earray_91 = store(earray_89,index_90,e20),
inference(clausify,[status(thm)],[hyp59]) ).
cnf(c_175,plain,
store(earray_89,index_90,e20) = earray_91,
inference(copy,[status(thm)],[c_174]) ).
fof(hyp60,axiom,
earray_98 = select(q21,seq),
file('theBenchmark.p',hyp60) ).
cnf(c_176,plain,
earray_98 = select(q21,seq),
inference(clausify,[status(thm)],[hyp60]) ).
cnf(c_177,plain,
select(q21,seq) = earray_98,
inference(copy,[status(thm)],[c_176]) ).
fof(hyp61,axiom,
elem_214 = select(earray_212,index_213),
file('theBenchmark.p',hyp61) ).
cnf(c_178,plain,
elem_214 = select(earray_212,index_213),
inference(clausify,[status(thm)],[hyp61]) ).
cnf(c_179,plain,
select(earray_212,index_213) = elem_214,
inference(copy,[status(thm)],[c_178]) ).
fof(hyp62,axiom,
index_0 = select(q,tail),
file('theBenchmark.p',hyp62) ).
cnf(c_180,plain,
index_0 = select(q,tail),
inference(clausify,[status(thm)],[hyp62]) ).
cnf(c_181,plain,
select(q,tail) = index_0,
inference(copy,[status(thm)],[c_180]) ).
fof(hyp63,axiom,
index_102 = s(index_99),
file('theBenchmark.p',hyp63) ).
cnf(c_182,plain,
index_102 = s(index_99),
inference(clausify,[status(thm)],[hyp63]) ).
cnf(c_183,plain,
s(index_99) = index_102,
inference(copy,[status(thm)],[c_182]) ).
fof(hyp64,axiom,
index_105 = select(q22,tail),
file('theBenchmark.p',hyp64) ).
cnf(c_184,plain,
index_105 = select(q22,tail),
inference(clausify,[status(thm)],[hyp64]) ).
cnf(c_185,plain,
select(q22,tail) = index_105,
inference(copy,[status(thm)],[c_184]) ).
fof(hyp65,axiom,
index_108 = s(index_105),
file('theBenchmark.p',hyp65) ).
cnf(c_186,plain,
index_108 = s(index_105),
inference(clausify,[status(thm)],[hyp65]) ).
cnf(c_187,plain,
s(index_105) = index_108,
inference(copy,[status(thm)],[c_186]) ).
fof(hyp66,axiom,
index_111 = select(q23,tail),
file('theBenchmark.p',hyp66) ).
cnf(c_188,plain,
index_111 = select(q23,tail),
inference(clausify,[status(thm)],[hyp66]) ).
cnf(c_189,plain,
select(q23,tail) = index_111,
inference(copy,[status(thm)],[c_188]) ).
fof(hyp67,axiom,
index_114 = s(index_111),
file('theBenchmark.p',hyp67) ).
cnf(c_190,plain,
index_114 = s(index_111),
inference(clausify,[status(thm)],[hyp67]) ).
cnf(c_191,plain,
s(index_111) = index_114,
inference(copy,[status(thm)],[c_190]) ).
fof(hyp68,axiom,
index_116 = select(queue_115,head),
file('theBenchmark.p',hyp68) ).
cnf(c_192,plain,
index_116 = select(queue_115,head),
inference(clausify,[status(thm)],[hyp68]) ).
cnf(c_193,plain,
select(queue_115,head) = index_116,
inference(copy,[status(thm)],[c_192]) ).
fof(hyp69,axiom,
index_117 = s(index_116),
file('theBenchmark.p',hyp69) ).
cnf(c_194,plain,
index_117 = s(index_116),
inference(clausify,[status(thm)],[hyp69]) ).
cnf(c_195,plain,
s(index_116) = index_117,
inference(copy,[status(thm)],[c_194]) ).
fof(hyp70,axiom,
index_12 = s(index_9),
file('theBenchmark.p',hyp70) ).
cnf(c_196,plain,
index_12 = s(index_9),
inference(clausify,[status(thm)],[hyp70]) ).
cnf(c_197,plain,
s(index_9) = index_12,
inference(copy,[status(thm)],[c_196]) ).
fof(hyp71,axiom,
index_120 = select(q24,tail),
file('theBenchmark.p',hyp71) ).
cnf(c_198,plain,
index_120 = select(q24,tail),
inference(clausify,[status(thm)],[hyp71]) ).
cnf(c_199,plain,
select(q24,tail) = index_120,
inference(copy,[status(thm)],[c_198]) ).
fof(hyp72,axiom,
index_123 = s(index_120),
file('theBenchmark.p',hyp72) ).
cnf(c_200,plain,
index_123 = s(index_120),
inference(clausify,[status(thm)],[hyp72]) ).
cnf(c_201,plain,
s(index_120) = index_123,
inference(copy,[status(thm)],[c_200]) ).
fof(hyp73,axiom,
index_126 = select(q25,tail),
file('theBenchmark.p',hyp73) ).
cnf(c_202,plain,
index_126 = select(q25,tail),
inference(clausify,[status(thm)],[hyp73]) ).
cnf(c_203,plain,
select(q25,tail) = index_126,
inference(copy,[status(thm)],[c_202]) ).
fof(hyp74,axiom,
index_129 = s(index_126),
file('theBenchmark.p',hyp74) ).
cnf(c_204,plain,
index_129 = s(index_126),
inference(clausify,[status(thm)],[hyp74]) ).
cnf(c_205,plain,
s(index_126) = index_129,
inference(copy,[status(thm)],[c_204]) ).
fof(hyp75,axiom,
index_132 = select(q26,tail),
file('theBenchmark.p',hyp75) ).
cnf(c_206,plain,
index_132 = select(q26,tail),
inference(clausify,[status(thm)],[hyp75]) ).
cnf(c_207,plain,
select(q26,tail) = index_132,
inference(copy,[status(thm)],[c_206]) ).
fof(hyp76,axiom,
index_135 = s(index_132),
file('theBenchmark.p',hyp76) ).
cnf(c_208,plain,
index_135 = s(index_132),
inference(clausify,[status(thm)],[hyp76]) ).
cnf(c_209,plain,
s(index_132) = index_135,
inference(copy,[status(thm)],[c_208]) ).
fof(hyp77,axiom,
index_137 = select(queue_136,head),
file('theBenchmark.p',hyp77) ).
cnf(c_210,plain,
index_137 = select(queue_136,head),
inference(clausify,[status(thm)],[hyp77]) ).
cnf(c_211,plain,
select(queue_136,head) = index_137,
inference(copy,[status(thm)],[c_210]) ).
fof(hyp78,axiom,
index_138 = s(index_137),
file('theBenchmark.p',hyp78) ).
cnf(c_212,plain,
index_138 = s(index_137),
inference(clausify,[status(thm)],[hyp78]) ).
cnf(c_213,plain,
s(index_137) = index_138,
inference(copy,[status(thm)],[c_212]) ).
fof(hyp79,axiom,
index_141 = select(q27,tail),
file('theBenchmark.p',hyp79) ).
cnf(c_214,plain,
index_141 = select(q27,tail),
inference(clausify,[status(thm)],[hyp79]) ).
cnf(c_215,plain,
select(q27,tail) = index_141,
inference(copy,[status(thm)],[c_214]) ).
fof(hyp80,axiom,
index_144 = s(index_141),
file('theBenchmark.p',hyp80) ).
cnf(c_216,plain,
index_144 = s(index_141),
inference(clausify,[status(thm)],[hyp80]) ).
cnf(c_217,plain,
s(index_141) = index_144,
inference(copy,[status(thm)],[c_216]) ).
fof(hyp81,axiom,
index_147 = select(q28,tail),
file('theBenchmark.p',hyp81) ).
cnf(c_218,plain,
index_147 = select(q28,tail),
inference(clausify,[status(thm)],[hyp81]) ).
cnf(c_219,plain,
select(q28,tail) = index_147,
inference(copy,[status(thm)],[c_218]) ).
fof(hyp82,axiom,
index_15 = select(q10,tail),
file('theBenchmark.p',hyp82) ).
cnf(c_220,plain,
index_15 = select(q10,tail),
inference(clausify,[status(thm)],[hyp82]) ).
cnf(c_221,plain,
select(q10,tail) = index_15,
inference(copy,[status(thm)],[c_220]) ).
fof(hyp83,axiom,
index_150 = s(index_147),
file('theBenchmark.p',hyp83) ).
cnf(c_222,plain,
index_150 = s(index_147),
inference(clausify,[status(thm)],[hyp83]) ).
cnf(c_223,plain,
s(index_147) = index_150,
inference(copy,[status(thm)],[c_222]) ).
fof(hyp84,axiom,
index_153 = select(q2,tail),
file('theBenchmark.p',hyp84) ).
cnf(c_224,plain,
index_153 = select(q2,tail),
inference(clausify,[status(thm)],[hyp84]) ).
cnf(c_225,plain,
select(q2,tail) = index_153,
inference(copy,[status(thm)],[c_224]) ).
fof(hyp85,axiom,
index_156 = s(index_153),
file('theBenchmark.p',hyp85) ).
cnf(c_226,plain,
index_156 = s(index_153),
inference(clausify,[status(thm)],[hyp85]) ).
cnf(c_227,plain,
s(index_153) = index_156,
inference(copy,[status(thm)],[c_226]) ).
fof(hyp86,axiom,
index_158 = select(queue_157,head),
file('theBenchmark.p',hyp86) ).
cnf(c_228,plain,
index_158 = select(queue_157,head),
inference(clausify,[status(thm)],[hyp86]) ).
cnf(c_229,plain,
select(queue_157,head) = index_158,
inference(copy,[status(thm)],[c_228]) ).
fof(hyp87,axiom,
index_159 = s(index_158),
file('theBenchmark.p',hyp87) ).
cnf(c_230,plain,
index_159 = s(index_158),
inference(clausify,[status(thm)],[hyp87]) ).
cnf(c_231,plain,
s(index_158) = index_159,
inference(copy,[status(thm)],[c_230]) ).
fof(hyp88,axiom,
index_162 = select(q29,tail),
file('theBenchmark.p',hyp88) ).
cnf(c_232,plain,
index_162 = select(q29,tail),
inference(clausify,[status(thm)],[hyp88]) ).
cnf(c_233,plain,
select(q29,tail) = index_162,
inference(copy,[status(thm)],[c_232]) ).
fof(hyp90,axiom,
index_167 = select(queue_166,head),
file('theBenchmark.p',hyp90) ).
cnf(c_236,plain,
index_167 = select(queue_166,head),
inference(clausify,[status(thm)],[hyp90]) ).
cnf(c_237,plain,
select(queue_166,head) = index_167,
inference(copy,[status(thm)],[c_236]) ).
fof(hyp91,axiom,
index_168 = s(index_167),
file('theBenchmark.p',hyp91) ).
cnf(c_238,plain,
index_168 = s(index_167),
inference(clausify,[status(thm)],[hyp91]) ).
cnf(c_239,plain,
s(index_167) = index_168,
inference(copy,[status(thm)],[c_238]) ).
fof(hyp92,axiom,
index_171 = select(q3,tail),
file('theBenchmark.p',hyp92) ).
cnf(c_240,plain,
index_171 = select(q3,tail),
inference(clausify,[status(thm)],[hyp92]) ).
cnf(c_241,plain,
select(q3,tail) = index_171,
inference(copy,[status(thm)],[c_240]) ).
fof(hyp93,axiom,
index_174 = s(index_171),
file('theBenchmark.p',hyp93) ).
cnf(c_242,plain,
index_174 = s(index_171),
inference(clausify,[status(thm)],[hyp93]) ).
cnf(c_243,plain,
s(index_171) = index_174,
inference(copy,[status(thm)],[c_242]) ).
fof(hyp94,axiom,
index_177 = select(q4,tail),
file('theBenchmark.p',hyp94) ).
cnf(c_244,plain,
index_177 = select(q4,tail),
inference(clausify,[status(thm)],[hyp94]) ).
cnf(c_245,plain,
select(q4,tail) = index_177,
inference(copy,[status(thm)],[c_244]) ).
fof(hyp95,axiom,
index_18 = s(index_15),
file('theBenchmark.p',hyp95) ).
cnf(c_246,plain,
index_18 = s(index_15),
inference(clausify,[status(thm)],[hyp95]) ).
cnf(c_247,plain,
s(index_15) = index_18,
inference(copy,[status(thm)],[c_246]) ).
fof(hyp96,axiom,
index_180 = s(index_177),
file('theBenchmark.p',hyp96) ).
cnf(c_248,plain,
index_180 = s(index_177),
inference(clausify,[status(thm)],[hyp96]) ).
cnf(c_249,plain,
s(index_177) = index_180,
inference(copy,[status(thm)],[c_248]) ).
fof(hyp97,axiom,
index_183 = select(q5,tail),
file('theBenchmark.p',hyp97) ).
cnf(c_250,plain,
index_183 = select(q5,tail),
inference(clausify,[status(thm)],[hyp97]) ).
cnf(c_251,plain,
select(q5,tail) = index_183,
inference(copy,[status(thm)],[c_250]) ).
fof(hyp98,axiom,
index_186 = s(index_183),
file('theBenchmark.p',hyp98) ).
cnf(c_252,plain,
index_186 = s(index_183),
inference(clausify,[status(thm)],[hyp98]) ).
cnf(c_253,plain,
s(index_183) = index_186,
inference(copy,[status(thm)],[c_252]) ).
fof(hyp99,axiom,
index_188 = select(queue_187,head),
file('theBenchmark.p',hyp99) ).
cnf(c_254,plain,
index_188 = select(queue_187,head),
inference(clausify,[status(thm)],[hyp99]) ).
cnf(c_255,plain,
select(queue_187,head) = index_188,
inference(copy,[status(thm)],[c_254]) ).
fof(hyp100,axiom,
index_189 = s(index_188),
file('theBenchmark.p',hyp100) ).
cnf(c_256,plain,
index_189 = s(index_188),
inference(clausify,[status(thm)],[hyp100]) ).
cnf(c_257,plain,
s(index_188) = index_189,
inference(copy,[status(thm)],[c_256]) ).
fof(hyp101,axiom,
index_192 = select(q6,tail),
file('theBenchmark.p',hyp101) ).
cnf(c_258,plain,
index_192 = select(q6,tail),
inference(clausify,[status(thm)],[hyp101]) ).
cnf(c_259,plain,
select(q6,tail) = index_192,
inference(copy,[status(thm)],[c_258]) ).
fof(hyp102,axiom,
index_195 = s(index_192),
file('theBenchmark.p',hyp102) ).
cnf(c_260,plain,
index_195 = s(index_192),
inference(clausify,[status(thm)],[hyp102]) ).
cnf(c_261,plain,
s(index_192) = index_195,
inference(copy,[status(thm)],[c_260]) ).
fof(hyp103,axiom,
index_198 = select(q7,tail),
file('theBenchmark.p',hyp103) ).
cnf(c_262,plain,
index_198 = select(q7,tail),
inference(clausify,[status(thm)],[hyp103]) ).
cnf(c_263,plain,
select(q7,tail) = index_198,
inference(copy,[status(thm)],[c_262]) ).
fof(hyp104,axiom,
index_201 = s(index_198),
file('theBenchmark.p',hyp104) ).
cnf(c_264,plain,
index_201 = s(index_198),
inference(clausify,[status(thm)],[hyp104]) ).
cnf(c_265,plain,
s(index_198) = index_201,
inference(copy,[status(thm)],[c_264]) ).
fof(hyp105,axiom,
index_204 = select(q8,tail),
file('theBenchmark.p',hyp105) ).
cnf(c_266,plain,
index_204 = select(q8,tail),
inference(clausify,[status(thm)],[hyp105]) ).
cnf(c_267,plain,
select(q8,tail) = index_204,
inference(copy,[status(thm)],[c_266]) ).
fof(hyp106,axiom,
index_207 = s(index_204),
file('theBenchmark.p',hyp106) ).
cnf(c_268,plain,
index_207 = s(index_204),
inference(clausify,[status(thm)],[hyp106]) ).
cnf(c_269,plain,
s(index_204) = index_207,
inference(copy,[status(thm)],[c_268]) ).
fof(hyp107,axiom,
index_209 = select(queue_208,head),
file('theBenchmark.p',hyp107) ).
cnf(c_270,plain,
index_209 = select(queue_208,head),
inference(clausify,[status(thm)],[hyp107]) ).
cnf(c_271,plain,
select(queue_208,head) = index_209,
inference(copy,[status(thm)],[c_270]) ).
fof(hyp108,axiom,
index_21 = select(q11,tail),
file('theBenchmark.p',hyp108) ).
cnf(c_272,plain,
index_21 = select(q11,tail),
inference(clausify,[status(thm)],[hyp108]) ).
cnf(c_273,plain,
select(q11,tail) = index_21,
inference(copy,[status(thm)],[c_272]) ).
fof(hyp109,axiom,
index_210 = s(index_209),
file('theBenchmark.p',hyp109) ).
cnf(c_274,plain,
index_210 = s(index_209),
inference(clausify,[status(thm)],[hyp109]) ).
cnf(c_275,plain,
s(index_209) = index_210,
inference(copy,[status(thm)],[c_274]) ).
fof(hyp110,axiom,
index_213 = select(q30,head),
file('theBenchmark.p',hyp110) ).
cnf(c_276,plain,
index_213 = select(q30,head),
inference(clausify,[status(thm)],[hyp110]) ).
cnf(c_277,plain,
select(q30,head) = index_213,
inference(copy,[status(thm)],[c_276]) ).
fof(hyp111,axiom,
index_24 = s(index_21),
file('theBenchmark.p',hyp111) ).
cnf(c_278,plain,
index_24 = s(index_21),
inference(clausify,[status(thm)],[hyp111]) ).
cnf(c_279,plain,
s(index_21) = index_24,
inference(copy,[status(thm)],[c_278]) ).
fof(hyp112,axiom,
index_26 = select(queue_25,head),
file('theBenchmark.p',hyp112) ).
cnf(c_280,plain,
index_26 = select(queue_25,head),
inference(clausify,[status(thm)],[hyp112]) ).
cnf(c_281,plain,
select(queue_25,head) = index_26,
inference(copy,[status(thm)],[c_280]) ).
fof(hyp113,axiom,
index_27 = s(index_26),
file('theBenchmark.p',hyp113) ).
cnf(c_282,plain,
index_27 = s(index_26),
inference(clausify,[status(thm)],[hyp113]) ).
cnf(c_283,plain,
s(index_26) = index_27,
inference(copy,[status(thm)],[c_282]) ).
fof(hyp114,axiom,
index_3 = select(q0,tail),
file('theBenchmark.p',hyp114) ).
cnf(c_284,plain,
index_3 = select(q0,tail),
inference(clausify,[status(thm)],[hyp114]) ).
cnf(c_285,plain,
select(q0,tail) = index_3,
inference(copy,[status(thm)],[c_284]) ).
fof(hyp115,axiom,
index_30 = select(q12,tail),
file('theBenchmark.p',hyp115) ).
cnf(c_286,plain,
index_30 = select(q12,tail),
inference(clausify,[status(thm)],[hyp115]) ).
cnf(c_287,plain,
select(q12,tail) = index_30,
inference(copy,[status(thm)],[c_286]) ).
fof(hyp116,axiom,
index_33 = s(index_30),
file('theBenchmark.p',hyp116) ).
cnf(c_288,plain,
index_33 = s(index_30),
inference(clausify,[status(thm)],[hyp116]) ).
cnf(c_289,plain,
s(index_30) = index_33,
inference(copy,[status(thm)],[c_288]) ).
fof(hyp117,axiom,
index_36 = select(q13,tail),
file('theBenchmark.p',hyp117) ).
cnf(c_290,plain,
index_36 = select(q13,tail),
inference(clausify,[status(thm)],[hyp117]) ).
cnf(c_291,plain,
select(q13,tail) = index_36,
inference(copy,[status(thm)],[c_290]) ).
fof(hyp118,axiom,
index_39 = s(index_36),
file('theBenchmark.p',hyp118) ).
cnf(c_292,plain,
index_39 = s(index_36),
inference(clausify,[status(thm)],[hyp118]) ).
cnf(c_293,plain,
s(index_36) = index_39,
inference(copy,[status(thm)],[c_292]) ).
fof(hyp119,axiom,
index_42 = select(q14,tail),
file('theBenchmark.p',hyp119) ).
cnf(c_294,plain,
index_42 = select(q14,tail),
inference(clausify,[status(thm)],[hyp119]) ).
cnf(c_295,plain,
select(q14,tail) = index_42,
inference(copy,[status(thm)],[c_294]) ).
fof(hyp120,axiom,
index_45 = s(index_42),
file('theBenchmark.p',hyp120) ).
cnf(c_296,plain,
index_45 = s(index_42),
inference(clausify,[status(thm)],[hyp120]) ).
cnf(c_297,plain,
s(index_42) = index_45,
inference(copy,[status(thm)],[c_296]) ).
fof(hyp121,axiom,
index_47 = select(queue_46,head),
file('theBenchmark.p',hyp121) ).
cnf(c_298,plain,
index_47 = select(queue_46,head),
inference(clausify,[status(thm)],[hyp121]) ).
cnf(c_299,plain,
select(queue_46,head) = index_47,
inference(copy,[status(thm)],[c_298]) ).
fof(hyp122,axiom,
index_48 = s(index_47),
file('theBenchmark.p',hyp122) ).
cnf(c_300,plain,
index_48 = s(index_47),
inference(clausify,[status(thm)],[hyp122]) ).
cnf(c_301,plain,
s(index_47) = index_48,
inference(copy,[status(thm)],[c_300]) ).
fof(hyp123,axiom,
index_51 = select(q15,tail),
file('theBenchmark.p',hyp123) ).
cnf(c_302,plain,
index_51 = select(q15,tail),
inference(clausify,[status(thm)],[hyp123]) ).
cnf(c_303,plain,
select(q15,tail) = index_51,
inference(copy,[status(thm)],[c_302]) ).
fof(hyp124,axiom,
index_54 = s(index_51),
file('theBenchmark.p',hyp124) ).
cnf(c_304,plain,
index_54 = s(index_51),
inference(clausify,[status(thm)],[hyp124]) ).
cnf(c_305,plain,
s(index_51) = index_54,
inference(copy,[status(thm)],[c_304]) ).
fof(hyp125,axiom,
index_57 = select(q16,tail),
file('theBenchmark.p',hyp125) ).
cnf(c_306,plain,
index_57 = select(q16,tail),
inference(clausify,[status(thm)],[hyp125]) ).
cnf(c_307,plain,
select(q16,tail) = index_57,
inference(copy,[status(thm)],[c_306]) ).
fof(hyp126,axiom,
index_6 = s(index_3),
file('theBenchmark.p',hyp126) ).
cnf(c_308,plain,
index_6 = s(index_3),
inference(clausify,[status(thm)],[hyp126]) ).
cnf(c_309,plain,
s(index_3) = index_6,
inference(copy,[status(thm)],[c_308]) ).
fof(hyp127,axiom,
index_60 = s(index_57),
file('theBenchmark.p',hyp127) ).
cnf(c_310,plain,
index_60 = s(index_57),
inference(clausify,[status(thm)],[hyp127]) ).
cnf(c_311,plain,
s(index_57) = index_60,
inference(copy,[status(thm)],[c_310]) ).
fof(hyp128,axiom,
index_63 = select(q17,tail),
file('theBenchmark.p',hyp128) ).
cnf(c_312,plain,
index_63 = select(q17,tail),
inference(clausify,[status(thm)],[hyp128]) ).
cnf(c_313,plain,
select(q17,tail) = index_63,
inference(copy,[status(thm)],[c_312]) ).
fof(hyp129,axiom,
index_66 = s(index_63),
file('theBenchmark.p',hyp129) ).
cnf(c_314,plain,
index_66 = s(index_63),
inference(clausify,[status(thm)],[hyp129]) ).
cnf(c_315,plain,
s(index_63) = index_66,
inference(copy,[status(thm)],[c_314]) ).
fof(hyp130,axiom,
index_68 = select(queue_67,head),
file('theBenchmark.p',hyp130) ).
cnf(c_316,plain,
index_68 = select(queue_67,head),
inference(clausify,[status(thm)],[hyp130]) ).
cnf(c_317,plain,
select(queue_67,head) = index_68,
inference(copy,[status(thm)],[c_316]) ).
fof(hyp131,axiom,
index_69 = s(index_68),
file('theBenchmark.p',hyp131) ).
cnf(c_318,plain,
index_69 = s(index_68),
inference(clausify,[status(thm)],[hyp131]) ).
cnf(c_319,plain,
s(index_68) = index_69,
inference(copy,[status(thm)],[c_318]) ).
fof(hyp132,axiom,
index_72 = select(q18,tail),
file('theBenchmark.p',hyp132) ).
cnf(c_320,plain,
index_72 = select(q18,tail),
inference(clausify,[status(thm)],[hyp132]) ).
cnf(c_321,plain,
select(q18,tail) = index_72,
inference(copy,[status(thm)],[c_320]) ).
fof(hyp133,axiom,
index_75 = s(index_72),
file('theBenchmark.p',hyp133) ).
cnf(c_322,plain,
index_75 = s(index_72),
inference(clausify,[status(thm)],[hyp133]) ).
cnf(c_323,plain,
s(index_72) = index_75,
inference(copy,[status(thm)],[c_322]) ).
fof(hyp134,axiom,
index_78 = select(q1,tail),
file('theBenchmark.p',hyp134) ).
cnf(c_324,plain,
index_78 = select(q1,tail),
inference(clausify,[status(thm)],[hyp134]) ).
cnf(c_325,plain,
select(q1,tail) = index_78,
inference(copy,[status(thm)],[c_324]) ).
fof(hyp135,axiom,
index_81 = s(index_78),
file('theBenchmark.p',hyp135) ).
cnf(c_326,plain,
index_81 = s(index_78),
inference(clausify,[status(thm)],[hyp135]) ).
cnf(c_327,plain,
s(index_78) = index_81,
inference(copy,[status(thm)],[c_326]) ).
fof(hyp136,axiom,
index_84 = select(q19,tail),
file('theBenchmark.p',hyp136) ).
cnf(c_328,plain,
index_84 = select(q19,tail),
inference(clausify,[status(thm)],[hyp136]) ).
cnf(c_329,plain,
select(q19,tail) = index_84,
inference(copy,[status(thm)],[c_328]) ).
fof(hyp137,axiom,
index_87 = s(index_84),
file('theBenchmark.p',hyp137) ).
cnf(c_330,plain,
index_87 = s(index_84),
inference(clausify,[status(thm)],[hyp137]) ).
cnf(c_331,plain,
s(index_84) = index_87,
inference(copy,[status(thm)],[c_330]) ).
fof(hyp138,axiom,
index_9 = select(q9,tail),
file('theBenchmark.p',hyp138) ).
cnf(c_332,plain,
index_9 = select(q9,tail),
inference(clausify,[status(thm)],[hyp138]) ).
cnf(c_333,plain,
select(q9,tail) = index_9,
inference(copy,[status(thm)],[c_332]) ).
fof(hyp139,axiom,
index_90 = select(q20,tail),
file('theBenchmark.p',hyp139) ).
cnf(c_334,plain,
index_90 = select(q20,tail),
inference(clausify,[status(thm)],[hyp139]) ).
cnf(c_335,plain,
select(q20,tail) = index_90,
inference(copy,[status(thm)],[c_334]) ).
fof(hyp140,axiom,
index_93 = s(index_90),
file('theBenchmark.p',hyp140) ).
cnf(c_336,plain,
index_93 = s(index_90),
inference(clausify,[status(thm)],[hyp140]) ).
cnf(c_337,plain,
s(index_90) = index_93,
inference(copy,[status(thm)],[c_336]) ).
fof(hyp141,axiom,
index_95 = select(queue_94,head),
file('theBenchmark.p',hyp141) ).
cnf(c_338,plain,
index_95 = select(queue_94,head),
inference(clausify,[status(thm)],[hyp141]) ).
cnf(c_339,plain,
select(queue_94,head) = index_95,
inference(copy,[status(thm)],[c_338]) ).
fof(hyp142,axiom,
index_96 = s(index_95),
file('theBenchmark.p',hyp142) ).
cnf(c_340,plain,
index_96 = s(index_95),
inference(clausify,[status(thm)],[hyp142]) ).
cnf(c_341,plain,
s(index_95) = index_96,
inference(copy,[status(thm)],[c_340]) ).
fof(hyp143,axiom,
index_99 = select(q21,tail),
file('theBenchmark.p',hyp143) ).
cnf(c_342,plain,
index_99 = select(q21,tail),
inference(clausify,[status(thm)],[hyp143]) ).
cnf(c_343,plain,
select(q21,tail) = index_99,
inference(copy,[status(thm)],[c_342]) ).
fof(hyp144,axiom,
queue_1 = store(q,head,index_0),
file('theBenchmark.p',hyp144) ).
cnf(c_344,plain,
queue_1 = store(q,head,index_0),
inference(clausify,[status(thm)],[hyp144]) ).
cnf(c_345,plain,
store(q,head,index_0) = queue_1,
inference(copy,[status(thm)],[c_344]) ).
fof(hyp145,axiom,
queue_101 = store(q21,seq,earray_100),
file('theBenchmark.p',hyp145) ).
cnf(c_346,plain,
queue_101 = store(q21,seq,earray_100),
inference(clausify,[status(thm)],[hyp145]) ).
cnf(c_347,plain,
store(q21,seq,earray_100) = queue_101,
inference(copy,[status(thm)],[c_346]) ).
fof(hyp146,axiom,
queue_103 = store(queue_101,tail,index_102),
file('theBenchmark.p',hyp146) ).
cnf(c_348,plain,
queue_103 = store(queue_101,tail,index_102),
inference(clausify,[status(thm)],[hyp146]) ).
cnf(c_349,plain,
store(queue_101,tail,index_102) = queue_103,
inference(copy,[status(thm)],[c_348]) ).
fof(hyp147,axiom,
queue_107 = store(q22,seq,earray_106),
file('theBenchmark.p',hyp147) ).
cnf(c_350,plain,
queue_107 = store(q22,seq,earray_106),
inference(clausify,[status(thm)],[hyp147]) ).
cnf(c_351,plain,
store(q22,seq,earray_106) = queue_107,
inference(copy,[status(thm)],[c_350]) ).
fof(hyp148,axiom,
queue_109 = store(queue_107,tail,index_108),
file('theBenchmark.p',hyp148) ).
cnf(c_352,plain,
queue_109 = store(queue_107,tail,index_108),
inference(clausify,[status(thm)],[hyp148]) ).
cnf(c_353,plain,
store(queue_107,tail,index_108) = queue_109,
inference(copy,[status(thm)],[c_352]) ).
fof(hyp149,axiom,
queue_11 = store(q9,seq,earray_10),
file('theBenchmark.p',hyp149) ).
cnf(c_354,plain,
queue_11 = store(q9,seq,earray_10),
inference(clausify,[status(thm)],[hyp149]) ).
cnf(c_355,plain,
store(q9,seq,earray_10) = queue_11,
inference(copy,[status(thm)],[c_354]) ).
fof(hyp150,axiom,
queue_113 = store(q23,seq,earray_112),
file('theBenchmark.p',hyp150) ).
cnf(c_356,plain,
queue_113 = store(q23,seq,earray_112),
inference(clausify,[status(thm)],[hyp150]) ).
cnf(c_357,plain,
store(q23,seq,earray_112) = queue_113,
inference(copy,[status(thm)],[c_356]) ).
fof(hyp151,axiom,
queue_115 = store(queue_113,tail,index_114),
file('theBenchmark.p',hyp151) ).
cnf(c_358,plain,
queue_115 = store(queue_113,tail,index_114),
inference(clausify,[status(thm)],[hyp151]) ).
cnf(c_359,plain,
store(queue_113,tail,index_114) = queue_115,
inference(copy,[status(thm)],[c_358]) ).
fof(hyp152,axiom,
queue_118 = store(queue_115,head,index_117),
file('theBenchmark.p',hyp152) ).
cnf(c_360,plain,
queue_118 = store(queue_115,head,index_117),
inference(clausify,[status(thm)],[hyp152]) ).
cnf(c_361,plain,
store(queue_115,head,index_117) = queue_118,
inference(copy,[status(thm)],[c_360]) ).
fof(hyp153,axiom,
queue_122 = store(q24,seq,earray_121),
file('theBenchmark.p',hyp153) ).
cnf(c_362,plain,
queue_122 = store(q24,seq,earray_121),
inference(clausify,[status(thm)],[hyp153]) ).
cnf(c_363,plain,
store(q24,seq,earray_121) = queue_122,
inference(copy,[status(thm)],[c_362]) ).
fof(hyp154,axiom,
queue_124 = store(queue_122,tail,index_123),
file('theBenchmark.p',hyp154) ).
cnf(c_364,plain,
queue_124 = store(queue_122,tail,index_123),
inference(clausify,[status(thm)],[hyp154]) ).
cnf(c_365,plain,
store(queue_122,tail,index_123) = queue_124,
inference(copy,[status(thm)],[c_364]) ).
fof(hyp155,axiom,
queue_128 = store(q25,seq,earray_127),
file('theBenchmark.p',hyp155) ).
cnf(c_366,plain,
queue_128 = store(q25,seq,earray_127),
inference(clausify,[status(thm)],[hyp155]) ).
cnf(c_367,plain,
store(q25,seq,earray_127) = queue_128,
inference(copy,[status(thm)],[c_366]) ).
fof(hyp156,axiom,
queue_13 = store(queue_11,tail,index_12),
file('theBenchmark.p',hyp156) ).
cnf(c_368,plain,
queue_13 = store(queue_11,tail,index_12),
inference(clausify,[status(thm)],[hyp156]) ).
cnf(c_369,plain,
store(queue_11,tail,index_12) = queue_13,
inference(copy,[status(thm)],[c_368]) ).
fof(hyp157,axiom,
queue_130 = store(queue_128,tail,index_129),
file('theBenchmark.p',hyp157) ).
cnf(c_370,plain,
queue_130 = store(queue_128,tail,index_129),
inference(clausify,[status(thm)],[hyp157]) ).
cnf(c_371,plain,
store(queue_128,tail,index_129) = queue_130,
inference(copy,[status(thm)],[c_370]) ).
fof(hyp158,axiom,
queue_134 = store(q26,seq,earray_133),
file('theBenchmark.p',hyp158) ).
cnf(c_372,plain,
queue_134 = store(q26,seq,earray_133),
inference(clausify,[status(thm)],[hyp158]) ).
cnf(c_373,plain,
store(q26,seq,earray_133) = queue_134,
inference(copy,[status(thm)],[c_372]) ).
fof(hyp159,axiom,
queue_136 = store(queue_134,tail,index_135),
file('theBenchmark.p',hyp159) ).
cnf(c_374,plain,
queue_136 = store(queue_134,tail,index_135),
inference(clausify,[status(thm)],[hyp159]) ).
cnf(c_375,plain,
store(queue_134,tail,index_135) = queue_136,
inference(copy,[status(thm)],[c_374]) ).
fof(hyp160,axiom,
queue_139 = store(queue_136,head,index_138),
file('theBenchmark.p',hyp160) ).
cnf(c_376,plain,
queue_139 = store(queue_136,head,index_138),
inference(clausify,[status(thm)],[hyp160]) ).
cnf(c_377,plain,
store(queue_136,head,index_138) = queue_139,
inference(copy,[status(thm)],[c_376]) ).
fof(hyp161,axiom,
queue_143 = store(q27,seq,earray_142),
file('theBenchmark.p',hyp161) ).
cnf(c_378,plain,
queue_143 = store(q27,seq,earray_142),
inference(clausify,[status(thm)],[hyp161]) ).
cnf(c_379,plain,
store(q27,seq,earray_142) = queue_143,
inference(copy,[status(thm)],[c_378]) ).
fof(hyp162,axiom,
queue_145 = store(queue_143,tail,index_144),
file('theBenchmark.p',hyp162) ).
cnf(c_380,plain,
queue_145 = store(queue_143,tail,index_144),
inference(clausify,[status(thm)],[hyp162]) ).
cnf(c_381,plain,
store(queue_143,tail,index_144) = queue_145,
inference(copy,[status(thm)],[c_380]) ).
fof(hyp163,axiom,
queue_149 = store(q28,seq,earray_148),
file('theBenchmark.p',hyp163) ).
cnf(c_382,plain,
queue_149 = store(q28,seq,earray_148),
inference(clausify,[status(thm)],[hyp163]) ).
cnf(c_383,plain,
store(q28,seq,earray_148) = queue_149,
inference(copy,[status(thm)],[c_382]) ).
fof(hyp164,axiom,
queue_151 = store(queue_149,tail,index_150),
file('theBenchmark.p',hyp164) ).
cnf(c_384,plain,
queue_151 = store(queue_149,tail,index_150),
inference(clausify,[status(thm)],[hyp164]) ).
cnf(c_385,plain,
store(queue_149,tail,index_150) = queue_151,
inference(copy,[status(thm)],[c_384]) ).
fof(hyp165,axiom,
queue_155 = store(q2,seq,earray_154),
file('theBenchmark.p',hyp165) ).
cnf(c_386,plain,
queue_155 = store(q2,seq,earray_154),
inference(clausify,[status(thm)],[hyp165]) ).
cnf(c_387,plain,
store(q2,seq,earray_154) = queue_155,
inference(copy,[status(thm)],[c_386]) ).
fof(hyp166,axiom,
queue_157 = store(queue_155,tail,index_156),
file('theBenchmark.p',hyp166) ).
cnf(c_388,plain,
queue_157 = store(queue_155,tail,index_156),
inference(clausify,[status(thm)],[hyp166]) ).
cnf(c_389,plain,
store(queue_155,tail,index_156) = queue_157,
inference(copy,[status(thm)],[c_388]) ).
fof(hyp167,axiom,
queue_160 = store(queue_157,head,index_159),
file('theBenchmark.p',hyp167) ).
cnf(c_390,plain,
queue_160 = store(queue_157,head,index_159),
inference(clausify,[status(thm)],[hyp167]) ).
cnf(c_391,plain,
store(queue_157,head,index_159) = queue_160,
inference(copy,[status(thm)],[c_390]) ).
fof(hyp168,axiom,
queue_164 = store(q29,seq,earray_163),
file('theBenchmark.p',hyp168) ).
cnf(c_392,plain,
queue_164 = store(q29,seq,earray_163),
inference(clausify,[status(thm)],[hyp168]) ).
cnf(c_393,plain,
store(q29,seq,earray_163) = queue_164,
inference(copy,[status(thm)],[c_392]) ).
fof(hyp169,axiom,
queue_166 = store(queue_164,tail,index_165),
file('theBenchmark.p',hyp169) ).
cnf(c_394,plain,
queue_166 = store(queue_164,tail,index_165),
inference(clausify,[status(thm)],[hyp169]) ).
cnf(c_395,plain,
store(queue_164,tail,index_165) = queue_166,
inference(copy,[status(thm)],[c_394]) ).
fof(hyp170,axiom,
queue_169 = store(queue_166,head,index_168),
file('theBenchmark.p',hyp170) ).
cnf(c_396,plain,
queue_169 = store(queue_166,head,index_168),
inference(clausify,[status(thm)],[hyp170]) ).
cnf(c_397,plain,
store(queue_166,head,index_168) = queue_169,
inference(copy,[status(thm)],[c_396]) ).
fof(hyp171,axiom,
queue_17 = store(q10,seq,earray_16),
file('theBenchmark.p',hyp171) ).
cnf(c_398,plain,
queue_17 = store(q10,seq,earray_16),
inference(clausify,[status(thm)],[hyp171]) ).
cnf(c_399,plain,
store(q10,seq,earray_16) = queue_17,
inference(copy,[status(thm)],[c_398]) ).
fof(hyp172,axiom,
queue_173 = store(q3,seq,earray_172),
file('theBenchmark.p',hyp172) ).
cnf(c_400,plain,
queue_173 = store(q3,seq,earray_172),
inference(clausify,[status(thm)],[hyp172]) ).
cnf(c_401,plain,
store(q3,seq,earray_172) = queue_173,
inference(copy,[status(thm)],[c_400]) ).
fof(hyp173,axiom,
queue_175 = store(queue_173,tail,index_174),
file('theBenchmark.p',hyp173) ).
cnf(c_402,plain,
queue_175 = store(queue_173,tail,index_174),
inference(clausify,[status(thm)],[hyp173]) ).
cnf(c_403,plain,
store(queue_173,tail,index_174) = queue_175,
inference(copy,[status(thm)],[c_402]) ).
fof(hyp174,axiom,
queue_179 = store(q4,seq,earray_178),
file('theBenchmark.p',hyp174) ).
cnf(c_404,plain,
queue_179 = store(q4,seq,earray_178),
inference(clausify,[status(thm)],[hyp174]) ).
cnf(c_405,plain,
store(q4,seq,earray_178) = queue_179,
inference(copy,[status(thm)],[c_404]) ).
fof(hyp175,axiom,
queue_181 = store(queue_179,tail,index_180),
file('theBenchmark.p',hyp175) ).
cnf(c_406,plain,
queue_181 = store(queue_179,tail,index_180),
inference(clausify,[status(thm)],[hyp175]) ).
cnf(c_407,plain,
store(queue_179,tail,index_180) = queue_181,
inference(copy,[status(thm)],[c_406]) ).
fof(hyp176,axiom,
queue_185 = store(q5,seq,earray_184),
file('theBenchmark.p',hyp176) ).
cnf(c_408,plain,
queue_185 = store(q5,seq,earray_184),
inference(clausify,[status(thm)],[hyp176]) ).
cnf(c_409,plain,
store(q5,seq,earray_184) = queue_185,
inference(copy,[status(thm)],[c_408]) ).
fof(hyp177,axiom,
queue_187 = store(queue_185,tail,index_186),
file('theBenchmark.p',hyp177) ).
cnf(c_410,plain,
queue_187 = store(queue_185,tail,index_186),
inference(clausify,[status(thm)],[hyp177]) ).
cnf(c_411,plain,
store(queue_185,tail,index_186) = queue_187,
inference(copy,[status(thm)],[c_410]) ).
fof(hyp178,axiom,
queue_19 = store(queue_17,tail,index_18),
file('theBenchmark.p',hyp178) ).
cnf(c_412,plain,
queue_19 = store(queue_17,tail,index_18),
inference(clausify,[status(thm)],[hyp178]) ).
cnf(c_413,plain,
store(queue_17,tail,index_18) = queue_19,
inference(copy,[status(thm)],[c_412]) ).
fof(hyp179,axiom,
queue_190 = store(queue_187,head,index_189),
file('theBenchmark.p',hyp179) ).
cnf(c_414,plain,
queue_190 = store(queue_187,head,index_189),
inference(clausify,[status(thm)],[hyp179]) ).
cnf(c_415,plain,
store(queue_187,head,index_189) = queue_190,
inference(copy,[status(thm)],[c_414]) ).
fof(hyp180,axiom,
queue_194 = store(q6,seq,earray_193),
file('theBenchmark.p',hyp180) ).
cnf(c_416,plain,
queue_194 = store(q6,seq,earray_193),
inference(clausify,[status(thm)],[hyp180]) ).
cnf(c_417,plain,
store(q6,seq,earray_193) = queue_194,
inference(copy,[status(thm)],[c_416]) ).
fof(hyp181,axiom,
queue_196 = store(queue_194,tail,index_195),
file('theBenchmark.p',hyp181) ).
cnf(c_418,plain,
queue_196 = store(queue_194,tail,index_195),
inference(clausify,[status(thm)],[hyp181]) ).
cnf(c_419,plain,
store(queue_194,tail,index_195) = queue_196,
inference(copy,[status(thm)],[c_418]) ).
fof(hyp182,axiom,
queue_200 = store(q7,seq,earray_199),
file('theBenchmark.p',hyp182) ).
cnf(c_420,plain,
queue_200 = store(q7,seq,earray_199),
inference(clausify,[status(thm)],[hyp182]) ).
cnf(c_421,plain,
store(q7,seq,earray_199) = queue_200,
inference(copy,[status(thm)],[c_420]) ).
fof(hyp183,axiom,
queue_202 = store(queue_200,tail,index_201),
file('theBenchmark.p',hyp183) ).
cnf(c_422,plain,
queue_202 = store(queue_200,tail,index_201),
inference(clausify,[status(thm)],[hyp183]) ).
cnf(c_423,plain,
store(queue_200,tail,index_201) = queue_202,
inference(copy,[status(thm)],[c_422]) ).
fof(hyp184,axiom,
queue_206 = store(q8,seq,earray_205),
file('theBenchmark.p',hyp184) ).
cnf(c_424,plain,
queue_206 = store(q8,seq,earray_205),
inference(clausify,[status(thm)],[hyp184]) ).
cnf(c_425,plain,
store(q8,seq,earray_205) = queue_206,
inference(copy,[status(thm)],[c_424]) ).
fof(hyp185,axiom,
queue_208 = store(queue_206,tail,index_207),
file('theBenchmark.p',hyp185) ).
cnf(c_426,plain,
queue_208 = store(queue_206,tail,index_207),
inference(clausify,[status(thm)],[hyp185]) ).
cnf(c_427,plain,
store(queue_206,tail,index_207) = queue_208,
inference(copy,[status(thm)],[c_426]) ).
fof(hyp186,axiom,
queue_211 = store(queue_208,head,index_210),
file('theBenchmark.p',hyp186) ).
cnf(c_428,plain,
queue_211 = store(queue_208,head,index_210),
inference(clausify,[status(thm)],[hyp186]) ).
cnf(c_429,plain,
store(queue_208,head,index_210) = queue_211,
inference(copy,[status(thm)],[c_428]) ).
fof(hyp187,axiom,
queue_23 = store(q11,seq,earray_22),
file('theBenchmark.p',hyp187) ).
cnf(c_430,plain,
queue_23 = store(q11,seq,earray_22),
inference(clausify,[status(thm)],[hyp187]) ).
cnf(c_431,plain,
store(q11,seq,earray_22) = queue_23,
inference(copy,[status(thm)],[c_430]) ).
fof(hyp188,axiom,
queue_25 = store(queue_23,tail,index_24),
file('theBenchmark.p',hyp188) ).
cnf(c_432,plain,
queue_25 = store(queue_23,tail,index_24),
inference(clausify,[status(thm)],[hyp188]) ).
cnf(c_433,plain,
store(queue_23,tail,index_24) = queue_25,
inference(copy,[status(thm)],[c_432]) ).
fof(hyp189,axiom,
queue_28 = store(queue_25,head,index_27),
file('theBenchmark.p',hyp189) ).
cnf(c_434,plain,
queue_28 = store(queue_25,head,index_27),
inference(clausify,[status(thm)],[hyp189]) ).
cnf(c_435,plain,
store(queue_25,head,index_27) = queue_28,
inference(copy,[status(thm)],[c_434]) ).
fof(hyp190,axiom,
queue_32 = store(q12,seq,earray_31),
file('theBenchmark.p',hyp190) ).
cnf(c_436,plain,
queue_32 = store(q12,seq,earray_31),
inference(clausify,[status(thm)],[hyp190]) ).
cnf(c_437,plain,
store(q12,seq,earray_31) = queue_32,
inference(copy,[status(thm)],[c_436]) ).
fof(hyp191,axiom,
queue_34 = store(queue_32,tail,index_33),
file('theBenchmark.p',hyp191) ).
cnf(c_438,plain,
queue_34 = store(queue_32,tail,index_33),
inference(clausify,[status(thm)],[hyp191]) ).
cnf(c_439,plain,
store(queue_32,tail,index_33) = queue_34,
inference(copy,[status(thm)],[c_438]) ).
fof(hyp192,axiom,
queue_38 = store(q13,seq,earray_37),
file('theBenchmark.p',hyp192) ).
cnf(c_440,plain,
queue_38 = store(q13,seq,earray_37),
inference(clausify,[status(thm)],[hyp192]) ).
cnf(c_441,plain,
store(q13,seq,earray_37) = queue_38,
inference(copy,[status(thm)],[c_440]) ).
fof(hyp193,axiom,
queue_40 = store(queue_38,tail,index_39),
file('theBenchmark.p',hyp193) ).
cnf(c_442,plain,
queue_40 = store(queue_38,tail,index_39),
inference(clausify,[status(thm)],[hyp193]) ).
cnf(c_443,plain,
store(queue_38,tail,index_39) = queue_40,
inference(copy,[status(thm)],[c_442]) ).
fof(hyp194,axiom,
queue_44 = store(q14,seq,earray_43),
file('theBenchmark.p',hyp194) ).
cnf(c_444,plain,
queue_44 = store(q14,seq,earray_43),
inference(clausify,[status(thm)],[hyp194]) ).
cnf(c_445,plain,
store(q14,seq,earray_43) = queue_44,
inference(copy,[status(thm)],[c_444]) ).
fof(hyp195,axiom,
queue_46 = store(queue_44,tail,index_45),
file('theBenchmark.p',hyp195) ).
cnf(c_446,plain,
queue_46 = store(queue_44,tail,index_45),
inference(clausify,[status(thm)],[hyp195]) ).
cnf(c_447,plain,
store(queue_44,tail,index_45) = queue_46,
inference(copy,[status(thm)],[c_446]) ).
fof(hyp196,axiom,
queue_49 = store(queue_46,head,index_48),
file('theBenchmark.p',hyp196) ).
cnf(c_448,plain,
queue_49 = store(queue_46,head,index_48),
inference(clausify,[status(thm)],[hyp196]) ).
cnf(c_449,plain,
store(queue_46,head,index_48) = queue_49,
inference(copy,[status(thm)],[c_448]) ).
fof(hyp197,axiom,
queue_5 = store(q0,seq,earray_4),
file('theBenchmark.p',hyp197) ).
cnf(c_450,plain,
queue_5 = store(q0,seq,earray_4),
inference(clausify,[status(thm)],[hyp197]) ).
cnf(c_451,plain,
store(q0,seq,earray_4) = queue_5,
inference(copy,[status(thm)],[c_450]) ).
fof(hyp198,axiom,
queue_53 = store(q15,seq,earray_52),
file('theBenchmark.p',hyp198) ).
cnf(c_452,plain,
queue_53 = store(q15,seq,earray_52),
inference(clausify,[status(thm)],[hyp198]) ).
cnf(c_453,plain,
store(q15,seq,earray_52) = queue_53,
inference(copy,[status(thm)],[c_452]) ).
fof(hyp199,axiom,
queue_55 = store(queue_53,tail,index_54),
file('theBenchmark.p',hyp199) ).
cnf(c_454,plain,
queue_55 = store(queue_53,tail,index_54),
inference(clausify,[status(thm)],[hyp199]) ).
cnf(c_455,plain,
store(queue_53,tail,index_54) = queue_55,
inference(copy,[status(thm)],[c_454]) ).
fof(hyp200,axiom,
queue_59 = store(q16,seq,earray_58),
file('theBenchmark.p',hyp200) ).
cnf(c_456,plain,
queue_59 = store(q16,seq,earray_58),
inference(clausify,[status(thm)],[hyp200]) ).
cnf(c_457,plain,
store(q16,seq,earray_58) = queue_59,
inference(copy,[status(thm)],[c_456]) ).
fof(hyp201,axiom,
queue_61 = store(queue_59,tail,index_60),
file('theBenchmark.p',hyp201) ).
cnf(c_458,plain,
queue_61 = store(queue_59,tail,index_60),
inference(clausify,[status(thm)],[hyp201]) ).
cnf(c_459,plain,
store(queue_59,tail,index_60) = queue_61,
inference(copy,[status(thm)],[c_458]) ).
fof(hyp202,axiom,
queue_65 = store(q17,seq,earray_64),
file('theBenchmark.p',hyp202) ).
cnf(c_460,plain,
queue_65 = store(q17,seq,earray_64),
inference(clausify,[status(thm)],[hyp202]) ).
cnf(c_461,plain,
store(q17,seq,earray_64) = queue_65,
inference(copy,[status(thm)],[c_460]) ).
fof(hyp203,axiom,
queue_67 = store(queue_65,tail,index_66),
file('theBenchmark.p',hyp203) ).
cnf(c_462,plain,
queue_67 = store(queue_65,tail,index_66),
inference(clausify,[status(thm)],[hyp203]) ).
cnf(c_463,plain,
store(queue_65,tail,index_66) = queue_67,
inference(copy,[status(thm)],[c_462]) ).
fof(hyp204,axiom,
queue_7 = store(queue_5,tail,index_6),
file('theBenchmark.p',hyp204) ).
cnf(c_464,plain,
queue_7 = store(queue_5,tail,index_6),
inference(clausify,[status(thm)],[hyp204]) ).
cnf(c_465,plain,
store(queue_5,tail,index_6) = queue_7,
inference(copy,[status(thm)],[c_464]) ).
fof(hyp205,axiom,
queue_70 = store(queue_67,head,index_69),
file('theBenchmark.p',hyp205) ).
cnf(c_466,plain,
queue_70 = store(queue_67,head,index_69),
inference(clausify,[status(thm)],[hyp205]) ).
cnf(c_467,plain,
store(queue_67,head,index_69) = queue_70,
inference(copy,[status(thm)],[c_466]) ).
fof(hyp206,axiom,
queue_74 = store(q18,seq,earray_73),
file('theBenchmark.p',hyp206) ).
cnf(c_468,plain,
queue_74 = store(q18,seq,earray_73),
inference(clausify,[status(thm)],[hyp206]) ).
cnf(c_469,plain,
store(q18,seq,earray_73) = queue_74,
inference(copy,[status(thm)],[c_468]) ).
fof(hyp207,axiom,
queue_76 = store(queue_74,tail,index_75),
file('theBenchmark.p',hyp207) ).
cnf(c_470,plain,
queue_76 = store(queue_74,tail,index_75),
inference(clausify,[status(thm)],[hyp207]) ).
cnf(c_471,plain,
store(queue_74,tail,index_75) = queue_76,
inference(copy,[status(thm)],[c_470]) ).
fof(hyp208,axiom,
queue_80 = store(q1,seq,earray_79),
file('theBenchmark.p',hyp208) ).
cnf(c_472,plain,
queue_80 = store(q1,seq,earray_79),
inference(clausify,[status(thm)],[hyp208]) ).
cnf(c_473,plain,
store(q1,seq,earray_79) = queue_80,
inference(copy,[status(thm)],[c_472]) ).
fof(hyp209,axiom,
queue_82 = store(queue_80,tail,index_81),
file('theBenchmark.p',hyp209) ).
cnf(c_474,plain,
queue_82 = store(queue_80,tail,index_81),
inference(clausify,[status(thm)],[hyp209]) ).
cnf(c_475,plain,
store(queue_80,tail,index_81) = queue_82,
inference(copy,[status(thm)],[c_474]) ).
fof(hyp210,axiom,
queue_86 = store(q19,seq,earray_85),
file('theBenchmark.p',hyp210) ).
cnf(c_476,plain,
queue_86 = store(q19,seq,earray_85),
inference(clausify,[status(thm)],[hyp210]) ).
cnf(c_477,plain,
store(q19,seq,earray_85) = queue_86,
inference(copy,[status(thm)],[c_476]) ).
fof(hyp211,axiom,
queue_88 = store(queue_86,tail,index_87),
file('theBenchmark.p',hyp211) ).
cnf(c_478,plain,
queue_88 = store(queue_86,tail,index_87),
inference(clausify,[status(thm)],[hyp211]) ).
cnf(c_479,plain,
store(queue_86,tail,index_87) = queue_88,
inference(copy,[status(thm)],[c_478]) ).
fof(hyp212,axiom,
queue_92 = store(q20,seq,earray_91),
file('theBenchmark.p',hyp212) ).
cnf(c_480,plain,
queue_92 = store(q20,seq,earray_91),
inference(clausify,[status(thm)],[hyp212]) ).
cnf(c_481,plain,
store(q20,seq,earray_91) = queue_92,
inference(copy,[status(thm)],[c_480]) ).
fof(hyp213,axiom,
queue_94 = store(queue_92,tail,index_93),
file('theBenchmark.p',hyp213) ).
cnf(c_482,plain,
queue_94 = store(queue_92,tail,index_93),
inference(clausify,[status(thm)],[hyp213]) ).
cnf(c_483,plain,
store(queue_92,tail,index_93) = queue_94,
inference(copy,[status(thm)],[c_482]) ).
fof(hyp214,axiom,
queue_97 = store(queue_94,head,index_96),
file('theBenchmark.p',hyp214) ).
cnf(c_484,plain,
queue_97 = store(queue_94,head,index_96),
inference(clausify,[status(thm)],[hyp214]) ).
cnf(c_485,plain,
store(queue_94,head,index_96) = queue_97,
inference(copy,[status(thm)],[c_484]) ).
fof(hyp215,axiom,
q0 = queue_1,
file('theBenchmark.p',hyp215) ).
cnf(c_486,plain,
q0 = queue_1,
inference(clausify,[status(thm)],[hyp215]) ).
cnf(c_487,plain,
queue_1 = q0,
inference(copy,[status(thm)],[c_486]) ).
fof(hyp216,axiom,
q1 = queue_7,
file('theBenchmark.p',hyp216) ).
cnf(c_488,plain,
q1 = queue_7,
inference(clausify,[status(thm)],[hyp216]) ).
cnf(c_489,plain,
queue_7 = q1,
inference(copy,[status(thm)],[c_488]) ).
fof(hyp217,axiom,
q10 = queue_13,
file('theBenchmark.p',hyp217) ).
cnf(c_490,plain,
q10 = queue_13,
inference(clausify,[status(thm)],[hyp217]) ).
cnf(c_491,plain,
queue_13 = q10,
inference(copy,[status(thm)],[c_490]) ).
fof(hyp218,axiom,
q11 = queue_19,
file('theBenchmark.p',hyp218) ).
cnf(c_492,plain,
q11 = queue_19,
inference(clausify,[status(thm)],[hyp218]) ).
cnf(c_493,plain,
queue_19 = q11,
inference(copy,[status(thm)],[c_492]) ).
fof(hyp219,axiom,
q12 = queue_28,
file('theBenchmark.p',hyp219) ).
cnf(c_494,plain,
q12 = queue_28,
inference(clausify,[status(thm)],[hyp219]) ).
cnf(c_495,plain,
queue_28 = q12,
inference(copy,[status(thm)],[c_494]) ).
fof(hyp220,axiom,
q13 = queue_34,
file('theBenchmark.p',hyp220) ).
cnf(c_496,plain,
q13 = queue_34,
inference(clausify,[status(thm)],[hyp220]) ).
cnf(c_497,plain,
queue_34 = q13,
inference(copy,[status(thm)],[c_496]) ).
fof(hyp221,axiom,
q14 = queue_40,
file('theBenchmark.p',hyp221) ).
cnf(c_498,plain,
q14 = queue_40,
inference(clausify,[status(thm)],[hyp221]) ).
cnf(c_499,plain,
queue_40 = q14,
inference(copy,[status(thm)],[c_498]) ).
fof(hyp222,axiom,
q15 = queue_49,
file('theBenchmark.p',hyp222) ).
cnf(c_500,plain,
q15 = queue_49,
inference(clausify,[status(thm)],[hyp222]) ).
cnf(c_501,plain,
queue_49 = q15,
inference(copy,[status(thm)],[c_500]) ).
fof(hyp223,axiom,
q16 = queue_55,
file('theBenchmark.p',hyp223) ).
cnf(c_502,plain,
q16 = queue_55,
inference(clausify,[status(thm)],[hyp223]) ).
cnf(c_503,plain,
queue_55 = q16,
inference(copy,[status(thm)],[c_502]) ).
fof(hyp224,axiom,
q17 = queue_61,
file('theBenchmark.p',hyp224) ).
cnf(c_504,plain,
q17 = queue_61,
inference(clausify,[status(thm)],[hyp224]) ).
cnf(c_505,plain,
queue_61 = q17,
inference(copy,[status(thm)],[c_504]) ).
fof(hyp225,axiom,
q18 = queue_70,
file('theBenchmark.p',hyp225) ).
cnf(c_506,plain,
q18 = queue_70,
inference(clausify,[status(thm)],[hyp225]) ).
cnf(c_507,plain,
queue_70 = q18,
inference(copy,[status(thm)],[c_506]) ).
fof(hyp226,axiom,
q19 = queue_76,
file('theBenchmark.p',hyp226) ).
cnf(c_508,plain,
q19 = queue_76,
inference(clausify,[status(thm)],[hyp226]) ).
cnf(c_509,plain,
queue_76 = q19,
inference(copy,[status(thm)],[c_508]) ).
fof(hyp227,axiom,
q2 = queue_82,
file('theBenchmark.p',hyp227) ).
cnf(c_510,plain,
q2 = queue_82,
inference(clausify,[status(thm)],[hyp227]) ).
cnf(c_511,plain,
queue_82 = q2,
inference(copy,[status(thm)],[c_510]) ).
fof(hyp228,axiom,
q20 = queue_88,
file('theBenchmark.p',hyp228) ).
cnf(c_512,plain,
q20 = queue_88,
inference(clausify,[status(thm)],[hyp228]) ).
cnf(c_513,plain,
queue_88 = q20,
inference(copy,[status(thm)],[c_512]) ).
fof(hyp229,axiom,
q21 = queue_97,
file('theBenchmark.p',hyp229) ).
cnf(c_514,plain,
q21 = queue_97,
inference(clausify,[status(thm)],[hyp229]) ).
cnf(c_515,plain,
queue_97 = q21,
inference(copy,[status(thm)],[c_514]) ).
fof(hyp230,axiom,
q22 = queue_103,
file('theBenchmark.p',hyp230) ).
cnf(c_516,plain,
q22 = queue_103,
inference(clausify,[status(thm)],[hyp230]) ).
cnf(c_517,plain,
queue_103 = q22,
inference(copy,[status(thm)],[c_516]) ).
fof(hyp231,axiom,
q23 = queue_109,
file('theBenchmark.p',hyp231) ).
cnf(c_518,plain,
q23 = queue_109,
inference(clausify,[status(thm)],[hyp231]) ).
cnf(c_519,plain,
queue_109 = q23,
inference(copy,[status(thm)],[c_518]) ).
fof(hyp232,axiom,
q24 = queue_118,
file('theBenchmark.p',hyp232) ).
cnf(c_520,plain,
q24 = queue_118,
inference(clausify,[status(thm)],[hyp232]) ).
cnf(c_521,plain,
queue_118 = q24,
inference(copy,[status(thm)],[c_520]) ).
fof(hyp233,axiom,
q25 = queue_124,
file('theBenchmark.p',hyp233) ).
cnf(c_522,plain,
q25 = queue_124,
inference(clausify,[status(thm)],[hyp233]) ).
cnf(c_523,plain,
queue_124 = q25,
inference(copy,[status(thm)],[c_522]) ).
fof(hyp234,axiom,
q26 = queue_130,
file('theBenchmark.p',hyp234) ).
cnf(c_524,plain,
q26 = queue_130,
inference(clausify,[status(thm)],[hyp234]) ).
cnf(c_525,plain,
queue_130 = q26,
inference(copy,[status(thm)],[c_524]) ).
fof(hyp235,axiom,
q27 = queue_139,
file('theBenchmark.p',hyp235) ).
cnf(c_526,plain,
q27 = queue_139,
inference(clausify,[status(thm)],[hyp235]) ).
cnf(c_527,plain,
queue_139 = q27,
inference(copy,[status(thm)],[c_526]) ).
fof(hyp236,axiom,
q28 = queue_145,
file('theBenchmark.p',hyp236) ).
cnf(c_528,plain,
q28 = queue_145,
inference(clausify,[status(thm)],[hyp236]) ).
cnf(c_529,plain,
queue_145 = q28,
inference(copy,[status(thm)],[c_528]) ).
fof(hyp237,axiom,
q29 = queue_151,
file('theBenchmark.p',hyp237) ).
cnf(c_530,plain,
q29 = queue_151,
inference(clausify,[status(thm)],[hyp237]) ).
cnf(c_531,plain,
queue_151 = q29,
inference(copy,[status(thm)],[c_530]) ).
fof(hyp238,axiom,
q3 = queue_160,
file('theBenchmark.p',hyp238) ).
cnf(c_532,plain,
q3 = queue_160,
inference(clausify,[status(thm)],[hyp238]) ).
cnf(c_533,plain,
queue_160 = q3,
inference(copy,[status(thm)],[c_532]) ).
fof(hyp239,axiom,
q30 = queue_169,
file('theBenchmark.p',hyp239) ).
cnf(c_534,plain,
q30 = queue_169,
inference(clausify,[status(thm)],[hyp239]) ).
cnf(c_535,plain,
queue_169 = q30,
inference(copy,[status(thm)],[c_534]) ).
fof(hyp240,axiom,
q4 = queue_175,
file('theBenchmark.p',hyp240) ).
cnf(c_536,plain,
q4 = queue_175,
inference(clausify,[status(thm)],[hyp240]) ).
cnf(c_537,plain,
queue_175 = q4,
inference(copy,[status(thm)],[c_536]) ).
fof(hyp241,axiom,
q5 = queue_181,
file('theBenchmark.p',hyp241) ).
cnf(c_538,plain,
q5 = queue_181,
inference(clausify,[status(thm)],[hyp241]) ).
cnf(c_539,plain,
queue_181 = q5,
inference(copy,[status(thm)],[c_538]) ).
fof(hyp242,axiom,
q6 = queue_190,
file('theBenchmark.p',hyp242) ).
cnf(c_540,plain,
q6 = queue_190,
inference(clausify,[status(thm)],[hyp242]) ).
cnf(c_541,plain,
queue_190 = q6,
inference(copy,[status(thm)],[c_540]) ).
fof(hyp243,axiom,
q7 = queue_196,
file('theBenchmark.p',hyp243) ).
cnf(c_542,plain,
q7 = queue_196,
inference(clausify,[status(thm)],[hyp243]) ).
cnf(c_543,plain,
queue_196 = q7,
inference(copy,[status(thm)],[c_542]) ).
fof(hyp244,axiom,
q8 = queue_202,
file('theBenchmark.p',hyp244) ).
cnf(c_544,plain,
q8 = queue_202,
inference(clausify,[status(thm)],[hyp244]) ).
cnf(c_545,plain,
queue_202 = q8,
inference(copy,[status(thm)],[c_544]) ).
fof(hyp245,axiom,
q9 = queue_211,
file('theBenchmark.p',hyp245) ).
cnf(c_546,plain,
q9 = queue_211,
inference(clausify,[status(thm)],[hyp245]) ).
cnf(c_547,plain,
queue_211 = q9,
inference(copy,[status(thm)],[c_546]) ).
fof(goal,axiom,
elem_214 != e10,
file('theBenchmark.p',goal) ).
cnf(c_548,plain,
elem_214 != e10,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_549,plain,
store(q,head,index_0) = q0,
inference(paramod,[status(thm)],[c_487,c_345]) ).
cnf(c_550,plain,
store(queue_5,tail,index_6) = q1,
inference(paramod,[status(thm)],[c_489,c_465]) ).
cnf(c_551,plain,
store(queue_11,tail,index_12) = q10,
inference(paramod,[status(thm)],[c_491,c_369]) ).
cnf(c_552,plain,
store(queue_17,tail,index_18) = q11,
inference(paramod,[status(thm)],[c_493,c_413]) ).
cnf(c_553,plain,
store(queue_25,head,index_27) = q12,
inference(paramod,[status(thm)],[c_495,c_435]) ).
cnf(c_554,plain,
store(queue_32,tail,index_33) = q13,
inference(paramod,[status(thm)],[c_497,c_439]) ).
cnf(c_555,plain,
store(queue_38,tail,index_39) = q14,
inference(paramod,[status(thm)],[c_499,c_443]) ).
cnf(c_556,plain,
store(queue_46,head,index_48) = q15,
inference(paramod,[status(thm)],[c_501,c_449]) ).
cnf(c_557,plain,
store(queue_53,tail,index_54) = q16,
inference(paramod,[status(thm)],[c_503,c_455]) ).
cnf(c_558,plain,
store(queue_59,tail,index_60) = q17,
inference(paramod,[status(thm)],[c_505,c_459]) ).
cnf(c_559,plain,
store(queue_67,head,index_69) = q18,
inference(paramod,[status(thm)],[c_507,c_467]) ).
cnf(c_560,plain,
store(queue_74,tail,index_75) = q19,
inference(paramod,[status(thm)],[c_509,c_471]) ).
cnf(c_561,plain,
store(queue_80,tail,index_81) = q2,
inference(paramod,[status(thm)],[c_511,c_475]) ).
cnf(c_562,plain,
store(queue_86,tail,index_87) = q20,
inference(paramod,[status(thm)],[c_513,c_479]) ).
cnf(c_563,plain,
store(queue_94,head,index_96) = q21,
inference(paramod,[status(thm)],[c_515,c_485]) ).
cnf(c_564,plain,
store(queue_101,tail,index_102) = q22,
inference(paramod,[status(thm)],[c_517,c_349]) ).
cnf(c_565,plain,
store(queue_107,tail,index_108) = q23,
inference(paramod,[status(thm)],[c_519,c_353]) ).
cnf(c_566,plain,
store(queue_115,head,index_117) = q24,
inference(paramod,[status(thm)],[c_521,c_361]) ).
cnf(c_567,plain,
store(queue_122,tail,index_123) = q25,
inference(paramod,[status(thm)],[c_523,c_365]) ).
cnf(c_568,plain,
store(queue_128,tail,index_129) = q26,
inference(paramod,[status(thm)],[c_525,c_371]) ).
cnf(c_569,plain,
store(queue_136,head,index_138) = q27,
inference(paramod,[status(thm)],[c_527,c_377]) ).
cnf(c_570,plain,
store(queue_143,tail,index_144) = q28,
inference(paramod,[status(thm)],[c_529,c_381]) ).
cnf(c_571,plain,
store(queue_149,tail,index_150) = q29,
inference(paramod,[status(thm)],[c_531,c_385]) ).
cnf(c_572,plain,
store(queue_157,head,index_159) = q3,
inference(paramod,[status(thm)],[c_533,c_391]) ).
cnf(c_573,plain,
store(queue_166,head,index_168) = q30,
inference(paramod,[status(thm)],[c_535,c_397]) ).
cnf(c_574,plain,
store(queue_173,tail,index_174) = q4,
inference(paramod,[status(thm)],[c_537,c_403]) ).
cnf(c_575,plain,
store(queue_179,tail,index_180) = q5,
inference(paramod,[status(thm)],[c_539,c_407]) ).
cnf(c_576,plain,
store(queue_187,head,index_189) = q6,
inference(paramod,[status(thm)],[c_541,c_415]) ).
cnf(c_577,plain,
store(queue_194,tail,index_195) = q7,
inference(paramod,[status(thm)],[c_543,c_419]) ).
cnf(c_578,plain,
store(queue_200,tail,index_201) = q8,
inference(paramod,[status(thm)],[c_545,c_423]) ).
cnf(c_579,plain,
store(queue_208,head,index_210) = q9,
inference(paramod,[status(thm)],[c_547,c_429]) ).
cnf(c_13938,plain,
( select(earray_100,A) = select(earray_98,A)
| index_99 = A ),
inference(paramod,[status(thm)],[c_59,c_2]) ).
cnf(c_586,plain,
( select(earray_98,A) = select(earray_100,A)
| index_99 = A ),
inference(copy,[status(thm)],[c_13938]) ).
cnf(c_589,plain,
( select(earray_106,A) = select(earray_104,A)
| index_105 = A ),
inference(paramod,[status(thm)],[c_63,c_2]) ).
cnf(c_592,plain,
( select(earray_112,A) = select(earray_110,A)
| index_111 = A ),
inference(paramod,[status(thm)],[c_67,c_2]) ).
cnf(c_595,plain,
( select(earray_121,A) = select(earray_119,A)
| index_120 = A ),
inference(paramod,[status(thm)],[c_71,c_2]) ).
cnf(c_598,plain,
( select(earray_127,A) = select(earray_125,A)
| index_126 = A ),
inference(paramod,[status(thm)],[c_75,c_2]) ).
cnf(c_601,plain,
( select(earray_133,A) = select(earray_131,A)
| index_132 = A ),
inference(paramod,[status(thm)],[c_79,c_2]) ).
cnf(c_605,plain,
( select(earray_142,A) = select(earray_140,A)
| index_141 = A ),
inference(paramod,[status(thm)],[c_85,c_2]) ).
cnf(c_608,plain,
( select(earray_148,A) = select(earray_146,A)
| index_147 = A ),
inference(paramod,[status(thm)],[c_89,c_2]) ).
cnf(c_612,plain,
select(earray_16,index_15) = e10,
inference(paramod,[status(thm)],[c_95,c_1]) ).
cnf(c_616,plain,
( select(earray_163,A) = select(earray_161,A)
| index_162 = A ),
inference(paramod,[status(thm)],[c_99,c_2]) ).
cnf(c_639,plain,
( select(earray_22,A) = select(earray_20,A)
| index_21 = A ),
inference(paramod,[status(thm)],[c_131,c_2]) ).
cnf(c_642,plain,
( select(earray_31,A) = select(earray_29,A)
| index_30 = A ),
inference(paramod,[status(thm)],[c_135,c_2]) ).
cnf(c_645,plain,
( select(earray_37,A) = select(earray_35,A)
| index_36 = A ),
inference(paramod,[status(thm)],[c_139,c_2]) ).
cnf(c_650,plain,
( select(earray_43,A) = select(earray_41,A)
| index_42 = A ),
inference(paramod,[status(thm)],[c_145,c_2]) ).
cnf(c_653,plain,
( select(earray_52,A) = select(earray_50,A)
| index_51 = A ),
inference(paramod,[status(thm)],[c_149,c_2]) ).
cnf(c_656,plain,
( select(earray_58,A) = select(earray_56,A)
| index_57 = A ),
inference(paramod,[status(thm)],[c_153,c_2]) ).
cnf(c_659,plain,
( select(earray_64,A) = select(earray_62,A)
| index_63 = A ),
inference(paramod,[status(thm)],[c_157,c_2]) ).
cnf(c_662,plain,
( select(earray_73,A) = select(earray_71,A)
| index_72 = A ),
inference(paramod,[status(thm)],[c_161,c_2]) ).
cnf(c_669,plain,
( select(earray_85,A) = select(earray_83,A)
| index_84 = A ),
inference(paramod,[status(thm)],[c_171,c_2]) ).
cnf(c_672,plain,
( select(earray_91,A) = select(earray_89,A)
| index_90 = A ),
inference(paramod,[status(thm)],[c_175,c_2]) ).
cnf(c_13939,plain,
( select(store(q,A,B),tail) = index_0
| A = tail ),
inference(paramod,[status(thm)],[c_181,c_2]) ).
cnf(c_675,plain,
( select(store(q,A,B),tail) = index_0
| tail = A ),
inference(copy,[status(thm)],[c_13939]) ).
cnf(c_1523,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_37]) ).
cnf(c_1524,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_38]) ).
cnf(c_1525,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_39]) ).
cnf(c_1526,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_40]) ).
cnf(c_1527,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_41]) ).
cnf(c_1528,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_42]) ).
cnf(c_1529,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_18)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_43]) ).
cnf(c_1530,plain,
s(s(s(s(s(s(s(s(s(s(s(index_18))))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_44]) ).
cnf(c_1531,plain,
s(s(s(s(s(s(s(s(s(s(index_18)))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_45]) ).
cnf(c_1532,plain,
s(s(s(s(s(s(s(s(s(index_18))))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_46]) ).
cnf(c_1533,plain,
s(s(s(s(s(s(s(s(index_18)))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_47]) ).
cnf(c_1534,plain,
s(s(s(s(s(s(s(index_18))))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_48]) ).
cnf(c_1535,plain,
s(s(s(s(s(s(index_18)))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_49]) ).
cnf(c_1536,plain,
s(s(s(s(s(index_18))))) != index_15,
inference(paramod,[status(thm)],[c_247,c_50]) ).
cnf(c_1537,plain,
s(s(s(s(index_18)))) != index_15,
inference(paramod,[status(thm)],[c_247,c_51]) ).
cnf(c_1538,plain,
s(s(s(index_18))) != index_15,
inference(paramod,[status(thm)],[c_247,c_52]) ).
cnf(c_1539,plain,
s(s(index_18)) != index_15,
inference(paramod,[status(thm)],[c_247,c_53]) ).
cnf(c_1540,plain,
s(index_18) != index_15,
inference(paramod,[status(thm)],[c_247,c_54]) ).
cnf(c_1541,plain,
index_18 != index_15,
inference(paramod,[status(thm)],[c_247,c_55]) ).
cnf(c_2717,plain,
select(queue_101,seq) = earray_100,
inference(paramod,[status(thm)],[c_347,c_1]) ).
cnf(c_2718,plain,
( select(queue_101,A) = select(q21,A)
| seq = A ),
inference(paramod,[status(thm)],[c_347,c_2]) ).
cnf(c_2719,plain,
select(queue_107,seq) = earray_106,
inference(paramod,[status(thm)],[c_351,c_1]) ).
cnf(c_2720,plain,
( select(queue_107,A) = select(q22,A)
| seq = A ),
inference(paramod,[status(thm)],[c_351,c_2]) ).
cnf(c_2722,plain,
( select(queue_11,A) = select(q9,A)
| seq = A ),
inference(paramod,[status(thm)],[c_355,c_2]) ).
cnf(c_2723,plain,
select(queue_113,seq) = earray_112,
inference(paramod,[status(thm)],[c_357,c_1]) ).
cnf(c_2724,plain,
( select(queue_113,A) = select(q23,A)
| seq = A ),
inference(paramod,[status(thm)],[c_357,c_2]) ).
cnf(c_2725,plain,
select(queue_115,tail) = index_114,
inference(paramod,[status(thm)],[c_359,c_1]) ).
cnf(c_13940,plain,
( select(queue_115,A) = select(queue_113,A)
| tail = A ),
inference(paramod,[status(thm)],[c_359,c_2]) ).
cnf(c_2726,plain,
( select(queue_113,A) = select(queue_115,A)
| tail = A ),
inference(copy,[status(thm)],[c_13940]) ).
cnf(c_2727,plain,
select(queue_122,seq) = earray_121,
inference(paramod,[status(thm)],[c_363,c_1]) ).
cnf(c_2728,plain,
( select(queue_122,A) = select(q24,A)
| seq = A ),
inference(paramod,[status(thm)],[c_363,c_2]) ).
cnf(c_2729,plain,
select(queue_128,seq) = earray_127,
inference(paramod,[status(thm)],[c_367,c_1]) ).
cnf(c_2730,plain,
( select(queue_128,A) = select(q25,A)
| seq = A ),
inference(paramod,[status(thm)],[c_367,c_2]) ).
cnf(c_2731,plain,
select(queue_134,seq) = earray_133,
inference(paramod,[status(thm)],[c_373,c_1]) ).
cnf(c_2732,plain,
( select(queue_134,A) = select(q26,A)
| seq = A ),
inference(paramod,[status(thm)],[c_373,c_2]) ).
cnf(c_2733,plain,
select(queue_136,tail) = index_135,
inference(paramod,[status(thm)],[c_375,c_1]) ).
cnf(c_13941,plain,
( select(queue_136,A) = select(queue_134,A)
| tail = A ),
inference(paramod,[status(thm)],[c_375,c_2]) ).
cnf(c_2734,plain,
( select(queue_134,A) = select(queue_136,A)
| tail = A ),
inference(copy,[status(thm)],[c_13941]) ).
cnf(c_2735,plain,
select(queue_143,seq) = earray_142,
inference(paramod,[status(thm)],[c_379,c_1]) ).
cnf(c_2736,plain,
( select(queue_143,A) = select(q27,A)
| seq = A ),
inference(paramod,[status(thm)],[c_379,c_2]) ).
cnf(c_2737,plain,
select(queue_149,seq) = earray_148,
inference(paramod,[status(thm)],[c_383,c_1]) ).
cnf(c_2738,plain,
( select(queue_149,A) = select(q28,A)
| seq = A ),
inference(paramod,[status(thm)],[c_383,c_2]) ).
cnf(c_2740,plain,
( select(queue_155,A) = select(q2,A)
| seq = A ),
inference(paramod,[status(thm)],[c_387,c_2]) ).
cnf(c_2741,plain,
select(queue_157,tail) = index_156,
inference(paramod,[status(thm)],[c_389,c_1]) ).
cnf(c_13942,plain,
( select(queue_157,A) = select(queue_155,A)
| tail = A ),
inference(paramod,[status(thm)],[c_389,c_2]) ).
cnf(c_2742,plain,
( select(queue_155,A) = select(queue_157,A)
| tail = A ),
inference(copy,[status(thm)],[c_13942]) ).
cnf(c_2743,plain,
select(queue_164,seq) = earray_163,
inference(paramod,[status(thm)],[c_393,c_1]) ).
cnf(c_2744,plain,
( select(queue_164,A) = select(q29,A)
| seq = A ),
inference(paramod,[status(thm)],[c_393,c_2]) ).
cnf(c_13943,plain,
( select(queue_166,A) = select(queue_164,A)
| tail = A ),
inference(paramod,[status(thm)],[c_395,c_2]) ).
cnf(c_2746,plain,
( select(queue_164,A) = select(queue_166,A)
| tail = A ),
inference(copy,[status(thm)],[c_13943]) ).
cnf(c_2747,plain,
select(queue_17,seq) = earray_16,
inference(paramod,[status(thm)],[c_399,c_1]) ).
cnf(c_2748,plain,
( select(queue_17,A) = select(q10,A)
| seq = A ),
inference(paramod,[status(thm)],[c_399,c_2]) ).
cnf(c_2750,plain,
( select(queue_173,A) = select(q3,A)
| seq = A ),
inference(paramod,[status(thm)],[c_401,c_2]) ).
cnf(c_2752,plain,
( select(queue_179,A) = select(q4,A)
| seq = A ),
inference(paramod,[status(thm)],[c_405,c_2]) ).
cnf(c_2754,plain,
( select(queue_185,A) = select(q5,A)
| seq = A ),
inference(paramod,[status(thm)],[c_409,c_2]) ).
cnf(c_2755,plain,
select(queue_187,tail) = index_186,
inference(paramod,[status(thm)],[c_411,c_1]) ).
cnf(c_13944,plain,
( select(queue_187,A) = select(queue_185,A)
| tail = A ),
inference(paramod,[status(thm)],[c_411,c_2]) ).
cnf(c_2756,plain,
( select(queue_185,A) = select(queue_187,A)
| tail = A ),
inference(copy,[status(thm)],[c_13944]) ).
cnf(c_2758,plain,
( select(queue_194,A) = select(q6,A)
| seq = A ),
inference(paramod,[status(thm)],[c_417,c_2]) ).
cnf(c_2760,plain,
( select(queue_200,A) = select(q7,A)
| seq = A ),
inference(paramod,[status(thm)],[c_421,c_2]) ).
cnf(c_2762,plain,
( select(queue_206,A) = select(q8,A)
| seq = A ),
inference(paramod,[status(thm)],[c_425,c_2]) ).
cnf(c_2763,plain,
select(queue_208,tail) = index_207,
inference(paramod,[status(thm)],[c_427,c_1]) ).
cnf(c_13945,plain,
( select(queue_208,A) = select(queue_206,A)
| tail = A ),
inference(paramod,[status(thm)],[c_427,c_2]) ).
cnf(c_2764,plain,
( select(queue_206,A) = select(queue_208,A)
| tail = A ),
inference(copy,[status(thm)],[c_13945]) ).
cnf(c_2765,plain,
select(queue_23,seq) = earray_22,
inference(paramod,[status(thm)],[c_431,c_1]) ).
cnf(c_2766,plain,
( select(queue_23,A) = select(q11,A)
| seq = A ),
inference(paramod,[status(thm)],[c_431,c_2]) ).
cnf(c_2767,plain,
select(queue_25,tail) = index_24,
inference(paramod,[status(thm)],[c_433,c_1]) ).
cnf(c_13946,plain,
( select(queue_25,A) = select(queue_23,A)
| tail = A ),
inference(paramod,[status(thm)],[c_433,c_2]) ).
cnf(c_2768,plain,
( select(queue_23,A) = select(queue_25,A)
| tail = A ),
inference(copy,[status(thm)],[c_13946]) ).
cnf(c_2769,plain,
select(queue_32,seq) = earray_31,
inference(paramod,[status(thm)],[c_437,c_1]) ).
cnf(c_2770,plain,
( select(queue_32,A) = select(q12,A)
| seq = A ),
inference(paramod,[status(thm)],[c_437,c_2]) ).
cnf(c_2771,plain,
select(queue_38,seq) = earray_37,
inference(paramod,[status(thm)],[c_441,c_1]) ).
cnf(c_2772,plain,
( select(queue_38,A) = select(q13,A)
| seq = A ),
inference(paramod,[status(thm)],[c_441,c_2]) ).
cnf(c_2773,plain,
select(queue_44,seq) = earray_43,
inference(paramod,[status(thm)],[c_445,c_1]) ).
cnf(c_2774,plain,
( select(queue_44,A) = select(q14,A)
| seq = A ),
inference(paramod,[status(thm)],[c_445,c_2]) ).
cnf(c_2775,plain,
select(queue_46,tail) = index_45,
inference(paramod,[status(thm)],[c_447,c_1]) ).
cnf(c_13947,plain,
( select(queue_46,A) = select(queue_44,A)
| tail = A ),
inference(paramod,[status(thm)],[c_447,c_2]) ).
cnf(c_2776,plain,
( select(queue_44,A) = select(queue_46,A)
| tail = A ),
inference(copy,[status(thm)],[c_13947]) ).
cnf(c_2778,plain,
( select(queue_5,A) = select(q0,A)
| seq = A ),
inference(paramod,[status(thm)],[c_451,c_2]) ).
cnf(c_2779,plain,
select(queue_53,seq) = earray_52,
inference(paramod,[status(thm)],[c_453,c_1]) ).
cnf(c_2780,plain,
( select(queue_53,A) = select(q15,A)
| seq = A ),
inference(paramod,[status(thm)],[c_453,c_2]) ).
cnf(c_2781,plain,
select(queue_59,seq) = earray_58,
inference(paramod,[status(thm)],[c_457,c_1]) ).
cnf(c_2782,plain,
( select(queue_59,A) = select(q16,A)
| seq = A ),
inference(paramod,[status(thm)],[c_457,c_2]) ).
cnf(c_2783,plain,
select(queue_65,seq) = earray_64,
inference(paramod,[status(thm)],[c_461,c_1]) ).
cnf(c_2784,plain,
( select(queue_65,A) = select(q17,A)
| seq = A ),
inference(paramod,[status(thm)],[c_461,c_2]) ).
cnf(c_2785,plain,
select(queue_67,tail) = index_66,
inference(paramod,[status(thm)],[c_463,c_1]) ).
cnf(c_13948,plain,
( select(queue_67,A) = select(queue_65,A)
| tail = A ),
inference(paramod,[status(thm)],[c_463,c_2]) ).
cnf(c_2786,plain,
( select(queue_65,A) = select(queue_67,A)
| tail = A ),
inference(copy,[status(thm)],[c_13948]) ).
cnf(c_2787,plain,
select(queue_74,seq) = earray_73,
inference(paramod,[status(thm)],[c_469,c_1]) ).
cnf(c_2788,plain,
( select(queue_74,A) = select(q18,A)
| seq = A ),
inference(paramod,[status(thm)],[c_469,c_2]) ).
cnf(c_2790,plain,
( select(queue_80,A) = select(q1,A)
| seq = A ),
inference(paramod,[status(thm)],[c_473,c_2]) ).
cnf(c_2791,plain,
select(queue_86,seq) = earray_85,
inference(paramod,[status(thm)],[c_477,c_1]) ).
cnf(c_2792,plain,
( select(queue_86,A) = select(q19,A)
| seq = A ),
inference(paramod,[status(thm)],[c_477,c_2]) ).
cnf(c_2793,plain,
select(queue_92,seq) = earray_91,
inference(paramod,[status(thm)],[c_481,c_1]) ).
cnf(c_2794,plain,
( select(queue_92,A) = select(q20,A)
| seq = A ),
inference(paramod,[status(thm)],[c_481,c_2]) ).
cnf(c_2795,plain,
select(queue_94,tail) = index_93,
inference(paramod,[status(thm)],[c_483,c_1]) ).
cnf(c_13949,plain,
( select(queue_94,A) = select(queue_92,A)
| tail = A ),
inference(paramod,[status(thm)],[c_483,c_2]) ).
cnf(c_2796,plain,
( select(queue_92,A) = select(queue_94,A)
| tail = A ),
inference(copy,[status(thm)],[c_13949]) ).
cnf(c_2797,plain,
select(q0,head) = index_0,
inference(paramod,[status(thm)],[c_549,c_1]) ).
cnf(c_13950,plain,
select(q1,tail) = index_6,
inference(paramod,[status(thm)],[c_550,c_1]) ).
cnf(c_13951,plain,
index_78 = index_6,
inference(paramod,[status(thm)],[c_325,c_13950]) ).
cnf(c_2799,plain,
index_6 = index_78,
inference(copy,[status(thm)],[c_13951]) ).
cnf(c_13952,plain,
( select(q1,A) = select(queue_5,A)
| tail = A ),
inference(paramod,[status(thm)],[c_550,c_2]) ).
cnf(c_2800,plain,
( select(queue_5,A) = select(q1,A)
| tail = A ),
inference(copy,[status(thm)],[c_13952]) ).
cnf(c_2852,plain,
s(index_3) = index_78,
inference(paramod,[status(thm)],[c_2799,c_309]) ).
cnf(c_13953,plain,
select(q10,tail) = index_12,
inference(paramod,[status(thm)],[c_551,c_1]) ).
cnf(c_13954,plain,
index_15 = index_12,
inference(paramod,[status(thm)],[c_221,c_13953]) ).
cnf(c_2853,plain,
index_12 = index_15,
inference(copy,[status(thm)],[c_13954]) ).
cnf(c_13955,plain,
( select(q10,A) = select(queue_11,A)
| tail = A ),
inference(paramod,[status(thm)],[c_551,c_2]) ).
cnf(c_2854,plain,
( select(queue_11,A) = select(q10,A)
| tail = A ),
inference(copy,[status(thm)],[c_13955]) ).
cnf(c_2906,plain,
s(index_9) = index_15,
inference(paramod,[status(thm)],[c_2853,c_197]) ).
cnf(c_13956,plain,
select(q11,tail) = index_18,
inference(paramod,[status(thm)],[c_552,c_1]) ).
cnf(c_13957,plain,
index_21 = index_18,
inference(paramod,[status(thm)],[c_273,c_13956]) ).
cnf(c_2907,plain,
index_18 = index_21,
inference(copy,[status(thm)],[c_13957]) ).
cnf(c_13958,plain,
( select(q11,A) = select(queue_17,A)
| tail = A ),
inference(paramod,[status(thm)],[c_552,c_2]) ).
cnf(c_2908,plain,
( select(queue_17,A) = select(q11,A)
| tail = A ),
inference(copy,[status(thm)],[c_13958]) ).
cnf(c_2958,plain,
index_21 != index_15,
inference(paramod,[status(thm)],[c_2907,c_1541]) ).
cnf(c_13959,plain,
s(index_21) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1540]) ).
cnf(c_2959,plain,
index_24 != index_15,
inference(paramod,[status(thm)],[c_279,c_13959]) ).
cnf(c_13960,plain,
s(s(index_21)) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1539]) ).
cnf(c_2960,plain,
s(index_24) != index_15,
inference(paramod,[status(thm)],[c_279,c_13960]) ).
cnf(c_13961,plain,
s(s(s(index_21))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1538]) ).
cnf(c_2961,plain,
s(s(index_24)) != index_15,
inference(paramod,[status(thm)],[c_279,c_13961]) ).
cnf(c_13962,plain,
s(s(s(s(index_21)))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1537]) ).
cnf(c_2962,plain,
s(s(s(index_24))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13962]) ).
cnf(c_13963,plain,
s(s(s(s(s(index_21))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1536]) ).
cnf(c_2963,plain,
s(s(s(s(index_24)))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13963]) ).
cnf(c_13964,plain,
s(s(s(s(s(s(index_21)))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1535]) ).
cnf(c_2964,plain,
s(s(s(s(s(index_24))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13964]) ).
cnf(c_13965,plain,
s(s(s(s(s(s(s(index_21))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1534]) ).
cnf(c_2965,plain,
s(s(s(s(s(s(index_24)))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13965]) ).
cnf(c_13966,plain,
s(s(s(s(s(s(s(s(index_21)))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1533]) ).
cnf(c_2966,plain,
s(s(s(s(s(s(s(index_24))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13966]) ).
cnf(c_13967,plain,
s(s(s(s(s(s(s(s(s(index_21))))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1532]) ).
cnf(c_2967,plain,
s(s(s(s(s(s(s(s(index_24)))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13967]) ).
cnf(c_13968,plain,
s(s(s(s(s(s(s(s(s(s(index_21)))))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1531]) ).
cnf(c_2968,plain,
s(s(s(s(s(s(s(s(s(index_24))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13968]) ).
cnf(c_13969,plain,
s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1530]) ).
cnf(c_2969,plain,
s(s(s(s(s(s(s(s(s(s(index_24)))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13969]) ).
cnf(c_13970,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1529]) ).
cnf(c_2970,plain,
s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13970]) ).
cnf(c_13971,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_21))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1528]) ).
cnf(c_2971,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13971]) ).
cnf(c_13972,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_21)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_2907,c_1527]) ).
cnf(c_2972,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13972]) ).
cnf(c_13973,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_2907,c_1526]) ).
cnf(c_2973,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13973]) ).
cnf(c_13974,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_2907,c_1525]) ).
cnf(c_2974,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13974]) ).
cnf(c_13975,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_2907,c_1524]) ).
cnf(c_2975,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24)))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13975]) ).
cnf(c_13976,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_2907,c_1523]) ).
cnf(c_2976,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_24))))))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_279,c_13976]) ).
cnf(c_3010,plain,
select(q12,head) = index_27,
inference(paramod,[status(thm)],[c_553,c_1]) ).
cnf(c_13977,plain,
( select(q12,A) = select(queue_25,A)
| head = A ),
inference(paramod,[status(thm)],[c_553,c_2]) ).
cnf(c_3011,plain,
( select(queue_25,A) = select(q12,A)
| head = A ),
inference(copy,[status(thm)],[c_13977]) ).
cnf(c_13978,plain,
select(q13,tail) = index_33,
inference(paramod,[status(thm)],[c_554,c_1]) ).
cnf(c_13979,plain,
index_36 = index_33,
inference(paramod,[status(thm)],[c_291,c_13978]) ).
cnf(c_3012,plain,
index_33 = index_36,
inference(copy,[status(thm)],[c_13979]) ).
cnf(c_13980,plain,
( select(q13,A) = select(queue_32,A)
| tail = A ),
inference(paramod,[status(thm)],[c_554,c_2]) ).
cnf(c_3013,plain,
( select(queue_32,A) = select(q13,A)
| tail = A ),
inference(copy,[status(thm)],[c_13980]) ).
cnf(c_3065,plain,
s(index_30) = index_36,
inference(paramod,[status(thm)],[c_3012,c_289]) ).
cnf(c_13981,plain,
select(q14,tail) = index_39,
inference(paramod,[status(thm)],[c_555,c_1]) ).
cnf(c_13982,plain,
index_42 = index_39,
inference(paramod,[status(thm)],[c_295,c_13981]) ).
cnf(c_3066,plain,
index_39 = index_42,
inference(copy,[status(thm)],[c_13982]) ).
cnf(c_13983,plain,
( select(q14,A) = select(queue_38,A)
| tail = A ),
inference(paramod,[status(thm)],[c_555,c_2]) ).
cnf(c_3067,plain,
( select(queue_38,A) = select(q14,A)
| tail = A ),
inference(copy,[status(thm)],[c_13983]) ).
cnf(c_3168,plain,
s(index_36) = index_42,
inference(paramod,[status(thm)],[c_3066,c_293]) ).
cnf(c_3169,plain,
select(q15,head) = index_48,
inference(paramod,[status(thm)],[c_556,c_1]) ).
cnf(c_13984,plain,
( select(q15,A) = select(queue_46,A)
| head = A ),
inference(paramod,[status(thm)],[c_556,c_2]) ).
cnf(c_3170,plain,
( select(queue_46,A) = select(q15,A)
| head = A ),
inference(copy,[status(thm)],[c_13984]) ).
cnf(c_13985,plain,
select(q16,tail) = index_54,
inference(paramod,[status(thm)],[c_557,c_1]) ).
cnf(c_13986,plain,
index_57 = index_54,
inference(paramod,[status(thm)],[c_307,c_13985]) ).
cnf(c_3171,plain,
index_54 = index_57,
inference(copy,[status(thm)],[c_13986]) ).
cnf(c_13987,plain,
( select(q16,A) = select(queue_53,A)
| tail = A ),
inference(paramod,[status(thm)],[c_557,c_2]) ).
cnf(c_3172,plain,
( select(queue_53,A) = select(q16,A)
| tail = A ),
inference(copy,[status(thm)],[c_13987]) ).
cnf(c_3224,plain,
s(index_51) = index_57,
inference(paramod,[status(thm)],[c_3171,c_305]) ).
cnf(c_13988,plain,
select(q17,tail) = index_60,
inference(paramod,[status(thm)],[c_558,c_1]) ).
cnf(c_13989,plain,
index_63 = index_60,
inference(paramod,[status(thm)],[c_313,c_13988]) ).
cnf(c_3225,plain,
index_60 = index_63,
inference(copy,[status(thm)],[c_13989]) ).
cnf(c_13990,plain,
( select(q17,A) = select(queue_59,A)
| tail = A ),
inference(paramod,[status(thm)],[c_558,c_2]) ).
cnf(c_3226,plain,
( select(queue_59,A) = select(q17,A)
| tail = A ),
inference(copy,[status(thm)],[c_13990]) ).
cnf(c_3327,plain,
s(index_57) = index_63,
inference(paramod,[status(thm)],[c_3225,c_311]) ).
cnf(c_3328,plain,
select(q18,head) = index_69,
inference(paramod,[status(thm)],[c_559,c_1]) ).
cnf(c_13991,plain,
( select(q18,A) = select(queue_67,A)
| head = A ),
inference(paramod,[status(thm)],[c_559,c_2]) ).
cnf(c_3329,plain,
( select(queue_67,A) = select(q18,A)
| head = A ),
inference(copy,[status(thm)],[c_13991]) ).
cnf(c_13992,plain,
select(q19,tail) = index_75,
inference(paramod,[status(thm)],[c_560,c_1]) ).
cnf(c_13993,plain,
index_84 = index_75,
inference(paramod,[status(thm)],[c_329,c_13992]) ).
cnf(c_3330,plain,
index_75 = index_84,
inference(copy,[status(thm)],[c_13993]) ).
cnf(c_13994,plain,
( select(q19,A) = select(queue_74,A)
| tail = A ),
inference(paramod,[status(thm)],[c_560,c_2]) ).
cnf(c_3331,plain,
( select(queue_74,A) = select(q19,A)
| tail = A ),
inference(copy,[status(thm)],[c_13994]) ).
cnf(c_3383,plain,
s(index_72) = index_84,
inference(paramod,[status(thm)],[c_3330,c_323]) ).
cnf(c_13995,plain,
select(q2,tail) = index_81,
inference(paramod,[status(thm)],[c_561,c_1]) ).
cnf(c_13996,plain,
index_153 = index_81,
inference(paramod,[status(thm)],[c_225,c_13995]) ).
cnf(c_3384,plain,
index_81 = index_153,
inference(copy,[status(thm)],[c_13996]) ).
cnf(c_13997,plain,
( select(q2,A) = select(queue_80,A)
| tail = A ),
inference(paramod,[status(thm)],[c_561,c_2]) ).
cnf(c_3385,plain,
( select(queue_80,A) = select(q2,A)
| tail = A ),
inference(copy,[status(thm)],[c_13997]) ).
cnf(c_3486,plain,
s(index_78) = index_153,
inference(paramod,[status(thm)],[c_3384,c_327]) ).
cnf(c_13998,plain,
select(q20,tail) = index_87,
inference(paramod,[status(thm)],[c_562,c_1]) ).
cnf(c_13999,plain,
index_90 = index_87,
inference(paramod,[status(thm)],[c_335,c_13998]) ).
cnf(c_3487,plain,
index_87 = index_90,
inference(copy,[status(thm)],[c_13999]) ).
cnf(c_14000,plain,
( select(q20,A) = select(queue_86,A)
| tail = A ),
inference(paramod,[status(thm)],[c_562,c_2]) ).
cnf(c_3488,plain,
( select(queue_86,A) = select(q20,A)
| tail = A ),
inference(copy,[status(thm)],[c_14000]) ).
cnf(c_3589,plain,
s(index_84) = index_90,
inference(paramod,[status(thm)],[c_3487,c_331]) ).
cnf(c_3590,plain,
select(q21,head) = index_96,
inference(paramod,[status(thm)],[c_563,c_1]) ).
cnf(c_14001,plain,
( select(q21,A) = select(queue_94,A)
| head = A ),
inference(paramod,[status(thm)],[c_563,c_2]) ).
cnf(c_3591,plain,
( select(queue_94,A) = select(q21,A)
| head = A ),
inference(copy,[status(thm)],[c_14001]) ).
cnf(c_14002,plain,
select(q22,tail) = index_102,
inference(paramod,[status(thm)],[c_564,c_1]) ).
cnf(c_14003,plain,
index_105 = index_102,
inference(paramod,[status(thm)],[c_185,c_14002]) ).
cnf(c_3592,plain,
index_102 = index_105,
inference(copy,[status(thm)],[c_14003]) ).
cnf(c_14004,plain,
( select(q22,A) = select(queue_101,A)
| tail = A ),
inference(paramod,[status(thm)],[c_564,c_2]) ).
cnf(c_3593,plain,
( select(queue_101,A) = select(q22,A)
| tail = A ),
inference(copy,[status(thm)],[c_14004]) ).
cnf(c_3645,plain,
s(index_99) = index_105,
inference(paramod,[status(thm)],[c_3592,c_183]) ).
cnf(c_14005,plain,
select(q23,tail) = index_108,
inference(paramod,[status(thm)],[c_565,c_1]) ).
cnf(c_14006,plain,
index_111 = index_108,
inference(paramod,[status(thm)],[c_189,c_14005]) ).
cnf(c_3646,plain,
index_108 = index_111,
inference(copy,[status(thm)],[c_14006]) ).
cnf(c_14007,plain,
( select(q23,A) = select(queue_107,A)
| tail = A ),
inference(paramod,[status(thm)],[c_565,c_2]) ).
cnf(c_3647,plain,
( select(queue_107,A) = select(q23,A)
| tail = A ),
inference(copy,[status(thm)],[c_14007]) ).
cnf(c_3748,plain,
s(index_105) = index_111,
inference(paramod,[status(thm)],[c_3646,c_187]) ).
cnf(c_3749,plain,
select(q24,head) = index_117,
inference(paramod,[status(thm)],[c_566,c_1]) ).
cnf(c_14008,plain,
( select(q24,A) = select(queue_115,A)
| head = A ),
inference(paramod,[status(thm)],[c_566,c_2]) ).
cnf(c_3750,plain,
( select(queue_115,A) = select(q24,A)
| head = A ),
inference(copy,[status(thm)],[c_14008]) ).
cnf(c_14009,plain,
select(q25,tail) = index_123,
inference(paramod,[status(thm)],[c_567,c_1]) ).
cnf(c_14010,plain,
index_126 = index_123,
inference(paramod,[status(thm)],[c_203,c_14009]) ).
cnf(c_3751,plain,
index_123 = index_126,
inference(copy,[status(thm)],[c_14010]) ).
cnf(c_14011,plain,
( select(q25,A) = select(queue_122,A)
| tail = A ),
inference(paramod,[status(thm)],[c_567,c_2]) ).
cnf(c_3752,plain,
( select(queue_122,A) = select(q25,A)
| tail = A ),
inference(copy,[status(thm)],[c_14011]) ).
cnf(c_3804,plain,
s(index_120) = index_126,
inference(paramod,[status(thm)],[c_3751,c_201]) ).
cnf(c_14012,plain,
select(q26,tail) = index_129,
inference(paramod,[status(thm)],[c_568,c_1]) ).
cnf(c_14013,plain,
index_132 = index_129,
inference(paramod,[status(thm)],[c_207,c_14012]) ).
cnf(c_3805,plain,
index_129 = index_132,
inference(copy,[status(thm)],[c_14013]) ).
cnf(c_14014,plain,
( select(q26,A) = select(queue_128,A)
| tail = A ),
inference(paramod,[status(thm)],[c_568,c_2]) ).
cnf(c_3806,plain,
( select(queue_128,A) = select(q26,A)
| tail = A ),
inference(copy,[status(thm)],[c_14014]) ).
cnf(c_3907,plain,
s(index_126) = index_132,
inference(paramod,[status(thm)],[c_3805,c_205]) ).
cnf(c_3908,plain,
select(q27,head) = index_138,
inference(paramod,[status(thm)],[c_569,c_1]) ).
cnf(c_14015,plain,
( select(q27,A) = select(queue_136,A)
| head = A ),
inference(paramod,[status(thm)],[c_569,c_2]) ).
cnf(c_3909,plain,
( select(queue_136,A) = select(q27,A)
| head = A ),
inference(copy,[status(thm)],[c_14015]) ).
cnf(c_14016,plain,
select(q28,tail) = index_144,
inference(paramod,[status(thm)],[c_570,c_1]) ).
cnf(c_14017,plain,
index_147 = index_144,
inference(paramod,[status(thm)],[c_219,c_14016]) ).
cnf(c_3910,plain,
index_144 = index_147,
inference(copy,[status(thm)],[c_14017]) ).
cnf(c_14018,plain,
( select(q28,A) = select(queue_143,A)
| tail = A ),
inference(paramod,[status(thm)],[c_570,c_2]) ).
cnf(c_3911,plain,
( select(queue_143,A) = select(q28,A)
| tail = A ),
inference(copy,[status(thm)],[c_14018]) ).
cnf(c_3963,plain,
s(index_141) = index_147,
inference(paramod,[status(thm)],[c_3910,c_217]) ).
cnf(c_14019,plain,
select(q29,tail) = index_150,
inference(paramod,[status(thm)],[c_571,c_1]) ).
cnf(c_14020,plain,
index_162 = index_150,
inference(paramod,[status(thm)],[c_233,c_14019]) ).
cnf(c_3964,plain,
index_150 = index_162,
inference(copy,[status(thm)],[c_14020]) ).
cnf(c_14021,plain,
( select(q29,A) = select(queue_149,A)
| tail = A ),
inference(paramod,[status(thm)],[c_571,c_2]) ).
cnf(c_3965,plain,
( select(queue_149,A) = select(q29,A)
| tail = A ),
inference(copy,[status(thm)],[c_14021]) ).
cnf(c_4066,plain,
s(index_147) = index_162,
inference(paramod,[status(thm)],[c_3964,c_223]) ).
cnf(c_4067,plain,
select(q3,head) = index_159,
inference(paramod,[status(thm)],[c_572,c_1]) ).
cnf(c_14022,plain,
( select(q3,A) = select(queue_157,A)
| head = A ),
inference(paramod,[status(thm)],[c_572,c_2]) ).
cnf(c_4068,plain,
( select(queue_157,A) = select(q3,A)
| head = A ),
inference(copy,[status(thm)],[c_14022]) ).
cnf(c_14023,plain,
select(q30,head) = index_168,
inference(paramod,[status(thm)],[c_573,c_1]) ).
cnf(c_4069,plain,
index_213 = index_168,
inference(paramod,[status(thm)],[c_277,c_14023]) ).
cnf(c_14024,plain,
( select(q30,A) = select(queue_166,A)
| head = A ),
inference(paramod,[status(thm)],[c_573,c_2]) ).
cnf(c_4070,plain,
( select(queue_166,A) = select(q30,A)
| head = A ),
inference(copy,[status(thm)],[c_14024]) ).
cnf(c_4074,plain,
select(earray_212,index_168) = elem_214,
inference(paramod,[status(thm)],[c_4069,c_179]) ).
cnf(c_14025,plain,
select(q4,tail) = index_174,
inference(paramod,[status(thm)],[c_574,c_1]) ).
cnf(c_14026,plain,
index_177 = index_174,
inference(paramod,[status(thm)],[c_245,c_14025]) ).
cnf(c_4075,plain,
index_174 = index_177,
inference(copy,[status(thm)],[c_14026]) ).
cnf(c_14027,plain,
( select(q4,A) = select(queue_173,A)
| tail = A ),
inference(paramod,[status(thm)],[c_574,c_2]) ).
cnf(c_4076,plain,
( select(queue_173,A) = select(q4,A)
| tail = A ),
inference(copy,[status(thm)],[c_14027]) ).
cnf(c_4128,plain,
s(index_171) = index_177,
inference(paramod,[status(thm)],[c_4075,c_243]) ).
cnf(c_14028,plain,
select(q5,tail) = index_180,
inference(paramod,[status(thm)],[c_575,c_1]) ).
cnf(c_14029,plain,
index_183 = index_180,
inference(paramod,[status(thm)],[c_251,c_14028]) ).
cnf(c_4129,plain,
index_180 = index_183,
inference(copy,[status(thm)],[c_14029]) ).
cnf(c_14030,plain,
( select(q5,A) = select(queue_179,A)
| tail = A ),
inference(paramod,[status(thm)],[c_575,c_2]) ).
cnf(c_4130,plain,
( select(queue_179,A) = select(q5,A)
| tail = A ),
inference(copy,[status(thm)],[c_14030]) ).
cnf(c_4231,plain,
s(index_177) = index_183,
inference(paramod,[status(thm)],[c_4129,c_249]) ).
cnf(c_4232,plain,
select(q6,head) = index_189,
inference(paramod,[status(thm)],[c_576,c_1]) ).
cnf(c_14031,plain,
( select(q6,A) = select(queue_187,A)
| head = A ),
inference(paramod,[status(thm)],[c_576,c_2]) ).
cnf(c_4233,plain,
( select(queue_187,A) = select(q6,A)
| head = A ),
inference(copy,[status(thm)],[c_14031]) ).
cnf(c_14032,plain,
select(q7,tail) = index_195,
inference(paramod,[status(thm)],[c_577,c_1]) ).
cnf(c_14033,plain,
index_198 = index_195,
inference(paramod,[status(thm)],[c_263,c_14032]) ).
cnf(c_4234,plain,
index_195 = index_198,
inference(copy,[status(thm)],[c_14033]) ).
cnf(c_14034,plain,
( select(q7,A) = select(queue_194,A)
| tail = A ),
inference(paramod,[status(thm)],[c_577,c_2]) ).
cnf(c_4235,plain,
( select(queue_194,A) = select(q7,A)
| tail = A ),
inference(copy,[status(thm)],[c_14034]) ).
cnf(c_4287,plain,
s(index_192) = index_198,
inference(paramod,[status(thm)],[c_4234,c_261]) ).
cnf(c_14035,plain,
select(q8,tail) = index_201,
inference(paramod,[status(thm)],[c_578,c_1]) ).
cnf(c_14036,plain,
index_204 = index_201,
inference(paramod,[status(thm)],[c_267,c_14035]) ).
cnf(c_4288,plain,
index_201 = index_204,
inference(copy,[status(thm)],[c_14036]) ).
cnf(c_14037,plain,
( select(q8,A) = select(queue_200,A)
| tail = A ),
inference(paramod,[status(thm)],[c_578,c_2]) ).
cnf(c_4289,plain,
( select(queue_200,A) = select(q8,A)
| tail = A ),
inference(copy,[status(thm)],[c_14037]) ).
cnf(c_4390,plain,
s(index_198) = index_204,
inference(paramod,[status(thm)],[c_4288,c_265]) ).
cnf(c_4391,plain,
select(q9,head) = index_210,
inference(paramod,[status(thm)],[c_579,c_1]) ).
cnf(c_14038,plain,
( select(q9,A) = select(queue_208,A)
| head = A ),
inference(paramod,[status(thm)],[c_579,c_2]) ).
cnf(c_4392,plain,
( select(queue_208,A) = select(q9,A)
| head = A ),
inference(copy,[status(thm)],[c_14038]) ).
cnf(c_14039,plain,
( select(queue_101,head) = index_96
| seq = head ),
inference(paramod,[status(thm)],[c_3590,c_2718]) ).
cnf(c_14040,plain,
( select(queue_101,head) = index_96
| head = seq ),
inference(copy,[status(thm)],[c_14039]) ).
cnf(c_5252,plain,
select(queue_101,head) = index_96,
inference(resolve,[status(thm)],[c_4,c_14040]) ).
cnf(c_14041,plain,
( select(queue_11,head) = index_210
| seq = head ),
inference(paramod,[status(thm)],[c_4391,c_2722]) ).
cnf(c_14042,plain,
( select(queue_11,head) = index_210
| head = seq ),
inference(copy,[status(thm)],[c_14041]) ).
cnf(c_5279,plain,
select(queue_11,head) = index_210,
inference(resolve,[status(thm)],[c_4,c_14042]) ).
cnf(c_14043,plain,
( select(queue_113,head) = index_116
| tail = head ),
inference(paramod,[status(thm)],[c_193,c_2726]) ).
cnf(c_14044,plain,
( select(queue_113,head) = index_116
| head = tail ),
inference(copy,[status(thm)],[c_14043]) ).
cnf(c_5309,plain,
select(queue_113,head) = index_116,
inference(resolve,[status(thm)],[c_3,c_14044]) ).
cnf(c_14045,plain,
( select(queue_115,seq) = earray_112
| tail = seq ),
inference(paramod,[status(thm)],[c_2726,c_2723]) ).
cnf(c_5312,plain,
select(queue_115,seq) = earray_112,
inference(resolve,[status(thm)],[c_5,c_14045]) ).
cnf(c_14046,plain,
( index_116 = select(q23,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5309,c_2724]) ).
cnf(c_14047,plain,
( index_116 = select(q23,head)
| head = seq ),
inference(copy,[status(thm)],[c_14046]) ).
cnf(c_14048,plain,
( select(q23,head) = index_116
| head = seq ),
inference(copy,[status(thm)],[c_14047]) ).
cnf(c_5321,plain,
select(q23,head) = index_116,
inference(resolve,[status(thm)],[c_4,c_14048]) ).
cnf(c_14049,plain,
( select(queue_122,head) = index_117
| seq = head ),
inference(paramod,[status(thm)],[c_3749,c_2728]) ).
cnf(c_14050,plain,
( select(queue_122,head) = index_117
| head = seq ),
inference(copy,[status(thm)],[c_14049]) ).
cnf(c_5336,plain,
select(queue_122,head) = index_117,
inference(resolve,[status(thm)],[c_4,c_14050]) ).
cnf(c_14051,plain,
( select(queue_134,head) = index_137
| tail = head ),
inference(paramod,[status(thm)],[c_211,c_2734]) ).
cnf(c_14052,plain,
( select(queue_134,head) = index_137
| head = tail ),
inference(copy,[status(thm)],[c_14051]) ).
cnf(c_5370,plain,
select(queue_134,head) = index_137,
inference(resolve,[status(thm)],[c_3,c_14052]) ).
cnf(c_14053,plain,
( select(queue_136,seq) = earray_133
| tail = seq ),
inference(paramod,[status(thm)],[c_2734,c_2731]) ).
cnf(c_5373,plain,
select(queue_136,seq) = earray_133,
inference(resolve,[status(thm)],[c_5,c_14053]) ).
cnf(c_14054,plain,
( index_137 = select(q26,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5370,c_2732]) ).
cnf(c_14055,plain,
( index_137 = select(q26,head)
| head = seq ),
inference(copy,[status(thm)],[c_14054]) ).
cnf(c_14056,plain,
( select(q26,head) = index_137
| head = seq ),
inference(copy,[status(thm)],[c_14055]) ).
cnf(c_5387,plain,
select(q26,head) = index_137,
inference(resolve,[status(thm)],[c_4,c_14056]) ).
cnf(c_14057,plain,
( select(queue_143,head) = index_138
| seq = head ),
inference(paramod,[status(thm)],[c_3908,c_2736]) ).
cnf(c_14058,plain,
( select(queue_143,head) = index_138
| head = seq ),
inference(copy,[status(thm)],[c_14057]) ).
cnf(c_5397,plain,
select(queue_143,head) = index_138,
inference(resolve,[status(thm)],[c_4,c_14058]) ).
cnf(c_14059,plain,
( select(queue_155,head) = index_158
| tail = head ),
inference(paramod,[status(thm)],[c_229,c_2742]) ).
cnf(c_14060,plain,
( select(queue_155,head) = index_158
| head = tail ),
inference(copy,[status(thm)],[c_14059]) ).
cnf(c_5436,plain,
select(queue_155,head) = index_158,
inference(resolve,[status(thm)],[c_3,c_14060]) ).
cnf(c_14061,plain,
( index_158 = select(q2,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5436,c_2740]) ).
cnf(c_14062,plain,
( index_158 = select(q2,head)
| head = seq ),
inference(copy,[status(thm)],[c_14061]) ).
cnf(c_14063,plain,
( select(q2,head) = index_158
| head = seq ),
inference(copy,[status(thm)],[c_14062]) ).
cnf(c_5448,plain,
select(q2,head) = index_158,
inference(resolve,[status(thm)],[c_4,c_14063]) ).
cnf(c_14064,plain,
( select(queue_164,head) = index_167
| tail = head ),
inference(paramod,[status(thm)],[c_237,c_2746]) ).
cnf(c_14065,plain,
( select(queue_164,head) = index_167
| head = tail ),
inference(copy,[status(thm)],[c_14064]) ).
cnf(c_5475,plain,
select(queue_164,head) = index_167,
inference(resolve,[status(thm)],[c_3,c_14065]) ).
cnf(c_14066,plain,
( select(queue_166,seq) = earray_163
| tail = seq ),
inference(paramod,[status(thm)],[c_2746,c_2743]) ).
cnf(c_5478,plain,
select(queue_166,seq) = earray_163,
inference(resolve,[status(thm)],[c_5,c_14066]) ).
cnf(c_14067,plain,
( index_167 = select(q29,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5475,c_2744]) ).
cnf(c_14068,plain,
( index_167 = select(q29,head)
| head = seq ),
inference(copy,[status(thm)],[c_14067]) ).
cnf(c_14069,plain,
( select(q29,head) = index_167
| head = seq ),
inference(copy,[status(thm)],[c_14068]) ).
cnf(c_5487,plain,
select(q29,head) = index_167,
inference(resolve,[status(thm)],[c_4,c_14069]) ).
cnf(c_14070,plain,
( select(queue_173,head) = index_159
| seq = head ),
inference(paramod,[status(thm)],[c_4067,c_2750]) ).
cnf(c_14071,plain,
( select(queue_173,head) = index_159
| head = seq ),
inference(copy,[status(thm)],[c_14070]) ).
cnf(c_5511,plain,
select(queue_173,head) = index_159,
inference(resolve,[status(thm)],[c_4,c_14071]) ).
cnf(c_14072,plain,
( select(queue_185,head) = index_188
| tail = head ),
inference(paramod,[status(thm)],[c_255,c_2756]) ).
cnf(c_14073,plain,
( select(queue_185,head) = index_188
| head = tail ),
inference(copy,[status(thm)],[c_14072]) ).
cnf(c_5550,plain,
select(queue_185,head) = index_188,
inference(resolve,[status(thm)],[c_3,c_14073]) ).
cnf(c_14074,plain,
( index_188 = select(q5,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5550,c_2754]) ).
cnf(c_14075,plain,
( index_188 = select(q5,head)
| head = seq ),
inference(copy,[status(thm)],[c_14074]) ).
cnf(c_14076,plain,
( select(q5,head) = index_188
| head = seq ),
inference(copy,[status(thm)],[c_14075]) ).
cnf(c_5562,plain,
select(q5,head) = index_188,
inference(resolve,[status(thm)],[c_4,c_14076]) ).
cnf(c_14077,plain,
( select(queue_194,head) = index_189
| seq = head ),
inference(paramod,[status(thm)],[c_4232,c_2758]) ).
cnf(c_14078,plain,
( select(queue_194,head) = index_189
| head = seq ),
inference(copy,[status(thm)],[c_14077]) ).
cnf(c_5577,plain,
select(queue_194,head) = index_189,
inference(resolve,[status(thm)],[c_4,c_14078]) ).
cnf(c_14079,plain,
( select(q0,tail) = index_0
| tail = head ),
inference(paramod,[status(thm)],[c_549,c_675]) ).
cnf(c_14080,plain,
( index_3 = index_0
| tail = head ),
inference(paramod,[status(thm)],[c_285,c_14079]) ).
cnf(c_14081,plain,
( index_3 = index_0
| head = tail ),
inference(copy,[status(thm)],[c_14080]) ).
cnf(c_14082,plain,
( index_0 = index_3
| head = tail ),
inference(copy,[status(thm)],[c_14081]) ).
cnf(c_5587,plain,
index_0 = index_3,
inference(resolve,[status(thm)],[c_3,c_14082]) ).
cnf(c_5595,plain,
select(q0,head) = index_3,
inference(paramod,[status(thm)],[c_5587,c_2797]) ).
cnf(c_14083,plain,
( select(queue_206,head) = index_209
| tail = head ),
inference(paramod,[status(thm)],[c_271,c_2764]) ).
cnf(c_14084,plain,
( select(queue_206,head) = index_209
| head = tail ),
inference(copy,[status(thm)],[c_14083]) ).
cnf(c_5631,plain,
select(queue_206,head) = index_209,
inference(resolve,[status(thm)],[c_3,c_14084]) ).
cnf(c_14085,plain,
( index_209 = select(q8,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5631,c_2762]) ).
cnf(c_14086,plain,
( index_209 = select(q8,head)
| head = seq ),
inference(copy,[status(thm)],[c_14085]) ).
cnf(c_14087,plain,
( select(q8,head) = index_209
| head = seq ),
inference(copy,[status(thm)],[c_14086]) ).
cnf(c_5643,plain,
select(q8,head) = index_209,
inference(resolve,[status(thm)],[c_4,c_14087]) ).
cnf(c_14088,plain,
( select(queue_23,head) = index_26
| tail = head ),
inference(paramod,[status(thm)],[c_281,c_2768]) ).
cnf(c_14089,plain,
( select(queue_23,head) = index_26
| head = tail ),
inference(copy,[status(thm)],[c_14088]) ).
cnf(c_5660,plain,
select(queue_23,head) = index_26,
inference(resolve,[status(thm)],[c_3,c_14089]) ).
cnf(c_14090,plain,
( select(queue_25,seq) = earray_22
| tail = seq ),
inference(paramod,[status(thm)],[c_2768,c_2765]) ).
cnf(c_5663,plain,
select(queue_25,seq) = earray_22,
inference(resolve,[status(thm)],[c_5,c_14090]) ).
cnf(c_14091,plain,
( index_26 = select(q11,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5660,c_2766]) ).
cnf(c_14092,plain,
( index_26 = select(q11,head)
| head = seq ),
inference(copy,[status(thm)],[c_14091]) ).
cnf(c_14093,plain,
( select(q11,head) = index_26
| head = seq ),
inference(copy,[status(thm)],[c_14092]) ).
cnf(c_5672,plain,
select(q11,head) = index_26,
inference(resolve,[status(thm)],[c_4,c_14093]) ).
cnf(c_14094,plain,
( select(queue_32,head) = index_27
| seq = head ),
inference(paramod,[status(thm)],[c_3010,c_2770]) ).
cnf(c_14095,plain,
( select(queue_32,head) = index_27
| head = seq ),
inference(copy,[status(thm)],[c_14094]) ).
cnf(c_5682,plain,
select(queue_32,head) = index_27,
inference(resolve,[status(thm)],[c_4,c_14095]) ).
cnf(c_14096,plain,
( select(queue_44,head) = index_47
| tail = head ),
inference(paramod,[status(thm)],[c_299,c_2776]) ).
cnf(c_14097,plain,
( select(queue_44,head) = index_47
| head = tail ),
inference(copy,[status(thm)],[c_14096]) ).
cnf(c_5711,plain,
select(queue_44,head) = index_47,
inference(resolve,[status(thm)],[c_3,c_14097]) ).
cnf(c_14098,plain,
( select(queue_46,seq) = earray_43
| tail = seq ),
inference(paramod,[status(thm)],[c_2776,c_2773]) ).
cnf(c_5714,plain,
select(queue_46,seq) = earray_43,
inference(resolve,[status(thm)],[c_5,c_14098]) ).
cnf(c_14099,plain,
( index_47 = select(q14,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5711,c_2774]) ).
cnf(c_14100,plain,
( index_47 = select(q14,head)
| head = seq ),
inference(copy,[status(thm)],[c_14099]) ).
cnf(c_14101,plain,
( select(q14,head) = index_47
| head = seq ),
inference(copy,[status(thm)],[c_14100]) ).
cnf(c_5723,plain,
select(q14,head) = index_47,
inference(resolve,[status(thm)],[c_4,c_14101]) ).
cnf(c_14102,plain,
( select(queue_5,head) = index_3
| seq = head ),
inference(paramod,[status(thm)],[c_5595,c_2778]) ).
cnf(c_14103,plain,
( select(queue_5,head) = index_3
| head = seq ),
inference(copy,[status(thm)],[c_14102]) ).
cnf(c_5733,plain,
select(queue_5,head) = index_3,
inference(resolve,[status(thm)],[c_4,c_14103]) ).
cnf(c_14104,plain,
( select(queue_53,head) = index_48
| seq = head ),
inference(paramod,[status(thm)],[c_3169,c_2780]) ).
cnf(c_14105,plain,
( select(queue_53,head) = index_48
| head = seq ),
inference(copy,[status(thm)],[c_14104]) ).
cnf(c_5746,plain,
select(queue_53,head) = index_48,
inference(resolve,[status(thm)],[c_4,c_14105]) ).
cnf(c_14106,plain,
( select(queue_65,head) = index_68
| tail = head ),
inference(paramod,[status(thm)],[c_317,c_2786]) ).
cnf(c_14107,plain,
( select(queue_65,head) = index_68
| head = tail ),
inference(copy,[status(thm)],[c_14106]) ).
cnf(c_5775,plain,
select(queue_65,head) = index_68,
inference(resolve,[status(thm)],[c_3,c_14107]) ).
cnf(c_14108,plain,
( select(queue_67,seq) = earray_64
| tail = seq ),
inference(paramod,[status(thm)],[c_2786,c_2783]) ).
cnf(c_5778,plain,
select(queue_67,seq) = earray_64,
inference(resolve,[status(thm)],[c_5,c_14108]) ).
cnf(c_14109,plain,
( index_68 = select(q17,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5775,c_2784]) ).
cnf(c_14110,plain,
( index_68 = select(q17,head)
| head = seq ),
inference(copy,[status(thm)],[c_14109]) ).
cnf(c_14111,plain,
( select(q17,head) = index_68
| head = seq ),
inference(copy,[status(thm)],[c_14110]) ).
cnf(c_5787,plain,
select(q17,head) = index_68,
inference(resolve,[status(thm)],[c_4,c_14111]) ).
cnf(c_14112,plain,
( select(queue_74,head) = index_69
| seq = head ),
inference(paramod,[status(thm)],[c_3328,c_2788]) ).
cnf(c_14113,plain,
( select(queue_74,head) = index_69
| head = seq ),
inference(copy,[status(thm)],[c_14112]) ).
cnf(c_5797,plain,
select(queue_74,head) = index_69,
inference(resolve,[status(thm)],[c_4,c_14113]) ).
cnf(c_14114,plain,
( select(queue_92,head) = index_95
| tail = head ),
inference(paramod,[status(thm)],[c_339,c_2796]) ).
cnf(c_14115,plain,
( select(queue_92,head) = index_95
| head = tail ),
inference(copy,[status(thm)],[c_14114]) ).
cnf(c_5835,plain,
select(queue_92,head) = index_95,
inference(resolve,[status(thm)],[c_3,c_14115]) ).
cnf(c_14116,plain,
( select(queue_94,seq) = earray_91
| tail = seq ),
inference(paramod,[status(thm)],[c_2796,c_2793]) ).
cnf(c_5838,plain,
select(queue_94,seq) = earray_91,
inference(resolve,[status(thm)],[c_5,c_14116]) ).
cnf(c_14117,plain,
( index_95 = select(q20,head)
| seq = head ),
inference(paramod,[status(thm)],[c_5835,c_2794]) ).
cnf(c_14118,plain,
( index_95 = select(q20,head)
| head = seq ),
inference(copy,[status(thm)],[c_14117]) ).
cnf(c_14119,plain,
( select(q20,head) = index_95
| head = seq ),
inference(copy,[status(thm)],[c_14118]) ).
cnf(c_5847,plain,
select(q20,head) = index_95,
inference(resolve,[status(thm)],[c_4,c_14119]) ).
cnf(c_14120,plain,
( select(q1,head) = index_3
| tail = head ),
inference(paramod,[status(thm)],[c_2800,c_5733]) ).
cnf(c_14121,plain,
( select(q1,head) = index_3
| head = tail ),
inference(copy,[status(thm)],[c_14120]) ).
cnf(c_5870,plain,
select(q1,head) = index_3,
inference(resolve,[status(thm)],[c_3,c_14121]) ).
cnf(c_14122,plain,
( select(queue_80,head) = index_3
| seq = head ),
inference(paramod,[status(thm)],[c_5870,c_2790]) ).
cnf(c_14123,plain,
( select(queue_80,head) = index_3
| head = seq ),
inference(copy,[status(thm)],[c_14122]) ).
cnf(c_5896,plain,
select(queue_80,head) = index_3,
inference(resolve,[status(thm)],[c_4,c_14123]) ).
cnf(c_14124,plain,
( select(q10,head) = index_210
| tail = head ),
inference(paramod,[status(thm)],[c_2854,c_5279]) ).
cnf(c_14125,plain,
( select(q10,head) = index_210
| head = tail ),
inference(copy,[status(thm)],[c_14124]) ).
cnf(c_5905,plain,
select(q10,head) = index_210,
inference(resolve,[status(thm)],[c_3,c_14125]) ).
cnf(c_14126,plain,
( select(queue_17,head) = index_210
| seq = head ),
inference(paramod,[status(thm)],[c_5905,c_2748]) ).
cnf(c_14127,plain,
( select(queue_17,head) = index_210
| head = seq ),
inference(copy,[status(thm)],[c_14126]) ).
cnf(c_5931,plain,
select(queue_17,head) = index_210,
inference(resolve,[status(thm)],[c_4,c_14127]) ).
cnf(c_14128,plain,
( select(queue_17,seq) = earray_20
| tail = seq ),
inference(paramod,[status(thm)],[c_123,c_2908]) ).
cnf(c_14129,plain,
( earray_16 = earray_20
| tail = seq ),
inference(paramod,[status(thm)],[c_2747,c_14128]) ).
cnf(c_14130,plain,
( earray_20 = earray_16
| tail = seq ),
inference(copy,[status(thm)],[c_14129]) ).
cnf(c_5936,plain,
earray_20 = earray_16,
inference(resolve,[status(thm)],[c_5,c_14130]) ).
cnf(c_14131,plain,
( select(queue_17,head) = index_26
| tail = head ),
inference(paramod,[status(thm)],[c_5672,c_2908]) ).
cnf(c_14132,plain,
( index_210 = index_26
| tail = head ),
inference(paramod,[status(thm)],[c_5931,c_14131]) ).
cnf(c_14133,plain,
( index_210 = index_26
| head = tail ),
inference(copy,[status(thm)],[c_14132]) ).
cnf(c_14134,plain,
( index_26 = index_210
| head = tail ),
inference(copy,[status(thm)],[c_14133]) ).
cnf(c_5940,plain,
index_26 = index_210,
inference(resolve,[status(thm)],[c_3,c_14134]) ).
cnf(c_5956,plain,
( select(earray_22,A) = select(earray_16,A)
| index_21 = A ),
inference(paramod,[status(thm)],[c_5936,c_639]) ).
cnf(c_6024,plain,
s(index_210) = index_27,
inference(paramod,[status(thm)],[c_5940,c_283]) ).
cnf(c_14135,plain,
( select(queue_25,seq) = earray_29
| head = seq ),
inference(paramod,[status(thm)],[c_133,c_3011]) ).
cnf(c_14136,plain,
( earray_22 = earray_29
| head = seq ),
inference(paramod,[status(thm)],[c_5663,c_14135]) ).
cnf(c_14137,plain,
( earray_29 = earray_22
| head = seq ),
inference(copy,[status(thm)],[c_14136]) ).
cnf(c_6076,plain,
earray_29 = earray_22,
inference(resolve,[status(thm)],[c_4,c_14137]) ).
cnf(c_14138,plain,
( select(queue_25,tail) = index_30
| head = tail ),
inference(paramod,[status(thm)],[c_287,c_3011]) ).
cnf(c_14139,plain,
( index_24 = index_30
| head = tail ),
inference(paramod,[status(thm)],[c_2767,c_14138]) ).
cnf(c_6077,plain,
index_24 = index_30,
inference(resolve,[status(thm)],[c_3,c_14139]) ).
cnf(c_6096,plain,
( select(earray_31,A) = select(earray_22,A)
| index_30 = A ),
inference(paramod,[status(thm)],[c_6076,c_642]) ).
cnf(c_14140,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_6077,c_2976]) ).
cnf(c_14141,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_3065,c_14140]) ).
cnf(c_14142,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_3168,c_14141]) ).
cnf(c_6134,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14142]) ).
cnf(c_14143,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_6077,c_2975]) ).
cnf(c_14144,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_3065,c_14143]) ).
cnf(c_14145,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14144]) ).
cnf(c_6135,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14145]) ).
cnf(c_14146,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_6077,c_2974]) ).
cnf(c_14147,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14146]) ).
cnf(c_14148,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14147]) ).
cnf(c_6136,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_45)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14148]) ).
cnf(c_14149,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2973]) ).
cnf(c_14150,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14149]) ).
cnf(c_14151,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_42)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14150]) ).
cnf(c_6137,plain,
s(s(s(s(s(s(s(s(s(s(s(index_45))))))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14151]) ).
cnf(c_14152,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2972]) ).
cnf(c_14153,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_36)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14152]) ).
cnf(c_14154,plain,
s(s(s(s(s(s(s(s(s(s(s(index_42))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14153]) ).
cnf(c_6138,plain,
s(s(s(s(s(s(s(s(s(s(index_45)))))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14154]) ).
cnf(c_14155,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_30)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2971]) ).
cnf(c_14156,plain,
s(s(s(s(s(s(s(s(s(s(s(index_36))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14155]) ).
cnf(c_14157,plain,
s(s(s(s(s(s(s(s(s(s(index_42)))))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14156]) ).
cnf(c_6139,plain,
s(s(s(s(s(s(s(s(s(index_45))))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14157]) ).
cnf(c_14158,plain,
s(s(s(s(s(s(s(s(s(s(s(index_30))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2970]) ).
cnf(c_14159,plain,
s(s(s(s(s(s(s(s(s(s(index_36)))))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14158]) ).
cnf(c_14160,plain,
s(s(s(s(s(s(s(s(s(index_42))))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14159]) ).
cnf(c_6140,plain,
s(s(s(s(s(s(s(s(index_45)))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14160]) ).
cnf(c_14161,plain,
s(s(s(s(s(s(s(s(s(s(index_30)))))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2969]) ).
cnf(c_14162,plain,
s(s(s(s(s(s(s(s(s(index_36))))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14161]) ).
cnf(c_14163,plain,
s(s(s(s(s(s(s(s(index_42)))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14162]) ).
cnf(c_6141,plain,
s(s(s(s(s(s(s(index_45))))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14163]) ).
cnf(c_14164,plain,
s(s(s(s(s(s(s(s(s(index_30))))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2968]) ).
cnf(c_14165,plain,
s(s(s(s(s(s(s(s(index_36)))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14164]) ).
cnf(c_14166,plain,
s(s(s(s(s(s(s(index_42))))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14165]) ).
cnf(c_6142,plain,
s(s(s(s(s(s(index_45)))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14166]) ).
cnf(c_14167,plain,
s(s(s(s(s(s(s(s(index_30)))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2967]) ).
cnf(c_14168,plain,
s(s(s(s(s(s(s(index_36))))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14167]) ).
cnf(c_14169,plain,
s(s(s(s(s(s(index_42)))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14168]) ).
cnf(c_6143,plain,
s(s(s(s(s(index_45))))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14169]) ).
cnf(c_14170,plain,
s(s(s(s(s(s(s(index_30))))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2966]) ).
cnf(c_14171,plain,
s(s(s(s(s(s(index_36)))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14170]) ).
cnf(c_14172,plain,
s(s(s(s(s(index_42))))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14171]) ).
cnf(c_6144,plain,
s(s(s(s(index_45)))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14172]) ).
cnf(c_14173,plain,
s(s(s(s(s(s(index_30)))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2965]) ).
cnf(c_14174,plain,
s(s(s(s(s(index_36))))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14173]) ).
cnf(c_14175,plain,
s(s(s(s(index_42)))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14174]) ).
cnf(c_6145,plain,
s(s(s(index_45))) != index_15,
inference(paramod,[status(thm)],[c_297,c_14175]) ).
cnf(c_14176,plain,
s(s(s(s(s(index_30))))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2964]) ).
cnf(c_14177,plain,
s(s(s(s(index_36)))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14176]) ).
cnf(c_14178,plain,
s(s(s(index_42))) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14177]) ).
cnf(c_6146,plain,
s(s(index_45)) != index_15,
inference(paramod,[status(thm)],[c_297,c_14178]) ).
cnf(c_14179,plain,
s(s(s(s(index_30)))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2963]) ).
cnf(c_14180,plain,
s(s(s(index_36))) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14179]) ).
cnf(c_14181,plain,
s(s(index_42)) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14180]) ).
cnf(c_6147,plain,
s(index_45) != index_15,
inference(paramod,[status(thm)],[c_297,c_14181]) ).
cnf(c_14182,plain,
s(s(s(index_30))) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2962]) ).
cnf(c_14183,plain,
s(s(index_36)) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14182]) ).
cnf(c_14184,plain,
s(index_42) != index_15,
inference(paramod,[status(thm)],[c_3168,c_14183]) ).
cnf(c_6148,plain,
index_45 != index_15,
inference(paramod,[status(thm)],[c_297,c_14184]) ).
cnf(c_14185,plain,
s(s(index_30)) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2961]) ).
cnf(c_14186,plain,
s(index_36) != index_15,
inference(paramod,[status(thm)],[c_3065,c_14185]) ).
cnf(c_6149,plain,
index_42 != index_15,
inference(paramod,[status(thm)],[c_3168,c_14186]) ).
cnf(c_14187,plain,
s(index_30) != index_15,
inference(paramod,[status(thm)],[c_6077,c_2960]) ).
cnf(c_6150,plain,
index_36 != index_15,
inference(paramod,[status(thm)],[c_3065,c_14187]) ).
cnf(c_6151,plain,
index_30 != index_15,
inference(paramod,[status(thm)],[c_6077,c_2959]) ).
cnf(c_14188,plain,
( select(queue_32,seq) = earray_35
| tail = seq ),
inference(paramod,[status(thm)],[c_137,c_3013]) ).
cnf(c_14189,plain,
( earray_31 = earray_35
| tail = seq ),
inference(paramod,[status(thm)],[c_2769,c_14188]) ).
cnf(c_14190,plain,
( earray_35 = earray_31
| tail = seq ),
inference(copy,[status(thm)],[c_14189]) ).
cnf(c_6257,plain,
earray_35 = earray_31,
inference(resolve,[status(thm)],[c_5,c_14190]) ).
cnf(c_14191,plain,
( select(q13,head) = index_27
| tail = head ),
inference(paramod,[status(thm)],[c_3013,c_5682]) ).
cnf(c_14192,plain,
( select(q13,head) = index_27
| head = tail ),
inference(copy,[status(thm)],[c_14191]) ).
cnf(c_6261,plain,
select(q13,head) = index_27,
inference(resolve,[status(thm)],[c_3,c_14192]) ).
cnf(c_6277,plain,
( select(earray_37,A) = select(earray_31,A)
| index_36 = A ),
inference(paramod,[status(thm)],[c_6257,c_645]) ).
cnf(c_14193,plain,
( select(queue_38,head) = index_27
| seq = head ),
inference(paramod,[status(thm)],[c_6261,c_2772]) ).
cnf(c_14194,plain,
( select(queue_38,head) = index_27
| head = seq ),
inference(copy,[status(thm)],[c_14193]) ).
cnf(c_6287,plain,
select(queue_38,head) = index_27,
inference(resolve,[status(thm)],[c_4,c_14194]) ).
cnf(c_14195,plain,
( select(queue_38,seq) = earray_41
| tail = seq ),
inference(paramod,[status(thm)],[c_143,c_3067]) ).
cnf(c_14196,plain,
( earray_37 = earray_41
| tail = seq ),
inference(paramod,[status(thm)],[c_2771,c_14195]) ).
cnf(c_14197,plain,
( earray_41 = earray_37
| tail = seq ),
inference(copy,[status(thm)],[c_14196]) ).
cnf(c_6292,plain,
earray_41 = earray_37,
inference(resolve,[status(thm)],[c_5,c_14197]) ).
cnf(c_14198,plain,
( select(queue_38,head) = index_47
| tail = head ),
inference(paramod,[status(thm)],[c_5723,c_3067]) ).
cnf(c_14199,plain,
( index_27 = index_47
| tail = head ),
inference(paramod,[status(thm)],[c_6287,c_14198]) ).
cnf(c_14200,plain,
( index_27 = index_47
| head = tail ),
inference(copy,[status(thm)],[c_14199]) ).
cnf(c_14201,plain,
( index_47 = index_27
| head = tail ),
inference(copy,[status(thm)],[c_14200]) ).
cnf(c_6296,plain,
index_47 = index_27,
inference(resolve,[status(thm)],[c_3,c_14201]) ).
cnf(c_6312,plain,
( select(earray_43,A) = select(earray_37,A)
| index_42 = A ),
inference(paramod,[status(thm)],[c_6292,c_650]) ).
cnf(c_6380,plain,
s(index_27) = index_48,
inference(paramod,[status(thm)],[c_6296,c_301]) ).
cnf(c_14202,plain,
( select(queue_46,seq) = earray_50
| head = seq ),
inference(paramod,[status(thm)],[c_147,c_3170]) ).
cnf(c_14203,plain,
( earray_43 = earray_50
| head = seq ),
inference(paramod,[status(thm)],[c_5714,c_14202]) ).
cnf(c_14204,plain,
( earray_50 = earray_43
| head = seq ),
inference(copy,[status(thm)],[c_14203]) ).
cnf(c_6480,plain,
earray_50 = earray_43,
inference(resolve,[status(thm)],[c_4,c_14204]) ).
cnf(c_14205,plain,
( select(queue_46,tail) = index_51
| head = tail ),
inference(paramod,[status(thm)],[c_303,c_3170]) ).
cnf(c_14206,plain,
( index_45 = index_51
| head = tail ),
inference(paramod,[status(thm)],[c_2775,c_14205]) ).
cnf(c_6481,plain,
index_45 = index_51,
inference(resolve,[status(thm)],[c_3,c_14206]) ).
cnf(c_6500,plain,
( select(earray_52,A) = select(earray_43,A)
| index_51 = A ),
inference(paramod,[status(thm)],[c_6480,c_653]) ).
cnf(c_6596,plain,
index_51 != index_15,
inference(paramod,[status(thm)],[c_6481,c_6148]) ).
cnf(c_14207,plain,
s(index_51) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6147]) ).
cnf(c_6597,plain,
index_57 != index_15,
inference(paramod,[status(thm)],[c_3224,c_14207]) ).
cnf(c_14208,plain,
s(s(index_51)) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6146]) ).
cnf(c_14209,plain,
s(index_57) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14208]) ).
cnf(c_6598,plain,
index_63 != index_15,
inference(paramod,[status(thm)],[c_3327,c_14209]) ).
cnf(c_14210,plain,
s(s(s(index_51))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6145]) ).
cnf(c_14211,plain,
s(s(index_57)) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14210]) ).
cnf(c_14212,plain,
s(index_63) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14211]) ).
cnf(c_6599,plain,
index_66 != index_15,
inference(paramod,[status(thm)],[c_315,c_14212]) ).
cnf(c_14213,plain,
s(s(s(s(index_51)))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6144]) ).
cnf(c_14214,plain,
s(s(s(index_57))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14213]) ).
cnf(c_14215,plain,
s(s(index_63)) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14214]) ).
cnf(c_6600,plain,
s(index_66) != index_15,
inference(paramod,[status(thm)],[c_315,c_14215]) ).
cnf(c_14216,plain,
s(s(s(s(s(index_51))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6143]) ).
cnf(c_14217,plain,
s(s(s(s(index_57)))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14216]) ).
cnf(c_14218,plain,
s(s(s(index_63))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14217]) ).
cnf(c_6601,plain,
s(s(index_66)) != index_15,
inference(paramod,[status(thm)],[c_315,c_14218]) ).
cnf(c_14219,plain,
s(s(s(s(s(s(index_51)))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6142]) ).
cnf(c_14220,plain,
s(s(s(s(s(index_57))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14219]) ).
cnf(c_14221,plain,
s(s(s(s(index_63)))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14220]) ).
cnf(c_6602,plain,
s(s(s(index_66))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14221]) ).
cnf(c_14222,plain,
s(s(s(s(s(s(s(index_51))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6141]) ).
cnf(c_14223,plain,
s(s(s(s(s(s(index_57)))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14222]) ).
cnf(c_14224,plain,
s(s(s(s(s(index_63))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14223]) ).
cnf(c_6603,plain,
s(s(s(s(index_66)))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14224]) ).
cnf(c_14225,plain,
s(s(s(s(s(s(s(s(index_51)))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6140]) ).
cnf(c_14226,plain,
s(s(s(s(s(s(s(index_57))))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14225]) ).
cnf(c_14227,plain,
s(s(s(s(s(s(index_63)))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14226]) ).
cnf(c_6604,plain,
s(s(s(s(s(index_66))))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14227]) ).
cnf(c_14228,plain,
s(s(s(s(s(s(s(s(s(index_51))))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6139]) ).
cnf(c_14229,plain,
s(s(s(s(s(s(s(s(index_57)))))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14228]) ).
cnf(c_14230,plain,
s(s(s(s(s(s(s(index_63))))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14229]) ).
cnf(c_6605,plain,
s(s(s(s(s(s(index_66)))))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14230]) ).
cnf(c_14231,plain,
s(s(s(s(s(s(s(s(s(s(index_51)))))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6138]) ).
cnf(c_14232,plain,
s(s(s(s(s(s(s(s(s(index_57))))))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14231]) ).
cnf(c_14233,plain,
s(s(s(s(s(s(s(s(index_63)))))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14232]) ).
cnf(c_6606,plain,
s(s(s(s(s(s(s(index_66))))))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14233]) ).
cnf(c_14234,plain,
s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6137]) ).
cnf(c_14235,plain,
s(s(s(s(s(s(s(s(s(s(index_57)))))))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14234]) ).
cnf(c_14236,plain,
s(s(s(s(s(s(s(s(s(index_63))))))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14235]) ).
cnf(c_6607,plain,
s(s(s(s(s(s(s(s(index_66)))))))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14236]) ).
cnf(c_14237,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6136]) ).
cnf(c_14238,plain,
s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14237]) ).
cnf(c_14239,plain,
s(s(s(s(s(s(s(s(s(s(index_63)))))))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14238]) ).
cnf(c_6608,plain,
s(s(s(s(s(s(s(s(s(index_66))))))))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14239]) ).
cnf(c_14240,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_51))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6135]) ).
cnf(c_14241,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_57)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14240]) ).
cnf(c_14242,plain,
s(s(s(s(s(s(s(s(s(s(s(index_63))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14241]) ).
cnf(c_6609,plain,
s(s(s(s(s(s(s(s(s(s(index_66)))))))))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14242]) ).
cnf(c_14243,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_51)))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_6481,c_6134]) ).
cnf(c_14244,plain,
s(s(s(s(s(s(s(s(s(s(s(s(s(index_57))))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3224,c_14243]) ).
cnf(c_14245,plain,
s(s(s(s(s(s(s(s(s(s(s(s(index_63)))))))))))) != index_15,
inference(paramod,[status(thm)],[c_3327,c_14244]) ).
cnf(c_6610,plain,
s(s(s(s(s(s(s(s(s(s(s(index_66))))))))))) != index_15,
inference(paramod,[status(thm)],[c_315,c_14245]) ).
cnf(c_14246,plain,
( select(queue_53,seq) = earray_56
| tail = seq ),
inference(paramod,[status(thm)],[c_151,c_3172]) ).
cnf(c_14247,plain,
( earray_52 = earray_56
| tail = seq ),
inference(paramod,[status(thm)],[c_2779,c_14246]) ).
cnf(c_14248,plain,
( earray_56 = earray_52
| tail = seq ),
inference(copy,[status(thm)],[c_14247]) ).
cnf(c_6799,plain,
earray_56 = earray_52,
inference(resolve,[status(thm)],[c_5,c_14248]) ).
cnf(c_14249,plain,
( select(q16,head) = index_48
| tail = head ),
inference(paramod,[status(thm)],[c_3172,c_5746]) ).
cnf(c_14250,plain,
( select(q16,head) = index_48
| head = tail ),
inference(copy,[status(thm)],[c_14249]) ).
cnf(c_6803,plain,
select(q16,head) = index_48,
inference(resolve,[status(thm)],[c_3,c_14250]) ).
cnf(c_6819,plain,
( select(earray_58,A) = select(earray_52,A)
| index_57 = A ),
inference(paramod,[status(thm)],[c_6799,c_656]) ).
cnf(c_14251,plain,
( select(queue_59,head) = index_48
| seq = head ),
inference(paramod,[status(thm)],[c_6803,c_2782]) ).
cnf(c_14252,plain,
( select(queue_59,head) = index_48
| head = seq ),
inference(copy,[status(thm)],[c_14251]) ).
cnf(c_6829,plain,
select(queue_59,head) = index_48,
inference(resolve,[status(thm)],[c_4,c_14252]) ).
cnf(c_14253,plain,
( select(queue_59,seq) = earray_62
| tail = seq ),
inference(paramod,[status(thm)],[c_155,c_3226]) ).
cnf(c_14254,plain,
( earray_58 = earray_62
| tail = seq ),
inference(paramod,[status(thm)],[c_2781,c_14253]) ).
cnf(c_14255,plain,
( earray_62 = earray_58
| tail = seq ),
inference(copy,[status(thm)],[c_14254]) ).
cnf(c_6834,plain,
earray_62 = earray_58,
inference(resolve,[status(thm)],[c_5,c_14255]) ).
cnf(c_14256,plain,
( select(queue_59,head) = index_68
| tail = head ),
inference(paramod,[status(thm)],[c_5787,c_3226]) ).
cnf(c_14257,plain,
( index_48 = index_68
| tail = head ),
inference(paramod,[status(thm)],[c_6829,c_14256]) ).
cnf(c_14258,plain,
( index_48 = index_68
| head = tail ),
inference(copy,[status(thm)],[c_14257]) ).
cnf(c_14259,plain,
( index_68 = index_48
| head = tail ),
inference(copy,[status(thm)],[c_14258]) ).
cnf(c_6838,plain,
index_68 = index_48,
inference(resolve,[status(thm)],[c_3,c_14259]) ).
cnf(c_6854,plain,
( select(earray_64,A) = select(earray_58,A)
| index_63 = A ),
inference(paramod,[status(thm)],[c_6834,c_659]) ).
cnf(c_6922,plain,
s(index_48) = index_69,
inference(paramod,[status(thm)],[c_6838,c_319]) ).
cnf(c_14260,plain,
( select(queue_67,seq) = earray_71
| head = seq ),
inference(paramod,[status(thm)],[c_159,c_3329]) ).
cnf(c_14261,plain,
( earray_64 = earray_71
| head = seq ),
inference(paramod,[status(thm)],[c_5778,c_14260]) ).
cnf(c_14262,plain,
( earray_71 = earray_64
| head = seq ),
inference(copy,[status(thm)],[c_14261]) ).
cnf(c_7069,plain,
earray_71 = earray_64,
inference(resolve,[status(thm)],[c_4,c_14262]) ).
cnf(c_14263,plain,
( select(queue_67,tail) = index_72
| head = tail ),
inference(paramod,[status(thm)],[c_321,c_3329]) ).
cnf(c_14264,plain,
( index_66 = index_72
| head = tail ),
inference(paramod,[status(thm)],[c_2785,c_14263]) ).
cnf(c_7070,plain,
index_66 = index_72,
inference(resolve,[status(thm)],[c_3,c_14264]) ).
cnf(c_7089,plain,
( select(earray_73,A) = select(earray_64,A)
| index_72 = A ),
inference(paramod,[status(thm)],[c_7069,c_662]) ).
cnf(c_14265,plain,
s(s(s(s(s(s(s(s(s(s(s(index_72))))))))))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6610]) ).
cnf(c_14266,plain,
s(s(s(s(s(s(s(s(s(s(index_84)))))))))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14265]) ).
cnf(c_14267,plain,
s(s(s(s(s(s(s(s(s(index_90))))))))) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14266]) ).
cnf(c_7262,plain,
s(s(s(s(s(s(s(s(index_93)))))))) != index_15,
inference(paramod,[status(thm)],[c_337,c_14267]) ).
cnf(c_14268,plain,
s(s(s(s(s(s(s(s(s(s(index_72)))))))))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6609]) ).
cnf(c_14269,plain,
s(s(s(s(s(s(s(s(s(index_84))))))))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14268]) ).
cnf(c_14270,plain,
s(s(s(s(s(s(s(s(index_90)))))))) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14269]) ).
cnf(c_7263,plain,
s(s(s(s(s(s(s(index_93))))))) != index_15,
inference(paramod,[status(thm)],[c_337,c_14270]) ).
cnf(c_14271,plain,
s(s(s(s(s(s(s(s(s(index_72))))))))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6608]) ).
cnf(c_14272,plain,
s(s(s(s(s(s(s(s(index_84)))))))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14271]) ).
cnf(c_14273,plain,
s(s(s(s(s(s(s(index_90))))))) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14272]) ).
cnf(c_7264,plain,
s(s(s(s(s(s(index_93)))))) != index_15,
inference(paramod,[status(thm)],[c_337,c_14273]) ).
cnf(c_14274,plain,
s(s(s(s(s(s(s(s(index_72)))))))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6607]) ).
cnf(c_14275,plain,
s(s(s(s(s(s(s(index_84))))))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14274]) ).
cnf(c_14276,plain,
s(s(s(s(s(s(index_90)))))) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14275]) ).
cnf(c_7265,plain,
s(s(s(s(s(index_93))))) != index_15,
inference(paramod,[status(thm)],[c_337,c_14276]) ).
cnf(c_14277,plain,
s(s(s(s(s(s(s(index_72))))))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6606]) ).
cnf(c_14278,plain,
s(s(s(s(s(s(index_84)))))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14277]) ).
cnf(c_14279,plain,
s(s(s(s(s(index_90))))) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14278]) ).
cnf(c_7266,plain,
s(s(s(s(index_93)))) != index_15,
inference(paramod,[status(thm)],[c_337,c_14279]) ).
cnf(c_14280,plain,
s(s(s(s(s(s(index_72)))))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6605]) ).
cnf(c_14281,plain,
s(s(s(s(s(index_84))))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14280]) ).
cnf(c_14282,plain,
s(s(s(s(index_90)))) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14281]) ).
cnf(c_7267,plain,
s(s(s(index_93))) != index_15,
inference(paramod,[status(thm)],[c_337,c_14282]) ).
cnf(c_14283,plain,
s(s(s(s(s(index_72))))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6604]) ).
cnf(c_14284,plain,
s(s(s(s(index_84)))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14283]) ).
cnf(c_14285,plain,
s(s(s(index_90))) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14284]) ).
cnf(c_7268,plain,
s(s(index_93)) != index_15,
inference(paramod,[status(thm)],[c_337,c_14285]) ).
cnf(c_14286,plain,
s(s(s(s(index_72)))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6603]) ).
cnf(c_14287,plain,
s(s(s(index_84))) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14286]) ).
cnf(c_14288,plain,
s(s(index_90)) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14287]) ).
cnf(c_7269,plain,
s(index_93) != index_15,
inference(paramod,[status(thm)],[c_337,c_14288]) ).
cnf(c_14289,plain,
s(s(s(index_72))) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6602]) ).
cnf(c_14290,plain,
s(s(index_84)) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14289]) ).
cnf(c_14291,plain,
s(index_90) != index_15,
inference(paramod,[status(thm)],[c_3589,c_14290]) ).
cnf(c_7270,plain,
index_93 != index_15,
inference(paramod,[status(thm)],[c_337,c_14291]) ).
cnf(c_14292,plain,
s(s(index_72)) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6601]) ).
cnf(c_14293,plain,
s(index_84) != index_15,
inference(paramod,[status(thm)],[c_3383,c_14292]) ).
cnf(c_7271,plain,
index_90 != index_15,
inference(paramod,[status(thm)],[c_3589,c_14293]) ).
cnf(c_14294,plain,
s(index_72) != index_15,
inference(paramod,[status(thm)],[c_7070,c_6600]) ).
cnf(c_7272,plain,
index_84 != index_15,
inference(paramod,[status(thm)],[c_3383,c_14294]) ).
cnf(c_7273,plain,
index_72 != index_15,
inference(paramod,[status(thm)],[c_7070,c_6599]) ).
cnf(c_14295,plain,
( select(queue_74,seq) = earray_83
| tail = seq ),
inference(paramod,[status(thm)],[c_169,c_3331]) ).
cnf(c_14296,plain,
( earray_73 = earray_83
| tail = seq ),
inference(paramod,[status(thm)],[c_2787,c_14295]) ).
cnf(c_14297,plain,
( earray_83 = earray_73
| tail = seq ),
inference(copy,[status(thm)],[c_14296]) ).
cnf(c_7517,plain,
earray_83 = earray_73,
inference(resolve,[status(thm)],[c_5,c_14297]) ).
cnf(c_14298,plain,
( select(q19,head) = index_69
| tail = head ),
inference(paramod,[status(thm)],[c_3331,c_5797]) ).
cnf(c_14299,plain,
( select(q19,head) = index_69
| head = tail ),
inference(copy,[status(thm)],[c_14298]) ).
cnf(c_7521,plain,
select(q19,head) = index_69,
inference(resolve,[status(thm)],[c_3,c_14299]) ).
cnf(c_7537,plain,
( select(earray_85,A) = select(earray_73,A)
| index_84 = A ),
inference(paramod,[status(thm)],[c_7517,c_669]) ).
cnf(c_14300,plain,
( select(queue_86,head) = index_69
| seq = head ),
inference(paramod,[status(thm)],[c_7521,c_2792]) ).
cnf(c_14301,plain,
( select(queue_86,head) = index_69
| head = seq ),
inference(copy,[status(thm)],[c_14300]) ).
cnf(c_7547,plain,
select(queue_86,head) = index_69,
inference(resolve,[status(thm)],[c_4,c_14301]) ).
cnf(c_14302,plain,
( select(queue_80,head) = index_158
| tail = head ),
inference(paramod,[status(thm)],[c_5448,c_3385]) ).
cnf(c_14303,plain,
( index_3 = index_158
| tail = head ),
inference(paramod,[status(thm)],[c_5896,c_14302]) ).
cnf(c_14304,plain,
( index_3 = index_158
| head = tail ),
inference(copy,[status(thm)],[c_14303]) ).
cnf(c_14305,plain,
( index_158 = index_3
| head = tail ),
inference(copy,[status(thm)],[c_14304]) ).
cnf(c_7555,plain,
index_158 = index_3,
inference(resolve,[status(thm)],[c_3,c_14305]) ).
cnf(c_14306,plain,
s(index_3) = index_159,
inference(paramod,[status(thm)],[c_7555,c_231]) ).
cnf(c_14307,plain,
index_78 = index_159,
inference(paramod,[status(thm)],[c_2852,c_14306]) ).
cnf(c_7640,plain,
index_159 = index_78,
inference(copy,[status(thm)],[c_14307]) ).
cnf(c_7645,plain,
select(queue_173,head) = index_78,
inference(paramod,[status(thm)],[c_7640,c_5511]) ).
cnf(c_14308,plain,
( select(queue_86,seq) = earray_89
| tail = seq ),
inference(paramod,[status(thm)],[c_173,c_3488]) ).
cnf(c_14309,plain,
( earray_85 = earray_89
| tail = seq ),
inference(paramod,[status(thm)],[c_2791,c_14308]) ).
cnf(c_14310,plain,
( earray_89 = earray_85
| tail = seq ),
inference(copy,[status(thm)],[c_14309]) ).
cnf(c_7656,plain,
earray_89 = earray_85,
inference(resolve,[status(thm)],[c_5,c_14310]) ).
cnf(c_14311,plain,
( select(queue_86,head) = index_95
| tail = head ),
inference(paramod,[status(thm)],[c_5847,c_3488]) ).
cnf(c_14312,plain,
( index_69 = index_95
| tail = head ),
inference(paramod,[status(thm)],[c_7547,c_14311]) ).
cnf(c_14313,plain,
( index_69 = index_95
| head = tail ),
inference(copy,[status(thm)],[c_14312]) ).
cnf(c_14314,plain,
( index_95 = index_69
| head = tail ),
inference(copy,[status(thm)],[c_14313]) ).
cnf(c_7660,plain,
index_95 = index_69,
inference(resolve,[status(thm)],[c_3,c_14314]) ).
cnf(c_7676,plain,
( select(earray_91,A) = select(earray_85,A)
| index_90 = A ),
inference(paramod,[status(thm)],[c_7656,c_672]) ).
cnf(c_7744,plain,
s(index_69) = index_96,
inference(paramod,[status(thm)],[c_7660,c_341]) ).
cnf(c_14315,plain,
( select(queue_94,seq) = earray_98
| head = seq ),
inference(paramod,[status(thm)],[c_177,c_3591]) ).
cnf(c_14316,plain,
( earray_91 = earray_98
| head = seq ),
inference(paramod,[status(thm)],[c_5838,c_14315]) ).
cnf(c_14317,plain,
( earray_98 = earray_91
| head = seq ),
inference(copy,[status(thm)],[c_14316]) ).
cnf(c_7937,plain,
earray_98 = earray_91,
inference(resolve,[status(thm)],[c_4,c_14317]) ).
cnf(c_14318,plain,
( select(queue_94,tail) = index_99
| head = tail ),
inference(paramod,[status(thm)],[c_343,c_3591]) ).
cnf(c_14319,plain,
( index_93 = index_99
| head = tail ),
inference(paramod,[status(thm)],[c_2795,c_14318]) ).
cnf(c_7938,plain,
index_93 = index_99,
inference(resolve,[status(thm)],[c_3,c_14319]) ).
cnf(c_7960,plain,
( select(earray_91,A) = select(earray_100,A)
| index_99 = A ),
inference(paramod,[status(thm)],[c_7937,c_586]) ).
cnf(c_8181,plain,
index_99 != index_15,
inference(paramod,[status(thm)],[c_7938,c_7270]) ).
cnf(c_14320,plain,
s(index_99) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7269]) ).
cnf(c_14321,plain,
index_105 != index_15,
inference(paramod,[status(thm)],[c_3645,c_14320]) ).
cnf(c_8182,plain,
index_15 != index_105,
inference(copy,[status(thm)],[c_14321]) ).
cnf(c_14322,plain,
s(s(index_99)) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7268]) ).
cnf(c_14323,plain,
s(index_105) != index_15,
inference(paramod,[status(thm)],[c_3645,c_14322]) ).
cnf(c_14324,plain,
index_111 != index_15,
inference(paramod,[status(thm)],[c_3748,c_14323]) ).
cnf(c_8183,plain,
index_15 != index_111,
inference(copy,[status(thm)],[c_14324]) ).
cnf(c_14325,plain,
s(s(s(index_99))) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7267]) ).
cnf(c_14326,plain,
s(s(index_105)) != index_15,
inference(paramod,[status(thm)],[c_3645,c_14325]) ).
cnf(c_14327,plain,
s(index_111) != index_15,
inference(paramod,[status(thm)],[c_3748,c_14326]) ).
cnf(c_8184,plain,
index_114 != index_15,
inference(paramod,[status(thm)],[c_191,c_14327]) ).
cnf(c_14328,plain,
s(s(s(s(index_99)))) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7266]) ).
cnf(c_14329,plain,
s(s(s(index_105))) != index_15,
inference(paramod,[status(thm)],[c_3645,c_14328]) ).
cnf(c_14330,plain,
s(s(index_111)) != index_15,
inference(paramod,[status(thm)],[c_3748,c_14329]) ).
cnf(c_8185,plain,
s(index_114) != index_15,
inference(paramod,[status(thm)],[c_191,c_14330]) ).
cnf(c_14331,plain,
s(s(s(s(s(index_99))))) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7265]) ).
cnf(c_14332,plain,
s(s(s(s(index_105)))) != index_15,
inference(paramod,[status(thm)],[c_3645,c_14331]) ).
cnf(c_14333,plain,
s(s(s(index_111))) != index_15,
inference(paramod,[status(thm)],[c_3748,c_14332]) ).
cnf(c_8186,plain,
s(s(index_114)) != index_15,
inference(paramod,[status(thm)],[c_191,c_14333]) ).
cnf(c_14334,plain,
s(s(s(s(s(s(index_99)))))) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7264]) ).
cnf(c_14335,plain,
s(s(s(s(s(index_105))))) != index_15,
inference(paramod,[status(thm)],[c_3645,c_14334]) ).
cnf(c_14336,plain,
s(s(s(s(index_111)))) != index_15,
inference(paramod,[status(thm)],[c_3748,c_14335]) ).
cnf(c_8187,plain,
s(s(s(index_114))) != index_15,
inference(paramod,[status(thm)],[c_191,c_14336]) ).
cnf(c_14337,plain,
s(s(s(s(s(s(s(index_99))))))) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7263]) ).
cnf(c_14338,plain,
s(s(s(s(s(s(index_105)))))) != index_15,
inference(paramod,[status(thm)],[c_3645,c_14337]) ).
cnf(c_14339,plain,
s(s(s(s(s(index_111))))) != index_15,
inference(paramod,[status(thm)],[c_3748,c_14338]) ).
cnf(c_8188,plain,
s(s(s(s(index_114)))) != index_15,
inference(paramod,[status(thm)],[c_191,c_14339]) ).
cnf(c_14340,plain,
s(s(s(s(s(s(s(s(index_99)))))))) != index_15,
inference(paramod,[status(thm)],[c_7938,c_7262]) ).
cnf(c_14341,plain,
s(s(s(s(s(s(s(index_105))))))) != index_15,
inference(paramod,[status(thm)],[c_3645,c_14340]) ).
cnf(c_14342,plain,
s(s(s(s(s(s(index_111)))))) != index_15,
inference(paramod,[status(thm)],[c_3748,c_14341]) ).
cnf(c_8189,plain,
s(s(s(s(s(index_114))))) != index_15,
inference(paramod,[status(thm)],[c_191,c_14342]) ).
cnf(c_14343,plain,
( select(queue_101,seq) = earray_104
| tail = seq ),
inference(paramod,[status(thm)],[c_61,c_3593]) ).
cnf(c_14344,plain,
( earray_100 = earray_104
| tail = seq ),
inference(paramod,[status(thm)],[c_2717,c_14343]) ).
cnf(c_14345,plain,
( earray_104 = earray_100
| tail = seq ),
inference(copy,[status(thm)],[c_14344]) ).
cnf(c_8507,plain,
earray_104 = earray_100,
inference(resolve,[status(thm)],[c_5,c_14345]) ).
cnf(c_14346,plain,
( select(q22,head) = index_96
| tail = head ),
inference(paramod,[status(thm)],[c_3593,c_5252]) ).
cnf(c_14347,plain,
( select(q22,head) = index_96
| head = tail ),
inference(copy,[status(thm)],[c_14346]) ).
cnf(c_8511,plain,
select(q22,head) = index_96,
inference(resolve,[status(thm)],[c_3,c_14347]) ).
cnf(c_8527,plain,
( select(earray_106,A) = select(earray_100,A)
| index_105 = A ),
inference(paramod,[status(thm)],[c_8507,c_589]) ).
cnf(c_14348,plain,
( select(queue_107,head) = index_96
| seq = head ),
inference(paramod,[status(thm)],[c_8511,c_2720]) ).
cnf(c_14349,plain,
( select(queue_107,head) = index_96
| head = seq ),
inference(copy,[status(thm)],[c_14348]) ).
cnf(c_8537,plain,
select(queue_107,head) = index_96,
inference(resolve,[status(thm)],[c_4,c_14349]) ).
cnf(c_14350,plain,
( select(queue_107,seq) = earray_110
| tail = seq ),
inference(paramod,[status(thm)],[c_65,c_3647]) ).
cnf(c_14351,plain,
( earray_106 = earray_110
| tail = seq ),
inference(paramod,[status(thm)],[c_2719,c_14350]) ).
cnf(c_14352,plain,
( earray_110 = earray_106
| tail = seq ),
inference(copy,[status(thm)],[c_14351]) ).
cnf(c_8542,plain,
earray_110 = earray_106,
inference(resolve,[status(thm)],[c_5,c_14352]) ).
cnf(c_14353,plain,
( select(queue_107,head) = index_116
| tail = head ),
inference(paramod,[status(thm)],[c_5321,c_3647]) ).
cnf(c_14354,plain,
( index_96 = index_116
| tail = head ),
inference(paramod,[status(thm)],[c_8537,c_14353]) ).
cnf(c_14355,plain,
( index_96 = index_116
| head = tail ),
inference(copy,[status(thm)],[c_14354]) ).
cnf(c_8546,plain,
index_96 = index_116,
inference(resolve,[status(thm)],[c_3,c_14355]) ).
cnf(c_8562,plain,
( select(earray_112,A) = select(earray_106,A)
| index_111 = A ),
inference(paramod,[status(thm)],[c_8542,c_592]) ).
cnf(c_8767,plain,
s(index_69) = index_116,
inference(paramod,[status(thm)],[c_8546,c_7744]) ).
cnf(c_14356,plain,
( select(queue_115,seq) = earray_119
| head = seq ),
inference(paramod,[status(thm)],[c_69,c_3750]) ).
cnf(c_14357,plain,
( earray_112 = earray_119
| head = seq ),
inference(paramod,[status(thm)],[c_5312,c_14356]) ).
cnf(c_14358,plain,
( earray_119 = earray_112
| head = seq ),
inference(copy,[status(thm)],[c_14357]) ).
cnf(c_8833,plain,
earray_119 = earray_112,
inference(resolve,[status(thm)],[c_4,c_14358]) ).
cnf(c_14359,plain,
( select(queue_115,tail) = index_120
| head = tail ),
inference(paramod,[status(thm)],[c_199,c_3750]) ).
cnf(c_14360,plain,
( index_114 = index_120
| head = tail ),
inference(paramod,[status(thm)],[c_2725,c_14359]) ).
cnf(c_8834,plain,
index_114 = index_120,
inference(resolve,[status(thm)],[c_3,c_14360]) ).
cnf(c_8853,plain,
( select(earray_121,A) = select(earray_112,A)
| index_120 = A ),
inference(paramod,[status(thm)],[c_8833,c_595]) ).
cnf(c_14361,plain,
s(s(s(s(s(index_120))))) != index_15,
inference(paramod,[status(thm)],[c_8834,c_8189]) ).
cnf(c_14362,plain,
s(s(s(s(index_126)))) != index_15,
inference(paramod,[status(thm)],[c_3804,c_14361]) ).
cnf(c_14363,plain,
s(s(s(index_132))) != index_15,
inference(paramod,[status(thm)],[c_3907,c_14362]) ).
cnf(c_9146,plain,
s(s(index_135)) != index_15,
inference(paramod,[status(thm)],[c_209,c_14363]) ).
cnf(c_14364,plain,
s(s(s(s(index_120)))) != index_15,
inference(paramod,[status(thm)],[c_8834,c_8188]) ).
cnf(c_14365,plain,
s(s(s(index_126))) != index_15,
inference(paramod,[status(thm)],[c_3804,c_14364]) ).
cnf(c_14366,plain,
s(s(index_132)) != index_15,
inference(paramod,[status(thm)],[c_3907,c_14365]) ).
cnf(c_9147,plain,
s(index_135) != index_15,
inference(paramod,[status(thm)],[c_209,c_14366]) ).
cnf(c_14367,plain,
s(s(s(index_120))) != index_15,
inference(paramod,[status(thm)],[c_8834,c_8187]) ).
cnf(c_14368,plain,
s(s(index_126)) != index_15,
inference(paramod,[status(thm)],[c_3804,c_14367]) ).
cnf(c_14369,plain,
s(index_132) != index_15,
inference(paramod,[status(thm)],[c_3907,c_14368]) ).
cnf(c_9148,plain,
index_135 != index_15,
inference(paramod,[status(thm)],[c_209,c_14369]) ).
cnf(c_14370,plain,
s(s(index_120)) != index_15,
inference(paramod,[status(thm)],[c_8834,c_8186]) ).
cnf(c_14371,plain,
s(index_126) != index_15,
inference(paramod,[status(thm)],[c_3804,c_14370]) ).
cnf(c_14372,plain,
index_132 != index_15,
inference(paramod,[status(thm)],[c_3907,c_14371]) ).
cnf(c_9149,plain,
index_15 != index_132,
inference(copy,[status(thm)],[c_14372]) ).
cnf(c_14373,plain,
s(index_120) != index_15,
inference(paramod,[status(thm)],[c_8834,c_8185]) ).
cnf(c_14374,plain,
index_126 != index_15,
inference(paramod,[status(thm)],[c_3804,c_14373]) ).
cnf(c_9150,plain,
index_15 != index_126,
inference(copy,[status(thm)],[c_14374]) ).
cnf(c_14375,plain,
index_120 != index_15,
inference(paramod,[status(thm)],[c_8834,c_8184]) ).
cnf(c_9151,plain,
index_15 != index_120,
inference(copy,[status(thm)],[c_14375]) ).
cnf(c_14376,plain,
( select(queue_122,seq) = earray_125
| tail = seq ),
inference(paramod,[status(thm)],[c_73,c_3752]) ).
cnf(c_14377,plain,
( earray_121 = earray_125
| tail = seq ),
inference(paramod,[status(thm)],[c_2727,c_14376]) ).
cnf(c_14378,plain,
( earray_125 = earray_121
| tail = seq ),
inference(copy,[status(thm)],[c_14377]) ).
cnf(c_9512,plain,
earray_125 = earray_121,
inference(resolve,[status(thm)],[c_5,c_14378]) ).
cnf(c_14379,plain,
( select(q25,head) = index_117
| tail = head ),
inference(paramod,[status(thm)],[c_3752,c_5336]) ).
cnf(c_14380,plain,
( select(q25,head) = index_117
| head = tail ),
inference(copy,[status(thm)],[c_14379]) ).
cnf(c_9516,plain,
select(q25,head) = index_117,
inference(resolve,[status(thm)],[c_3,c_14380]) ).
cnf(c_9532,plain,
( select(earray_127,A) = select(earray_121,A)
| index_126 = A ),
inference(paramod,[status(thm)],[c_9512,c_598]) ).
cnf(c_14381,plain,
( select(queue_128,head) = index_117
| seq = head ),
inference(paramod,[status(thm)],[c_9516,c_2730]) ).
cnf(c_14382,plain,
( select(queue_128,head) = index_117
| head = seq ),
inference(copy,[status(thm)],[c_14381]) ).
cnf(c_9542,plain,
select(queue_128,head) = index_117,
inference(resolve,[status(thm)],[c_4,c_14382]) ).
cnf(c_14383,plain,
( select(queue_128,seq) = earray_131
| tail = seq ),
inference(paramod,[status(thm)],[c_77,c_3806]) ).
cnf(c_14384,plain,
( earray_127 = earray_131
| tail = seq ),
inference(paramod,[status(thm)],[c_2729,c_14383]) ).
cnf(c_14385,plain,
( earray_131 = earray_127
| tail = seq ),
inference(copy,[status(thm)],[c_14384]) ).
cnf(c_9547,plain,
earray_131 = earray_127,
inference(resolve,[status(thm)],[c_5,c_14385]) ).
cnf(c_14386,plain,
( select(queue_128,head) = index_137
| tail = head ),
inference(paramod,[status(thm)],[c_5387,c_3806]) ).
cnf(c_14387,plain,
( index_117 = index_137
| tail = head ),
inference(paramod,[status(thm)],[c_9542,c_14386]) ).
cnf(c_14388,plain,
( index_117 = index_137
| head = tail ),
inference(copy,[status(thm)],[c_14387]) ).
cnf(c_14389,plain,
( index_137 = index_117
| head = tail ),
inference(copy,[status(thm)],[c_14388]) ).
cnf(c_9551,plain,
index_137 = index_117,
inference(resolve,[status(thm)],[c_3,c_14389]) ).
cnf(c_9567,plain,
( select(earray_133,A) = select(earray_127,A)
| index_132 = A ),
inference(paramod,[status(thm)],[c_9547,c_601]) ).
cnf(c_9635,plain,
s(index_117) = index_138,
inference(paramod,[status(thm)],[c_9551,c_213]) ).
cnf(c_14390,plain,
( select(queue_136,seq) = earray_140
| head = seq ),
inference(paramod,[status(thm)],[c_83,c_3909]) ).
cnf(c_14391,plain,
( earray_133 = earray_140
| head = seq ),
inference(paramod,[status(thm)],[c_5373,c_14390]) ).
cnf(c_14392,plain,
( earray_140 = earray_133
| head = seq ),
inference(copy,[status(thm)],[c_14391]) ).
cnf(c_9927,plain,
earray_140 = earray_133,
inference(resolve,[status(thm)],[c_4,c_14392]) ).
cnf(c_14393,plain,
( select(queue_136,tail) = index_141
| head = tail ),
inference(paramod,[status(thm)],[c_215,c_3909]) ).
cnf(c_14394,plain,
( index_135 = index_141
| head = tail ),
inference(paramod,[status(thm)],[c_2733,c_14393]) ).
cnf(c_9928,plain,
index_135 = index_141,
inference(resolve,[status(thm)],[c_3,c_14394]) ).
cnf(c_9947,plain,
( select(earray_142,A) = select(earray_133,A)
| index_141 = A ),
inference(paramod,[status(thm)],[c_9927,c_605]) ).
cnf(c_14395,plain,
index_141 != index_15,
inference(paramod,[status(thm)],[c_9928,c_9148]) ).
cnf(c_10277,plain,
index_15 != index_141,
inference(copy,[status(thm)],[c_14395]) ).
cnf(c_14396,plain,
s(index_141) != index_15,
inference(paramod,[status(thm)],[c_9928,c_9147]) ).
cnf(c_14397,plain,
index_147 != index_15,
inference(paramod,[status(thm)],[c_3963,c_14396]) ).
cnf(c_10278,plain,
index_15 != index_147,
inference(copy,[status(thm)],[c_14397]) ).
cnf(c_14398,plain,
s(s(index_141)) != index_15,
inference(paramod,[status(thm)],[c_9928,c_9146]) ).
cnf(c_14399,plain,
s(index_147) != index_15,
inference(paramod,[status(thm)],[c_3963,c_14398]) ).
cnf(c_10279,plain,
index_162 != index_15,
inference(paramod,[status(thm)],[c_4066,c_14399]) ).
cnf(c_14400,plain,
( select(queue_143,seq) = earray_146
| tail = seq ),
inference(paramod,[status(thm)],[c_87,c_3911]) ).
cnf(c_14401,plain,
( earray_142 = earray_146
| tail = seq ),
inference(paramod,[status(thm)],[c_2735,c_14400]) ).
cnf(c_14402,plain,
( earray_146 = earray_142
| tail = seq ),
inference(copy,[status(thm)],[c_14401]) ).
cnf(c_10718,plain,
earray_146 = earray_142,
inference(resolve,[status(thm)],[c_5,c_14402]) ).
cnf(c_14403,plain,
( select(q28,head) = index_138
| tail = head ),
inference(paramod,[status(thm)],[c_3911,c_5397]) ).
cnf(c_14404,plain,
( select(q28,head) = index_138
| head = tail ),
inference(copy,[status(thm)],[c_14403]) ).
cnf(c_10722,plain,
select(q28,head) = index_138,
inference(resolve,[status(thm)],[c_3,c_14404]) ).
cnf(c_10738,plain,
( select(earray_148,A) = select(earray_142,A)
| index_147 = A ),
inference(paramod,[status(thm)],[c_10718,c_608]) ).
cnf(c_14405,plain,
( select(queue_149,head) = index_138
| seq = head ),
inference(paramod,[status(thm)],[c_10722,c_2738]) ).
cnf(c_14406,plain,
( select(queue_149,head) = index_138
| head = seq ),
inference(copy,[status(thm)],[c_14405]) ).
cnf(c_10753,plain,
select(queue_149,head) = index_138,
inference(resolve,[status(thm)],[c_4,c_14406]) ).
cnf(c_14407,plain,
( select(queue_149,seq) = earray_161
| tail = seq ),
inference(paramod,[status(thm)],[c_97,c_3965]) ).
cnf(c_14408,plain,
( earray_148 = earray_161
| tail = seq ),
inference(paramod,[status(thm)],[c_2737,c_14407]) ).
cnf(c_14409,plain,
( earray_161 = earray_148
| tail = seq ),
inference(copy,[status(thm)],[c_14408]) ).
cnf(c_10763,plain,
earray_161 = earray_148,
inference(resolve,[status(thm)],[c_5,c_14409]) ).
cnf(c_14410,plain,
( select(queue_149,head) = index_167
| tail = head ),
inference(paramod,[status(thm)],[c_5487,c_3965]) ).
cnf(c_14411,plain,
( index_138 = index_167
| tail = head ),
inference(paramod,[status(thm)],[c_10753,c_14410]) ).
cnf(c_14412,plain,
( index_138 = index_167
| head = tail ),
inference(copy,[status(thm)],[c_14411]) ).
cnf(c_14413,plain,
( index_167 = index_138
| head = tail ),
inference(copy,[status(thm)],[c_14412]) ).
cnf(c_10767,plain,
index_167 = index_138,
inference(resolve,[status(thm)],[c_3,c_14413]) ).
cnf(c_10783,plain,
( select(earray_163,A) = select(earray_148,A)
| index_162 = A ),
inference(paramod,[status(thm)],[c_10763,c_616]) ).
cnf(c_10851,plain,
s(index_138) = index_168,
inference(paramod,[status(thm)],[c_10767,c_239]) ).
cnf(c_14414,plain,
( select(queue_157,tail) = index_171
| head = tail ),
inference(paramod,[status(thm)],[c_241,c_4068]) ).
cnf(c_14415,plain,
( index_156 = index_171
| head = tail ),
inference(paramod,[status(thm)],[c_2741,c_14414]) ).
cnf(c_11182,plain,
index_156 = index_171,
inference(resolve,[status(thm)],[c_3,c_14415]) ).
cnf(c_11357,plain,
s(index_153) = index_171,
inference(paramod,[status(thm)],[c_11182,c_227]) ).
cnf(c_14416,plain,
( select(queue_166,seq) = earray_212
| head = seq ),
inference(paramod,[status(thm)],[c_129,c_4070]) ).
cnf(c_14417,plain,
( earray_163 = earray_212
| head = seq ),
inference(paramod,[status(thm)],[c_5478,c_14416]) ).
cnf(c_14418,plain,
( earray_212 = earray_163
| head = seq ),
inference(copy,[status(thm)],[c_14417]) ).
cnf(c_11367,plain,
earray_212 = earray_163,
inference(resolve,[status(thm)],[c_4,c_14418]) ).
cnf(c_11382,plain,
select(earray_163,index_168) = elem_214,
inference(paramod,[status(thm)],[c_11367,c_4074]) ).
cnf(c_14419,plain,
( select(q4,head) = index_78
| tail = head ),
inference(paramod,[status(thm)],[c_4076,c_7645]) ).
cnf(c_14420,plain,
( select(q4,head) = index_78
| head = tail ),
inference(copy,[status(thm)],[c_14419]) ).
cnf(c_11397,plain,
select(q4,head) = index_78,
inference(resolve,[status(thm)],[c_3,c_14420]) ).
cnf(c_14421,plain,
( select(queue_179,head) = index_78
| seq = head ),
inference(paramod,[status(thm)],[c_11397,c_2752]) ).
cnf(c_14422,plain,
( select(queue_179,head) = index_78
| head = seq ),
inference(copy,[status(thm)],[c_14421]) ).
cnf(c_11423,plain,
select(queue_179,head) = index_78,
inference(resolve,[status(thm)],[c_4,c_14422]) ).
cnf(c_14423,plain,
( select(queue_179,head) = index_188
| tail = head ),
inference(paramod,[status(thm)],[c_5562,c_4130]) ).
cnf(c_14424,plain,
( index_78 = index_188
| tail = head ),
inference(paramod,[status(thm)],[c_11423,c_14423]) ).
cnf(c_14425,plain,
( index_78 = index_188
| head = tail ),
inference(copy,[status(thm)],[c_14424]) ).
cnf(c_14426,plain,
( index_188 = index_78
| head = tail ),
inference(copy,[status(thm)],[c_14425]) ).
cnf(c_11432,plain,
index_188 = index_78,
inference(resolve,[status(thm)],[c_3,c_14426]) ).
cnf(c_14427,plain,
s(index_78) = index_189,
inference(paramod,[status(thm)],[c_11432,c_257]) ).
cnf(c_14428,plain,
index_153 = index_189,
inference(paramod,[status(thm)],[c_3486,c_14427]) ).
cnf(c_11516,plain,
index_189 = index_153,
inference(copy,[status(thm)],[c_14428]) ).
cnf(c_11521,plain,
select(queue_194,head) = index_153,
inference(paramod,[status(thm)],[c_11516,c_5577]) ).
cnf(c_14429,plain,
( select(queue_187,tail) = index_192
| head = tail ),
inference(paramod,[status(thm)],[c_259,c_4233]) ).
cnf(c_14430,plain,
( index_186 = index_192
| head = tail ),
inference(paramod,[status(thm)],[c_2755,c_14429]) ).
cnf(c_11529,plain,
index_186 = index_192,
inference(resolve,[status(thm)],[c_3,c_14430]) ).
cnf(c_11842,plain,
s(index_183) = index_192,
inference(paramod,[status(thm)],[c_11529,c_253]) ).
cnf(c_14431,plain,
( select(q7,head) = index_153
| tail = head ),
inference(paramod,[status(thm)],[c_4235,c_11521]) ).
cnf(c_14432,plain,
( select(q7,head) = index_153
| head = tail ),
inference(copy,[status(thm)],[c_14431]) ).
cnf(c_11851,plain,
select(q7,head) = index_153,
inference(resolve,[status(thm)],[c_3,c_14432]) ).
cnf(c_14433,plain,
( select(queue_200,head) = index_153
| seq = head ),
inference(paramod,[status(thm)],[c_11851,c_2760]) ).
cnf(c_14434,plain,
( select(queue_200,head) = index_153
| head = seq ),
inference(copy,[status(thm)],[c_14433]) ).
cnf(c_11877,plain,
select(queue_200,head) = index_153,
inference(resolve,[status(thm)],[c_4,c_14434]) ).
cnf(c_14435,plain,
( select(queue_200,head) = index_209
| tail = head ),
inference(paramod,[status(thm)],[c_5643,c_4289]) ).
cnf(c_14436,plain,
( index_153 = index_209
| tail = head ),
inference(paramod,[status(thm)],[c_11877,c_14435]) ).
cnf(c_14437,plain,
( index_153 = index_209
| head = tail ),
inference(copy,[status(thm)],[c_14436]) ).
cnf(c_14438,plain,
( index_209 = index_153
| head = tail ),
inference(copy,[status(thm)],[c_14437]) ).
cnf(c_11886,plain,
index_209 = index_153,
inference(resolve,[status(thm)],[c_3,c_14438]) ).
cnf(c_14439,plain,
s(index_153) = index_210,
inference(paramod,[status(thm)],[c_11886,c_275]) ).
cnf(c_14440,plain,
index_171 = index_210,
inference(paramod,[status(thm)],[c_11357,c_14439]) ).
cnf(c_11970,plain,
index_210 = index_171,
inference(copy,[status(thm)],[c_14440]) ).
cnf(c_14441,plain,
s(index_171) = index_27,
inference(paramod,[status(thm)],[c_11970,c_6024]) ).
cnf(c_14442,plain,
index_177 = index_27,
inference(paramod,[status(thm)],[c_4128,c_14441]) ).
cnf(c_12022,plain,
index_27 = index_177,
inference(copy,[status(thm)],[c_14442]) ).
cnf(c_14443,plain,
s(index_177) = index_48,
inference(paramod,[status(thm)],[c_12022,c_6380]) ).
cnf(c_14444,plain,
index_183 = index_48,
inference(paramod,[status(thm)],[c_4231,c_14443]) ).
cnf(c_12102,plain,
index_48 = index_183,
inference(copy,[status(thm)],[c_14444]) ).
cnf(c_14445,plain,
s(index_183) = index_69,
inference(paramod,[status(thm)],[c_12102,c_6922]) ).
cnf(c_14446,plain,
index_192 = index_69,
inference(paramod,[status(thm)],[c_11842,c_14445]) ).
cnf(c_12182,plain,
index_69 = index_192,
inference(copy,[status(thm)],[c_14446]) ).
cnf(c_14447,plain,
s(index_192) = index_116,
inference(paramod,[status(thm)],[c_12182,c_8767]) ).
cnf(c_14448,plain,
index_198 = index_116,
inference(paramod,[status(thm)],[c_4287,c_14447]) ).
cnf(c_12262,plain,
index_116 = index_198,
inference(copy,[status(thm)],[c_14448]) ).
cnf(c_14449,plain,
s(index_198) = index_117,
inference(paramod,[status(thm)],[c_12262,c_195]) ).
cnf(c_14450,plain,
index_204 = index_117,
inference(paramod,[status(thm)],[c_4390,c_14449]) ).
cnf(c_12377,plain,
index_117 = index_204,
inference(copy,[status(thm)],[c_14450]) ).
cnf(c_14451,plain,
s(index_204) = index_138,
inference(paramod,[status(thm)],[c_12377,c_9635]) ).
cnf(c_12429,plain,
index_207 = index_138,
inference(paramod,[status(thm)],[c_269,c_14451]) ).
cnf(c_12548,plain,
select(queue_208,tail) = index_138,
inference(paramod,[status(thm)],[c_12429,c_2763]) ).
cnf(c_14452,plain,
( select(queue_208,tail) = index_9
| head = tail ),
inference(paramod,[status(thm)],[c_333,c_4392]) ).
cnf(c_14453,plain,
( index_138 = index_9
| head = tail ),
inference(paramod,[status(thm)],[c_12548,c_14452]) ).
cnf(c_12553,plain,
index_138 = index_9,
inference(resolve,[status(thm)],[c_3,c_14453]) ).
cnf(c_14454,plain,
s(index_9) = index_168,
inference(paramod,[status(thm)],[c_12553,c_10851]) ).
cnf(c_14455,plain,
index_15 = index_168,
inference(paramod,[status(thm)],[c_2906,c_14454]) ).
cnf(c_12595,plain,
index_168 = index_15,
inference(copy,[status(thm)],[c_14455]) ).
cnf(c_13034,plain,
select(earray_163,index_15) = elem_214,
inference(paramod,[status(thm)],[c_12595,c_11382]) ).
cnf(c_14456,plain,
( select(earray_22,index_15) = e10
| index_21 = index_15 ),
inference(paramod,[status(thm)],[c_612,c_5956]) ).
cnf(c_13047,plain,
select(earray_22,index_15) = e10,
inference(resolve,[status(thm)],[c_2958,c_14456]) ).
cnf(c_14457,plain,
( select(earray_31,index_15) = e10
| index_30 = index_15 ),
inference(paramod,[status(thm)],[c_13047,c_6096]) ).
cnf(c_13058,plain,
select(earray_31,index_15) = e10,
inference(resolve,[status(thm)],[c_6151,c_14457]) ).
cnf(c_14458,plain,
( select(earray_37,index_15) = e10
| index_36 = index_15 ),
inference(paramod,[status(thm)],[c_13058,c_6277]) ).
cnf(c_13072,plain,
select(earray_37,index_15) = e10,
inference(resolve,[status(thm)],[c_6150,c_14458]) ).
cnf(c_14459,plain,
( select(earray_43,index_15) = e10
| index_42 = index_15 ),
inference(paramod,[status(thm)],[c_13072,c_6312]) ).
cnf(c_13090,plain,
select(earray_43,index_15) = e10,
inference(resolve,[status(thm)],[c_6149,c_14459]) ).
cnf(c_14460,plain,
( select(earray_52,index_15) = e10
| index_51 = index_15 ),
inference(paramod,[status(thm)],[c_13090,c_6500]) ).
cnf(c_13112,plain,
select(earray_52,index_15) = e10,
inference(resolve,[status(thm)],[c_6596,c_14460]) ).
cnf(c_14461,plain,
( select(earray_58,index_15) = e10
| index_57 = index_15 ),
inference(paramod,[status(thm)],[c_13112,c_6819]) ).
cnf(c_13138,plain,
select(earray_58,index_15) = e10,
inference(resolve,[status(thm)],[c_6597,c_14461]) ).
cnf(c_14462,plain,
( select(earray_64,index_15) = e10
| index_63 = index_15 ),
inference(paramod,[status(thm)],[c_13138,c_6854]) ).
cnf(c_13168,plain,
select(earray_64,index_15) = e10,
inference(resolve,[status(thm)],[c_6598,c_14462]) ).
cnf(c_14463,plain,
( select(earray_73,index_15) = e10
| index_72 = index_15 ),
inference(paramod,[status(thm)],[c_13168,c_7089]) ).
cnf(c_13212,plain,
select(earray_73,index_15) = e10,
inference(resolve,[status(thm)],[c_7273,c_14463]) ).
cnf(c_14464,plain,
( select(earray_85,index_15) = e10
| index_84 = index_15 ),
inference(paramod,[status(thm)],[c_13212,c_7537]) ).
cnf(c_13265,plain,
select(earray_85,index_15) = e10,
inference(resolve,[status(thm)],[c_7272,c_14464]) ).
cnf(c_14465,plain,
( select(earray_91,index_15) = e10
| index_90 = index_15 ),
inference(paramod,[status(thm)],[c_13265,c_7676]) ).
cnf(c_13338,plain,
select(earray_91,index_15) = e10,
inference(resolve,[status(thm)],[c_7271,c_14465]) ).
cnf(c_14466,plain,
( select(earray_100,index_15) = e10
| index_99 = index_15 ),
inference(paramod,[status(thm)],[c_7960,c_13338]) ).
cnf(c_13399,plain,
select(earray_100,index_15) = e10,
inference(resolve,[status(thm)],[c_8181,c_14466]) ).
cnf(c_14467,plain,
( select(earray_106,index_15) = e10
| index_105 = index_15 ),
inference(paramod,[status(thm)],[c_13399,c_8527]) ).
cnf(c_14468,plain,
( select(earray_106,index_15) = e10
| index_15 = index_105 ),
inference(copy,[status(thm)],[c_14467]) ).
cnf(c_13463,plain,
select(earray_106,index_15) = e10,
inference(resolve,[status(thm)],[c_8182,c_14468]) ).
cnf(c_14469,plain,
( select(earray_112,index_15) = e10
| index_111 = index_15 ),
inference(paramod,[status(thm)],[c_13463,c_8562]) ).
cnf(c_14470,plain,
( select(earray_112,index_15) = e10
| index_15 = index_111 ),
inference(copy,[status(thm)],[c_14469]) ).
cnf(c_13537,plain,
select(earray_112,index_15) = e10,
inference(resolve,[status(thm)],[c_8183,c_14470]) ).
cnf(c_14471,plain,
( select(earray_121,index_15) = e10
| index_120 = index_15 ),
inference(paramod,[status(thm)],[c_13537,c_8853]) ).
cnf(c_14472,plain,
( select(earray_121,index_15) = e10
| index_15 = index_120 ),
inference(copy,[status(thm)],[c_14471]) ).
cnf(c_13605,plain,
select(earray_121,index_15) = e10,
inference(resolve,[status(thm)],[c_9151,c_14472]) ).
cnf(c_14473,plain,
( select(earray_127,index_15) = e10
| index_126 = index_15 ),
inference(paramod,[status(thm)],[c_13605,c_9532]) ).
cnf(c_14474,plain,
( select(earray_127,index_15) = e10
| index_15 = index_126 ),
inference(copy,[status(thm)],[c_14473]) ).
cnf(c_13667,plain,
select(earray_127,index_15) = e10,
inference(resolve,[status(thm)],[c_9150,c_14474]) ).
cnf(c_14475,plain,
( select(earray_133,index_15) = e10
| index_132 = index_15 ),
inference(paramod,[status(thm)],[c_13667,c_9567]) ).
cnf(c_14476,plain,
( select(earray_133,index_15) = e10
| index_15 = index_132 ),
inference(copy,[status(thm)],[c_14475]) ).
cnf(c_13733,plain,
select(earray_133,index_15) = e10,
inference(resolve,[status(thm)],[c_9149,c_14476]) ).
cnf(c_14477,plain,
( select(earray_142,index_15) = e10
| index_141 = index_15 ),
inference(paramod,[status(thm)],[c_13733,c_9947]) ).
cnf(c_14478,plain,
( select(earray_142,index_15) = e10
| index_15 = index_141 ),
inference(copy,[status(thm)],[c_14477]) ).
cnf(c_13803,plain,
select(earray_142,index_15) = e10,
inference(resolve,[status(thm)],[c_10277,c_14478]) ).
cnf(c_14479,plain,
( select(earray_148,index_15) = e10
| index_147 = index_15 ),
inference(paramod,[status(thm)],[c_13803,c_10738]) ).
cnf(c_14480,plain,
( select(earray_148,index_15) = e10
| index_15 = index_147 ),
inference(copy,[status(thm)],[c_14479]) ).
cnf(c_13877,plain,
select(earray_148,index_15) = e10,
inference(resolve,[status(thm)],[c_10278,c_14480]) ).
cnf(c_14481,plain,
( select(earray_148,index_15) = elem_214
| index_162 = index_15 ),
inference(paramod,[status(thm)],[c_10783,c_13034]) ).
cnf(c_14482,plain,
( e10 = elem_214
| index_162 = index_15 ),
inference(paramod,[status(thm)],[c_13877,c_14481]) ).
cnf(c_14483,plain,
( elem_214 = e10
| index_162 = index_15 ),
inference(copy,[status(thm)],[c_14482]) ).
cnf(c_14484,plain,
elem_214 = e10,
inference(resolve,[status(thm)],[c_10279,c_14483]) ).
cnf(c_13937,plain,
$false,
inference(resolve,[status(thm)],[c_548,c_14484]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV569-1.030 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/5.36 % Computer : n005.cluster.edu
% 0.07/5.36 % Model : x86_64 x86_64
% 0.07/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/5.36 % Memory : 8046.5625MB
% 0.07/5.36 % OS : Linux 6.8.0-71-generic
% 0.07/5.36 % CPULimit : 300
% 0.07/5.36 % WCLimit : 300
% 0.07/5.36 % DateTime : Sat Sep 26 14:30:37 UTC 2026
% 0.07/5.36 % CPUTime :
% 0.07/5.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/5.37 % Process 2353096 was started by sandbox2 on n005,
% 0.07/5.37 % Sat Sep 26 14:30:37 2026
% 0.07/5.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.07/5.37
% 0.07/5.37 % From the command line: assign(max_seconds, 300).
% 48.78/12.69
% 48.78/12.69 % given #500 (T,wt=5): 2755 select(queue_187,tail) = index_186. [para(411(a,1),1(a,1,1))].
% 48.78/12.69
% 48.78/12.69 % given #1000 (F,wt=4): 6330 s(index_48) != index_27. [back_rewrite(2204),rewrite([6296(3)])].
% 48.78/12.69
% 48.78/12.69 % given #1500 (A,wt=32): 1359 s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(index_165))))))))))))))))))))))))))))) != index_162. [para(235(a,1),26(a,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1))].
% 48.78/12.69
% 48.78/12.69 % given #2000 (T,wt=5): 13728 select(earray_133,index_51) = e15. [para(13662(a,1),9567(b,2)),flip(a),unit_del(a,9271)].
% 48.78/12.69
% 48.78/12.69 % SZS status Unsatisfiable for theBenchmark
% 48.78/12.69
% 48.78/12.69 % Proof 1 at 6.38 (+ 0.76) seconds.
% 48.78/12.69 % Length of proof is 936.
% 48.78/12.69 % Level of proof is 30.
% 48.78/12.69 % Maximum clause weight is 22.000.
% 48.78/12.69 % Given clauses 2101.
% 48.78/12.69
% 48.78/12.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------