%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV555-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:08:18 AM UTC 2026
% Result : Unsatisfiable 23.17s 8.39s
% Output : CNFRefutation 23.17s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% 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(hyp0,axiom,
a_20 = store(a1,i1,e_19),
file('theBenchmark.p',hyp0) ).
cnf(c_3,plain,
a_20 = store(a1,i1,e_19),
inference(clausify,[status(thm)],[hyp0]) ).
cnf(c_4,plain,
store(a1,i1,e_19) = a_20,
inference(copy,[status(thm)],[c_3]) ).
fof(hyp1,axiom,
a_22 = store(a2,i1,e_21),
file('theBenchmark.p',hyp1) ).
cnf(c_5,plain,
a_22 = store(a2,i1,e_21),
inference(clausify,[status(thm)],[hyp1]) ).
cnf(c_6,plain,
store(a2,i1,e_21) = a_22,
inference(copy,[status(thm)],[c_5]) ).
fof(hyp2,axiom,
a_24 = store(a_20,i2,e_23),
file('theBenchmark.p',hyp2) ).
cnf(c_7,plain,
a_24 = store(a_20,i2,e_23),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_8,plain,
store(a_20,i2,e_23) = a_24,
inference(copy,[status(thm)],[c_7]) ).
fof(hyp3,axiom,
a_26 = store(a_22,i2,e_25),
file('theBenchmark.p',hyp3) ).
cnf(c_9,plain,
a_26 = store(a_22,i2,e_25),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_10,plain,
store(a_22,i2,e_25) = a_26,
inference(copy,[status(thm)],[c_9]) ).
fof(hyp4,axiom,
a_28 = store(a_24,i3,e_27),
file('theBenchmark.p',hyp4) ).
cnf(c_11,plain,
a_28 = store(a_24,i3,e_27),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_12,plain,
store(a_24,i3,e_27) = a_28,
inference(copy,[status(thm)],[c_11]) ).
fof(hyp5,axiom,
a_30 = store(a_26,i3,e_29),
file('theBenchmark.p',hyp5) ).
cnf(c_13,plain,
a_30 = store(a_26,i3,e_29),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_14,plain,
store(a_26,i3,e_29) = a_30,
inference(copy,[status(thm)],[c_13]) ).
fof(hyp6,axiom,
a_32 = store(a_28,i4,e_31),
file('theBenchmark.p',hyp6) ).
cnf(c_15,plain,
a_32 = store(a_28,i4,e_31),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_16,plain,
store(a_28,i4,e_31) = a_32,
inference(copy,[status(thm)],[c_15]) ).
fof(hyp7,axiom,
a_34 = store(a_30,i4,e_33),
file('theBenchmark.p',hyp7) ).
cnf(c_17,plain,
a_34 = store(a_30,i4,e_33),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_18,plain,
store(a_30,i4,e_33) = a_34,
inference(copy,[status(thm)],[c_17]) ).
fof(hyp8,axiom,
e_19 = select(a2,i1),
file('theBenchmark.p',hyp8) ).
cnf(c_19,plain,
e_19 = select(a2,i1),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_20,plain,
select(a2,i1) = e_19,
inference(copy,[status(thm)],[c_19]) ).
fof(hyp9,axiom,
e_21 = select(a1,i1),
file('theBenchmark.p',hyp9) ).
cnf(c_21,plain,
e_21 = select(a1,i1),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_22,plain,
select(a1,i1) = e_21,
inference(copy,[status(thm)],[c_21]) ).
fof(hyp10,axiom,
e_23 = select(a_22,i2),
file('theBenchmark.p',hyp10) ).
cnf(c_23,plain,
e_23 = select(a_22,i2),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_24,plain,
select(a_22,i2) = e_23,
inference(copy,[status(thm)],[c_23]) ).
fof(hyp11,axiom,
e_25 = select(a_20,i2),
file('theBenchmark.p',hyp11) ).
cnf(c_25,plain,
e_25 = select(a_20,i2),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_26,plain,
select(a_20,i2) = e_25,
inference(copy,[status(thm)],[c_25]) ).
fof(hyp12,axiom,
e_27 = select(a_26,i3),
file('theBenchmark.p',hyp12) ).
cnf(c_27,plain,
e_27 = select(a_26,i3),
inference(clausify,[status(thm)],[hyp12]) ).
cnf(c_28,plain,
select(a_26,i3) = e_27,
inference(copy,[status(thm)],[c_27]) ).
fof(hyp13,axiom,
e_29 = select(a_24,i3),
file('theBenchmark.p',hyp13) ).
cnf(c_29,plain,
e_29 = select(a_24,i3),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_30,plain,
select(a_24,i3) = e_29,
inference(copy,[status(thm)],[c_29]) ).
fof(hyp14,axiom,
e_31 = select(a_30,i4),
file('theBenchmark.p',hyp14) ).
cnf(c_31,plain,
e_31 = select(a_30,i4),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_32,plain,
select(a_30,i4) = e_31,
inference(copy,[status(thm)],[c_31]) ).
fof(hyp15,axiom,
e_33 = select(a_28,i4),
file('theBenchmark.p',hyp15) ).
cnf(c_33,plain,
e_33 = select(a_28,i4),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_34,plain,
select(a_28,i4) = e_33,
inference(copy,[status(thm)],[c_33]) ).
fof(hyp16,axiom,
e_36 = select(a1,i_35),
file('theBenchmark.p',hyp16) ).
cnf(c_35,plain,
e_36 = select(a1,i_35),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_36,plain,
select(a1,i_35) = e_36,
inference(copy,[status(thm)],[c_35]) ).
fof(hyp17,axiom,
e_37 = select(a2,i_35),
file('theBenchmark.p',hyp17) ).
cnf(c_37,plain,
e_37 = select(a2,i_35),
inference(clausify,[status(thm)],[hyp17]) ).
cnf(c_38,plain,
select(a2,i_35) = e_37,
inference(copy,[status(thm)],[c_37]) ).
fof(hyp19,axiom,
a_32 = a_34,
file('theBenchmark.p',hyp19) ).
cnf(c_41,plain,
a_32 = a_34,
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_42,plain,
a_34 = a_32,
inference(copy,[status(thm)],[c_41]) ).
fof(goal,axiom,
e_36 != e_37,
file('theBenchmark.p',goal) ).
cnf(c_43,plain,
e_36 != e_37,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_44,plain,
e_37 != e_36,
inference(copy,[status(thm)],[c_43]) ).
cnf(c_48,plain,
select(a_20,i1) = e_19,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_49,plain,
( select(a_20,A) = select(a1,A)
| i1 = A ),
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_50,plain,
select(a_22,i1) = e_21,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_51,plain,
( select(a_22,A) = select(a2,A)
| i1 = A ),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_52,plain,
select(a_24,i2) = e_23,
inference(paramod,[status(thm)],[c_8,c_1]) ).
cnf(c_53,plain,
( select(a_24,A) = select(a_20,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_54,plain,
select(a_26,i2) = e_25,
inference(paramod,[status(thm)],[c_10,c_1]) ).
cnf(c_55,plain,
( select(a_26,A) = select(a_22,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_56,plain,
select(a_28,i3) = e_27,
inference(paramod,[status(thm)],[c_12,c_1]) ).
cnf(c_57,plain,
( select(a_28,A) = select(a_24,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_58,plain,
select(a_30,i3) = e_29,
inference(paramod,[status(thm)],[c_14,c_1]) ).
cnf(c_59,plain,
( select(a_30,A) = select(a_26,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_60,plain,
select(a_32,i4) = e_31,
inference(paramod,[status(thm)],[c_16,c_1]) ).
cnf(c_61,plain,
( select(a_32,A) = select(a_28,A)
| i4 = A ),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_62,plain,
select(a_34,i4) = e_33,
inference(paramod,[status(thm)],[c_18,c_1]) ).
cnf(c_63,plain,
( select(a_34,A) = select(a_30,A)
| i4 = A ),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_74,plain,
store(a_30,i4,e_33) = a_32,
inference(paramod,[status(thm)],[c_42,c_18]) ).
cnf(c_5214,plain,
( select(store(a_24,A,B),i2) = e_23
| A = i2 ),
inference(paramod,[status(thm)],[c_52,c_2]) ).
cnf(c_77,plain,
( select(store(a_24,A,B),i2) = e_23
| i2 = A ),
inference(copy,[status(thm)],[c_5214]) ).
cnf(c_5215,plain,
( select(store(a_26,A,B),i2) = e_25
| A = i2 ),
inference(paramod,[status(thm)],[c_54,c_2]) ).
cnf(c_78,plain,
( select(store(a_26,A,B),i2) = e_25
| i2 = A ),
inference(copy,[status(thm)],[c_5215]) ).
cnf(c_83,plain,
select(a_32,i4) = e_33,
inference(paramod,[status(thm)],[c_42,c_62]) ).
cnf(c_85,plain,
e_33 = e_31,
inference(paramod,[status(thm)],[c_83,c_60]) ).
cnf(c_87,plain,
select(a_28,i4) = e_31,
inference(paramod,[status(thm)],[c_85,c_34]) ).
cnf(c_91,plain,
( select(a_32,A) = select(a_30,A)
| i4 = A ),
inference(paramod,[status(thm)],[c_74,c_2]) ).
cnf(c_5216,plain,
( select(a1,i2) = e_25
| i1 = i2 ),
inference(paramod,[status(thm)],[c_49,c_26]) ).
cnf(c_94,plain,
( select(a1,i2) = e_25
| i2 = i1 ),
inference(copy,[status(thm)],[c_5216]) ).
cnf(c_5217,plain,
( select(a_20,i_35) = e_36
| i1 = i_35 ),
inference(paramod,[status(thm)],[c_36,c_49]) ).
cnf(c_95,plain,
( select(a_20,i_35) = e_36
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5217]) ).
cnf(c_5218,plain,
( select(a2,i2) = e_23
| i1 = i2 ),
inference(paramod,[status(thm)],[c_51,c_24]) ).
cnf(c_102,plain,
( select(a2,i2) = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_5218]) ).
cnf(c_5219,plain,
( select(a_22,i_35) = e_37
| i1 = i_35 ),
inference(paramod,[status(thm)],[c_38,c_51]) ).
cnf(c_103,plain,
( select(a_22,i_35) = e_37
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5219]) ).
cnf(c_111,plain,
( select(a_24,i1) = e_19
| i2 = i1 ),
inference(paramod,[status(thm)],[c_48,c_53]) ).
cnf(c_5220,plain,
( select(a_24,i_35) = e_36
| i2 = i_35
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_95,c_53]) ).
cnf(c_113,plain,
( select(a_24,i_35) = e_36
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5220]) ).
cnf(c_121,plain,
( select(a_26,i1) = e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_50,c_55]) ).
cnf(c_5221,plain,
( select(a_26,i_35) = e_37
| i2 = i_35
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_103,c_55]) ).
cnf(c_123,plain,
( select(a_26,i_35) = e_37
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5221]) ).
cnf(c_131,plain,
( select(a_28,i2) = e_23
| i3 = i2 ),
inference(paramod,[status(thm)],[c_52,c_57]) ).
cnf(c_134,plain,
( select(a_28,i1) = e_19
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_111,c_57]) ).
cnf(c_145,plain,
( select(a_30,i2) = e_25
| i3 = i2 ),
inference(paramod,[status(thm)],[c_54,c_59]) ).
cnf(c_147,plain,
( select(a_30,i1) = e_21
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_121,c_59]) ).
cnf(c_154,plain,
( select(a_32,i3) = e_27
| i4 = i3 ),
inference(paramod,[status(thm)],[c_56,c_61]) ).
cnf(c_155,plain,
( select(a_32,A) = select(a_24,A)
| i4 = A
| i3 = A ),
inference(paramod,[status(thm)],[c_57,c_61]) ).
cnf(c_156,plain,
( select(a_32,i2) = e_23
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_131,c_61]) ).
cnf(c_160,plain,
( select(a_34,i3) = e_29
| i4 = i3 ),
inference(paramod,[status(thm)],[c_58,c_63]) ).
cnf(c_165,plain,
( select(a_32,i3) = e_29
| i4 = i3 ),
inference(paramod,[status(thm)],[c_42,c_160]) ).
cnf(c_5222,plain,
( e_29 = e_27
| i4 = i3
| i4 = i3 ),
inference(paramod,[status(thm)],[c_165,c_154]) ).
cnf(c_168,plain,
( e_29 = e_27
| i4 = i3 ),
inference(copy,[status(thm)],[c_5222]) ).
cnf(c_179,plain,
( select(a_32,A) = select(a_26,A)
| i4 = A
| i3 = A ),
inference(paramod,[status(thm)],[c_59,c_91]) ).
cnf(c_180,plain,
( select(a_32,i2) = e_25
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_145,c_91]) ).
cnf(c_5223,plain,
( select(a_30,A) = select(a_28,A)
| i4 = A
| i4 = A ),
inference(paramod,[status(thm)],[c_91,c_61]) ).
cnf(c_181,plain,
( select(a_30,A) = select(a_28,A)
| i4 = A ),
inference(copy,[status(thm)],[c_5223]) ).
cnf(c_5224,plain,
( select(a_28,i_35) = e_36
| i3 = i_35
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_113,c_57]) ).
cnf(c_195,plain,
( select(a_28,i_35) = e_36
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5224]) ).
cnf(c_5225,plain,
( select(a_30,i_35) = e_37
| i3 = i_35
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_123,c_59]) ).
cnf(c_203,plain,
( select(a_30,i_35) = e_37
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5225]) ).
cnf(c_211,plain,
( select(a_30,i1) = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_134,c_181]) ).
cnf(c_5226,plain,
( e_25 = e_23
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_180,c_156]) ).
cnf(c_5227,plain,
( e_25 = e_23
| i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5226]) ).
cnf(c_234,plain,
( e_25 = e_23
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5227]) ).
cnf(c_238,plain,
( select(a1,i2) = e_23
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_234,c_94]) ).
cnf(c_5228,plain,
( select(a_32,i_35) = e_36
| i4 = i_35
| i3 = i_35
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_113,c_155]) ).
cnf(c_5229,plain,
( select(a_32,i_35) = e_36
| i4 = i_35
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5228]) ).
cnf(c_267,plain,
( select(a_32,i_35) = e_36
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5229]) ).
cnf(c_5230,plain,
( select(a_32,i_35) = e_37
| i4 = i_35
| i3 = i_35
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_123,c_179]) ).
cnf(c_5231,plain,
( select(a_32,i_35) = e_37
| i4 = i_35
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5230]) ).
cnf(c_277,plain,
( select(a_32,i_35) = e_37
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5231]) ).
cnf(c_5232,plain,
( e_19 = e_21
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_211,c_147]) ).
cnf(c_5233,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5232]) ).
cnf(c_5234,plain,
( e_21 = e_19
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5233]) ).
cnf(c_321,plain,
( e_21 = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5234]) ).
cnf(c_324,plain,
( select(a1,i1) = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_321,c_22]) ).
cnf(c_5235,plain,
( e_37 = e_36
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_277,c_267]) ).
cnf(c_5236,plain,
( e_37 = e_36
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5235]) ).
cnf(c_5237,plain,
( e_37 = e_36
| i_35 = i4
| i_35 = i3
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5236]) ).
cnf(c_5238,plain,
( e_37 = e_36
| i_35 = i4
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5237]) ).
cnf(c_5239,plain,
( e_37 = e_36
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5238]) ).
cnf(c_469,plain,
( i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_44,c_5239]) ).
cnf(c_5240,plain,
( select(a_28,i4) = e_36
| i_35 = i3
| i_35 = i2
| i_35 = i1
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_469,c_195]) ).
cnf(c_5241,plain,
( select(a_28,i4) = e_36
| i_35 = i3
| i_35 = i2
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5240]) ).
cnf(c_5242,plain,
( select(a_28,i4) = e_36
| i_35 = i3
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5241]) ).
cnf(c_477,plain,
( select(a_28,i4) = e_36
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5242]) ).
cnf(c_5243,plain,
( select(a_30,i4) = e_37
| i_35 = i3
| i_35 = i2
| i_35 = i1
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_469,c_203]) ).
cnf(c_5244,plain,
( select(a_30,i4) = e_37
| i_35 = i3
| i_35 = i2
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5243]) ).
cnf(c_5245,plain,
( select(a_30,i4) = e_37
| i_35 = i3
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5244]) ).
cnf(c_478,plain,
( select(a_30,i4) = e_37
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5245]) ).
cnf(c_584,plain,
( e_36 = e_31
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_477,c_87]) ).
cnf(c_599,plain,
( e_37 != e_31
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_584,c_44]) ).
cnf(c_612,plain,
( e_37 = e_31
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_478,c_32]) ).
cnf(c_5246,plain,
( i_35 = i3
| i_35 = i2
| i_35 = i1
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_612,c_599]) ).
cnf(c_5247,plain,
( i_35 = i3
| i_35 = i2
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5246]) ).
cnf(c_5248,plain,
( i_35 = i3
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5247]) ).
cnf(c_613,plain,
( i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5248]) ).
cnf(c_5249,plain,
( select(a_24,i3) = e_36
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_613,c_113]) ).
cnf(c_5250,plain,
( select(a_24,i3) = e_36
| i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5249]) ).
cnf(c_619,plain,
( select(a_24,i3) = e_36
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5250]) ).
cnf(c_5251,plain,
( select(a_26,i3) = e_37
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_613,c_123]) ).
cnf(c_5252,plain,
( select(a_26,i3) = e_37
| i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5251]) ).
cnf(c_620,plain,
( select(a_26,i3) = e_37
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5252]) ).
cnf(c_710,plain,
( e_36 = e_29
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_619,c_30]) ).
cnf(c_713,plain,
( e_37 != e_29
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_710,c_44]) ).
cnf(c_722,plain,
( e_37 != e_27
| i_35 = i2
| i_35 = i1
| i4 = i3 ),
inference(paramod,[status(thm)],[c_168,c_713]) ).
cnf(c_733,plain,
( e_37 = e_27
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_620,c_28]) ).
cnf(c_5253,plain,
( i_35 = i2
| i_35 = i1
| i4 = i3
| i_35 = i2
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_733,c_722]) ).
cnf(c_5254,plain,
( i_35 = i2
| i4 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5253]) ).
cnf(c_734,plain,
( i4 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5254]) ).
cnf(c_5255,plain,
( e_27 != e_29
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_733,c_713]) ).
cnf(c_5256,plain,
( e_29 != e_27
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5255]) ).
cnf(c_5257,plain,
( e_29 != e_27
| i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5256]) ).
cnf(c_743,plain,
( e_29 != e_27
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5257]) ).
cnf(c_5258,plain,
( select(a_20,i2) = e_36
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_734,c_95]) ).
cnf(c_749,plain,
( select(a_20,i2) = e_36
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5258]) ).
cnf(c_5259,plain,
( select(a_22,i2) = e_37
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_734,c_103]) ).
cnf(c_750,plain,
( select(a_22,i2) = e_37
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5259]) ).
cnf(c_797,plain,
( e_36 = e_25
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_749,c_26]) ).
cnf(c_800,plain,
( e_37 != e_25
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_797,c_44]) ).
cnf(c_806,plain,
( e_37 != e_23
| i4 = i3
| i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_234,c_800]) ).
cnf(c_814,plain,
( e_37 = e_23
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_750,c_24]) ).
cnf(c_5260,plain,
( i4 = i3
| i_35 = i1
| i4 = i2
| i3 = i2
| i4 = i3
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_814,c_806]) ).
cnf(c_5261,plain,
( i4 = i3
| i4 = i2
| i3 = i2
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5260]) ).
cnf(c_815,plain,
( i4 = i2
| i3 = i2
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5261]) ).
cnf(c_5262,plain,
( e_23 != e_25
| i4 = i3
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_814,c_800]) ).
cnf(c_5263,plain,
( e_25 != e_23
| i4 = i3
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5262]) ).
cnf(c_5264,plain,
( e_25 != e_23
| i4 = i3
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5263]) ).
cnf(c_822,plain,
( e_25 != e_23
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5264]) ).
cnf(c_824,plain,
( select(a1,i1) = e_36
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_815,c_36]) ).
cnf(c_825,plain,
( select(a2,i1) = e_37
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_815,c_38]) ).
cnf(c_834,plain,
( e_36 = e_21
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_824,c_22]) ).
cnf(c_837,plain,
( e_37 != e_21
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_834,c_44]) ).
cnf(c_841,plain,
( e_37 = e_19
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_825,c_20]) ).
cnf(c_5265,plain,
( e_19 != e_21
| i4 = i2
| i3 = i2
| i4 = i3
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_841,c_837]) ).
cnf(c_5266,plain,
( e_21 != e_19
| i4 = i2
| i3 = i2
| i4 = i3
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_5265]) ).
cnf(c_5267,plain,
( e_21 != e_19
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_5266]) ).
cnf(c_5268,plain,
( e_21 != e_19
| i4 = i2
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_5267]) ).
cnf(c_845,plain,
( e_21 != e_19
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_5268]) ).
cnf(c_846,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(resolve,[status(thm)],[c_845,c_321]) ).
cnf(c_849,plain,
( select(a_30,i3) = e_31
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_846,c_32]) ).
cnf(c_850,plain,
( select(a_28,i3) = e_33
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_846,c_34]) ).
cnf(c_1213,plain,
( e_31 = e_29
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_849,c_58]) ).
cnf(c_1217,plain,
( e_33 = e_29
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1213,c_85]) ).
cnf(c_1235,plain,
( e_33 = e_27
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_850,c_56]) ).
cnf(c_5269,plain,
( e_27 = e_29
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1235,c_1217]) ).
cnf(c_5270,plain,
( e_29 = e_27
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5269]) ).
cnf(c_5271,plain,
( e_29 = e_27
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5270]) ).
cnf(c_5272,plain,
( e_29 = e_27
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5271]) ).
cnf(c_5273,plain,
( e_29 = e_27
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5272]) ).
cnf(c_5274,plain,
( e_29 = e_27
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5273]) ).
cnf(c_1246,plain,
( e_29 = e_27
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5274]) ).
cnf(c_1259,plain,
( i_35 = i2
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_1246,c_743]) ).
cnf(c_1275,plain,
( select(a1,i2) = e_36
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1259,c_36]) ).
cnf(c_1276,plain,
( select(a2,i2) = e_37
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1259,c_38]) ).
cnf(c_5275,plain,
( e_36 = e_23
| i2 = i1
| i4 = i2
| i3 = i2
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1275,c_238]) ).
cnf(c_5276,plain,
( e_36 = e_23
| i2 = i1
| i4 = i2
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5275]) ).
cnf(c_5277,plain,
( e_36 = e_23
| i2 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5276]) ).
cnf(c_1684,plain,
( e_36 = e_23
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5277]) ).
cnf(c_1694,plain,
( e_37 != e_23
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1684,c_44]) ).
cnf(c_5278,plain,
( e_37 = e_23
| i2 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1276,c_102]) ).
cnf(c_1701,plain,
( e_37 = e_23
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5278]) ).
cnf(c_5279,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_1701,c_1694]) ).
cnf(c_5280,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5279]) ).
cnf(c_5281,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5280]) ).
cnf(c_5282,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5281]) ).
cnf(c_5283,plain,
( i_35 = i1
| i4 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5282]) ).
cnf(c_5284,plain,
( i_35 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5283]) ).
cnf(c_1703,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5284]) ).
cnf(c_1704,plain,
( select(a1,i1) = e_36
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1703,c_36]) ).
cnf(c_1705,plain,
( select(a2,i1) = e_37
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1703,c_38]) ).
cnf(c_5285,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1704,c_324]) ).
cnf(c_5286,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5285]) ).
cnf(c_5287,plain,
( e_36 = e_19
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5286]) ).
cnf(c_1711,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5287]) ).
cnf(c_1716,plain,
( e_37 != e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1711,c_44]) ).
cnf(c_1719,plain,
( e_37 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1705,c_20]) ).
cnf(c_5288,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_1719,c_1716]) ).
cnf(c_5289,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5288]) ).
cnf(c_5290,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5289]) ).
cnf(c_5291,plain,
( i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5290]) ).
cnf(c_5292,plain,
( i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5291]) ).
cnf(c_1720,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5292]) ).
cnf(c_1723,plain,
( select(a_30,i2) = e_31
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1720,c_32]) ).
cnf(c_1724,plain,
( select(a_28,i2) = e_33
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1720,c_34]) ).
cnf(c_5293,plain,
( e_31 = e_25
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1723,c_145]) ).
cnf(c_1777,plain,
( e_31 = e_25
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5293]) ).
cnf(c_1781,plain,
( e_33 = e_25
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1777,c_85]) ).
cnf(c_5294,plain,
( e_33 = e_23
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1724,c_131]) ).
cnf(c_1804,plain,
( e_33 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5294]) ).
cnf(c_5295,plain,
( e_23 = e_25
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1804,c_1781]) ).
cnf(c_5296,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5295]) ).
cnf(c_5297,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5296]) ).
cnf(c_5298,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5297]) ).
cnf(c_5299,plain,
( e_25 = e_23
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5298]) ).
cnf(c_1818,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5299]) ).
cnf(c_1832,plain,
( i4 = i3
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(resolve,[status(thm)],[c_1818,c_822]) ).
cnf(c_1846,plain,
( select(a1,i1) = e_36
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1832,c_36]) ).
cnf(c_1847,plain,
( select(a2,i1) = e_37
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1832,c_38]) ).
cnf(c_5300,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1846,c_324]) ).
cnf(c_5301,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5300]) ).
cnf(c_5302,plain,
( e_36 = e_19
| i4 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5301]) ).
cnf(c_1949,plain,
( e_36 = e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5302]) ).
cnf(c_1954,plain,
( e_37 != e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1949,c_44]) ).
cnf(c_1957,plain,
( e_37 = e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1847,c_20]) ).
cnf(c_5303,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(resolve,[status(thm)],[c_1957,c_1954]) ).
cnf(c_5304,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5303]) ).
cnf(c_5305,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5304]) ).
cnf(c_5306,plain,
( i4 = i3
| i4 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5305]) ).
cnf(c_5307,plain,
( i4 = i3
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5306]) ).
cnf(c_1958,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5307]) ).
cnf(c_5308,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1958,c_1720]) ).
cnf(c_5309,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5308]) ).
cnf(c_5310,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5309]) ).
cnf(c_5311,plain,
( i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5310]) ).
cnf(c_5312,plain,
( i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5311]) ).
cnf(c_1983,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5312]) ).
cnf(c_1986,plain,
( select(a_30,i1) = e_31
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1983,c_32]) ).
cnf(c_1987,plain,
( select(a_28,i1) = e_33
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1983,c_34]) ).
cnf(c_5313,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1986,c_147]) ).
cnf(c_5314,plain,
( e_31 = e_21
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5313]) ).
cnf(c_2045,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5314]) ).
cnf(c_2050,plain,
( e_33 = e_21
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2045,c_85]) ).
cnf(c_5315,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1987,c_134]) ).
cnf(c_5316,plain,
( e_33 = e_19
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5315]) ).
cnf(c_2075,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5316]) ).
cnf(c_5317,plain,
( e_19 = e_21
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2075,c_2050]) ).
cnf(c_5318,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5317]) ).
cnf(c_5319,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5318]) ).
cnf(c_5320,plain,
( e_21 = e_19
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5319]) ).
cnf(c_2094,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5320]) ).
cnf(c_5321,plain,
( i4 = i2
| i3 = i2
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(resolve,[status(thm)],[c_2094,c_845]) ).
cnf(c_2106,plain,
( i4 = i2
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5321]) ).
cnf(c_5322,plain,
( i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2106,c_1983]) ).
cnf(c_5323,plain,
( i3 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5322]) ).
cnf(c_5324,plain,
( i3 = i1
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5323]) ).
cnf(c_5325,plain,
( i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5324]) ).
cnf(c_2142,plain,
( i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5325]) ).
cnf(c_5326,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2142,c_1983]) ).
cnf(c_5327,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5326]) ).
cnf(c_5328,plain,
( i2 = i1
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5327]) ).
cnf(c_5329,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5328]) ).
cnf(c_2183,plain,
( i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_5329]) ).
cnf(c_2186,plain,
( select(a_26,i2) = e_27
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2183,c_28]) ).
cnf(c_2187,plain,
( select(a_24,i2) = e_29
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2183,c_30]) ).
cnf(c_2188,plain,
( select(a_28,i2) = e_27
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2183,c_56]) ).
cnf(c_2189,plain,
( select(a_30,i2) = e_29
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2183,c_58]) ).
cnf(c_5330,plain,
( i_35 = i2
| i_35 = i2
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2183,c_613]) ).
cnf(c_2205,plain,
( i_35 = i2
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5330]) ).
cnf(c_2243,plain,
( select(a1,i2) = e_36
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2205,c_36]) ).
cnf(c_2244,plain,
( select(a2,i2) = e_37
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2205,c_38]) ).
cnf(c_2257,plain,
( e_27 = e_25
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2186,c_54]) ).
cnf(c_2260,plain,
( select(a_28,i3) = e_25
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2257,c_56]) ).
cnf(c_2262,plain,
( e_29 = e_25
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2257,c_168]) ).
cnf(c_2283,plain,
( e_29 = e_23
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2187,c_52]) ).
cnf(c_2287,plain,
( select(a_30,i3) = e_23
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2283,c_58]) ).
cnf(c_5331,plain,
( e_23 = e_25
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2283,c_2262]) ).
cnf(c_5332,plain,
( e_25 = e_23
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5331]) ).
cnf(c_5333,plain,
( e_25 = e_23
| i4 = i3
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5332]) ).
cnf(c_2300,plain,
( e_25 = e_23
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5333]) ).
cnf(c_5334,plain,
( i4 = i3
| i_35 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_2300,c_822]) ).
cnf(c_2311,plain,
( i_35 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5334]) ).
cnf(c_2321,plain,
( select(a1,i1) = e_36
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2311,c_36]) ).
cnf(c_2322,plain,
( select(a2,i1) = e_37
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2311,c_38]) ).
cnf(c_2328,plain,
( select(a_30,i2) = e_27
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2188,c_181]) ).
cnf(c_5335,plain,
( select(a_30,i2) = e_23
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2283,c_2189]) ).
cnf(c_5336,plain,
( select(a_30,i2) = e_23
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5335]) ).
cnf(c_2350,plain,
( select(a_30,i2) = e_23
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5336]) ).
cnf(c_5337,plain,
( e_36 = e_25
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2243,c_94]) ).
cnf(c_2400,plain,
( e_36 = e_25
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5337]) ).
cnf(c_2403,plain,
( e_37 != e_25
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2400,c_44]) ).
cnf(c_5338,plain,
( e_37 = e_23
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2244,c_102]) ).
cnf(c_2410,plain,
( e_37 = e_23
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5338]) ).
cnf(c_5339,plain,
( e_23 != e_25
| i_35 = i1
| i3 = i1
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2410,c_2403]) ).
cnf(c_5340,plain,
( e_25 != e_23
| i_35 = i1
| i3 = i1
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5339]) ).
cnf(c_5341,plain,
( e_25 != e_23
| i_35 = i1
| i3 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5340]) ).
cnf(c_5342,plain,
( e_25 != e_23
| i_35 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5341]) ).
cnf(c_2418,plain,
( e_25 != e_23
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5342]) ).
cnf(c_2423,plain,
( e_36 = e_21
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2321,c_22]) ).
cnf(c_2426,plain,
( e_37 != e_21
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2423,c_44]) ).
cnf(c_5343,plain,
( e_37 != e_19
| i4 = i3
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_321,c_2426]) ).
cnf(c_5344,plain,
( e_37 != e_19
| i4 = i3
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5343]) ).
cnf(c_2428,plain,
( e_37 != e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5344]) ).
cnf(c_2432,plain,
( e_37 = e_19
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2322,c_20]) ).
cnf(c_5345,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_2432,c_2428]) ).
cnf(c_5346,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5345]) ).
cnf(c_5347,plain,
( i4 = i3
| i4 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5346]) ).
cnf(c_2433,plain,
( i4 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5347]) ).
cnf(c_2440,plain,
( select(a_30,i3) = e_31
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2433,c_32]) ).
cnf(c_2441,plain,
( select(a_28,i3) = e_33
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2433,c_34]) ).
cnf(c_5348,plain,
( e_27 = e_23
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2328,c_2350]) ).
cnf(c_5349,plain,
( e_27 = e_23
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5348]) ).
cnf(c_2502,plain,
( e_27 = e_23
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5349]) ).
cnf(c_5350,plain,
( e_23 = e_25
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2502,c_2257]) ).
cnf(c_5351,plain,
( e_25 = e_23
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5350]) ).
cnf(c_5352,plain,
( e_25 = e_23
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5351]) ).
cnf(c_2519,plain,
( e_25 = e_23
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5352]) ).
cnf(c_5353,plain,
( i_35 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_2519,c_2418]) ).
cnf(c_5354,plain,
( i_35 = i1
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5353]) ).
cnf(c_2532,plain,
( i_35 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5354]) ).
cnf(c_2542,plain,
( select(a1,i1) = e_36
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2532,c_36]) ).
cnf(c_2543,plain,
( select(a2,i1) = e_37
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2532,c_38]) ).
cnf(c_5355,plain,
( e_31 = e_23
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2440,c_2287]) ).
cnf(c_5356,plain,
( e_31 = e_23
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5355]) ).
cnf(c_2568,plain,
( e_31 = e_23
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5356]) ).
cnf(c_2588,plain,
( e_33 = e_23
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2568,c_85]) ).
cnf(c_5357,plain,
( e_33 = e_25
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2441,c_2260]) ).
cnf(c_5358,plain,
( e_33 = e_25
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5357]) ).
cnf(c_2603,plain,
( e_33 = e_25
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5358]) ).
cnf(c_5359,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2603,c_2588]) ).
cnf(c_5360,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5359]) ).
cnf(c_5361,plain,
( e_25 = e_23
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5360]) ).
cnf(c_2630,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5361]) ).
cnf(c_5362,plain,
( i_35 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_2630,c_2418]) ).
cnf(c_5363,plain,
( i_35 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5362]) ).
cnf(c_2671,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5363]) ).
cnf(c_2681,plain,
( select(a1,i1) = e_36
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2671,c_36]) ).
cnf(c_2682,plain,
( select(a2,i1) = e_37
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2671,c_38]) ).
cnf(c_2720,plain,
( e_36 = e_21
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2542,c_22]) ).
cnf(c_2722,plain,
( e_37 != e_21
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2720,c_44]) ).
cnf(c_2725,plain,
( e_37 = e_19
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2543,c_20]) ).
cnf(c_5364,plain,
( e_19 != e_21
| i4 = i2
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2725,c_2722]) ).
cnf(c_5365,plain,
( e_21 != e_19
| i4 = i2
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5364]) ).
cnf(c_5366,plain,
( e_21 != e_19
| i4 = i2
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5365]) ).
cnf(c_5367,plain,
( e_21 != e_19
| i4 = i2
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5366]) ).
cnf(c_2729,plain,
( e_21 != e_19
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5367]) ).
cnf(c_5368,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2681,c_324]) ).
cnf(c_5369,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5368]) ).
cnf(c_5370,plain,
( e_36 = e_19
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5369]) ).
cnf(c_2744,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5370]) ).
cnf(c_2749,plain,
( e_37 != e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2744,c_44]) ).
cnf(c_2752,plain,
( e_37 = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2682,c_20]) ).
cnf(c_5371,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_2752,c_2749]) ).
cnf(c_5372,plain,
( i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5371]) ).
cnf(c_5373,plain,
( i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5372]) ).
cnf(c_2753,plain,
( i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5373]) ).
cnf(c_2756,plain,
( select(a_30,i1) = e_31
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2753,c_32]) ).
cnf(c_2757,plain,
( select(a_28,i1) = e_33
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2753,c_34]) ).
cnf(c_5374,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2756,c_147]) ).
cnf(c_5375,plain,
( e_31 = e_21
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5374]) ).
cnf(c_2808,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5375]) ).
cnf(c_2813,plain,
( e_33 = e_21
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2808,c_85]) ).
cnf(c_5376,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2757,c_134]) ).
cnf(c_5377,plain,
( e_33 = e_19
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5376]) ).
cnf(c_2838,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5377]) ).
cnf(c_5378,plain,
( e_19 = e_21
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2838,c_2813]) ).
cnf(c_5379,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5378]) ).
cnf(c_5380,plain,
( e_21 = e_19
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5379]) ).
cnf(c_2857,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5380]) ).
cnf(c_5381,plain,
( i4 = i2
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_2857,c_2729]) ).
cnf(c_5382,plain,
( i4 = i2
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5381]) ).
cnf(c_2869,plain,
( i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5382]) ).
cnf(c_5383,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2869,c_2753]) ).
cnf(c_5384,plain,
( i2 = i1
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5383]) ).
cnf(c_5385,plain,
( i2 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5384]) ).
cnf(c_2906,plain,
( i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5385]) ).
cnf(c_2907,plain,
( store(a_24,i1,e_27) = a_28
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2906,c_12]) ).
cnf(c_2908,plain,
( store(a_26,i1,e_29) = a_30
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2906,c_14]) ).
cnf(c_2909,plain,
( select(a_26,i1) = e_27
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2906,c_28]) ).
cnf(c_2910,plain,
( select(a_24,i1) = e_29
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2906,c_30]) ).
cnf(c_2911,plain,
( select(a_28,i1) = e_27
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2906,c_56]) ).
cnf(c_2912,plain,
( select(a_30,i1) = e_29
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2906,c_58]) ).
cnf(c_5386,plain,
( i_35 = i1
| i_35 = i2
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2906,c_613]) ).
cnf(c_2933,plain,
( i_35 = i2
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5386]) ).
cnf(c_2965,plain,
( select(a1,i2) = e_36
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2933,c_36]) ).
cnf(c_2966,plain,
( select(a2,i2) = e_37
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2933,c_38]) ).
cnf(c_5387,plain,
( e_27 = e_21
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2909,c_121]) ).
cnf(c_2980,plain,
( e_27 = e_21
| i2 = i1 ),
inference(copy,[status(thm)],[c_5387]) ).
cnf(c_2983,plain,
( select(a_28,i3) = e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2980,c_56]) ).
cnf(c_2986,plain,
( e_29 = e_21
| i4 = i3
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2980,c_168]) ).
cnf(c_5388,plain,
( e_29 = e_19
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2910,c_111]) ).
cnf(c_3007,plain,
( e_29 = e_19
| i2 = i1 ),
inference(copy,[status(thm)],[c_5388]) ).
cnf(c_3011,plain,
( select(a_30,i3) = e_19
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3007,c_58]) ).
cnf(c_5389,plain,
( e_19 = e_21
| i4 = i3
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3007,c_2986]) ).
cnf(c_5390,plain,
( e_21 = e_19
| i4 = i3
| i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5389]) ).
cnf(c_3027,plain,
( e_21 = e_19
| i4 = i3
| i2 = i1 ),
inference(copy,[status(thm)],[c_5390]) ).
cnf(c_3127,plain,
( select(a_30,i1) = e_27
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2911,c_181]) ).
cnf(c_5391,plain,
( select(a_30,i1) = e_19
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3007,c_2912]) ).
cnf(c_3146,plain,
( select(a_30,i1) = e_19
| i2 = i1 ),
inference(copy,[status(thm)],[c_5391]) ).
cnf(c_5392,plain,
( select(a_28,i2) = e_23
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2907,c_77]) ).
cnf(c_3172,plain,
( select(a_28,i2) = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_5392]) ).
cnf(c_3179,plain,
( select(a_30,i2) = e_23
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3172,c_181]) ).
cnf(c_5393,plain,
( select(a_30,i2) = e_25
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2908,c_78]) ).
cnf(c_3192,plain,
( select(a_30,i2) = e_25
| i2 = i1 ),
inference(copy,[status(thm)],[c_5393]) ).
cnf(c_5394,plain,
( e_36 = e_25
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2965,c_94]) ).
cnf(c_3220,plain,
( e_36 = e_25
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5394]) ).
cnf(c_3224,plain,
( e_37 != e_25
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3220,c_44]) ).
cnf(c_5395,plain,
( e_37 = e_23
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_2966,c_102]) ).
cnf(c_3238,plain,
( e_37 = e_23
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5395]) ).
cnf(c_5396,plain,
( e_23 != e_25
| i_35 = i1
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3238,c_3224]) ).
cnf(c_5397,plain,
( e_25 != e_23
| i_35 = i1
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5396]) ).
cnf(c_5398,plain,
( e_25 != e_23
| i_35 = i1
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5397]) ).
cnf(c_3247,plain,
( e_25 != e_23
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5398]) ).
cnf(c_5399,plain,
( e_27 = e_19
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3127,c_3146]) ).
cnf(c_3256,plain,
( e_27 = e_19
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5399]) ).
cnf(c_5400,plain,
( e_19 = e_21
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3256,c_2980]) ).
cnf(c_5401,plain,
( e_21 = e_19
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5400]) ).
cnf(c_3278,plain,
( e_21 = e_19
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5401]) ).
cnf(c_5402,plain,
( e_23 = e_25
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3179,c_3192]) ).
cnf(c_5403,plain,
( e_25 = e_23
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5402]) ).
cnf(c_3309,plain,
( e_25 = e_23
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5403]) ).
cnf(c_5404,plain,
( i_35 = i1
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3309,c_3247]) ).
cnf(c_3310,plain,
( i_35 = i1
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5404]) ).
cnf(c_3321,plain,
( select(a1,i1) = e_36
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3310,c_36]) ).
cnf(c_3322,plain,
( select(a2,i1) = e_37
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3310,c_38]) ).
cnf(c_3340,plain,
( e_36 = e_21
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3321,c_22]) ).
cnf(c_3344,plain,
( e_37 != e_21
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3340,c_44]) ).
cnf(c_5405,plain,
( e_37 != e_19
| i4 = i2
| i2 = i1
| i4 = i3
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3027,c_3344]) ).
cnf(c_3346,plain,
( e_37 != e_19
| i4 = i2
| i4 = i3
| i2 = i1 ),
inference(copy,[status(thm)],[c_5405]) ).
cnf(c_3353,plain,
( e_37 = e_19
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3322,c_20]) ).
cnf(c_5406,plain,
( i4 = i2
| i4 = i3
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3353,c_3346]) ).
cnf(c_5407,plain,
( i4 = i2
| i4 = i3
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5406]) ).
cnf(c_3355,plain,
( i4 = i3
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5407]) ).
cnf(c_5408,plain,
( e_19 != e_21
| i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3353,c_3344]) ).
cnf(c_5409,plain,
( e_21 != e_19
| i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5408]) ).
cnf(c_5410,plain,
( e_21 != e_19
| i4 = i2
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5409]) ).
cnf(c_3359,plain,
( e_21 != e_19
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5410]) ).
cnf(c_3418,plain,
( select(a_30,i3) = e_31
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3355,c_32]) ).
cnf(c_3419,plain,
( select(a_28,i3) = e_33
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3355,c_34]) ).
cnf(c_5411,plain,
( e_31 = e_19
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3418,c_3011]) ).
cnf(c_3543,plain,
( e_31 = e_19
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5411]) ).
cnf(c_3563,plain,
( e_33 = e_19
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3543,c_85]) ).
cnf(c_5412,plain,
( e_33 = e_21
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3419,c_2983]) ).
cnf(c_3579,plain,
( e_33 = e_21
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5412]) ).
cnf(c_5413,plain,
( e_21 = e_19
| i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3579,c_3563]) ).
cnf(c_5414,plain,
( e_21 = e_19
| i4 = i2
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5413]) ).
cnf(c_3606,plain,
( e_21 = e_19
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5414]) ).
cnf(c_5415,plain,
( i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3606,c_3359]) ).
cnf(c_5416,plain,
( i4 = i2
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5415]) ).
cnf(c_3653,plain,
( i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_5416]) ).
cnf(c_3656,plain,
( select(a_30,i2) = e_31
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3653,c_32]) ).
cnf(c_3657,plain,
( select(a_28,i2) = e_33
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3653,c_34]) ).
cnf(c_5417,plain,
( e_31 = e_25
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3656,c_3192]) ).
cnf(c_3703,plain,
( e_31 = e_25
| i2 = i1 ),
inference(copy,[status(thm)],[c_5417]) ).
cnf(c_3708,plain,
( e_33 = e_25
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3703,c_85]) ).
cnf(c_5418,plain,
( e_33 = e_23
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3657,c_3172]) ).
cnf(c_3726,plain,
( e_33 = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_5418]) ).
cnf(c_5419,plain,
( e_23 = e_25
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3726,c_3708]) ).
cnf(c_5420,plain,
( e_25 = e_23
| i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5419]) ).
cnf(c_3741,plain,
( e_25 = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_5420]) ).
cnf(c_5421,plain,
( i_35 = i1
| i2 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3741,c_3247]) ).
cnf(c_3749,plain,
( i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5421]) ).
cnf(c_3763,plain,
( select(a1,i1) = e_36
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3749,c_36]) ).
cnf(c_3764,plain,
( select(a2,i1) = e_37
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3749,c_38]) ).
cnf(c_3789,plain,
( e_36 = e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3763,c_22]) ).
cnf(c_3793,plain,
( e_37 != e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3789,c_44]) ).
cnf(c_5422,plain,
( e_37 != e_19
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3278,c_3793]) ).
cnf(c_3796,plain,
( e_37 != e_19
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5422]) ).
cnf(c_3802,plain,
( e_37 = e_19
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3764,c_20]) ).
cnf(c_5423,plain,
( i4 = i1
| i2 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3802,c_3796]) ).
cnf(c_3803,plain,
( i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5423]) ).
cnf(c_5424,plain,
( i1 = i2
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3803,c_3653]) ).
cnf(c_5425,plain,
( i2 = i1
| i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5424]) ).
cnf(c_5426,plain,
( i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_5425]) ).
cnf(c_3833,plain,
i2 = i1,
inference(copy,[status(thm)],[c_5426]) ).
cnf(c_3836,plain,
select(a_22,i1) = e_23,
inference(paramod,[status(thm)],[c_3833,c_24]) ).
cnf(c_3837,plain,
select(a_20,i1) = e_25,
inference(paramod,[status(thm)],[c_3833,c_26]) ).
cnf(c_5427,plain,
( i4 = i3
| i_35 = i1
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_3833,c_734]) ).
cnf(c_3858,plain,
( i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5427]) ).
cnf(c_3898,plain,
( select(a1,i1) = e_36
| i4 = i3 ),
inference(paramod,[status(thm)],[c_3858,c_36]) ).
cnf(c_3899,plain,
( select(a2,i1) = e_37
| i4 = i3 ),
inference(paramod,[status(thm)],[c_3858,c_38]) ).
cnf(c_3904,plain,
e_23 = e_21,
inference(paramod,[status(thm)],[c_3836,c_50]) ).
cnf(c_3907,plain,
select(a_24,i2) = e_21,
inference(paramod,[status(thm)],[c_3904,c_52]) ).
cnf(c_3908,plain,
( select(a_28,i2) = e_21
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3904,c_131]) ).
cnf(c_3910,plain,
( e_25 = e_21
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3904,c_234]) ).
cnf(c_3935,plain,
e_25 = e_19,
inference(paramod,[status(thm)],[c_3837,c_48]) ).
cnf(c_3939,plain,
select(a_26,i2) = e_19,
inference(paramod,[status(thm)],[c_3935,c_54]) ).
cnf(c_3940,plain,
( select(a_30,i2) = e_19
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3935,c_145]) ).
cnf(c_5428,plain,
( e_19 = e_21
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3935,c_3910]) ).
cnf(c_3963,plain,
( e_21 = e_19
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5428]) ).
cnf(c_5429,plain,
( i4 = i2
| i3 = i2
| i4 = i3
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_3963,c_845]) ).
cnf(c_5430,plain,
( i4 = i2
| i4 = i3
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5429]) ).
cnf(c_3968,plain,
( i4 = i3
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5430]) ).
cnf(c_3970,plain,
( select(a1,i1) = e_19
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3963,c_22]) ).
cnf(c_3975,plain,
( select(a_30,i3) = e_31
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3968,c_32]) ).
cnf(c_3976,plain,
( select(a_28,i3) = e_33
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3968,c_34]) ).
cnf(c_4101,plain,
( e_36 = e_21
| i4 = i3 ),
inference(paramod,[status(thm)],[c_3898,c_22]) ).
cnf(c_4103,plain,
( e_37 != e_21
| i4 = i3 ),
inference(paramod,[status(thm)],[c_4101,c_44]) ).
cnf(c_4106,plain,
( e_37 = e_19
| i4 = i3 ),
inference(paramod,[status(thm)],[c_3899,c_20]) ).
cnf(c_5431,plain,
( e_19 != e_21
| i4 = i3
| i4 = i3 ),
inference(paramod,[status(thm)],[c_4106,c_4103]) ).
cnf(c_5432,plain,
( e_21 != e_19
| i4 = i3
| i4 = i3 ),
inference(copy,[status(thm)],[c_5431]) ).
cnf(c_4110,plain,
( e_21 != e_19
| i4 = i3 ),
inference(copy,[status(thm)],[c_5432]) ).
cnf(c_4276,plain,
( e_31 = e_29
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3975,c_58]) ).
cnf(c_4280,plain,
( e_33 = e_29
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4276,c_85]) ).
cnf(c_4294,plain,
( e_33 = e_27
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3976,c_56]) ).
cnf(c_5433,plain,
( e_27 = e_29
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4294,c_4280]) ).
cnf(c_5434,plain,
( e_29 = e_27
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5433]) ).
cnf(c_5435,plain,
( e_29 = e_27
| i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5434]) ).
cnf(c_4305,plain,
( e_29 = e_27
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5435]) ).
cnf(c_4314,plain,
( i_35 = i2
| i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_4305,c_743]) ).
cnf(c_5436,plain,
( i_35 = i1
| i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3833,c_4314]) ).
cnf(c_4336,plain,
( i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5436]) ).
cnf(c_4337,plain,
( select(a1,i1) = e_36
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4336,c_36]) ).
cnf(c_4338,plain,
( select(a2,i1) = e_37
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4336,c_38]) ).
cnf(c_5437,plain,
( e_36 = e_19
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4337,c_3970]) ).
cnf(c_5438,plain,
( e_36 = e_19
| i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5437]) ).
cnf(c_4571,plain,
( e_36 = e_19
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5438]) ).
cnf(c_4576,plain,
( e_37 != e_19
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4571,c_44]) ).
cnf(c_4579,plain,
( e_37 = e_19
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4338,c_20]) ).
cnf(c_5439,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_4579,c_4576]) ).
cnf(c_5440,plain,
( i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5439]) ).
cnf(c_4580,plain,
( i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5440]) ).
cnf(c_4583,plain,
( select(a_30,i2) = e_31
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4580,c_32]) ).
cnf(c_4584,plain,
( select(a_28,i2) = e_33
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4580,c_34]) ).
cnf(c_5441,plain,
( e_31 = e_19
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4583,c_3940]) ).
cnf(c_4671,plain,
( e_31 = e_19
| i3 = i2 ),
inference(copy,[status(thm)],[c_5441]) ).
cnf(c_4693,plain,
( e_33 = e_19
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4671,c_85]) ).
cnf(c_5442,plain,
( e_33 = e_21
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4584,c_3908]) ).
cnf(c_4711,plain,
( e_33 = e_21
| i3 = i2 ),
inference(copy,[status(thm)],[c_5442]) ).
cnf(c_5443,plain,
( e_21 = e_19
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4711,c_4693]) ).
cnf(c_4741,plain,
( e_21 = e_19
| i3 = i2 ),
inference(copy,[status(thm)],[c_5443]) ).
cnf(c_4789,plain,
( i4 = i3
| i3 = i2 ),
inference(resolve,[status(thm)],[c_4741,c_4110]) ).
cnf(c_5444,plain,
( i3 = i2
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_4789,c_4580]) ).
cnf(c_5445,plain,
( i3 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_5444]) ).
cnf(c_4818,plain,
i3 = i2,
inference(copy,[status(thm)],[c_5445]) ).
cnf(c_4821,plain,
select(a_26,i2) = e_27,
inference(paramod,[status(thm)],[c_4818,c_28]) ).
cnf(c_4822,plain,
select(a_24,i2) = e_29,
inference(paramod,[status(thm)],[c_4818,c_30]) ).
cnf(c_5446,plain,
( i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_4818,c_613]) ).
cnf(c_4840,plain,
( i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_5446]) ).
cnf(c_5447,plain,
( i_35 = i1
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_3833,c_4840]) ).
cnf(c_4918,plain,
i_35 = i1,
inference(copy,[status(thm)],[c_5447]) ).
cnf(c_4919,plain,
select(a1,i1) = e_36,
inference(paramod,[status(thm)],[c_4918,c_36]) ).
cnf(c_4920,plain,
select(a2,i1) = e_37,
inference(paramod,[status(thm)],[c_4918,c_38]) ).
cnf(c_4926,plain,
e_27 = e_19,
inference(paramod,[status(thm)],[c_4821,c_3939]) ).
cnf(c_4947,plain,
select(a_28,i3) = e_19,
inference(paramod,[status(thm)],[c_4926,c_56]) ).
cnf(c_4949,plain,
( e_29 = e_19
| i4 = i3 ),
inference(paramod,[status(thm)],[c_4926,c_168]) ).
cnf(c_4965,plain,
e_29 = e_21,
inference(paramod,[status(thm)],[c_4822,c_3907]) ).
cnf(c_4987,plain,
select(a_30,i3) = e_21,
inference(paramod,[status(thm)],[c_4965,c_58]) ).
cnf(c_5001,plain,
( e_21 = e_19
| i4 = i3 ),
inference(paramod,[status(thm)],[c_4965,c_4949]) ).
cnf(c_5448,plain,
( i4 = i3
| i4 = i3 ),
inference(resolve,[status(thm)],[c_5001,c_4110]) ).
cnf(c_5031,plain,
i4 = i3,
inference(copy,[status(thm)],[c_5448]) ).
cnf(c_5034,plain,
select(a_30,i3) = e_31,
inference(paramod,[status(thm)],[c_5031,c_32]) ).
cnf(c_5035,plain,
select(a_28,i3) = e_33,
inference(paramod,[status(thm)],[c_5031,c_34]) ).
cnf(c_5121,plain,
e_36 = e_21,
inference(paramod,[status(thm)],[c_4919,c_22]) ).
cnf(c_5123,plain,
e_37 != e_21,
inference(paramod,[status(thm)],[c_5121,c_44]) ).
cnf(c_5126,plain,
e_37 = e_19,
inference(paramod,[status(thm)],[c_4920,c_20]) ).
cnf(c_5449,plain,
e_19 != e_21,
inference(paramod,[status(thm)],[c_5126,c_5123]) ).
cnf(c_5130,plain,
e_21 != e_19,
inference(copy,[status(thm)],[c_5449]) ).
cnf(c_5134,plain,
e_31 = e_21,
inference(paramod,[status(thm)],[c_5034,c_4987]) ).
cnf(c_5162,plain,
e_33 = e_21,
inference(paramod,[status(thm)],[c_5134,c_85]) ).
cnf(c_5174,plain,
e_33 = e_19,
inference(paramod,[status(thm)],[c_5035,c_4947]) ).
cnf(c_5450,plain,
e_19 = e_21,
inference(paramod,[status(thm)],[c_5174,c_5162]) ).
cnf(c_5451,plain,
e_21 = e_19,
inference(copy,[status(thm)],[c_5450]) ).
cnf(c_5213,plain,
$false,
inference(resolve,[status(thm)],[c_5130,c_5451]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV555-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n008.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 14:26:31 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.39 % Process 3853018 was started by sandbox on n008,
% 0.10/5.39 % Sat Sep 26 14:26:31 2026
% 0.10/5.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/5.39
% 0.10/5.39 % From the command line: assign(max_seconds, 300).
% 23.17/8.39
% 23.17/8.39 % given #500 (T,wt=32): 231 i4 = i3 | i3 = i2 | i3 = A | select(store(a_20,A,B),i3) = e_27. [para(172(c,1),2(b,2)),flip(c)].
% 23.17/8.39
% 23.17/8.39 % given #1000 (W,wt=14): 3354 i2 = i1 | i4 = i2 | i4 = i1. [resolve(3353,c,3347,d),merge(c),merge(e)].
% 23.17/8.39
% 23.17/8.39 % SZS status Unsatisfiable for theBenchmark
% 23.17/8.39
% 23.17/8.39 % Proof 1 at 2.52 (+ 0.33) seconds.
% 23.17/8.39 % Length of proof is 346.
% 23.17/8.39 % Level of proof is 137.
% 23.17/8.39 % Maximum clause weight is 33.000.
% 23.17/8.39 % Given clauses 1306.
% 23.17/8.39
% 23.17/8.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------