%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV565-1.004 : 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 : n017.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:30 AM UTC 2026
% Result : Unsatisfiable 24.85s 3.56s
% Output : CNFRefutation 24.85s
% 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_4,plain,
a_20 = store(a1,i1,e_19),
inference(clausify,[status(thm)],[hyp0]) ).
cnf(c_5,plain,
store(a1,i1,e_19) = a_20,
inference(copy,[status(thm)],[c_4]) ).
fof(hyp1,axiom,
a_22 = store(a2,i1,e_21),
file('theBenchmark.p',hyp1) ).
cnf(c_6,plain,
a_22 = store(a2,i1,e_21),
inference(clausify,[status(thm)],[hyp1]) ).
cnf(c_7,plain,
store(a2,i1,e_21) = a_22,
inference(copy,[status(thm)],[c_6]) ).
fof(hyp2,axiom,
a_24 = store(a_20,i2,e_23),
file('theBenchmark.p',hyp2) ).
cnf(c_8,plain,
a_24 = store(a_20,i2,e_23),
inference(clausify,[status(thm)],[hyp2]) ).
cnf(c_9,plain,
store(a_20,i2,e_23) = a_24,
inference(copy,[status(thm)],[c_8]) ).
fof(hyp3,axiom,
a_26 = store(a_22,i2,e_25),
file('theBenchmark.p',hyp3) ).
cnf(c_10,plain,
a_26 = store(a_22,i2,e_25),
inference(clausify,[status(thm)],[hyp3]) ).
cnf(c_11,plain,
store(a_22,i2,e_25) = a_26,
inference(copy,[status(thm)],[c_10]) ).
fof(hyp4,axiom,
a_28 = store(a_24,i3,e_27),
file('theBenchmark.p',hyp4) ).
cnf(c_12,plain,
a_28 = store(a_24,i3,e_27),
inference(clausify,[status(thm)],[hyp4]) ).
cnf(c_13,plain,
store(a_24,i3,e_27) = a_28,
inference(copy,[status(thm)],[c_12]) ).
fof(hyp5,axiom,
a_30 = store(a_26,i3,e_29),
file('theBenchmark.p',hyp5) ).
cnf(c_14,plain,
a_30 = store(a_26,i3,e_29),
inference(clausify,[status(thm)],[hyp5]) ).
cnf(c_15,plain,
store(a_26,i3,e_29) = a_30,
inference(copy,[status(thm)],[c_14]) ).
fof(hyp6,axiom,
a_32 = store(a_28,i4,e_31),
file('theBenchmark.p',hyp6) ).
cnf(c_16,plain,
a_32 = store(a_28,i4,e_31),
inference(clausify,[status(thm)],[hyp6]) ).
cnf(c_17,plain,
store(a_28,i4,e_31) = a_32,
inference(copy,[status(thm)],[c_16]) ).
fof(hyp7,axiom,
a_34 = store(a_30,i4,e_33),
file('theBenchmark.p',hyp7) ).
cnf(c_18,plain,
a_34 = store(a_30,i4,e_33),
inference(clausify,[status(thm)],[hyp7]) ).
cnf(c_19,plain,
store(a_30,i4,e_33) = a_34,
inference(copy,[status(thm)],[c_18]) ).
fof(hyp8,axiom,
e_19 = select(a2,i1),
file('theBenchmark.p',hyp8) ).
cnf(c_20,plain,
e_19 = select(a2,i1),
inference(clausify,[status(thm)],[hyp8]) ).
cnf(c_21,plain,
select(a2,i1) = e_19,
inference(copy,[status(thm)],[c_20]) ).
fof(hyp9,axiom,
e_21 = select(a1,i1),
file('theBenchmark.p',hyp9) ).
cnf(c_22,plain,
e_21 = select(a1,i1),
inference(clausify,[status(thm)],[hyp9]) ).
cnf(c_23,plain,
select(a1,i1) = e_21,
inference(copy,[status(thm)],[c_22]) ).
fof(hyp10,axiom,
e_23 = select(a_22,i2),
file('theBenchmark.p',hyp10) ).
cnf(c_24,plain,
e_23 = select(a_22,i2),
inference(clausify,[status(thm)],[hyp10]) ).
cnf(c_25,plain,
select(a_22,i2) = e_23,
inference(copy,[status(thm)],[c_24]) ).
fof(hyp11,axiom,
e_25 = select(a_20,i2),
file('theBenchmark.p',hyp11) ).
cnf(c_26,plain,
e_25 = select(a_20,i2),
inference(clausify,[status(thm)],[hyp11]) ).
cnf(c_27,plain,
select(a_20,i2) = e_25,
inference(copy,[status(thm)],[c_26]) ).
fof(hyp12,axiom,
e_27 = select(a_26,i3),
file('theBenchmark.p',hyp12) ).
cnf(c_28,plain,
e_27 = select(a_26,i3),
inference(clausify,[status(thm)],[hyp12]) ).
cnf(c_29,plain,
select(a_26,i3) = e_27,
inference(copy,[status(thm)],[c_28]) ).
fof(hyp13,axiom,
e_29 = select(a_24,i3),
file('theBenchmark.p',hyp13) ).
cnf(c_30,plain,
e_29 = select(a_24,i3),
inference(clausify,[status(thm)],[hyp13]) ).
cnf(c_31,plain,
select(a_24,i3) = e_29,
inference(copy,[status(thm)],[c_30]) ).
fof(hyp14,axiom,
e_31 = select(a_30,i4),
file('theBenchmark.p',hyp14) ).
cnf(c_32,plain,
e_31 = select(a_30,i4),
inference(clausify,[status(thm)],[hyp14]) ).
cnf(c_33,plain,
select(a_30,i4) = e_31,
inference(copy,[status(thm)],[c_32]) ).
fof(hyp15,axiom,
e_33 = select(a_28,i4),
file('theBenchmark.p',hyp15) ).
cnf(c_34,plain,
e_33 = select(a_28,i4),
inference(clausify,[status(thm)],[hyp15]) ).
cnf(c_35,plain,
select(a_28,i4) = e_33,
inference(copy,[status(thm)],[c_34]) ).
fof(hyp16,axiom,
e_36 = select(a1,i_35),
file('theBenchmark.p',hyp16) ).
cnf(c_36,plain,
e_36 = select(a1,i_35),
inference(clausify,[status(thm)],[hyp16]) ).
cnf(c_37,plain,
select(a1,i_35) = e_36,
inference(copy,[status(thm)],[c_36]) ).
fof(hyp17,axiom,
e_37 = select(a2,i_35),
file('theBenchmark.p',hyp17) ).
cnf(c_38,plain,
e_37 = select(a2,i_35),
inference(clausify,[status(thm)],[hyp17]) ).
cnf(c_39,plain,
select(a2,i_35) = e_37,
inference(copy,[status(thm)],[c_38]) ).
fof(hyp19,axiom,
a_32 = a_34,
file('theBenchmark.p',hyp19) ).
cnf(c_42,plain,
a_32 = a_34,
inference(clausify,[status(thm)],[hyp19]) ).
cnf(c_43,plain,
a_34 = a_32,
inference(copy,[status(thm)],[c_42]) ).
fof(goal,axiom,
e_36 != e_37,
file('theBenchmark.p',goal) ).
cnf(c_44,plain,
e_36 != e_37,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_45,plain,
e_37 != e_36,
inference(copy,[status(thm)],[c_44]) ).
cnf(c_55,plain,
select(a_20,i1) = e_19,
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_56,plain,
( select(a_20,A) = select(a1,A)
| i1 = A ),
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_57,plain,
select(a_22,i1) = e_21,
inference(paramod,[status(thm)],[c_7,c_1]) ).
cnf(c_58,plain,
( select(a_22,A) = select(a2,A)
| i1 = A ),
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_59,plain,
select(a_24,i2) = e_23,
inference(paramod,[status(thm)],[c_9,c_1]) ).
cnf(c_60,plain,
( select(a_24,A) = select(a_20,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_9,c_2]) ).
cnf(c_61,plain,
select(a_26,i2) = e_25,
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_62,plain,
( select(a_26,A) = select(a_22,A)
| i2 = A ),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_63,plain,
select(a_28,i3) = e_27,
inference(paramod,[status(thm)],[c_13,c_1]) ).
cnf(c_64,plain,
( select(a_28,A) = select(a_24,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_65,plain,
select(a_30,i3) = e_29,
inference(paramod,[status(thm)],[c_15,c_1]) ).
cnf(c_66,plain,
( select(a_30,A) = select(a_26,A)
| i3 = A ),
inference(paramod,[status(thm)],[c_15,c_2]) ).
cnf(c_67,plain,
select(a_32,i4) = e_31,
inference(paramod,[status(thm)],[c_17,c_1]) ).
cnf(c_68,plain,
( select(a_32,A) = select(a_28,A)
| i4 = A ),
inference(paramod,[status(thm)],[c_17,c_2]) ).
cnf(c_69,plain,
select(a_34,i4) = e_33,
inference(paramod,[status(thm)],[c_19,c_1]) ).
cnf(c_70,plain,
( select(a_34,A) = select(a_30,A)
| i4 = A ),
inference(paramod,[status(thm)],[c_19,c_2]) ).
cnf(c_101,plain,
store(a_30,i4,e_33) = a_32,
inference(paramod,[status(thm)],[c_43,c_19]) ).
cnf(c_7039,plain,
( select(store(a_24,A,B),i2) = e_23
| A = i2 ),
inference(paramod,[status(thm)],[c_59,c_2]) ).
cnf(c_108,plain,
( select(store(a_24,A,B),i2) = e_23
| i2 = A ),
inference(copy,[status(thm)],[c_7039]) ).
cnf(c_7040,plain,
( select(store(a_26,A,B),i2) = e_25
| A = i2 ),
inference(paramod,[status(thm)],[c_61,c_2]) ).
cnf(c_111,plain,
( select(store(a_26,A,B),i2) = e_25
| i2 = A ),
inference(copy,[status(thm)],[c_7040]) ).
cnf(c_126,plain,
select(a_32,i4) = e_33,
inference(paramod,[status(thm)],[c_43,c_69]) ).
cnf(c_130,plain,
e_33 = e_31,
inference(paramod,[status(thm)],[c_126,c_67]) ).
cnf(c_132,plain,
select(a_28,i4) = e_31,
inference(paramod,[status(thm)],[c_130,c_35]) ).
cnf(c_140,plain,
( select(a_32,A) = select(a_30,A)
| i4 = A ),
inference(paramod,[status(thm)],[c_101,c_2]) ).
cnf(c_7041,plain,
( select(a1,i2) = e_25
| i1 = i2 ),
inference(paramod,[status(thm)],[c_56,c_27]) ).
cnf(c_145,plain,
( select(a1,i2) = e_25
| i2 = i1 ),
inference(copy,[status(thm)],[c_7041]) ).
cnf(c_7042,plain,
( select(a_20,i_35) = e_36
| i1 = i_35 ),
inference(paramod,[status(thm)],[c_37,c_56]) ).
cnf(c_146,plain,
( select(a_20,i_35) = e_36
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7042]) ).
cnf(c_7043,plain,
( select(a2,i2) = e_23
| i1 = i2 ),
inference(paramod,[status(thm)],[c_58,c_25]) ).
cnf(c_159,plain,
( select(a2,i2) = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_7043]) ).
cnf(c_7044,plain,
( select(a_22,i_35) = e_37
| i1 = i_35 ),
inference(paramod,[status(thm)],[c_39,c_58]) ).
cnf(c_160,plain,
( select(a_22,i_35) = e_37
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7044]) ).
cnf(c_174,plain,
( select(a_24,i1) = e_19
| i2 = i1 ),
inference(paramod,[status(thm)],[c_55,c_60]) ).
cnf(c_7045,plain,
( select(a_24,i_35) = e_36
| i2 = i_35
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_146,c_60]) ).
cnf(c_176,plain,
( select(a_24,i_35) = e_36
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7045]) ).
cnf(c_190,plain,
( select(a_26,i1) = e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_57,c_62]) ).
cnf(c_7046,plain,
( select(a_26,i_35) = e_37
| i2 = i_35
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_160,c_62]) ).
cnf(c_192,plain,
( select(a_26,i_35) = e_37
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7046]) ).
cnf(c_206,plain,
( select(a_28,i2) = e_23
| i3 = i2 ),
inference(paramod,[status(thm)],[c_59,c_64]) ).
cnf(c_209,plain,
( select(a_28,i1) = e_19
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_174,c_64]) ).
cnf(c_228,plain,
( select(a_30,i2) = e_25
| i3 = i2 ),
inference(paramod,[status(thm)],[c_61,c_66]) ).
cnf(c_230,plain,
( select(a_30,i1) = e_21
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_190,c_66]) ).
cnf(c_243,plain,
( select(a_32,i3) = e_27
| i4 = i3 ),
inference(paramod,[status(thm)],[c_63,c_68]) ).
cnf(c_244,plain,
( select(a_32,A) = select(a_24,A)
| i4 = A
| i3 = A ),
inference(paramod,[status(thm)],[c_64,c_68]) ).
cnf(c_245,plain,
( select(a_32,i2) = e_23
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_206,c_68]) ).
cnf(c_253,plain,
( select(a_34,i3) = e_29
| i4 = i3 ),
inference(paramod,[status(thm)],[c_65,c_70]) ).
cnf(c_260,plain,
( select(a_32,i3) = e_29
| i4 = i3 ),
inference(paramod,[status(thm)],[c_43,c_253]) ).
cnf(c_7047,plain,
( e_29 = e_27
| i4 = i3
| i4 = i3 ),
inference(paramod,[status(thm)],[c_260,c_243]) ).
cnf(c_265,plain,
( e_29 = e_27
| i4 = i3 ),
inference(copy,[status(thm)],[c_7047]) ).
cnf(c_286,plain,
( select(a_32,A) = select(a_26,A)
| i4 = A
| i3 = A ),
inference(paramod,[status(thm)],[c_66,c_140]) ).
cnf(c_287,plain,
( select(a_32,i2) = e_25
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_228,c_140]) ).
cnf(c_7048,plain,
( select(a_30,A) = select(a_28,A)
| i4 = A
| i4 = A ),
inference(paramod,[status(thm)],[c_140,c_68]) ).
cnf(c_288,plain,
( select(a_30,A) = select(a_28,A)
| i4 = A ),
inference(copy,[status(thm)],[c_7048]) ).
cnf(c_7049,plain,
( select(a_28,i_35) = e_36
| i3 = i_35
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_176,c_64]) ).
cnf(c_308,plain,
( select(a_28,i_35) = e_36
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7049]) ).
cnf(c_7050,plain,
( select(a_30,i_35) = e_37
| i3 = i_35
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_192,c_66]) ).
cnf(c_320,plain,
( select(a_30,i_35) = e_37
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7050]) ).
cnf(c_332,plain,
( select(a_30,i1) = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_209,c_288]) ).
cnf(c_7051,plain,
( e_25 = e_23
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_287,c_245]) ).
cnf(c_7052,plain,
( e_25 = e_23
| i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7051]) ).
cnf(c_371,plain,
( e_25 = e_23
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7052]) ).
cnf(c_375,plain,
( select(a1,i2) = e_23
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_371,c_145]) ).
cnf(c_7053,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_176,c_244]) ).
cnf(c_7054,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_7053]) ).
cnf(c_426,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_7054]) ).
cnf(c_7055,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_192,c_286]) ).
cnf(c_7056,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_7055]) ).
cnf(c_440,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_7056]) ).
cnf(c_7057,plain,
( e_19 = e_21
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_332,c_230]) ).
cnf(c_7058,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7057]) ).
cnf(c_7059,plain,
( e_21 = e_19
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7058]) ).
cnf(c_502,plain,
( e_21 = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7059]) ).
cnf(c_505,plain,
( select(a1,i1) = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_502,c_23]) ).
cnf(c_7060,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_440,c_426]) ).
cnf(c_7061,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_7060]) ).
cnf(c_7062,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_7061]) ).
cnf(c_7063,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_7062]) ).
cnf(c_7064,plain,
( e_37 = e_36
| i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7063]) ).
cnf(c_764,plain,
( i_35 = i4
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_45,c_7064]) ).
cnf(c_7065,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_764,c_308]) ).
cnf(c_7066,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_7065]) ).
cnf(c_7067,plain,
( select(a_28,i4) = e_36
| i_35 = i3
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7066]) ).
cnf(c_772,plain,
( select(a_28,i4) = e_36
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7067]) ).
cnf(c_7068,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_764,c_320]) ).
cnf(c_7069,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_7068]) ).
cnf(c_7070,plain,
( select(a_30,i4) = e_37
| i_35 = i3
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7069]) ).
cnf(c_773,plain,
( select(a_30,i4) = e_37
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7070]) ).
cnf(c_893,plain,
( e_36 = e_31
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_772,c_132]) ).
cnf(c_908,plain,
( e_37 != e_31
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_893,c_45]) ).
cnf(c_923,plain,
( e_37 = e_31
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_773,c_33]) ).
cnf(c_7071,plain,
( i_35 = i3
| i_35 = i2
| i_35 = i1
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_923,c_908]) ).
cnf(c_7072,plain,
( i_35 = i3
| i_35 = i2
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7071]) ).
cnf(c_7073,plain,
( i_35 = i3
| i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7072]) ).
cnf(c_924,plain,
( i_35 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7073]) ).
cnf(c_7074,plain,
( select(a_24,i3) = e_36
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_924,c_176]) ).
cnf(c_7075,plain,
( select(a_24,i3) = e_36
| i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7074]) ).
cnf(c_930,plain,
( select(a_24,i3) = e_36
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7075]) ).
cnf(c_7076,plain,
( select(a_26,i3) = e_37
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_924,c_192]) ).
cnf(c_7077,plain,
( select(a_26,i3) = e_37
| i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7076]) ).
cnf(c_931,plain,
( select(a_26,i3) = e_37
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7077]) ).
cnf(c_1031,plain,
( e_36 = e_29
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_930,c_31]) ).
cnf(c_1034,plain,
( e_37 != e_29
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1031,c_45]) ).
cnf(c_1043,plain,
( e_37 != e_27
| i_35 = i2
| i_35 = i1
| i4 = i3 ),
inference(paramod,[status(thm)],[c_265,c_1034]) ).
cnf(c_1056,plain,
( e_37 = e_27
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_931,c_29]) ).
cnf(c_7078,plain,
( i_35 = i2
| i_35 = i1
| i4 = i3
| i_35 = i2
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_1056,c_1043]) ).
cnf(c_7079,plain,
( i_35 = i2
| i4 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7078]) ).
cnf(c_1057,plain,
( i4 = i3
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7079]) ).
cnf(c_7080,plain,
( e_27 != e_29
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1056,c_1034]) ).
cnf(c_7081,plain,
( e_29 != e_27
| i_35 = i2
| i_35 = i1
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7080]) ).
cnf(c_7082,plain,
( e_29 != e_27
| i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7081]) ).
cnf(c_1066,plain,
( e_29 != e_27
| i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7082]) ).
cnf(c_7083,plain,
( select(a_20,i2) = e_36
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1057,c_146]) ).
cnf(c_1072,plain,
( select(a_20,i2) = e_36
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7083]) ).
cnf(c_7084,plain,
( select(a_22,i2) = e_37
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1057,c_160]) ).
cnf(c_1073,plain,
( select(a_22,i2) = e_37
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7084]) ).
cnf(c_1146,plain,
( e_36 = e_25
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1072,c_27]) ).
cnf(c_1149,plain,
( e_37 != e_25
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1146,c_45]) ).
cnf(c_1155,plain,
( e_37 != e_23
| i4 = i3
| i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_371,c_1149]) ).
cnf(c_1165,plain,
( e_37 = e_23
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1073,c_25]) ).
cnf(c_7085,plain,
( i4 = i3
| i_35 = i1
| i4 = i2
| i3 = i2
| i4 = i3
| i_35 = i1 ),
inference(resolve,[status(thm)],[c_1165,c_1155]) ).
cnf(c_7086,plain,
( i4 = i3
| i4 = i2
| i3 = i2
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7085]) ).
cnf(c_1166,plain,
( i4 = i2
| i3 = i2
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7086]) ).
cnf(c_7087,plain,
( e_23 != e_25
| i4 = i3
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_1165,c_1149]) ).
cnf(c_7088,plain,
( e_25 != e_23
| i4 = i3
| i_35 = i1
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7087]) ).
cnf(c_7089,plain,
( e_25 != e_23
| i4 = i3
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7088]) ).
cnf(c_1173,plain,
( e_25 != e_23
| i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7089]) ).
cnf(c_1175,plain,
( select(a1,i1) = e_36
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_1166,c_37]) ).
cnf(c_1176,plain,
( select(a2,i1) = e_37
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_1166,c_39]) ).
cnf(c_1199,plain,
( e_36 = e_21
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_1175,c_23]) ).
cnf(c_1202,plain,
( e_37 != e_21
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_1199,c_45]) ).
cnf(c_1208,plain,
( e_37 = e_19
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_1176,c_21]) ).
cnf(c_7090,plain,
( e_19 != e_21
| i4 = i2
| i3 = i2
| i4 = i3
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(paramod,[status(thm)],[c_1208,c_1202]) ).
cnf(c_7091,plain,
( e_21 != e_19
| i4 = i2
| i3 = i2
| i4 = i3
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_7090]) ).
cnf(c_7092,plain,
( e_21 != e_19
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_7091]) ).
cnf(c_7093,plain,
( e_21 != e_19
| i4 = i2
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_7092]) ).
cnf(c_1212,plain,
( e_21 != e_19
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(copy,[status(thm)],[c_7093]) ).
cnf(c_1213,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2
| i4 = i3 ),
inference(resolve,[status(thm)],[c_1212,c_502]) ).
cnf(c_1216,plain,
( select(a_30,i3) = e_31
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1213,c_33]) ).
cnf(c_1217,plain,
( select(a_28,i3) = e_33
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1213,c_35]) ).
cnf(c_1836,plain,
( e_31 = e_29
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1216,c_65]) ).
cnf(c_1840,plain,
( e_33 = e_29
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1836,c_130]) ).
cnf(c_1860,plain,
( e_33 = e_27
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1217,c_63]) ).
cnf(c_7094,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_1860,c_1840]) ).
cnf(c_7095,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_7094]) ).
cnf(c_7096,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_7095]) ).
cnf(c_7097,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_7096]) ).
cnf(c_7098,plain,
( e_29 = e_27
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7097]) ).
cnf(c_7099,plain,
( e_29 = e_27
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7098]) ).
cnf(c_1871,plain,
( e_29 = e_27
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7099]) ).
cnf(c_1884,plain,
( i_35 = i2
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_1871,c_1066]) ).
cnf(c_1900,plain,
( select(a1,i2) = e_36
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1884,c_37]) ).
cnf(c_1901,plain,
( select(a2,i2) = e_37
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_1884,c_39]) ).
cnf(c_7100,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_1900,c_375]) ).
cnf(c_7101,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_7100]) ).
cnf(c_7102,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_7101]) ).
cnf(c_2643,plain,
( e_36 = e_23
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7102]) ).
cnf(c_2653,plain,
( e_37 != e_23
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2643,c_45]) ).
cnf(c_7103,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_1901,c_159]) ).
cnf(c_2662,plain,
( e_37 = e_23
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7103]) ).
cnf(c_7104,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_2662,c_2653]) ).
cnf(c_7105,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_7104]) ).
cnf(c_7106,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_7105]) ).
cnf(c_7107,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_7106]) ).
cnf(c_7108,plain,
( i_35 = i1
| i4 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7107]) ).
cnf(c_7109,plain,
( i_35 = i1
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7108]) ).
cnf(c_2664,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7109]) ).
cnf(c_2665,plain,
( select(a1,i1) = e_36
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2664,c_37]) ).
cnf(c_2666,plain,
( select(a2,i1) = e_37
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2664,c_39]) ).
cnf(c_7110,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_2665,c_505]) ).
cnf(c_7111,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7110]) ).
cnf(c_7112,plain,
( e_36 = e_19
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7111]) ).
cnf(c_2674,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7112]) ).
cnf(c_2679,plain,
( e_37 != e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2674,c_45]) ).
cnf(c_2684,plain,
( e_37 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2666,c_21]) ).
cnf(c_7113,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_2684,c_2679]) ).
cnf(c_7114,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7113]) ).
cnf(c_7115,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7114]) ).
cnf(c_7116,plain,
( i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7115]) ).
cnf(c_7117,plain,
( i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7116]) ).
cnf(c_2685,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7117]) ).
cnf(c_2688,plain,
( select(a_30,i2) = e_31
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2685,c_33]) ).
cnf(c_2689,plain,
( select(a_28,i2) = e_33
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2685,c_35]) ).
cnf(c_7118,plain,
( e_31 = e_25
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2688,c_228]) ).
cnf(c_2744,plain,
( e_31 = e_25
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7118]) ).
cnf(c_2748,plain,
( e_33 = e_25
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2744,c_130]) ).
cnf(c_7119,plain,
( e_33 = e_23
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2689,c_206]) ).
cnf(c_2773,plain,
( e_33 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7119]) ).
cnf(c_7120,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_2773,c_2748]) ).
cnf(c_7121,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_7120]) ).
cnf(c_7122,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7121]) ).
cnf(c_7123,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7122]) ).
cnf(c_7124,plain,
( e_25 = e_23
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7123]) ).
cnf(c_2787,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7124]) ).
cnf(c_2801,plain,
( i4 = i3
| i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(resolve,[status(thm)],[c_2787,c_1173]) ).
cnf(c_2815,plain,
( select(a1,i1) = e_36
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2801,c_37]) ).
cnf(c_2816,plain,
( select(a2,i1) = e_37
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2801,c_39]) ).
cnf(c_7125,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_2815,c_505]) ).
cnf(c_7126,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7125]) ).
cnf(c_7127,plain,
( e_36 = e_19
| i4 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7126]) ).
cnf(c_2996,plain,
( e_36 = e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7127]) ).
cnf(c_3001,plain,
( e_37 != e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2996,c_45]) ).
cnf(c_3006,plain,
( e_37 = e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_2816,c_21]) ).
cnf(c_7128,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_3006,c_3001]) ).
cnf(c_7129,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7128]) ).
cnf(c_7130,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7129]) ).
cnf(c_7131,plain,
( i4 = i3
| i4 = i1
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7130]) ).
cnf(c_7132,plain,
( i4 = i3
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7131]) ).
cnf(c_3007,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7132]) ).
cnf(c_7133,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3007,c_2685]) ).
cnf(c_7134,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7133]) ).
cnf(c_7135,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7134]) ).
cnf(c_7136,plain,
( i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7135]) ).
cnf(c_7137,plain,
( i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7136]) ).
cnf(c_3032,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7137]) ).
cnf(c_3035,plain,
( select(a_30,i1) = e_31
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3032,c_33]) ).
cnf(c_3036,plain,
( select(a_28,i1) = e_33
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3032,c_35]) ).
cnf(c_7138,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3035,c_230]) ).
cnf(c_7139,plain,
( e_31 = e_21
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7138]) ).
cnf(c_3096,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7139]) ).
cnf(c_3101,plain,
( e_33 = e_21
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3096,c_130]) ).
cnf(c_7140,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3036,c_209]) ).
cnf(c_7141,plain,
( e_33 = e_19
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7140]) ).
cnf(c_3128,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7141]) ).
cnf(c_7142,plain,
( e_19 = e_21
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3128,c_3101]) ).
cnf(c_7143,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7142]) ).
cnf(c_7144,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7143]) ).
cnf(c_7145,plain,
( e_21 = e_19
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7144]) ).
cnf(c_3147,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7145]) ).
cnf(c_7146,plain,
( i4 = i2
| i3 = i2
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(resolve,[status(thm)],[c_3147,c_1212]) ).
cnf(c_3159,plain,
( i4 = i2
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7146]) ).
cnf(c_7147,plain,
( i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3159,c_3032]) ).
cnf(c_7148,plain,
( i3 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7147]) ).
cnf(c_7149,plain,
( i3 = i1
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7148]) ).
cnf(c_7150,plain,
( i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7149]) ).
cnf(c_3195,plain,
( i4 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7150]) ).
cnf(c_7151,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(paramod,[status(thm)],[c_3195,c_3032]) ).
cnf(c_7152,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7151]) ).
cnf(c_7153,plain,
( i2 = i1
| i3 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7152]) ).
cnf(c_7154,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7153]) ).
cnf(c_3236,plain,
( i3 = i1
| i2 = i1
| i3 = i2 ),
inference(copy,[status(thm)],[c_7154]) ).
cnf(c_3239,plain,
( select(a_26,i2) = e_27
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3236,c_29]) ).
cnf(c_3240,plain,
( select(a_24,i2) = e_29
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3236,c_31]) ).
cnf(c_3241,plain,
( select(a_28,i2) = e_27
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3236,c_63]) ).
cnf(c_3242,plain,
( select(a_30,i2) = e_29
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3236,c_65]) ).
cnf(c_7155,plain,
( i_35 = i2
| i_35 = i2
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3236,c_924]) ).
cnf(c_3258,plain,
( i_35 = i2
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7155]) ).
cnf(c_3296,plain,
( select(a1,i2) = e_36
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3258,c_37]) ).
cnf(c_3297,plain,
( select(a2,i2) = e_37
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3258,c_39]) ).
cnf(c_3312,plain,
( e_27 = e_25
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3239,c_61]) ).
cnf(c_3315,plain,
( select(a_28,i3) = e_25
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3312,c_63]) ).
cnf(c_3317,plain,
( e_29 = e_25
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3312,c_265]) ).
cnf(c_3340,plain,
( e_29 = e_23
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3240,c_59]) ).
cnf(c_3344,plain,
( select(a_30,i3) = e_23
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3340,c_65]) ).
cnf(c_7156,plain,
( e_23 = e_25
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3340,c_3317]) ).
cnf(c_7157,plain,
( e_25 = e_23
| i4 = i3
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7156]) ).
cnf(c_7158,plain,
( e_25 = e_23
| i4 = i3
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7157]) ).
cnf(c_3357,plain,
( e_25 = e_23
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7158]) ).
cnf(c_7159,plain,
( i4 = i3
| i_35 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3357,c_1173]) ).
cnf(c_3368,plain,
( i_35 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7159]) ).
cnf(c_3378,plain,
( select(a1,i1) = e_36
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3368,c_37]) ).
cnf(c_3379,plain,
( select(a2,i1) = e_37
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3368,c_39]) ).
cnf(c_3387,plain,
( select(a_30,i2) = e_27
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3241,c_288]) ).
cnf(c_7160,plain,
( select(a_30,i2) = e_23
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3340,c_3242]) ).
cnf(c_7161,plain,
( select(a_30,i2) = e_23
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7160]) ).
cnf(c_3411,plain,
( select(a_30,i2) = e_23
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7161]) ).
cnf(c_7162,plain,
( e_36 = e_25
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3296,c_145]) ).
cnf(c_3489,plain,
( e_36 = e_25
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7162]) ).
cnf(c_3492,plain,
( e_37 != e_25
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3489,c_45]) ).
cnf(c_7163,plain,
( e_37 = e_23
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3297,c_159]) ).
cnf(c_3501,plain,
( e_37 = e_23
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7163]) ).
cnf(c_7164,plain,
( e_23 != e_25
| i_35 = i1
| i3 = i1
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3501,c_3492]) ).
cnf(c_7165,plain,
( e_25 != e_23
| i_35 = i1
| i3 = i1
| i2 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7164]) ).
cnf(c_7166,plain,
( e_25 != e_23
| i_35 = i1
| i3 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7165]) ).
cnf(c_7167,plain,
( e_25 != e_23
| i_35 = i1
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7166]) ).
cnf(c_3509,plain,
( e_25 != e_23
| i_35 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7167]) ).
cnf(c_3544,plain,
( e_36 = e_21
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3378,c_23]) ).
cnf(c_3547,plain,
( e_37 != e_21
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3544,c_45]) ).
cnf(c_7168,plain,
( e_37 != e_19
| i4 = i3
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_502,c_3547]) ).
cnf(c_7169,plain,
( e_37 != e_19
| i4 = i3
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7168]) ).
cnf(c_3549,plain,
( e_37 != e_19
| i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7169]) ).
cnf(c_3555,plain,
( e_37 = e_19
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3379,c_21]) ).
cnf(c_7170,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3555,c_3549]) ).
cnf(c_7171,plain,
( i4 = i3
| i4 = i1
| i3 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7170]) ).
cnf(c_7172,plain,
( i4 = i3
| i4 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7171]) ).
cnf(c_3556,plain,
( i4 = i1
| i4 = i3
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7172]) ).
cnf(c_3563,plain,
( select(a_30,i3) = e_31
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3556,c_33]) ).
cnf(c_3564,plain,
( select(a_28,i3) = e_33
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3556,c_35]) ).
cnf(c_7173,plain,
( e_27 = e_23
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3387,c_3411]) ).
cnf(c_7174,plain,
( e_27 = e_23
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7173]) ).
cnf(c_3629,plain,
( e_27 = e_23
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7174]) ).
cnf(c_7175,plain,
( e_23 = e_25
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3629,c_3312]) ).
cnf(c_7176,plain,
( e_25 = e_23
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7175]) ).
cnf(c_7177,plain,
( e_25 = e_23
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7176]) ).
cnf(c_3646,plain,
( e_25 = e_23
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7177]) ).
cnf(c_7178,plain,
( i_35 = i1
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3646,c_3509]) ).
cnf(c_7179,plain,
( i_35 = i1
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7178]) ).
cnf(c_3659,plain,
( i_35 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7179]) ).
cnf(c_3669,plain,
( select(a1,i1) = e_36
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3659,c_37]) ).
cnf(c_3670,plain,
( select(a2,i1) = e_37
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3659,c_39]) ).
cnf(c_7180,plain,
( e_31 = e_23
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3563,c_3344]) ).
cnf(c_7181,plain,
( e_31 = e_23
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7180]) ).
cnf(c_3741,plain,
( e_31 = e_23
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7181]) ).
cnf(c_3761,plain,
( e_33 = e_23
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3741,c_130]) ).
cnf(c_7182,plain,
( e_33 = e_25
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3564,c_3315]) ).
cnf(c_7183,plain,
( e_33 = e_25
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7182]) ).
cnf(c_3778,plain,
( e_33 = e_25
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7183]) ).
cnf(c_7184,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3778,c_3761]) ).
cnf(c_7185,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7184]) ).
cnf(c_7186,plain,
( e_25 = e_23
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7185]) ).
cnf(c_3805,plain,
( e_25 = e_23
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7186]) ).
cnf(c_7187,plain,
( i_35 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_3805,c_3509]) ).
cnf(c_7188,plain,
( i_35 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7187]) ).
cnf(c_3846,plain,
( i_35 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7188]) ).
cnf(c_3856,plain,
( select(a1,i1) = e_36
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3846,c_37]) ).
cnf(c_3857,plain,
( select(a2,i1) = e_37
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3846,c_39]) ).
cnf(c_3943,plain,
( e_36 = e_21
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3669,c_23]) ).
cnf(c_3945,plain,
( e_37 != e_21
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3943,c_45]) ).
cnf(c_3950,plain,
( e_37 = e_19
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3670,c_21]) ).
cnf(c_7189,plain,
( e_19 != e_21
| i4 = i2
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3950,c_3945]) ).
cnf(c_7190,plain,
( e_21 != e_19
| i4 = i2
| i3 = i1
| i2 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7189]) ).
cnf(c_7191,plain,
( e_21 != e_19
| i4 = i2
| i3 = i1
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7190]) ).
cnf(c_7192,plain,
( e_21 != e_19
| i4 = i2
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7191]) ).
cnf(c_3954,plain,
( e_21 != e_19
| i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7192]) ).
cnf(c_7193,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3856,c_505]) ).
cnf(c_7194,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7193]) ).
cnf(c_7195,plain,
( e_36 = e_19
| i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7194]) ).
cnf(c_4033,plain,
( e_36 = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7195]) ).
cnf(c_4038,plain,
( e_37 != e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4033,c_45]) ).
cnf(c_4043,plain,
( e_37 = e_19
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_3857,c_21]) ).
cnf(c_7196,plain,
( i4 = i1
| i3 = i1
| i2 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_4043,c_4038]) ).
cnf(c_7197,plain,
( i4 = i1
| i3 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7196]) ).
cnf(c_7198,plain,
( i4 = i1
| i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7197]) ).
cnf(c_4044,plain,
( i4 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7198]) ).
cnf(c_4047,plain,
( select(a_30,i1) = e_31
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4044,c_33]) ).
cnf(c_4048,plain,
( select(a_28,i1) = e_33
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4044,c_35]) ).
cnf(c_7199,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4047,c_230]) ).
cnf(c_7200,plain,
( e_31 = e_21
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7199]) ).
cnf(c_4101,plain,
( e_31 = e_21
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7200]) ).
cnf(c_4106,plain,
( e_33 = e_21
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4101,c_130]) ).
cnf(c_7201,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4048,c_209]) ).
cnf(c_7202,plain,
( e_33 = e_19
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7201]) ).
cnf(c_4133,plain,
( e_33 = e_19
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7202]) ).
cnf(c_7203,plain,
( e_19 = e_21
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4133,c_4106]) ).
cnf(c_7204,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7203]) ).
cnf(c_7205,plain,
( e_21 = e_19
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7204]) ).
cnf(c_4152,plain,
( e_21 = e_19
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7205]) ).
cnf(c_7206,plain,
( i4 = i2
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_4152,c_3954]) ).
cnf(c_7207,plain,
( i4 = i2
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7206]) ).
cnf(c_4164,plain,
( i4 = i2
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7207]) ).
cnf(c_7208,plain,
( i2 = i1
| i3 = i1
| i2 = i1
| i3 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4164,c_4044]) ).
cnf(c_7209,plain,
( i2 = i1
| i3 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7208]) ).
cnf(c_7210,plain,
( i2 = i1
| i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7209]) ).
cnf(c_4201,plain,
( i3 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7210]) ).
cnf(c_4202,plain,
( store(a_24,i1,e_27) = a_28
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4201,c_13]) ).
cnf(c_4203,plain,
( store(a_26,i1,e_29) = a_30
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4201,c_15]) ).
cnf(c_4204,plain,
( select(a_26,i1) = e_27
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4201,c_29]) ).
cnf(c_4205,plain,
( select(a_24,i1) = e_29
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4201,c_31]) ).
cnf(c_4206,plain,
( select(a_28,i1) = e_27
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4201,c_63]) ).
cnf(c_4207,plain,
( select(a_30,i1) = e_29
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4201,c_65]) ).
cnf(c_7211,plain,
( i_35 = i1
| i_35 = i2
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4201,c_924]) ).
cnf(c_4228,plain,
( i_35 = i2
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7211]) ).
cnf(c_4260,plain,
( select(a1,i2) = e_36
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4228,c_37]) ).
cnf(c_4261,plain,
( select(a2,i2) = e_37
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4228,c_39]) ).
cnf(c_7212,plain,
( e_27 = e_21
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4204,c_190]) ).
cnf(c_4277,plain,
( e_27 = e_21
| i2 = i1 ),
inference(copy,[status(thm)],[c_7212]) ).
cnf(c_4280,plain,
( select(a_28,i3) = e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4277,c_63]) ).
cnf(c_4283,plain,
( e_29 = e_21
| i4 = i3
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4277,c_265]) ).
cnf(c_7213,plain,
( e_29 = e_19
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4205,c_174]) ).
cnf(c_4306,plain,
( e_29 = e_19
| i2 = i1 ),
inference(copy,[status(thm)],[c_7213]) ).
cnf(c_4310,plain,
( select(a_30,i3) = e_19
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4306,c_65]) ).
cnf(c_7214,plain,
( e_19 = e_21
| i4 = i3
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4306,c_4283]) ).
cnf(c_7215,plain,
( e_21 = e_19
| i4 = i3
| i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7214]) ).
cnf(c_4326,plain,
( e_21 = e_19
| i4 = i3
| i2 = i1 ),
inference(copy,[status(thm)],[c_7215]) ).
cnf(c_4428,plain,
( select(a_30,i1) = e_27
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4206,c_288]) ).
cnf(c_7216,plain,
( select(a_30,i1) = e_19
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4306,c_4207]) ).
cnf(c_4449,plain,
( select(a_30,i1) = e_19
| i2 = i1 ),
inference(copy,[status(thm)],[c_7216]) ).
cnf(c_7217,plain,
( select(a_28,i2) = e_23
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4202,c_108]) ).
cnf(c_4491,plain,
( select(a_28,i2) = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_7217]) ).
cnf(c_4500,plain,
( select(a_30,i2) = e_23
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4491,c_288]) ).
cnf(c_7218,plain,
( select(a_30,i2) = e_25
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4203,c_111]) ).
cnf(c_4513,plain,
( select(a_30,i2) = e_25
| i2 = i1 ),
inference(copy,[status(thm)],[c_7218]) ).
cnf(c_7219,plain,
( e_36 = e_25
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4260,c_145]) ).
cnf(c_4559,plain,
( e_36 = e_25
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7219]) ).
cnf(c_4563,plain,
( e_37 != e_25
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4559,c_45]) ).
cnf(c_7220,plain,
( e_37 = e_23
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4261,c_159]) ).
cnf(c_4579,plain,
( e_37 = e_23
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7220]) ).
cnf(c_7221,plain,
( e_23 != e_25
| i_35 = i1
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4579,c_4563]) ).
cnf(c_7222,plain,
( e_25 != e_23
| i_35 = i1
| i2 = i1
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7221]) ).
cnf(c_7223,plain,
( e_25 != e_23
| i_35 = i1
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7222]) ).
cnf(c_4588,plain,
( e_25 != e_23
| i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7223]) ).
cnf(c_7224,plain,
( e_27 = e_19
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4428,c_4449]) ).
cnf(c_4633,plain,
( e_27 = e_19
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7224]) ).
cnf(c_7225,plain,
( e_19 = e_21
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4633,c_4277]) ).
cnf(c_7226,plain,
( e_21 = e_19
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7225]) ).
cnf(c_4655,plain,
( e_21 = e_19
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7226]) ).
cnf(c_7227,plain,
( e_23 = e_25
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4500,c_4513]) ).
cnf(c_7228,plain,
( e_25 = e_23
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7227]) ).
cnf(c_4718,plain,
( e_25 = e_23
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7228]) ).
cnf(c_7229,plain,
( i_35 = i1
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(resolve,[status(thm)],[c_4718,c_4588]) ).
cnf(c_4719,plain,
( i_35 = i1
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7229]) ).
cnf(c_4730,plain,
( select(a1,i1) = e_36
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4719,c_37]) ).
cnf(c_4731,plain,
( select(a2,i1) = e_37
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4719,c_39]) ).
cnf(c_4807,plain,
( e_36 = e_21
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4730,c_23]) ).
cnf(c_4811,plain,
( e_37 != e_21
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4807,c_45]) ).
cnf(c_7230,plain,
( e_37 != e_19
| i4 = i2
| i2 = i1
| i4 = i3
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4326,c_4811]) ).
cnf(c_4813,plain,
( e_37 != e_19
| i4 = i2
| i4 = i3
| i2 = i1 ),
inference(copy,[status(thm)],[c_7230]) ).
cnf(c_4822,plain,
( e_37 = e_19
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4731,c_21]) ).
cnf(c_7231,plain,
( i4 = i2
| i4 = i3
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(resolve,[status(thm)],[c_4822,c_4813]) ).
cnf(c_7232,plain,
( i4 = i2
| i4 = i3
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7231]) ).
cnf(c_4824,plain,
( i4 = i3
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7232]) ).
cnf(c_7233,plain,
( e_19 != e_21
| i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4822,c_4811]) ).
cnf(c_7234,plain,
( e_21 != e_19
| i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7233]) ).
cnf(c_7235,plain,
( e_21 != e_19
| i4 = i2
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7234]) ).
cnf(c_4828,plain,
( e_21 != e_19
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7235]) ).
cnf(c_4887,plain,
( select(a_30,i3) = e_31
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4824,c_33]) ).
cnf(c_4888,plain,
( select(a_28,i3) = e_33
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4824,c_35]) ).
cnf(c_7236,plain,
( e_31 = e_19
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4887,c_4310]) ).
cnf(c_5032,plain,
( e_31 = e_19
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7236]) ).
cnf(c_5052,plain,
( e_33 = e_19
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5032,c_130]) ).
cnf(c_7237,plain,
( e_33 = e_21
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4888,c_4280]) ).
cnf(c_5070,plain,
( e_33 = e_21
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7237]) ).
cnf(c_7238,plain,
( e_21 = e_19
| i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5070,c_5052]) ).
cnf(c_7239,plain,
( e_21 = e_19
| i4 = i2
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7238]) ).
cnf(c_5097,plain,
( e_21 = e_19
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7239]) ).
cnf(c_7240,plain,
( i4 = i2
| i2 = i1
| i4 = i2
| i2 = i1 ),
inference(resolve,[status(thm)],[c_5097,c_4828]) ).
cnf(c_7241,plain,
( i4 = i2
| i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7240]) ).
cnf(c_5144,plain,
( i4 = i2
| i2 = i1 ),
inference(copy,[status(thm)],[c_7241]) ).
cnf(c_5147,plain,
( select(a_30,i2) = e_31
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5144,c_33]) ).
cnf(c_5148,plain,
( select(a_28,i2) = e_33
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5144,c_35]) ).
cnf(c_7242,plain,
( e_31 = e_25
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5147,c_4513]) ).
cnf(c_5196,plain,
( e_31 = e_25
| i2 = i1 ),
inference(copy,[status(thm)],[c_7242]) ).
cnf(c_5201,plain,
( e_33 = e_25
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5196,c_130]) ).
cnf(c_7243,plain,
( e_33 = e_23
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5148,c_4491]) ).
cnf(c_5221,plain,
( e_33 = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_7243]) ).
cnf(c_7244,plain,
( e_23 = e_25
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5221,c_5201]) ).
cnf(c_7245,plain,
( e_25 = e_23
| i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7244]) ).
cnf(c_5236,plain,
( e_25 = e_23
| i2 = i1 ),
inference(copy,[status(thm)],[c_7245]) ).
cnf(c_7246,plain,
( i_35 = i1
| i2 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_5236,c_4588]) ).
cnf(c_5244,plain,
( i_35 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7246]) ).
cnf(c_5258,plain,
( select(a1,i1) = e_36
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5244,c_37]) ).
cnf(c_5259,plain,
( select(a2,i1) = e_37
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5244,c_39]) ).
cnf(c_5322,plain,
( e_36 = e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5258,c_23]) ).
cnf(c_5326,plain,
( e_37 != e_21
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5322,c_45]) ).
cnf(c_7247,plain,
( e_37 != e_19
| i2 = i1
| i4 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_4655,c_5326]) ).
cnf(c_5329,plain,
( e_37 != e_19
| i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7247]) ).
cnf(c_5337,plain,
( e_37 = e_19
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5259,c_21]) ).
cnf(c_7248,plain,
( i4 = i1
| i2 = i1
| i2 = i1 ),
inference(resolve,[status(thm)],[c_5337,c_5329]) ).
cnf(c_5338,plain,
( i4 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7248]) ).
cnf(c_7249,plain,
( i1 = i2
| i2 = i1
| i2 = i1 ),
inference(paramod,[status(thm)],[c_5338,c_5144]) ).
cnf(c_7250,plain,
( i2 = i1
| i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7249]) ).
cnf(c_7251,plain,
( i2 = i1
| i2 = i1 ),
inference(copy,[status(thm)],[c_7250]) ).
cnf(c_5368,plain,
i2 = i1,
inference(copy,[status(thm)],[c_7251]) ).
cnf(c_5371,plain,
select(a_22,i1) = e_23,
inference(paramod,[status(thm)],[c_5368,c_25]) ).
cnf(c_5372,plain,
select(a_20,i1) = e_25,
inference(paramod,[status(thm)],[c_5368,c_27]) ).
cnf(c_7252,plain,
( i4 = i3
| i_35 = i1
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_5368,c_1057]) ).
cnf(c_5393,plain,
( i4 = i3
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7252]) ).
cnf(c_5433,plain,
( select(a1,i1) = e_36
| i4 = i3 ),
inference(paramod,[status(thm)],[c_5393,c_37]) ).
cnf(c_5434,plain,
( select(a2,i1) = e_37
| i4 = i3 ),
inference(paramod,[status(thm)],[c_5393,c_39]) ).
cnf(c_5441,plain,
e_23 = e_21,
inference(paramod,[status(thm)],[c_5371,c_57]) ).
cnf(c_5444,plain,
select(a_24,i2) = e_21,
inference(paramod,[status(thm)],[c_5441,c_59]) ).
cnf(c_5445,plain,
( select(a_28,i2) = e_21
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5441,c_206]) ).
cnf(c_5447,plain,
( e_25 = e_21
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5441,c_371]) ).
cnf(c_5474,plain,
e_25 = e_19,
inference(paramod,[status(thm)],[c_5372,c_55]) ).
cnf(c_5478,plain,
select(a_26,i2) = e_19,
inference(paramod,[status(thm)],[c_5474,c_61]) ).
cnf(c_5479,plain,
( select(a_30,i2) = e_19
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5474,c_228]) ).
cnf(c_7253,plain,
( e_19 = e_21
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5474,c_5447]) ).
cnf(c_5502,plain,
( e_21 = e_19
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7253]) ).
cnf(c_7254,plain,
( i4 = i2
| i3 = i2
| i4 = i3
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_5502,c_1212]) ).
cnf(c_7255,plain,
( i4 = i2
| i4 = i3
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7254]) ).
cnf(c_5507,plain,
( i4 = i3
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7255]) ).
cnf(c_5509,plain,
( select(a1,i1) = e_19
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5502,c_23]) ).
cnf(c_5514,plain,
( select(a_30,i3) = e_31
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5507,c_33]) ).
cnf(c_5515,plain,
( select(a_28,i3) = e_33
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5507,c_35]) ).
cnf(c_5662,plain,
( e_36 = e_21
| i4 = i3 ),
inference(paramod,[status(thm)],[c_5433,c_23]) ).
cnf(c_5664,plain,
( e_37 != e_21
| i4 = i3 ),
inference(paramod,[status(thm)],[c_5662,c_45]) ).
cnf(c_5669,plain,
( e_37 = e_19
| i4 = i3 ),
inference(paramod,[status(thm)],[c_5434,c_21]) ).
cnf(c_7256,plain,
( e_19 != e_21
| i4 = i3
| i4 = i3 ),
inference(paramod,[status(thm)],[c_5669,c_5664]) ).
cnf(c_7257,plain,
( e_21 != e_19
| i4 = i3
| i4 = i3 ),
inference(copy,[status(thm)],[c_7256]) ).
cnf(c_5673,plain,
( e_21 != e_19
| i4 = i3 ),
inference(copy,[status(thm)],[c_7257]) ).
cnf(c_5925,plain,
( e_31 = e_29
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5514,c_65]) ).
cnf(c_5929,plain,
( e_33 = e_29
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5925,c_130]) ).
cnf(c_5945,plain,
( e_33 = e_27
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5515,c_63]) ).
cnf(c_7258,plain,
( e_27 = e_29
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5945,c_5929]) ).
cnf(c_7259,plain,
( e_29 = e_27
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7258]) ).
cnf(c_7260,plain,
( e_29 = e_27
| i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7259]) ).
cnf(c_5956,plain,
( e_29 = e_27
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7260]) ).
cnf(c_5965,plain,
( i_35 = i2
| i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_5956,c_1066]) ).
cnf(c_7261,plain,
( i_35 = i1
| i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5368,c_5965]) ).
cnf(c_5987,plain,
( i_35 = i1
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7261]) ).
cnf(c_5988,plain,
( select(a1,i1) = e_36
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5987,c_37]) ).
cnf(c_5989,plain,
( select(a2,i1) = e_37
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5987,c_39]) ).
cnf(c_7262,plain,
( e_36 = e_19
| i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5988,c_5509]) ).
cnf(c_7263,plain,
( e_36 = e_19
| i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7262]) ).
cnf(c_6350,plain,
( e_36 = e_19
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7263]) ).
cnf(c_6355,plain,
( e_37 != e_19
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6350,c_45]) ).
cnf(c_6360,plain,
( e_37 = e_19
| i4 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_5989,c_21]) ).
cnf(c_7264,plain,
( i4 = i2
| i3 = i2
| i4 = i2
| i3 = i2 ),
inference(resolve,[status(thm)],[c_6360,c_6355]) ).
cnf(c_7265,plain,
( i4 = i2
| i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7264]) ).
cnf(c_6361,plain,
( i4 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7265]) ).
cnf(c_6364,plain,
( select(a_30,i2) = e_31
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6361,c_33]) ).
cnf(c_6365,plain,
( select(a_28,i2) = e_33
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6361,c_35]) ).
cnf(c_7266,plain,
( e_31 = e_19
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6364,c_5479]) ).
cnf(c_6454,plain,
( e_31 = e_19
| i3 = i2 ),
inference(copy,[status(thm)],[c_7266]) ).
cnf(c_6476,plain,
( e_33 = e_19
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6454,c_130]) ).
cnf(c_7267,plain,
( e_33 = e_21
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6365,c_5445]) ).
cnf(c_6496,plain,
( e_33 = e_21
| i3 = i2 ),
inference(copy,[status(thm)],[c_7267]) ).
cnf(c_7268,plain,
( e_21 = e_19
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6496,c_6476]) ).
cnf(c_6526,plain,
( e_21 = e_19
| i3 = i2 ),
inference(copy,[status(thm)],[c_7268]) ).
cnf(c_6574,plain,
( i4 = i3
| i3 = i2 ),
inference(resolve,[status(thm)],[c_6526,c_5673]) ).
cnf(c_7269,plain,
( i3 = i2
| i3 = i2
| i3 = i2 ),
inference(paramod,[status(thm)],[c_6574,c_6361]) ).
cnf(c_7270,plain,
( i3 = i2
| i3 = i2 ),
inference(copy,[status(thm)],[c_7269]) ).
cnf(c_6603,plain,
i3 = i2,
inference(copy,[status(thm)],[c_7270]) ).
cnf(c_6606,plain,
select(a_26,i2) = e_27,
inference(paramod,[status(thm)],[c_6603,c_29]) ).
cnf(c_6607,plain,
select(a_24,i2) = e_29,
inference(paramod,[status(thm)],[c_6603,c_31]) ).
cnf(c_7271,plain,
( i_35 = i2
| i_35 = i2
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_6603,c_924]) ).
cnf(c_6625,plain,
( i_35 = i2
| i_35 = i1 ),
inference(copy,[status(thm)],[c_7271]) ).
cnf(c_7272,plain,
( i_35 = i1
| i_35 = i1 ),
inference(paramod,[status(thm)],[c_5368,c_6625]) ).
cnf(c_6703,plain,
i_35 = i1,
inference(copy,[status(thm)],[c_7272]) ).
cnf(c_6704,plain,
select(a1,i1) = e_36,
inference(paramod,[status(thm)],[c_6703,c_37]) ).
cnf(c_6705,plain,
select(a2,i1) = e_37,
inference(paramod,[status(thm)],[c_6703,c_39]) ).
cnf(c_6713,plain,
e_27 = e_19,
inference(paramod,[status(thm)],[c_6606,c_5478]) ).
cnf(c_6734,plain,
select(a_28,i3) = e_19,
inference(paramod,[status(thm)],[c_6713,c_63]) ).
cnf(c_6736,plain,
( e_29 = e_19
| i4 = i3 ),
inference(paramod,[status(thm)],[c_6713,c_265]) ).
cnf(c_6754,plain,
e_29 = e_21,
inference(paramod,[status(thm)],[c_6607,c_5444]) ).
cnf(c_6776,plain,
select(a_30,i3) = e_21,
inference(paramod,[status(thm)],[c_6754,c_65]) ).
cnf(c_6790,plain,
( e_21 = e_19
| i4 = i3 ),
inference(paramod,[status(thm)],[c_6754,c_6736]) ).
cnf(c_7273,plain,
( i4 = i3
| i4 = i3 ),
inference(resolve,[status(thm)],[c_6790,c_5673]) ).
cnf(c_6820,plain,
i4 = i3,
inference(copy,[status(thm)],[c_7273]) ).
cnf(c_6823,plain,
select(a_30,i3) = e_31,
inference(paramod,[status(thm)],[c_6820,c_33]) ).
cnf(c_6824,plain,
select(a_28,i3) = e_33,
inference(paramod,[status(thm)],[c_6820,c_35]) ).
cnf(c_6924,plain,
e_36 = e_21,
inference(paramod,[status(thm)],[c_6704,c_23]) ).
cnf(c_6926,plain,
e_37 != e_21,
inference(paramod,[status(thm)],[c_6924,c_45]) ).
cnf(c_6931,plain,
e_37 = e_19,
inference(paramod,[status(thm)],[c_6705,c_21]) ).
cnf(c_7274,plain,
e_19 != e_21,
inference(paramod,[status(thm)],[c_6931,c_6926]) ).
cnf(c_6935,plain,
e_21 != e_19,
inference(copy,[status(thm)],[c_7274]) ).
cnf(c_6957,plain,
e_31 = e_21,
inference(paramod,[status(thm)],[c_6823,c_6776]) ).
cnf(c_6985,plain,
e_33 = e_21,
inference(paramod,[status(thm)],[c_6957,c_130]) ).
cnf(c_6999,plain,
e_33 = e_19,
inference(paramod,[status(thm)],[c_6824,c_6734]) ).
cnf(c_7275,plain,
e_19 = e_21,
inference(paramod,[status(thm)],[c_6999,c_6985]) ).
cnf(c_7276,plain,
e_21 = e_19,
inference(copy,[status(thm)],[c_7275]) ).
cnf(c_7038,plain,
$false,
inference(resolve,[status(thm)],[c_6935,c_7276]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV565-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 14:24:49 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 946888 was started by sandbox2 on n017,
% 0.10/0.37 % Sat Sep 26 14:24:49 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 24.85/3.56
% 24.85/3.56 % given #500 (T,wt=32): 361 i3 = i2 | i4 = i2 | i2 = A | select(store(a_34,A,B),i2) = e_25. [para(255(c,1),2(b,2)),flip(c)].
% 24.85/3.56
% 24.85/3.56 % given #1000 (T,wt=14): 4822 i2 = i1 | i4 = i2 | e_37 = e_19. [para(4731(c,1),21(a,1))].
% 24.85/3.56
% 24.85/3.56 % SZS status Unsatisfiable for theBenchmark
% 24.85/3.56
% 24.85/3.56 % Proof 1 at 2.72 (+ 0.43) seconds.
% 24.85/3.56 % Length of proof is 346.
% 24.85/3.56 % Level of proof is 137.
% 24.85/3.56 % Maximum clause weight is 33.000.
% 24.85/3.56 % Given clauses 1307.
% 24.85/3.56
% 24.85/3.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------