%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV555-1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:23:42 PM UTC 2026
% Result : Unsatisfiable 15.18s 3.07s
% Output : CNFRefutation 15.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 46
% Syntax : Number of formulae : 276 ( 114 unt; 0 def)
% Number of atoms : 916 ( 915 equ)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 643 ( 3 ~; 640 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 57 ( 57 usr; 55 con; 0-3 aty)
% Number of variables : 53 ( 0 sgn 53 !; 0 ?; 46 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
fof(f2,axiom,
! [X2,X3,X0,X1] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
a_44 = store(a1,i1,e_43),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f4,axiom,
a_46 = store(a2,i1,e_45),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f5,axiom,
a_48 = store(a_44,i2,e_47),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f6,axiom,
a_50 = store(a_46,i2,e_49),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f7,axiom,
a_52 = store(a_48,i3,e_51),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f8,axiom,
a_54 = store(a_50,i3,e_53),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f9,axiom,
a_56 = store(a_52,i4,e_55),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f10,axiom,
a_58 = store(a_54,i4,e_57),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f11,axiom,
a_60 = store(a_56,i5,e_59),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f12,axiom,
a_62 = store(a_58,i5,e_61),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f13,axiom,
a_64 = store(a_60,i6,e_63),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f14,axiom,
a_66 = store(a_62,i6,e_65),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f15,axiom,
a_68 = store(a_64,i7,e_67),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f16,axiom,
a_70 = store(a_66,i7,e_69),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f17,axiom,
a_72 = store(a_68,i8,e_71),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f18,axiom,
a_74 = store(a_70,i8,e_73),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f19,axiom,
a_76 = store(a_72,i9,e_75),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f20,axiom,
a_78 = store(a_74,i9,e_77),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f21,axiom,
a_80 = store(a_76,i10,e_79),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f22,axiom,
a_82 = store(a_78,i10,e_81),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f23,axiom,
e_43 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f24,axiom,
e_45 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f25,axiom,
e_47 = select(a_46,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f26,axiom,
e_49 = select(a_44,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f27,axiom,
e_51 = select(a_50,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f28,axiom,
e_53 = select(a_48,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp25) ).
fof(f29,axiom,
e_55 = select(a_54,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp26) ).
fof(f30,axiom,
e_57 = select(a_52,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp27) ).
fof(f31,axiom,
e_59 = select(a_58,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp28) ).
fof(f32,axiom,
e_61 = select(a_56,i5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp29) ).
fof(f33,axiom,
e_63 = select(a_62,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp30) ).
fof(f34,axiom,
e_65 = select(a_60,i6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp31) ).
fof(f35,axiom,
e_67 = select(a_66,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp32) ).
fof(f36,axiom,
e_69 = select(a_64,i7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp33) ).
fof(f37,axiom,
e_71 = select(a_70,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp34) ).
fof(f38,axiom,
e_73 = select(a_68,i8),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp35) ).
fof(f39,axiom,
e_75 = select(a_74,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp36) ).
fof(f40,axiom,
e_77 = select(a_72,i9),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp37) ).
fof(f41,axiom,
e_79 = select(a_78,i10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp38) ).
fof(f42,axiom,
e_81 = select(a_76,i10),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp39) ).
fof(f43,axiom,
e_84 = select(a1,i_83),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp40) ).
fof(f44,axiom,
e_85 = select(a2,i_83),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp41) ).
fof(f46,axiom,
a_80 = a_82,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp43) ).
fof(f47,negated_conjecture,
e_84 != e_85,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f48,plain,
store(a_76,i10,e_79) = a_82,
inference(definition_unfolding,[],[f21,f46]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_97,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X1 = X3 )
| ( select(store(X0,X1,X2),X3) = select(X0,X3) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_98,plain,
store(a1,i1,e_43) = a_44,
inference(cnf_transformation,[],[f3]) ).
tcf(c_99,plain,
store(a2,i1,e_45) = a_46,
inference(cnf_transformation,[],[f4]) ).
tcf(c_100,plain,
store(a_44,i2,e_47) = a_48,
inference(cnf_transformation,[],[f5]) ).
tcf(c_101,plain,
store(a_46,i2,e_49) = a_50,
inference(cnf_transformation,[],[f6]) ).
tcf(c_102,plain,
store(a_48,i3,e_51) = a_52,
inference(cnf_transformation,[],[f7]) ).
tcf(c_103,plain,
store(a_50,i3,e_53) = a_54,
inference(cnf_transformation,[],[f8]) ).
tcf(c_104,plain,
store(a_52,i4,e_55) = a_56,
inference(cnf_transformation,[],[f9]) ).
tcf(c_105,plain,
store(a_54,i4,e_57) = a_58,
inference(cnf_transformation,[],[f10]) ).
tcf(c_106,plain,
store(a_56,i5,e_59) = a_60,
inference(cnf_transformation,[],[f11]) ).
tcf(c_107,plain,
store(a_58,i5,e_61) = a_62,
inference(cnf_transformation,[],[f12]) ).
tcf(c_108,plain,
store(a_60,i6,e_63) = a_64,
inference(cnf_transformation,[],[f13]) ).
tcf(c_109,plain,
store(a_62,i6,e_65) = a_66,
inference(cnf_transformation,[],[f14]) ).
tcf(c_110,plain,
store(a_64,i7,e_67) = a_68,
inference(cnf_transformation,[],[f15]) ).
tcf(c_111,plain,
store(a_66,i7,e_69) = a_70,
inference(cnf_transformation,[],[f16]) ).
tcf(c_112,plain,
store(a_68,i8,e_71) = a_72,
inference(cnf_transformation,[],[f17]) ).
tcf(c_113,plain,
store(a_70,i8,e_73) = a_74,
inference(cnf_transformation,[],[f18]) ).
tcf(c_114,plain,
store(a_72,i9,e_75) = a_76,
inference(cnf_transformation,[],[f19]) ).
tcf(c_115,plain,
store(a_74,i9,e_77) = a_78,
inference(cnf_transformation,[],[f20]) ).
tcf(c_116,plain,
store(a_76,i10,e_79) = a_82,
inference(cnf_transformation,[],[f48]) ).
tcf(c_117,plain,
store(a_78,i10,e_81) = a_82,
inference(cnf_transformation,[],[f22]) ).
tcf(c_118,plain,
select(a2,i1) = e_43,
inference(cnf_transformation,[],[f23]) ).
tcf(c_119,plain,
select(a1,i1) = e_45,
inference(cnf_transformation,[],[f24]) ).
tcf(c_120,plain,
select(a_46,i2) = e_47,
inference(cnf_transformation,[],[f25]) ).
tcf(c_121,plain,
select(a_44,i2) = e_49,
inference(cnf_transformation,[],[f26]) ).
tcf(c_122,plain,
select(a_50,i3) = e_51,
inference(cnf_transformation,[],[f27]) ).
tcf(c_123,plain,
select(a_48,i3) = e_53,
inference(cnf_transformation,[],[f28]) ).
tcf(c_124,plain,
select(a_54,i4) = e_55,
inference(cnf_transformation,[],[f29]) ).
tcf(c_125,plain,
select(a_52,i4) = e_57,
inference(cnf_transformation,[],[f30]) ).
tcf(c_126,plain,
select(a_58,i5) = e_59,
inference(cnf_transformation,[],[f31]) ).
tcf(c_127,plain,
select(a_56,i5) = e_61,
inference(cnf_transformation,[],[f32]) ).
tcf(c_128,plain,
select(a_62,i6) = e_63,
inference(cnf_transformation,[],[f33]) ).
tcf(c_129,plain,
select(a_60,i6) = e_65,
inference(cnf_transformation,[],[f34]) ).
tcf(c_130,plain,
select(a_66,i7) = e_67,
inference(cnf_transformation,[],[f35]) ).
tcf(c_131,plain,
select(a_64,i7) = e_69,
inference(cnf_transformation,[],[f36]) ).
tcf(c_132,plain,
select(a_70,i8) = e_71,
inference(cnf_transformation,[],[f37]) ).
tcf(c_133,plain,
select(a_68,i8) = e_73,
inference(cnf_transformation,[],[f38]) ).
tcf(c_134,plain,
select(a_74,i9) = e_75,
inference(cnf_transformation,[],[f39]) ).
tcf(c_135,plain,
select(a_72,i9) = e_77,
inference(cnf_transformation,[],[f40]) ).
tcf(c_136,plain,
select(a_78,i10) = e_79,
inference(cnf_transformation,[],[f41]) ).
tcf(c_137,plain,
select(a_76,i10) = e_81,
inference(cnf_transformation,[],[f42]) ).
tcf(c_138,plain,
select(a1,i_83) = e_84,
inference(cnf_transformation,[],[f43]) ).
tcf(c_139,plain,
select(a2,i_83) = e_85,
inference(cnf_transformation,[],[f44]) ).
tcf(c_141,negated_conjecture,
e_84 != e_85,
inference(cnf_transformation,[],[f47]) ).
tcf(c_245,negated_conjecture,
e_84 != e_85,
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_377,plain,
select(a_44,i1) = e_43,
inference(superposition,[status(thm)],[c_98,c_96]) ).
tcf(c_378,plain,
select(a_46,i1) = e_45,
inference(superposition,[status(thm)],[c_99,c_96]) ).
tcf(c_379,plain,
select(a_48,i2) = e_47,
inference(superposition,[status(thm)],[c_100,c_96]) ).
tcf(c_380,plain,
select(a_50,i2) = e_49,
inference(superposition,[status(thm)],[c_101,c_96]) ).
tcf(c_381,plain,
select(a_52,i3) = e_51,
inference(superposition,[status(thm)],[c_102,c_96]) ).
tcf(c_382,plain,
select(a_54,i3) = e_53,
inference(superposition,[status(thm)],[c_103,c_96]) ).
tcf(c_383,plain,
select(a_56,i4) = e_55,
inference(superposition,[status(thm)],[c_104,c_96]) ).
tcf(c_384,plain,
select(a_58,i4) = e_57,
inference(superposition,[status(thm)],[c_105,c_96]) ).
tcf(c_385,plain,
select(a_60,i5) = e_59,
inference(superposition,[status(thm)],[c_106,c_96]) ).
tcf(c_386,plain,
select(a_62,i5) = e_61,
inference(superposition,[status(thm)],[c_107,c_96]) ).
tcf(c_387,plain,
select(a_64,i6) = e_63,
inference(superposition,[status(thm)],[c_108,c_96]) ).
tcf(c_388,plain,
select(a_66,i6) = e_65,
inference(superposition,[status(thm)],[c_109,c_96]) ).
tcf(c_389,plain,
select(a_68,i7) = e_67,
inference(superposition,[status(thm)],[c_110,c_96]) ).
tcf(c_390,plain,
select(a_70,i7) = e_69,
inference(superposition,[status(thm)],[c_111,c_96]) ).
tcf(c_391,plain,
select(a_72,i8) = e_71,
inference(superposition,[status(thm)],[c_112,c_96]) ).
tcf(c_392,plain,
select(a_74,i8) = e_73,
inference(superposition,[status(thm)],[c_113,c_96]) ).
tcf(c_393,plain,
select(a_76,i9) = e_75,
inference(superposition,[status(thm)],[c_114,c_96]) ).
tcf(c_397,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_44,X0) = select(a1,X0) ) ),
inference(superposition,[status(thm)],[c_98,c_97]) ).
tcf(c_398,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_46,X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_99,c_97]) ).
tcf(c_399,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_44,X0) = select(a_48,X0) ) ),
inference(superposition,[status(thm)],[c_100,c_97]) ).
tcf(c_400,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_46,X0) = select(a_50,X0) ) ),
inference(superposition,[status(thm)],[c_101,c_97]) ).
tcf(c_401,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(a_48,X0) = select(a_52,X0) ) ),
inference(superposition,[status(thm)],[c_102,c_97]) ).
tcf(c_402,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(a_50,X0) = select(a_54,X0) ) ),
inference(superposition,[status(thm)],[c_103,c_97]) ).
tcf(c_403,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_52,X0) = select(a_56,X0) ) ),
inference(superposition,[status(thm)],[c_104,c_97]) ).
tcf(c_404,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_54,X0) = select(a_58,X0) ) ),
inference(superposition,[status(thm)],[c_105,c_97]) ).
tcf(c_405,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_56,X0) = select(a_60,X0) ) ),
inference(superposition,[status(thm)],[c_106,c_97]) ).
tcf(c_406,plain,
! [X0: $i] :
( ( X0 = i5 )
| ( select(a_58,X0) = select(a_62,X0) ) ),
inference(superposition,[status(thm)],[c_107,c_97]) ).
tcf(c_407,plain,
! [X0: $i] :
( ( X0 = i6 )
| ( select(a_60,X0) = select(a_64,X0) ) ),
inference(superposition,[status(thm)],[c_108,c_97]) ).
tcf(c_408,plain,
! [X0: $i] :
( ( X0 = i6 )
| ( select(a_62,X0) = select(a_66,X0) ) ),
inference(superposition,[status(thm)],[c_109,c_97]) ).
tcf(c_409,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( select(a_64,X0) = select(a_68,X0) ) ),
inference(superposition,[status(thm)],[c_110,c_97]) ).
tcf(c_410,plain,
! [X0: $i] :
( ( X0 = i7 )
| ( select(a_66,X0) = select(a_70,X0) ) ),
inference(superposition,[status(thm)],[c_111,c_97]) ).
tcf(c_411,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_68,X0) = select(a_72,X0) ) ),
inference(superposition,[status(thm)],[c_112,c_97]) ).
tcf(c_412,plain,
! [X0: $i] :
( ( X0 = i8 )
| ( select(a_70,X0) = select(a_74,X0) ) ),
inference(superposition,[status(thm)],[c_113,c_97]) ).
tcf(c_413,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( select(a_72,X0) = select(a_76,X0) ) ),
inference(superposition,[status(thm)],[c_114,c_97]) ).
tcf(c_466,plain,
! [X0: $i] :
( ( X0 = i9 )
| ( select(a_74,X0) = select(a_78,X0) ) ),
inference(superposition,[status(thm)],[c_115,c_97]) ).
tcf(c_467,plain,
select(a_78,i9) = e_77,
inference(superposition,[status(thm)],[c_115,c_96]) ).
tcf(c_471,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( select(a_76,X0) = select(a_82,X0) ) ),
inference(superposition,[status(thm)],[c_116,c_97]) ).
tcf(c_472,plain,
select(a_82,i10) = e_79,
inference(superposition,[status(thm)],[c_116,c_96]) ).
tcf(c_476,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( select(a_78,X0) = select(a_82,X0) ) ),
inference(superposition,[status(thm)],[c_117,c_97]) ).
tcf(c_477,plain,
select(a_82,i10) = e_81,
inference(superposition,[status(thm)],[c_117,c_96]) ).
tcf(c_478,plain,
e_79 = e_81,
inference(light_normalisation,[status(thm)],[c_477,c_472]) ).
tcf(c_482,plain,
select(a_76,i10) = e_79,
inference(demodulation,[status(thm)],[c_137,c_478]) ).
tcf(c_492,plain,
( ( i1 = i2 )
| ( select(a1,i2) = e_49 ) ),
inference(superposition,[status(thm)],[c_397,c_121]) ).
tcf(c_506,plain,
( ( i1 = i2 )
| ( select(a2,i2) = e_47 ) ),
inference(superposition,[status(thm)],[c_398,c_120]) ).
tcf(c_520,plain,
( ( i2 = i3 )
| ( select(a_44,i3) = e_53 ) ),
inference(superposition,[status(thm)],[c_399,c_123]) ).
tcf(c_530,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(a1,i3) = e_53 ) ),
inference(superposition,[status(thm)],[c_397,c_520]) ).
tcf(c_543,plain,
( ( i2 = i3 )
| ( select(a_46,i3) = e_51 ) ),
inference(superposition,[status(thm)],[c_400,c_122]) ).
tcf(c_551,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(a2,i3) = e_51 ) ),
inference(superposition,[status(thm)],[c_398,c_543]) ).
tcf(c_567,plain,
( ( i3 = i4 )
| ( select(a_48,i4) = e_57 ) ),
inference(superposition,[status(thm)],[c_401,c_125]) ).
tcf(c_575,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(a_44,i4) = e_57 ) ),
inference(superposition,[status(thm)],[c_399,c_567]) ).
tcf(c_586,plain,
( ( i3 = i4 )
| ( select(a_50,i4) = e_55 ) ),
inference(superposition,[status(thm)],[c_402,c_124]) ).
tcf(c_594,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(a_46,i4) = e_55 ) ),
inference(superposition,[status(thm)],[c_400,c_586]) ).
tcf(c_605,plain,
( ( i4 = i5 )
| ( select(a_52,i5) = e_61 ) ),
inference(superposition,[status(thm)],[c_403,c_127]) ).
tcf(c_613,plain,
( ( i4 = i5 )
| ( i3 = i5 )
| ( select(a_48,i5) = e_61 ) ),
inference(superposition,[status(thm)],[c_401,c_605]) ).
tcf(c_629,plain,
( ( i4 = i5 )
| ( select(a_54,i5) = e_59 ) ),
inference(superposition,[status(thm)],[c_404,c_126]) ).
tcf(c_637,plain,
( ( i4 = i5 )
| ( i3 = i5 )
| ( select(a_50,i5) = e_59 ) ),
inference(superposition,[status(thm)],[c_402,c_629]) ).
tcf(c_649,plain,
( ( i5 = i6 )
| ( select(a_56,i6) = e_65 ) ),
inference(superposition,[status(thm)],[c_405,c_129]) ).
tcf(c_661,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( select(a_52,i6) = e_65 ) ),
inference(superposition,[status(thm)],[c_403,c_649]) ).
tcf(c_672,plain,
( ( i5 = i6 )
| ( select(a_58,i6) = e_63 ) ),
inference(superposition,[status(thm)],[c_406,c_128]) ).
tcf(c_680,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( select(a_54,i6) = e_63 ) ),
inference(superposition,[status(thm)],[c_404,c_672]) ).
tcf(c_697,plain,
( ( i6 = i7 )
| ( select(a_60,i7) = e_69 ) ),
inference(superposition,[status(thm)],[c_407,c_131]) ).
tcf(c_705,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( select(a_56,i7) = e_69 ) ),
inference(superposition,[status(thm)],[c_405,c_697]) ).
tcf(c_716,plain,
( ( i6 = i7 )
| ( select(a_62,i7) = e_67 ) ),
inference(superposition,[status(thm)],[c_408,c_130]) ).
tcf(c_741,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( select(a_58,i7) = e_67 ) ),
inference(superposition,[status(thm)],[c_406,c_716]) ).
tcf(c_753,plain,
( ( i7 = i8 )
| ( select(a_64,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_409,c_133]) ).
tcf(c_779,plain,
( ( i7 = i8 )
| ( select(a_66,i8) = e_71 ) ),
inference(superposition,[status(thm)],[c_410,c_132]) ).
tcf(c_787,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( select(a_60,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_407,c_753]) ).
tcf(c_796,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( select(a_62,i8) = e_71 ) ),
inference(superposition,[status(thm)],[c_408,c_779]) ).
tcf(c_807,plain,
( ( i8 = i9 )
| ( select(a_68,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_411,c_135]) ).
tcf(c_815,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( select(a_64,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_409,c_807]) ).
tcf(c_826,plain,
( ( i8 = i9 )
| ( select(a_70,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_412,c_134]) ).
tcf(c_834,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( select(a_66,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_410,c_826]) ).
tcf(c_849,plain,
( ( i9 = i10 )
| ( select(a_72,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_413,c_482]) ).
tcf(c_857,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( select(a_68,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_411,c_849]) ).
tcf(c_868,plain,
( ( i9 = i10 )
| ( select(a_74,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_466,c_136]) ).
tcf(c_876,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( select(a_70,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_412,c_868]) ).
tcf(c_900,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( select(a_76,X0) = select(a_78,X0) ) ),
inference(superposition,[status(thm)],[c_476,c_471]) ).
tcf(c_913,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( select(a_74,X0) = select(a_76,X0) ) ),
inference(superposition,[status(thm)],[c_900,c_466]) ).
tcf(c_914,plain,
( ( i9 = i10 )
| ( select(a_76,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_900,c_467]) ).
tcf(c_915,plain,
( ( e_75 = e_77 )
| ( i9 = i10 ) ),
inference(light_normalisation,[status(thm)],[c_914,c_393]) ).
tcf(c_962,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i1 = i4 )
| ( select(a1,i4) = e_57 ) ),
inference(superposition,[status(thm)],[c_397,c_575]) ).
tcf(c_974,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i1 = i4 )
| ( select(a2,i4) = e_55 ) ),
inference(superposition,[status(thm)],[c_398,c_594]) ).
tcf(c_986,plain,
( ( i4 = i5 )
| ( i3 = i5 )
| ( i2 = i5 )
| ( select(a_44,i5) = e_61 ) ),
inference(superposition,[status(thm)],[c_399,c_613]) ).
tcf(c_998,plain,
( ( i4 = i5 )
| ( i3 = i5 )
| ( i2 = i5 )
| ( select(a_46,i5) = e_59 ) ),
inference(superposition,[status(thm)],[c_400,c_637]) ).
tcf(c_1029,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( i3 = i6 )
| ( select(a_48,i6) = e_65 ) ),
inference(superposition,[status(thm)],[c_401,c_661]) ).
tcf(c_1041,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( i3 = i6 )
| ( select(a_50,i6) = e_63 ) ),
inference(superposition,[status(thm)],[c_402,c_680]) ).
tcf(c_1053,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( select(a_52,i7) = e_69 ) ),
inference(superposition,[status(thm)],[c_403,c_705]) ).
tcf(c_1065,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( select(a_54,i7) = e_67 ) ),
inference(superposition,[status(thm)],[c_404,c_741]) ).
tcf(c_1077,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( select(a_56,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_405,c_787]) ).
tcf(c_1089,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( select(a_58,i8) = e_71 ) ),
inference(superposition,[status(thm)],[c_406,c_796]) ).
tcf(c_1101,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( select(a_60,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_407,c_815]) ).
tcf(c_1115,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( select(a_62,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_408,c_834]) ).
tcf(c_1158,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( select(a_64,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_409,c_857]) ).
tcf(c_1170,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( select(a_66,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_410,c_876]) ).
tcf(c_1187,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( select(a_72,X0) = select(a_74,X0) ) ),
inference(superposition,[status(thm)],[c_913,c_413]) ).
tcf(c_1203,plain,
( ( i8 = i10 )
| ( i8 = i9 )
| ( select(a_72,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_1187,c_392]) ).
tcf(c_1204,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( select(a_70,X0) = select(a_72,X0) ) ),
inference(superposition,[status(thm)],[c_1187,c_412]) ).
tcf(c_1206,plain,
( ( e_71 = e_73 )
| ( i8 = i10 )
| ( i8 = i9 ) ),
inference(light_normalisation,[status(thm)],[c_1203,c_391]) ).
tcf(c_1277,plain,
( ( i4 = i5 )
| ( i3 = i5 )
| ( i2 = i5 )
| ( i1 = i5 )
| ( select(a1,i5) = e_61 ) ),
inference(superposition,[status(thm)],[c_397,c_986]) ).
tcf(c_1292,plain,
( ( i4 = i5 )
| ( i3 = i5 )
| ( i2 = i5 )
| ( i1 = i5 )
| ( select(a2,i5) = e_59 ) ),
inference(superposition,[status(thm)],[c_398,c_998]) ).
tcf(c_1307,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( i3 = i6 )
| ( i2 = i6 )
| ( select(a_44,i6) = e_65 ) ),
inference(superposition,[status(thm)],[c_399,c_1029]) ).
tcf(c_1322,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( i3 = i6 )
| ( i2 = i6 )
| ( select(a_46,i6) = e_63 ) ),
inference(superposition,[status(thm)],[c_400,c_1041]) ).
tcf(c_1337,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( i3 = i7 )
| ( select(a_48,i7) = e_69 ) ),
inference(superposition,[status(thm)],[c_401,c_1053]) ).
tcf(c_1385,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( i3 = i7 )
| ( select(a_50,i7) = e_67 ) ),
inference(superposition,[status(thm)],[c_402,c_1065]) ).
tcf(c_1400,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( select(a_52,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_403,c_1077]) ).
tcf(c_1415,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( select(a_54,i8) = e_71 ) ),
inference(superposition,[status(thm)],[c_404,c_1089]) ).
tcf(c_1430,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( select(a_56,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_405,c_1101]) ).
tcf(c_1445,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( select(a_58,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_406,c_1115]) ).
tcf(c_1460,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( select(a_60,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_407,c_1158]) ).
tcf(c_1475,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( select(a_62,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_408,c_1170]) ).
tcf(c_1496,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( select(a_68,X0) = select(a_70,X0) ) ),
inference(superposition,[status(thm)],[c_1204,c_411]) ).
tcf(c_1533,plain,
( ( i7 = i10 )
| ( i7 = i9 )
| ( i7 = i8 )
| ( select(a_68,i7) = e_69 ) ),
inference(superposition,[status(thm)],[c_1496,c_390]) ).
tcf(c_1534,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( select(a_66,X0) = select(a_68,X0) ) ),
inference(superposition,[status(thm)],[c_1496,c_410]) ).
tcf(c_1537,plain,
( ( e_67 = e_69 )
| ( i7 = i10 )
| ( i7 = i9 )
| ( i7 = i8 ) ),
inference(light_normalisation,[status(thm)],[c_1533,c_389]) ).
tcf(c_1556,plain,
( ( i7 = i10 )
| ( i7 = i9 )
| ( i7 = i8 )
| ( store(a_66,i7,e_67) = a_70 ) ),
inference(superposition,[status(thm)],[c_1537,c_111]) ).
tcf(c_1570,plain,
( ( i7 = i10 )
| ( i7 = i9 )
| ( i7 = i8 )
| ( select(a_70,i7) = e_67 ) ),
inference(superposition,[status(thm)],[c_1556,c_96]) ).
tcf(c_1592,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( i3 = i6 )
| ( i2 = i6 )
| ( i1 = i6 )
| ( select(a1,i6) = e_65 ) ),
inference(superposition,[status(thm)],[c_397,c_1307]) ).
tcf(c_1623,plain,
( ( i5 = i6 )
| ( i4 = i6 )
| ( i3 = i6 )
| ( i2 = i6 )
| ( i1 = i6 )
| ( select(a2,i6) = e_63 ) ),
inference(superposition,[status(thm)],[c_398,c_1322]) ).
tcf(c_1641,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( i3 = i7 )
| ( i2 = i7 )
| ( select(a_44,i7) = e_69 ) ),
inference(superposition,[status(thm)],[c_399,c_1337]) ).
tcf(c_1659,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( i3 = i7 )
| ( i2 = i7 )
| ( select(a_46,i7) = e_67 ) ),
inference(superposition,[status(thm)],[c_400,c_1385]) ).
tcf(c_1683,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( i3 = i8 )
| ( select(a_48,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_401,c_1400]) ).
tcf(c_1707,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( i3 = i8 )
| ( select(a_50,i8) = e_71 ) ),
inference(superposition,[status(thm)],[c_402,c_1415]) ).
tcf(c_1725,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( select(a_52,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_403,c_1430]) ).
tcf(c_1763,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( select(a_54,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_404,c_1445]) ).
tcf(c_1781,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( select(a_56,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_405,c_1460]) ).
tcf(c_1799,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( select(a_58,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_406,c_1475]) ).
tcf(c_1824,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( select(a_64,X0) = select(a_66,X0) ) ),
inference(superposition,[status(thm)],[c_1534,c_409]) ).
tcf(c_1850,plain,
( ( i6 = i10 )
| ( i6 = i9 )
| ( i6 = i8 )
| ( i6 = i7 )
| ( select(a_64,i6) = e_65 ) ),
inference(superposition,[status(thm)],[c_1824,c_388]) ).
tcf(c_1851,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( select(a_62,X0) = select(a_64,X0) ) ),
inference(superposition,[status(thm)],[c_1824,c_408]) ).
tcf(c_1855,plain,
( ( e_63 = e_65 )
| ( i6 = i10 )
| ( i6 = i9 )
| ( i6 = i8 )
| ( i6 = i7 ) ),
inference(light_normalisation,[status(thm)],[c_1850,c_387]) ).
tcf(c_1890,plain,
( ( i6 = i10 )
| ( i6 = i9 )
| ( i6 = i8 )
| ( i6 = i7 )
| ( store(a_62,i6,e_63) = a_66 ) ),
inference(superposition,[status(thm)],[c_1855,c_109]) ).
tcf(c_1907,plain,
( ( i6 = i10 )
| ( i6 = i9 )
| ( i6 = i8 )
| ( i6 = i7 )
| ( select(a_66,i6) = e_63 ) ),
inference(superposition,[status(thm)],[c_1890,c_96]) ).
tcf(c_1933,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( i3 = i7 )
| ( i2 = i7 )
| ( i1 = i7 )
| ( select(a1,i7) = e_69 ) ),
inference(superposition,[status(thm)],[c_397,c_1641]) ).
tcf(c_1954,plain,
( ( i6 = i7 )
| ( i5 = i7 )
| ( i4 = i7 )
| ( i3 = i7 )
| ( i2 = i7 )
| ( i1 = i7 )
| ( select(a2,i7) = e_67 ) ),
inference(superposition,[status(thm)],[c_398,c_1659]) ).
tcf(c_1988,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( i3 = i8 )
| ( i2 = i8 )
| ( select(a_44,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_399,c_1683]) ).
tcf(c_2009,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( i3 = i8 )
| ( i2 = i8 )
| ( select(a_46,i8) = e_71 ) ),
inference(superposition,[status(thm)],[c_400,c_1707]) ).
tcf(c_2030,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( i3 = i9 )
| ( select(a_48,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_401,c_1725]) ).
tcf(c_2079,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( i3 = i9 )
| ( select(a_50,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_402,c_1763]) ).
tcf(c_2100,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( select(a_52,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_403,c_1781]) ).
tcf(c_2121,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( select(a_54,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_404,c_1799]) ).
tcf(c_2154,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( select(a_60,X0) = select(a_62,X0) ) ),
inference(superposition,[status(thm)],[c_1851,c_407]) ).
tcf(c_2202,plain,
( ( i5 = i10 )
| ( i5 = i9 )
| ( i5 = i8 )
| ( i5 = i7 )
| ( i5 = i6 )
| ( select(a_60,i5) = e_61 ) ),
inference(superposition,[status(thm)],[c_2154,c_386]) ).
tcf(c_2203,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( select(a_58,X0) = select(a_60,X0) ) ),
inference(superposition,[status(thm)],[c_2154,c_406]) ).
tcf(c_2208,plain,
( ( e_59 = e_61 )
| ( i5 = i10 )
| ( i5 = i9 )
| ( i5 = i8 )
| ( i5 = i7 )
| ( i5 = i6 ) ),
inference(light_normalisation,[status(thm)],[c_2202,c_385]) ).
tcf(c_2299,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( i3 = i8 )
| ( i2 = i8 )
| ( i1 = i8 )
| ( select(a1,i8) = e_73 ) ),
inference(superposition,[status(thm)],[c_397,c_1988]) ).
tcf(c_2323,plain,
( ( i7 = i8 )
| ( i6 = i8 )
| ( i5 = i8 )
| ( i4 = i8 )
| ( i3 = i8 )
| ( i2 = i8 )
| ( i1 = i8 )
| ( select(a2,i8) = e_71 ) ),
inference(superposition,[status(thm)],[c_398,c_2009]) ).
tcf(c_2347,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( i3 = i9 )
| ( i2 = i9 )
| ( select(a_44,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_399,c_2030]) ).
tcf(c_2371,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( i3 = i9 )
| ( i2 = i9 )
| ( select(a_46,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_400,c_2079]) ).
tcf(c_2397,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( i3 = i10 )
| ( select(a_48,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_401,c_2100]) ).
tcf(c_2421,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( i3 = i10 )
| ( select(a_50,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_402,c_2121]) ).
tcf(c_2479,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( select(a_56,X0) = select(a_58,X0) ) ),
inference(superposition,[status(thm)],[c_2203,c_405]) ).
tcf(c_2515,plain,
( ( i4 = i10 )
| ( i4 = i9 )
| ( i4 = i8 )
| ( i4 = i7 )
| ( i4 = i6 )
| ( i4 = i5 )
| ( select(a_56,i4) = e_57 ) ),
inference(superposition,[status(thm)],[c_2479,c_384]) ).
tcf(c_2516,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( select(a_54,X0) = select(a_56,X0) ) ),
inference(superposition,[status(thm)],[c_2479,c_404]) ).
tcf(c_2522,plain,
( ( e_55 = e_57 )
| ( i4 = i10 )
| ( i4 = i9 )
| ( i4 = i8 )
| ( i4 = i7 )
| ( i4 = i6 )
| ( i4 = i5 ) ),
inference(light_normalisation,[status(thm)],[c_2515,c_383]) ).
tcf(c_2553,plain,
( ( i4 = i10 )
| ( i4 = i9 )
| ( i4 = i8 )
| ( i4 = i7 )
| ( i4 = i6 )
| ( i4 = i5 )
| ( store(a_54,i4,e_55) = a_58 ) ),
inference(superposition,[status(thm)],[c_2522,c_105]) ).
tcf(c_2576,plain,
( ( i4 = i10 )
| ( i4 = i9 )
| ( i4 = i8 )
| ( i4 = i7 )
| ( i4 = i6 )
| ( i4 = i5 )
| ( select(a_58,i4) = e_55 ) ),
inference(superposition,[status(thm)],[c_2553,c_96]) ).
tcf(c_2626,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( i3 = i9 )
| ( i2 = i9 )
| ( i1 = i9 )
| ( select(a1,i9) = e_77 ) ),
inference(superposition,[status(thm)],[c_397,c_2347]) ).
tcf(c_2654,plain,
( ( i8 = i9 )
| ( i7 = i9 )
| ( i6 = i9 )
| ( i5 = i9 )
| ( i4 = i9 )
| ( i3 = i9 )
| ( i2 = i9 )
| ( i1 = i9 )
| ( select(a2,i9) = e_75 ) ),
inference(superposition,[status(thm)],[c_398,c_2371]) ).
tcf(c_2682,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( i3 = i10 )
| ( i2 = i10 )
| ( select(a_44,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_399,c_2397]) ).
tcf(c_2709,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( i3 = i10 )
| ( i2 = i10 )
| ( select(a_46,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_400,c_2421]) ).
tcf(c_2746,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( select(a_52,X0) = select(a_54,X0) ) ),
inference(superposition,[status(thm)],[c_2516,c_403]) ).
tcf(c_2829,plain,
( ( i3 = i10 )
| ( i3 = i9 )
| ( i3 = i8 )
| ( i3 = i7 )
| ( i3 = i6 )
| ( i3 = i5 )
| ( i3 = i4 )
| ( select(a_52,i3) = e_53 ) ),
inference(superposition,[status(thm)],[c_2746,c_382]) ).
tcf(c_2830,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(a_50,X0) = select(a_52,X0) ) ),
inference(superposition,[status(thm)],[c_2746,c_402]) ).
tcf(c_2837,plain,
( ( e_51 = e_53 )
| ( i3 = i10 )
| ( i3 = i9 )
| ( i3 = i8 )
| ( i3 = i7 )
| ( i3 = i6 )
| ( i3 = i5 )
| ( i3 = i4 ) ),
inference(light_normalisation,[status(thm)],[c_2829,c_381]) ).
tcf(c_2955,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( i3 = i10 )
| ( i2 = i10 )
| ( i1 = i10 )
| ( select(a1,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_397,c_2682]) ).
tcf(c_2985,plain,
( ( i9 = i10 )
| ( i8 = i10 )
| ( i7 = i10 )
| ( i6 = i10 )
| ( i5 = i10 )
| ( i4 = i10 )
| ( i3 = i10 )
| ( i2 = i10 )
| ( i1 = i10 )
| ( select(a2,i10) = e_79 ) ),
inference(superposition,[status(thm)],[c_398,c_2709]) ).
tcf(c_3026,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(a_48,X0) = select(a_50,X0) ) ),
inference(superposition,[status(thm)],[c_2830,c_401]) ).
tcf(c_3108,plain,
( ( i2 = i10 )
| ( i2 = i9 )
| ( i2 = i8 )
| ( i2 = i7 )
| ( i2 = i6 )
| ( i2 = i5 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( select(a_48,i2) = e_49 ) ),
inference(superposition,[status(thm)],[c_3026,c_380]) ).
tcf(c_3109,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( select(a_46,X0) = select(a_48,X0) ) ),
inference(superposition,[status(thm)],[c_3026,c_400]) ).
tcf(c_3117,plain,
( ( e_47 = e_49 )
| ( i2 = i10 )
| ( i2 = i9 )
| ( i2 = i8 )
| ( i2 = i7 )
| ( i2 = i6 )
| ( i2 = i5 )
| ( i2 = i4 )
| ( i2 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_3108,c_379]) ).
tcf(c_3156,plain,
( ( i2 = i10 )
| ( i2 = i9 )
| ( i2 = i8 )
| ( i2 = i7 )
| ( i2 = i6 )
| ( i2 = i5 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( store(a_46,i2,e_47) = a_50 ) ),
inference(superposition,[status(thm)],[c_3117,c_101]) ).
tcf(c_3185,plain,
( ( i2 = i10 )
| ( i2 = i9 )
| ( i2 = i8 )
| ( i2 = i7 )
| ( i2 = i6 )
| ( i2 = i5 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( select(a_50,i2) = e_47 ) ),
inference(superposition,[status(thm)],[c_3156,c_96]) ).
tcf(c_3259,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( select(a_44,X0) = select(a_46,X0) ) ),
inference(superposition,[status(thm)],[c_3109,c_399]) ).
tcf(c_3310,plain,
( ( i1 = i10 )
| ( i1 = i9 )
| ( i1 = i8 )
| ( i1 = i7 )
| ( i1 = i6 )
| ( i1 = i5 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_44,i1) = e_45 ) ),
inference(superposition,[status(thm)],[c_3259,c_378]) ).
tcf(c_3311,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( X0 = i1 )
| ( select(a_44,X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_3259,c_398]) ).
tcf(c_3320,plain,
( ( e_43 = e_45 )
| ( i1 = i10 )
| ( i1 = i9 )
| ( i1 = i8 )
| ( i1 = i7 )
| ( i1 = i6 )
| ( i1 = i5 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3310,c_377]) ).
tcf(c_3363,plain,
( ( i1 = i10 )
| ( i1 = i9 )
| ( i1 = i8 )
| ( i1 = i7 )
| ( i1 = i6 )
| ( i1 = i5 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( store(a2,i1,e_43) = a_46 ) ),
inference(superposition,[status(thm)],[c_3320,c_99]) ).
tcf(c_3409,plain,
! [X0: $i] :
( ( X0 = i10 )
| ( X0 = i9 )
| ( X0 = i8 )
| ( X0 = i7 )
| ( X0 = i6 )
| ( X0 = i5 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( X0 = i1 )
| ( select(a1,X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_3311,c_397]) ).
tcf(c_3451,plain,
( ( i1 = i10 )
| ( i1 = i9 )
| ( i1 = i8 )
| ( i1 = i7 )
| ( i1 = i6 )
| ( i1 = i5 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_46,i1) = e_43 ) ),
inference(superposition,[status(thm)],[c_3363,c_96]) ).
tcf(c_3488,plain,
( ( i10 = i_83 )
| ( i9 = i_83 )
| ( i8 = i_83 )
| ( i7 = i_83 )
| ( i6 = i_83 )
| ( i5 = i_83 )
| ( i4 = i_83 )
| ( i3 = i_83 )
| ( i2 = i_83 )
| ( i1 = i_83 )
| ( select(a1,i_83) = e_85 ) ),
inference(superposition,[status(thm)],[c_3409,c_139]) ).
tcf(c_3498,plain,
( ( e_84 = e_85 )
| ( i10 = i_83 )
| ( i9 = i_83 )
| ( i8 = i_83 )
| ( i7 = i_83 )
| ( i6 = i_83 )
| ( i5 = i_83 )
| ( i4 = i_83 )
| ( i3 = i_83 )
| ( i2 = i_83 )
| ( i1 = i_83 ) ),
inference(light_normalisation,[status(thm)],[c_3488,c_138]) ).
tcf(c_3499,plain,
( ( i10 = i_83 )
| ( i9 = i_83 )
| ( i8 = i_83 )
| ( i7 = i_83 )
| ( i6 = i_83 )
| ( i5 = i_83 )
| ( i4 = i_83 )
| ( i3 = i_83 )
| ( i2 = i_83 )
| ( i1 = i_83 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3498,c_245]) ).
tcf(c_15884,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_3499,c_3451,c_3185,c_3117,c_2985,c_2955,c_2837,c_2829,c_2709,c_2682,c_2654,c_2626,c_2576,c_2522,c_2421,c_2397,c_2371,c_2347,c_2323,c_2299,c_2208,c_2121,c_2100,c_2079,c_2030,c_2009,c_1988,c_1954,c_1933,c_1907,c_1799,c_1781,c_1763,c_1725,c_1707,c_1683,c_1659,c_1641,c_1623,c_1592,c_1570,c_1537,c_1475,c_1460,c_1445,c_1430,c_1415,c_1400,c_1385,c_1337,c_1322,c_1307,c_1292,c_1277,c_1206,c_1170,c_1158,c_1115,c_1101,c_1089,c_1077,c_1065,c_1053,c_1041,c_1029,c_998,c_986,c_974,c_962,c_915,c_876,c_868,c_857,c_849,c_834,c_826,c_815,c_807,c_796,c_787,c_779,c_753,c_741,c_716,c_705,c_697,c_680,c_672,c_661,c_649,c_637,c_629,c_613,c_605,c_594,c_586,c_575,c_567,c_551,c_543,c_530,c_520,c_506,c_492,c_482,c_467,c_393,c_392,c_391,c_390,c_389,c_388,c_387,c_386,c_385,c_384,c_383,c_382,c_381,c_380,c_379,c_378,c_377,c_245,c_139,c_138,c_136,c_135,c_134,c_133,c_132,c_131,c_130,c_129,c_128,c_127,c_126,c_125,c_124,c_123,c_122,c_121,c_120,c_119,c_118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV555-1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/0.43 % Computer : n026.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Thu Sep 24 20:32:25 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.20/0.50 Running first-order theorem proving
% 0.20/0.50 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.51
% 0.20/0.51 % ======== iProver multi-core TPTP/SMT =========
% 0.20/0.51
% 0.20/0.51 % Detected problem language: tptp
% 0.20/0.53 % Proving...
% 15.18/3.07 % SZS status Started for theBenchmark.p
% 15.18/3.07 % SZS status Unsatisfiable for theBenchmark.p
% 15.18/3.07
% 15.18/3.07 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.18/3.07
% 15.18/3.07 % ------ iProver source info
% 15.18/3.07
% 15.18/3.07 % git: date: 2026-07-19 20:42:38 +0200
% 15.18/3.07 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.18/3.07 % git: non_committed_changes: false
% 15.18/3.07
% 15.18/3.07 % ------ Parsing...% successful
% 15.18/3.07
% 15.18/3.07
% 15.18/3.07 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.18/3.07
% 15.18/3.07 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 15.18/3.07
% 15.18/3.07 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.18/3.07
% 15.18/3.07 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 15.18/3.07 % ------ Proving...
% 15.18/3.07 % ------ Problem Properties
% 15.18/3.07
% 15.18/3.07 %
% 15.18/3.07 % clauses 46
% 15.18/3.07 % conjectures 1
% 15.18/3.07 % EPR 1
% 15.18/3.07 % Horn 45
% 15.18/3.07 % unary 45
% 15.18/3.07 % binary 1
% 15.18/3.07 % lits 47
% 15.18/3.07 % lits eq 47
% 15.18/3.07 % fd_pure 0
% 15.18/3.07 % fd_pseudo 0
% 15.18/3.07 % fd_cond 0
% 15.18/3.07 % fd_pseudo_cond 1
% 15.18/3.07 % AC symbols 0
% 15.18/3.07
% 15.18/3.07 % ------ Schedule dynamic 5 is on
% 15.18/3.07
% 15.18/3.07 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 15.18/3.07
% 15.18/3.07
% 15.18/3.07 % ------
% 15.18/3.07 % Current options:
% 15.18/3.07 % ------
% 15.18/3.07
% 15.18/3.07
% 15.18/3.07 %
% 15.18/3.07
% 15.18/3.07 % ------ Proving...
% 15.18/3.07 %
% 15.18/3.07
% 15.18/3.07 % SZS status Unsatisfiable for theBenchmark.p
% 15.18/3.07
% 15.18/3.07 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 15.18/3.08
% 15.18/3.08
%------------------------------------------------------------------------------