%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV555-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n004.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:32 PM UTC 2026
% Result : Unsatisfiable 0.15s 6.08s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p',a2) ).
fof(f3,axiom,
a_20 = store(a1,i1,e_19),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp0) ).
fof(f4,axiom,
a_22 = store(a2,i1,e_21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp1) ).
fof(f5,axiom,
a_24 = store(a_20,i2,e_23),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp2) ).
fof(f6,axiom,
a_26 = store(a_22,i2,e_25),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp3) ).
fof(f7,axiom,
a_28 = store(a_24,i3,e_27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp4) ).
fof(f8,axiom,
a_30 = store(a_26,i3,e_29),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp5) ).
fof(f9,axiom,
a_32 = store(a_28,i4,e_31),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp6) ).
fof(f10,axiom,
a_34 = store(a_30,i4,e_33),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp7) ).
fof(f11,axiom,
e_19 = select(a2,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp8) ).
fof(f12,axiom,
e_21 = select(a1,i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp9) ).
fof(f13,axiom,
e_23 = select(a_22,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp10) ).
fof(f14,axiom,
e_25 = select(a_20,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp11) ).
fof(f15,axiom,
e_27 = select(a_26,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp12) ).
fof(f16,axiom,
e_29 = select(a_24,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp13) ).
fof(f17,axiom,
e_31 = select(a_30,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp14) ).
fof(f18,axiom,
e_33 = select(a_28,i4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp15) ).
fof(f19,axiom,
e_36 = select(a1,i_35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp16) ).
fof(f20,axiom,
e_37 = select(a2,i_35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp17) ).
fof(f22,axiom,
a_32 = a_34,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hyp19) ).
fof(f23,negated_conjecture,
e_36 != e_37,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal) ).
fof(f24,plain,
store(a_28,i4,e_31) = a_34,
inference(definition_unfolding,[],[f9,f22]) ).
tcf(c_72,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_73,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_74,plain,
store(a1,i1,e_19) = a_20,
inference(cnf_transformation,[],[f3]) ).
tcf(c_75,plain,
store(a2,i1,e_21) = a_22,
inference(cnf_transformation,[],[f4]) ).
tcf(c_76,plain,
store(a_20,i2,e_23) = a_24,
inference(cnf_transformation,[],[f5]) ).
tcf(c_77,plain,
store(a_22,i2,e_25) = a_26,
inference(cnf_transformation,[],[f6]) ).
tcf(c_78,plain,
store(a_24,i3,e_27) = a_28,
inference(cnf_transformation,[],[f7]) ).
tcf(c_79,plain,
store(a_26,i3,e_29) = a_30,
inference(cnf_transformation,[],[f8]) ).
tcf(c_80,plain,
store(a_28,i4,e_31) = a_34,
inference(cnf_transformation,[],[f24]) ).
tcf(c_81,plain,
store(a_30,i4,e_33) = a_34,
inference(cnf_transformation,[],[f10]) ).
tcf(c_82,plain,
select(a2,i1) = e_19,
inference(cnf_transformation,[],[f11]) ).
tcf(c_83,plain,
select(a1,i1) = e_21,
inference(cnf_transformation,[],[f12]) ).
tcf(c_84,plain,
select(a_22,i2) = e_23,
inference(cnf_transformation,[],[f13]) ).
tcf(c_85,plain,
select(a_20,i2) = e_25,
inference(cnf_transformation,[],[f14]) ).
tcf(c_86,plain,
select(a_26,i3) = e_27,
inference(cnf_transformation,[],[f15]) ).
tcf(c_87,plain,
select(a_24,i3) = e_29,
inference(cnf_transformation,[],[f16]) ).
tcf(c_88,plain,
select(a_30,i4) = e_31,
inference(cnf_transformation,[],[f17]) ).
tcf(c_89,plain,
select(a_28,i4) = e_33,
inference(cnf_transformation,[],[f18]) ).
tcf(c_90,plain,
select(a1,i_35) = e_36,
inference(cnf_transformation,[],[f19]) ).
tcf(c_91,plain,
select(a2,i_35) = e_37,
inference(cnf_transformation,[],[f20]) ).
tcf(c_93,negated_conjecture,
e_36 != e_37,
inference(cnf_transformation,[],[f23]) ).
tcf(c_149,negated_conjecture,
e_36 != e_37,
inference(demodulation,[status(thm)],[c_93]) ).
tcf(c_233,plain,
select(a_20,i1) = e_19,
inference(superposition,[status(thm)],[c_74,c_72]) ).
tcf(c_234,plain,
select(a_22,i1) = e_21,
inference(superposition,[status(thm)],[c_75,c_72]) ).
tcf(c_235,plain,
select(a_24,i2) = e_23,
inference(superposition,[status(thm)],[c_76,c_72]) ).
tcf(c_236,plain,
select(a_26,i2) = e_25,
inference(superposition,[status(thm)],[c_77,c_72]) ).
tcf(c_237,plain,
select(a_28,i3) = e_27,
inference(superposition,[status(thm)],[c_78,c_72]) ).
tcf(c_238,plain,
select(a_30,i3) = e_29,
inference(superposition,[status(thm)],[c_79,c_72]) ).
tcf(c_239,plain,
select(a_34,i4) = e_31,
inference(superposition,[status(thm)],[c_80,c_72]) ).
tcf(c_240,plain,
select(a_34,i4) = e_33,
inference(superposition,[status(thm)],[c_81,c_72]) ).
tcf(c_244,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_20,X0) = select(a1,X0) ) ),
inference(superposition,[status(thm)],[c_74,c_73]) ).
tcf(c_245,plain,
! [X0: $i] :
( ( X0 = i1 )
| ( select(a_22,X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_75,c_73]) ).
tcf(c_246,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_20,X0) = select(a_24,X0) ) ),
inference(superposition,[status(thm)],[c_76,c_73]) ).
tcf(c_247,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_22,X0) = select(a_26,X0) ) ),
inference(superposition,[status(thm)],[c_77,c_73]) ).
tcf(c_248,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(a_24,X0) = select(a_28,X0) ) ),
inference(superposition,[status(thm)],[c_78,c_73]) ).
tcf(c_249,plain,
! [X0: $i] :
( ( X0 = i3 )
| ( select(a_26,X0) = select(a_30,X0) ) ),
inference(superposition,[status(thm)],[c_79,c_73]) ).
tcf(c_250,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_28,X0) = select(a_34,X0) ) ),
inference(superposition,[status(thm)],[c_80,c_73]) ).
tcf(c_251,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_30,X0) = select(a_34,X0) ) ),
inference(superposition,[status(thm)],[c_81,c_73]) ).
tcf(c_277,plain,
e_31 = e_33,
inference(light_normalisation,[status(thm)],[c_240,c_239]) ).
tcf(c_278,plain,
store(a_30,i4,e_31) = a_34,
inference(demodulation,[status(thm)],[c_81,c_277]) ).
tcf(c_279,plain,
select(a_28,i4) = e_31,
inference(demodulation,[status(thm)],[c_89,c_277]) ).
tcf(c_288,plain,
( ( i1 = i2 )
| ( select(a1,i2) = e_25 ) ),
inference(superposition,[status(thm)],[c_244,c_85]) ).
tcf(c_302,plain,
( ( i1 = i2 )
| ( select(a2,i2) = e_23 ) ),
inference(superposition,[status(thm)],[c_245,c_84]) ).
tcf(c_316,plain,
( ( i2 = i3 )
| ( select(a_20,i3) = e_29 ) ),
inference(superposition,[status(thm)],[c_246,c_87]) ).
tcf(c_324,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(a1,i3) = e_29 ) ),
inference(superposition,[status(thm)],[c_244,c_316]) ).
tcf(c_335,plain,
( ( i2 = i3 )
| ( select(a_22,i3) = e_27 ) ),
inference(superposition,[status(thm)],[c_247,c_86]) ).
tcf(c_343,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( select(a2,i3) = e_27 ) ),
inference(superposition,[status(thm)],[c_245,c_335]) ).
tcf(c_354,plain,
( ( i3 = i4 )
| ( select(a_24,i4) = e_31 ) ),
inference(superposition,[status(thm)],[c_248,c_279]) ).
tcf(c_362,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(a_20,i4) = e_31 ) ),
inference(superposition,[status(thm)],[c_246,c_354]) ).
tcf(c_373,plain,
( ( i3 = i4 )
| ( select(a_26,i4) = e_31 ) ),
inference(superposition,[status(thm)],[c_249,c_88]) ).
tcf(c_383,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( select(a_22,i4) = e_31 ) ),
inference(superposition,[status(thm)],[c_247,c_373]) ).
tcf(c_403,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( select(a_28,X0) = select(a_30,X0) ) ),
inference(superposition,[status(thm)],[c_251,c_250]) ).
tcf(c_415,plain,
( ( i3 = i4 )
| ( select(a_28,i3) = e_29 ) ),
inference(superposition,[status(thm)],[c_403,c_238]) ).
tcf(c_416,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( select(a_26,X0) = select(a_28,X0) ) ),
inference(superposition,[status(thm)],[c_403,c_249]) ).
tcf(c_417,plain,
( ( e_27 = e_29 )
| ( i3 = i4 ) ),
inference(light_normalisation,[status(thm)],[c_415,c_237]) ).
tcf(c_461,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i1 = i4 )
| ( select(a1,i4) = e_31 ) ),
inference(superposition,[status(thm)],[c_244,c_362]) ).
tcf(c_473,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i1 = i4 )
| ( select(a2,i4) = e_31 ) ),
inference(superposition,[status(thm)],[c_245,c_383]) ).
tcf(c_490,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( select(a_24,X0) = select(a_26,X0) ) ),
inference(superposition,[status(thm)],[c_416,c_248]) ).
tcf(c_506,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( select(a_24,i2) = e_25 ) ),
inference(superposition,[status(thm)],[c_490,c_236]) ).
tcf(c_507,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( select(a_22,X0) = select(a_24,X0) ) ),
inference(superposition,[status(thm)],[c_490,c_247]) ).
tcf(c_509,plain,
( ( e_23 = e_25 )
| ( i2 = i4 )
| ( i2 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_506,c_235]) ).
tcf(c_528,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( store(a_22,i2,e_23) = a_26 ) ),
inference(superposition,[status(thm)],[c_509,c_77]) ).
tcf(c_539,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( select(a_26,i2) = e_23 ) ),
inference(superposition,[status(thm)],[c_528,c_72]) ).
tcf(c_575,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( select(a_20,X0) = select(a_22,X0) ) ),
inference(superposition,[status(thm)],[c_507,c_246]) ).
tcf(c_596,plain,
( ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_20,i1) = e_21 ) ),
inference(superposition,[status(thm)],[c_575,c_234]) ).
tcf(c_597,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( X0 = i1 )
| ( select(a_20,X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_575,c_245]) ).
tcf(c_600,plain,
( ( e_19 = e_21 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_596,c_233]) ).
tcf(c_659,plain,
! [X0: $i] :
( ( X0 = i4 )
| ( X0 = i3 )
| ( X0 = i2 )
| ( X0 = i1 )
| ( select(a1,X0) = select(a2,X0) ) ),
inference(superposition,[status(thm)],[c_597,c_244]) ).
tcf(c_684,plain,
( ( i4 = i_35 )
| ( i3 = i_35 )
| ( i2 = i_35 )
| ( i1 = i_35 )
| ( select(a1,i_35) = e_37 ) ),
inference(superposition,[status(thm)],[c_659,c_91]) ).
tcf(c_688,plain,
( ( e_36 = e_37 )
| ( i4 = i_35 )
| ( i3 = i_35 )
| ( i2 = i_35 )
| ( i1 = i_35 ) ),
inference(light_normalisation,[status(thm)],[c_684,c_90]) ).
tcf(c_689,plain,
( ( i4 = i_35 )
| ( i3 = i_35 )
| ( i2 = i_35 )
| ( i1 = i_35 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_688,c_149]) ).
tcf(c_702,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i1 = i_35 )
| ( select(a2,i4) = e_37 ) ),
inference(superposition,[status(thm)],[c_689,c_91]) ).
tcf(c_703,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i1 = i_35 )
| ( select(a1,i4) = e_36 ) ),
inference(superposition,[status(thm)],[c_689,c_90]) ).
tcf(c_740,plain,
( ( e_31 = e_37 )
| ( i3 = i_35 )
| ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i1 = i_35 )
| ( i1 = i4 ) ),
inference(superposition,[status(thm)],[c_702,c_473]) ).
tcf(c_773,plain,
( ( e_31 = e_36 )
| ( i3 = i_35 )
| ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i1 = i_35 )
| ( i1 = i4 ) ),
inference(superposition,[status(thm)],[c_461,c_703]) ).
tcf(c_796,plain,
( ( i3 = i_35 )
| ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( e_31 != e_36 ) ),
inference(superposition,[status(thm)],[c_740,c_149]) ).
tcf(c_804,plain,
( ( i3 = i_35 )
| ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i1 = i_35 )
| ( i1 = i4 ) ),
inference(global_subsumption_just,[status(thm)],[c_796,c_773,c_796]) ).
tcf(c_820,plain,
( ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( select(a2,i3) = e_37 ) ),
inference(superposition,[status(thm)],[c_804,c_91]) ).
tcf(c_821,plain,
( ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( select(a1,i3) = e_36 ) ),
inference(superposition,[status(thm)],[c_804,c_90]) ).
tcf(c_849,plain,
( ( e_27 = e_37 )
| ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 ) ),
inference(superposition,[status(thm)],[c_820,c_343]) ).
tcf(c_870,plain,
( ( e_29 = e_36 )
| ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 ) ),
inference(superposition,[status(thm)],[c_324,c_821]) ).
tcf(c_896,plain,
( ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( e_27 != e_36 ) ),
inference(superposition,[status(thm)],[c_849,c_149]) ).
tcf(c_937,plain,
( ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( e_27 != e_29 ) ),
inference(superposition,[status(thm)],[c_870,c_896]) ).
tcf(c_950,plain,
( ( i3 = i4 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 ) ),
inference(global_subsumption_just,[status(thm)],[c_937,c_417,c_937]) ).
tcf(c_970,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( select(a2,i2) = e_37 ) ),
inference(superposition,[status(thm)],[c_950,c_91]) ).
tcf(c_971,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( select(a1,i2) = e_36 ) ),
inference(superposition,[status(thm)],[c_950,c_90]) ).
tcf(c_1003,plain,
( ( i3 = i4 )
| ( e_23 = e_37 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_970,c_302]) ).
tcf(c_1026,plain,
( ( i3 = i4 )
| ( e_25 = e_36 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_288,c_971]) ).
tcf(c_1052,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_36 ) ),
inference(superposition,[status(thm)],[c_1003,c_149]) ).
tcf(c_1094,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_25 ) ),
inference(superposition,[status(thm)],[c_1026,c_1052]) ).
tcf(c_1109,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_1094,c_509,c_1094]) ).
tcf(c_1131,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i1) = e_37 ) ),
inference(superposition,[status(thm)],[c_1109,c_91]) ).
tcf(c_1132,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i1) = e_36 ) ),
inference(superposition,[status(thm)],[c_1109,c_90]) ).
tcf(c_1133,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( e_21 = e_36 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_1132,c_83]) ).
tcf(c_1141,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( e_19 = e_37 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_1131,c_82]) ).
tcf(c_1177,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_36 ) ),
inference(superposition,[status(thm)],[c_1141,c_149]) ).
tcf(c_1199,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_21 ) ),
inference(superposition,[status(thm)],[c_1133,c_1177]) ).
tcf(c_1215,plain,
( ( i3 = i4 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_1199,c_600,c_1199]) ).
tcf(c_1229,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i3) = e_36 ) ),
inference(superposition,[status(thm)],[c_1215,c_703]) ).
tcf(c_1230,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i3) = e_37 ) ),
inference(superposition,[status(thm)],[c_1215,c_702]) ).
tcf(c_1237,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( store(a_30,i3,e_31) = a_34 ) ),
inference(superposition,[status(thm)],[c_1215,c_278]) ).
tcf(c_1238,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_28,i3) = e_31 ) ),
inference(superposition,[status(thm)],[c_1215,c_279]) ).
tcf(c_1241,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_30,i3) = e_31 ) ),
inference(superposition,[status(thm)],[c_1215,c_88]) ).
tcf(c_1242,plain,
( ( e_29 = e_31 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_1241,c_238]) ).
tcf(c_1255,plain,
( ( e_27 = e_31 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_1238,c_237]) ).
tcf(c_1320,plain,
! [X0: $i] :
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i3 )
| ( select(a_30,X0) = select(a_34,X0) ) ),
inference(superposition,[status(thm)],[c_1237,c_73]) ).
tcf(c_1387,plain,
( ( e_29 = e_36 )
| ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_324,c_1229]) ).
tcf(c_1419,plain,
( ( e_27 = e_37 )
| ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_1230,c_343]) ).
tcf(c_1530,plain,
! [X0: $i] :
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i4 )
| ( X0 = i3 )
| ( select(a_28,X0) = select(a_30,X0) ) ),
inference(superposition,[status(thm)],[c_1320,c_250]) ).
tcf(c_1583,plain,
( ( e_27 = e_29 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_1242,c_1255]) ).
tcf(c_1769,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_36 ) ),
inference(superposition,[status(thm)],[c_1419,c_149]) ).
tcf(c_1797,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_29 ) ),
inference(superposition,[status(thm)],[c_1387,c_1769]) ).
tcf(c_1826,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_1797,c_1583,c_1797]) ).
tcf(c_1848,plain,
( ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i3) = e_37 ) ),
inference(superposition,[status(thm)],[c_1826,c_91]) ).
tcf(c_1849,plain,
( ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i3) = e_36 ) ),
inference(superposition,[status(thm)],[c_1826,c_90]) ).
tcf(c_1885,plain,
( ( e_27 = e_37 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_1848,c_343]) ).
tcf(c_1910,plain,
( ( e_29 = e_36 )
| ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_324,c_1849]) ).
tcf(c_1936,plain,
( ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_36 ) ),
inference(superposition,[status(thm)],[c_1885,c_149]) ).
tcf(c_2032,plain,
( ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_29 ) ),
inference(superposition,[status(thm)],[c_1910,c_1936]) ).
tcf(c_2129,plain,
( ( i2 = i_35 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_2032,c_1583,c_2032]) ).
tcf(c_2149,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i2) = e_37 ) ),
inference(superposition,[status(thm)],[c_2129,c_91]) ).
tcf(c_2150,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i2) = e_36 ) ),
inference(superposition,[status(thm)],[c_2129,c_90]) ).
tcf(c_2182,plain,
( ( e_23 = e_37 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_2149,c_302]) ).
tcf(c_2204,plain,
( ( e_25 = e_36 )
| ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_288,c_2150]) ).
tcf(c_2227,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_36 ) ),
inference(superposition,[status(thm)],[c_2182,c_149]) ).
tcf(c_2263,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_25 ) ),
inference(superposition,[status(thm)],[c_2204,c_2227]) ).
tcf(c_2271,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_2263,c_509,c_2263]) ).
tcf(c_2291,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i1) = e_37 ) ),
inference(superposition,[status(thm)],[c_2271,c_91]) ).
tcf(c_2292,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i1) = e_36 ) ),
inference(superposition,[status(thm)],[c_2271,c_90]) ).
tcf(c_2293,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( e_21 = e_36 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_2292,c_83]) ).
tcf(c_2300,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( e_19 = e_37 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_2291,c_82]) ).
tcf(c_2331,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_36 ) ),
inference(superposition,[status(thm)],[c_2300,c_149]) ).
tcf(c_2350,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_21 ) ),
inference(superposition,[status(thm)],[c_2293,c_2331]) ).
tcf(c_2357,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_2350,c_600,c_2350]) ).
tcf(c_2369,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i2) = e_36 ) ),
inference(superposition,[status(thm)],[c_2357,c_703]) ).
tcf(c_2370,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i2) = e_37 ) ),
inference(superposition,[status(thm)],[c_2357,c_702]) ).
tcf(c_2377,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( store(a_30,i2,e_31) = a_34 ) ),
inference(superposition,[status(thm)],[c_2357,c_278]) ).
tcf(c_2378,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_28,i2) = e_31 ) ),
inference(superposition,[status(thm)],[c_2357,c_279]) ).
tcf(c_2380,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( store(a_28,i2,e_31) = a_34 ) ),
inference(superposition,[status(thm)],[c_2357,c_80]) ).
tcf(c_2381,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_30,i2) = e_31 ) ),
inference(superposition,[status(thm)],[c_2357,c_88]) ).
tcf(c_2450,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_26,i2) = e_31 ) ),
inference(superposition,[status(thm)],[c_2381,c_249]) ).
tcf(c_2451,plain,
( ( e_25 = e_31 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_2450,c_236]) ).
tcf(c_2467,plain,
! [X0: $i] :
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i2 )
| ( select(a_28,X0) = select(a_34,X0) ) ),
inference(superposition,[status(thm)],[c_2380,c_73]) ).
tcf(c_2517,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_24,i2) = e_31 ) ),
inference(superposition,[status(thm)],[c_2378,c_248]) ).
tcf(c_2518,plain,
( ( e_23 = e_31 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_2517,c_235]) ).
tcf(c_2534,plain,
( ( e_23 = e_25 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_2451,c_2518]) ).
tcf(c_2601,plain,
! [X0: $i] :
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i2 )
| ( select(a_30,X0) = select(a_34,X0) ) ),
inference(superposition,[status(thm)],[c_2377,c_73]) ).
tcf(c_2636,plain,
( ( i3 = i_35 )
| ( e_25 = e_36 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_288,c_2369]) ).
tcf(c_2665,plain,
( ( i3 = i_35 )
| ( e_23 = e_37 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_2370,c_302]) ).
tcf(c_2906,plain,
! [X0: $i] :
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i2 )
| ( select(a_28,X0) = select(a_30,X0) ) ),
inference(superposition,[status(thm)],[c_2601,c_2467]) ).
tcf(c_2934,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_36 ) ),
inference(superposition,[status(thm)],[c_2665,c_149]) ).
tcf(c_2959,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_25 ) ),
inference(superposition,[status(thm)],[c_2636,c_2934]) ).
tcf(c_2968,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_2959,c_2534,c_2959]) ).
tcf(c_2988,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i3) = e_37 ) ),
inference(superposition,[status(thm)],[c_2968,c_91]) ).
tcf(c_2989,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i3) = e_36 ) ),
inference(superposition,[status(thm)],[c_2968,c_90]) ).
tcf(c_3031,plain,
( ( e_27 = e_37 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_2988,c_343]) ).
tcf(c_3053,plain,
( ( e_29 = e_36 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_324,c_2989]) ).
tcf(c_3079,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_28,i3) = e_29 ) ),
inference(superposition,[status(thm)],[c_2906,c_238]) ).
tcf(c_3082,plain,
( ( e_27 = e_29 )
| ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3079,c_237]) ).
tcf(c_3159,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_36 ) ),
inference(superposition,[status(thm)],[c_3031,c_149]) ).
tcf(c_3195,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_29 ) ),
inference(superposition,[status(thm)],[c_3053,c_3159]) ).
tcf(c_3203,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_3195,c_3082,c_3195]) ).
tcf(c_3221,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i2) = e_37 ) ),
inference(superposition,[status(thm)],[c_3203,c_91]) ).
tcf(c_3222,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i2) = e_36 ) ),
inference(superposition,[status(thm)],[c_3203,c_90]) ).
tcf(c_3250,plain,
( ( e_23 = e_37 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_3221,c_302]) ).
tcf(c_3269,plain,
( ( e_25 = e_36 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_288,c_3222]) ).
tcf(c_3289,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_36 ) ),
inference(superposition,[status(thm)],[c_3250,c_149]) ).
tcf(c_3320,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_25 ) ),
inference(superposition,[status(thm)],[c_3269,c_3289]) ).
tcf(c_3327,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_3320,c_2534,c_3320]) ).
tcf(c_3345,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i1) = e_37 ) ),
inference(superposition,[status(thm)],[c_3327,c_91]) ).
tcf(c_3346,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i1) = e_36 ) ),
inference(superposition,[status(thm)],[c_3327,c_90]) ).
tcf(c_3347,plain,
( ( i2 = i3 )
| ( e_21 = e_36 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3346,c_83]) ).
tcf(c_3353,plain,
( ( i2 = i3 )
| ( e_19 = e_37 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3345,c_82]) ).
tcf(c_3379,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_36 ) ),
inference(superposition,[status(thm)],[c_3353,c_149]) ).
tcf(c_3395,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_21 ) ),
inference(superposition,[status(thm)],[c_3347,c_3379]) ).
tcf(c_3401,plain,
( ( i1 = i2 )
| ( i1 = i3 )
| ( i1 = i4 )
| ( i2 = i3 ) ),
inference(global_subsumption_just,[status(thm)],[c_1530,c_600,c_3395]) ).
tcf(c_3402,plain,
( ( i2 = i3 )
| ( i1 = i4 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(renaming,[status(thm)],[c_3401]) ).
tcf(c_3411,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i1) = e_36 ) ),
inference(superposition,[status(thm)],[c_3402,c_703]) ).
tcf(c_3412,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i1) = e_37 ) ),
inference(superposition,[status(thm)],[c_3402,c_702]) ).
tcf(c_3419,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( store(a_30,i1,e_31) = a_34 ) ),
inference(superposition,[status(thm)],[c_3402,c_278]) ).
tcf(c_3420,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_28,i1) = e_31 ) ),
inference(superposition,[status(thm)],[c_3402,c_279]) ).
tcf(c_3422,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( store(a_28,i1,e_31) = a_34 ) ),
inference(superposition,[status(thm)],[c_3402,c_80]) ).
tcf(c_3423,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_30,i1) = e_31 ) ),
inference(superposition,[status(thm)],[c_3402,c_88]) ).
tcf(c_3468,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( e_19 = e_37 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3412,c_82]) ).
tcf(c_3476,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( e_21 = e_36 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3411,c_83]) ).
tcf(c_3495,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_26,i1) = e_31 ) ),
inference(superposition,[status(thm)],[c_3423,c_249]) ).
tcf(c_3508,plain,
! [X0: $i] :
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i1 )
| ( select(a_28,X0) = select(a_34,X0) ) ),
inference(superposition,[status(thm)],[c_3422,c_73]) ).
tcf(c_3548,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_24,i1) = e_31 ) ),
inference(superposition,[status(thm)],[c_3420,c_248]) ).
tcf(c_3578,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_22,i1) = e_31 ) ),
inference(superposition,[status(thm)],[c_3495,c_247]) ).
tcf(c_3579,plain,
( ( i2 = i3 )
| ( e_21 = e_31 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3578,c_234]) ).
tcf(c_3618,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_20,i1) = e_31 ) ),
inference(superposition,[status(thm)],[c_3548,c_246]) ).
tcf(c_3619,plain,
( ( i2 = i3 )
| ( e_19 = e_31 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_3618,c_233]) ).
tcf(c_3640,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_36 ) ),
inference(superposition,[status(thm)],[c_3468,c_149]) ).
tcf(c_3676,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_21 ) ),
inference(superposition,[status(thm)],[c_3476,c_3640]) ).
tcf(c_3710,plain,
! [X0: $i] :
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i1 )
| ( select(a_30,X0) = select(a_34,X0) ) ),
inference(superposition,[status(thm)],[c_3419,c_73]) ).
tcf(c_3752,plain,
! [X0: $i] :
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( X0 = i1 )
| ( select(a_28,X0) = select(a_30,X0) ) ),
inference(superposition,[status(thm)],[c_3710,c_3508]) ).
tcf(c_3771,plain,
( ( i2 = i3 )
| ( e_19 = e_21 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_3619,c_3579]) ).
tcf(c_3815,plain,
( ( i3 = i_35 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3676,c_3771]) ).
tcf(c_3891,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i3) = e_37 ) ),
inference(superposition,[status(thm)],[c_3815,c_91]) ).
tcf(c_3892,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i3) = e_36 ) ),
inference(superposition,[status(thm)],[c_3815,c_90]) ).
tcf(c_3929,plain,
( ( e_27 = e_37 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_3891,c_343]) ).
tcf(c_3948,plain,
( ( e_29 = e_36 )
| ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_324,c_3892]) ).
tcf(c_3968,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_36 ) ),
inference(superposition,[status(thm)],[c_3929,c_149]) ).
tcf(c_3999,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_27 != e_29 ) ),
inference(superposition,[status(thm)],[c_3948,c_3968]) ).
tcf(c_4321,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a_28,i3) = e_29 ) ),
inference(superposition,[status(thm)],[c_3752,c_238]) ).
tcf(c_4324,plain,
( ( e_27 = e_29 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_4321,c_237]) ).
tcf(c_4372,plain,
( ( i2 = i_35 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3999,c_4324]) ).
tcf(c_4408,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i2) = e_37 ) ),
inference(superposition,[status(thm)],[c_4372,c_91]) ).
tcf(c_4409,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i2) = e_36 ) ),
inference(superposition,[status(thm)],[c_4372,c_90]) ).
tcf(c_4440,plain,
( ( e_23 = e_37 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_4408,c_302]) ).
tcf(c_4456,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_36 ) ),
inference(superposition,[status(thm)],[c_4440,c_149]) ).
tcf(c_4483,plain,
( ( e_25 = e_36 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_288,c_4409]) ).
tcf(c_4538,plain,
( ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_23 != e_25 ) ),
inference(superposition,[status(thm)],[c_4483,c_4456]) ).
tcf(c_4554,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i_35 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_509,c_4538]) ).
tcf(c_4578,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a2,i1) = e_37 ) ),
inference(superposition,[status(thm)],[c_4554,c_91]) ).
tcf(c_4579,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( select(a1,i1) = e_36 ) ),
inference(superposition,[status(thm)],[c_4554,c_90]) ).
tcf(c_4580,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( e_21 = e_36 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_4579,c_83]) ).
tcf(c_4586,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( e_19 = e_37 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_4578,c_82]) ).
tcf(c_4623,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_36 ) ),
inference(superposition,[status(thm)],[c_4586,c_149]) ).
tcf(c_4645,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 )
| ( e_19 != e_21 ) ),
inference(superposition,[status(thm)],[c_4580,c_4623]) ).
tcf(c_4652,plain,
( ( i2 = i4 )
| ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(global_subsumption_just,[status(thm)],[c_4645,c_3771,c_4645]) ).
tcf(c_4667,plain,
( ( i2 = i3 )
| ( i1 = i3 )
| ( i1 = i2 ) ),
inference(superposition,[status(thm)],[c_4652,c_3402]) ).
tcf(c_8002,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_4667,c_950,c_804,c_689,c_600,c_539,c_506,c_417,c_383,c_373,c_362,c_354,c_343,c_335,c_324,c_316,c_302,c_288,c_279,c_238,c_237,c_236,c_235,c_234,c_233,c_149,c_91,c_90,c_88,c_87,c_86,c_85,c_84,c_83,c_82]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV555-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/5.37 % Computer : n004.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Thu Sep 24 20:29:26 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/5.41 Running first-order theorem proving
% 0.15/5.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.43
% 0.15/5.43 % ======== iProver multi-core TPTP/SMT =========
% 0.15/5.43
% 0.15/5.43 % Detected problem language: tptp
% 0.15/5.44 % Proving...
% 0.15/6.08 % SZS status Started for theBenchmark.p
% 0.15/6.08 % SZS status Unsatisfiable for theBenchmark.p
% 0.15/6.08
% 0.15/6.08 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 0.15/6.08
% 0.15/6.08 % ------ iProver source info
% 0.15/6.08
% 0.15/6.08 % git: date: 2026-07-19 20:42:38 +0200
% 0.15/6.08 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 0.15/6.08 % git: non_committed_changes: false
% 0.15/6.08
% 0.15/6.08 % ------ Parsing...% successful
% 0.15/6.08
% 0.15/6.08
% 0.15/6.08 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 0.15/6.08
% 0.15/6.08 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 0.15/6.08
% 0.15/6.08 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 0.15/6.08
% 0.15/6.08 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 0.15/6.08 % ------ Proving...
% 0.15/6.08 % ------ Problem Properties
% 0.15/6.08
% 0.15/6.08 %
% 0.15/6.08 % clauses 22
% 0.15/6.08 % conjectures 1
% 0.15/6.08 % EPR 1
% 0.15/6.08 % Horn 21
% 0.15/6.08 % unary 21
% 0.15/6.08 % binary 1
% 0.15/6.08 % lits 23
% 0.15/6.08 % lits eq 23
% 0.15/6.08 % fd_pure 0
% 0.15/6.08 % fd_pseudo 0
% 0.15/6.08 % fd_cond 0
% 0.15/6.08 % fd_pseudo_cond 1
% 0.15/6.08 % AC symbols 0
% 0.15/6.08
% 0.15/6.08 % ------ Schedule dynamic 5 is on
% 0.15/6.08
% 0.15/6.08 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 0.15/6.08
% 0.15/6.08
% 0.15/6.08 % ------
% 0.15/6.08 % Current options:
% 0.15/6.08 % ------
% 0.15/6.08
% 0.15/6.08
% 0.15/6.08 %
% 0.15/6.08
% 0.15/6.08 % ------ Proving...
% 0.15/6.08 %
% 0.15/6.08
% 0.15/6.08 % SZS status Unsatisfiable for theBenchmark.p
% 0.15/6.08
% 0.15/6.08 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 0.15/6.09
% 0.15/6.09
%------------------------------------------------------------------------------