%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWV540-1.004 : 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 : n007.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:17 PM UTC 2026
% Result : Unsatisfiable 33.92s 6.49s
% Output : CNFRefutation 40.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 28
% Syntax : Number of formulae : 238 ( 130 unt; 0 def)
% Number of atoms : 349 ( 348 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 118 ( 7 ~; 111 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 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 : 28 ( 28 usr; 26 con; 0-3 aty)
% Number of variables : 82 ( 0 sgn 82 !; 0 ?; 64 :)
% 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,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
fof(f4,axiom,
! [X2,X3,X0,X1] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
fof(f5,axiom,
! [X2,X3,X0,X1,X4] :
( store(store(X2,X0,X3),X1,X4) = store(store(X2,X1,X4),X0,X3)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).
fof(f8,axiom,
a_420 = store(a_418,i0,e_419),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f9,axiom,
a_422 = store(a_420,i3,e_421),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f10,axiom,
a_424 = store(a_422,i3,e_423),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f11,axiom,
a_426 = store(a_424,i2,e_425),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f12,axiom,
a_428 = store(a_426,i2,e_427),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f13,axiom,
a_430 = store(a_428,i0,e_429),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f14,axiom,
a_431 = store(a_418,i3,e_421),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f15,axiom,
a_432 = store(a_431,i0,e_419),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f16,axiom,
a_434 = store(a_432,i3,e_433),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f17,axiom,
a_436 = store(a_434,i2,e_435),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f18,axiom,
a_438 = store(a_436,i0,e_437),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f19,axiom,
a_440 = store(a_438,i2,e_439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f21,axiom,
e_419 = select(a_418,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f22,axiom,
e_421 = select(a_418,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f23,axiom,
e_423 = select(a_422,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp17) ).
fof(f24,axiom,
e_425 = select(a_422,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp18) ).
fof(f25,axiom,
e_427 = select(a_426,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp19) ).
fof(f26,axiom,
e_429 = select(a_426,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp20) ).
fof(f27,axiom,
e_433 = select(a_432,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp21) ).
fof(f28,axiom,
e_435 = select(a_432,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp22) ).
fof(f29,axiom,
e_437 = select(a_436,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp23) ).
fof(f30,axiom,
e_439 = select(a_436,i0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp24) ).
fof(f31,negated_conjecture,
a_430 != a_440,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[],[f1]) ).
tcf(c_81,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_82,plain,
! [X0: $i,X1: $i] : store(X0,X1,select(X0,X1)) = X0,
inference(cnf_transformation,[],[f3]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
inference(cnf_transformation,[],[f4]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X1 = X3 )
| ( store(store(X0,X1,X2),X3,X4) = store(store(X0,X3,X4),X1,X2) ) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_87,plain,
store(a_418,i0,e_419) = a_420,
inference(cnf_transformation,[],[f8]) ).
tcf(c_88,plain,
store(a_420,i3,e_421) = a_422,
inference(cnf_transformation,[],[f9]) ).
tcf(c_89,plain,
store(a_422,i3,e_423) = a_424,
inference(cnf_transformation,[],[f10]) ).
tcf(c_90,plain,
store(a_424,i2,e_425) = a_426,
inference(cnf_transformation,[],[f11]) ).
tcf(c_91,plain,
store(a_426,i2,e_427) = a_428,
inference(cnf_transformation,[],[f12]) ).
tcf(c_92,plain,
store(a_428,i0,e_429) = a_430,
inference(cnf_transformation,[],[f13]) ).
tcf(c_93,plain,
store(a_418,i3,e_421) = a_431,
inference(cnf_transformation,[],[f14]) ).
tcf(c_94,plain,
store(a_431,i0,e_419) = a_432,
inference(cnf_transformation,[],[f15]) ).
tcf(c_95,plain,
store(a_432,i3,e_433) = a_434,
inference(cnf_transformation,[],[f16]) ).
tcf(c_96,plain,
store(a_434,i2,e_435) = a_436,
inference(cnf_transformation,[],[f17]) ).
tcf(c_97,plain,
store(a_436,i0,e_437) = a_438,
inference(cnf_transformation,[],[f18]) ).
tcf(c_98,plain,
store(a_438,i2,e_439) = a_440,
inference(cnf_transformation,[],[f19]) ).
tcf(c_100,plain,
select(a_418,i3) = e_419,
inference(cnf_transformation,[],[f21]) ).
tcf(c_101,plain,
select(a_418,i0) = e_421,
inference(cnf_transformation,[],[f22]) ).
tcf(c_102,plain,
select(a_422,i2) = e_423,
inference(cnf_transformation,[],[f23]) ).
tcf(c_103,plain,
select(a_422,i3) = e_425,
inference(cnf_transformation,[],[f24]) ).
tcf(c_104,plain,
select(a_426,i0) = e_427,
inference(cnf_transformation,[],[f25]) ).
tcf(c_105,plain,
select(a_426,i2) = e_429,
inference(cnf_transformation,[],[f26]) ).
tcf(c_106,plain,
select(a_432,i2) = e_433,
inference(cnf_transformation,[],[f27]) ).
tcf(c_107,plain,
select(a_432,i3) = e_435,
inference(cnf_transformation,[],[f28]) ).
tcf(c_108,plain,
select(a_436,i2) = e_437,
inference(cnf_transformation,[],[f29]) ).
tcf(c_109,plain,
select(a_436,i0) = e_439,
inference(cnf_transformation,[],[f30]) ).
tcf(c_110,negated_conjecture,
a_430 != a_440,
inference(cnf_transformation,[],[f31]) ).
tcf(c_192,negated_conjecture,
a_430 != a_440,
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_290,plain,
select(a_420,i0) = e_419,
inference(superposition,[status(thm)],[c_87,c_80]) ).
tcf(c_291,plain,
select(a_422,i3) = e_421,
inference(superposition,[status(thm)],[c_88,c_80]) ).
tcf(c_292,plain,
select(a_424,i3) = e_423,
inference(superposition,[status(thm)],[c_89,c_80]) ).
tcf(c_293,plain,
select(a_426,i2) = e_425,
inference(superposition,[status(thm)],[c_90,c_80]) ).
tcf(c_296,plain,
select(a_431,i3) = e_421,
inference(superposition,[status(thm)],[c_93,c_80]) ).
tcf(c_297,plain,
select(a_432,i0) = e_419,
inference(superposition,[status(thm)],[c_94,c_80]) ).
tcf(c_298,plain,
select(a_434,i3) = e_433,
inference(superposition,[status(thm)],[c_95,c_80]) ).
tcf(c_299,plain,
select(a_436,i2) = e_435,
inference(superposition,[status(thm)],[c_96,c_80]) ).
tcf(c_302,plain,
e_421 = e_425,
inference(demodulation,[status(thm)],[c_103,c_291]) ).
tcf(c_303,plain,
store(a_424,i2,e_421) = a_426,
inference(demodulation,[status(thm)],[c_90,c_302]) ).
tcf(c_304,plain,
e_425 = e_429,
inference(demodulation,[status(thm)],[c_105,c_293]) ).
tcf(c_305,plain,
store(a_428,i0,e_425) = a_430,
inference(demodulation,[status(thm)],[c_92,c_304]) ).
tcf(c_306,plain,
e_435 = e_437,
inference(demodulation,[status(thm)],[c_108,c_299]) ).
tcf(c_307,plain,
store(a_436,i0,e_435) = a_438,
inference(demodulation,[status(thm)],[c_97,c_306]) ).
tcf(c_311,plain,
store(a_418,i0,e_421) = a_418,
inference(superposition,[status(thm)],[c_101,c_82]) ).
tcf(c_312,plain,
store(a_422,i2,e_423) = a_422,
inference(superposition,[status(thm)],[c_102,c_82]) ).
tcf(c_313,plain,
store(a_426,i0,e_427) = a_426,
inference(superposition,[status(thm)],[c_104,c_82]) ).
tcf(c_324,plain,
! [X0: $i] : store(a_418,i0,X0) = store(a_420,i0,X0),
inference(superposition,[status(thm)],[c_87,c_83]) ).
tcf(c_325,plain,
! [X0: $i] : store(a_420,i3,X0) = store(a_422,i3,X0),
inference(superposition,[status(thm)],[c_88,c_83]) ).
tcf(c_326,plain,
! [X0: $i] : store(a_422,i3,X0) = store(a_424,i3,X0),
inference(superposition,[status(thm)],[c_89,c_83]) ).
tcf(c_328,plain,
! [X0: $i] : store(a_418,i3,X0) = store(a_431,i3,X0),
inference(superposition,[status(thm)],[c_93,c_83]) ).
tcf(c_329,plain,
! [X0: $i] : store(a_431,i0,X0) = store(a_432,i0,X0),
inference(superposition,[status(thm)],[c_94,c_83]) ).
tcf(c_330,plain,
! [X0: $i] : store(a_432,i3,X0) = store(a_434,i3,X0),
inference(superposition,[status(thm)],[c_95,c_83]) ).
tcf(c_331,plain,
! [X0: $i] : store(a_434,i2,X0) = store(a_436,i2,X0),
inference(superposition,[status(thm)],[c_96,c_83]) ).
tcf(c_338,plain,
store(a_422,i3,e_421) = a_422,
inference(demodulation,[status(thm)],[c_88,c_325]) ).
tcf(c_339,plain,
store(a_432,i0,e_419) = a_432,
inference(demodulation,[status(thm)],[c_94,c_329]) ).
tcf(c_340,plain,
store(a_436,i2,e_435) = a_436,
inference(demodulation,[status(thm)],[c_96,c_331]) ).
tcf(c_358,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_418,X0) = select(a_420,X0) ) ),
inference(superposition,[status(thm)],[c_87,c_81]) ).
tcf(c_402,plain,
select(a_426,i2) = e_421,
inference(light_normalisation,[status(thm)],[c_293,c_302]) ).
tcf(c_403,plain,
store(a_426,i2,e_421) = a_426,
inference(superposition,[status(thm)],[c_402,c_82]) ).
tcf(c_433,plain,
! [X0: $i,X1: $i] :
( ( X0 = i0 )
| ( store(store(a_418,X0,X1),i0,e_419) = store(a_420,X0,X1) ) ),
inference(superposition,[status(thm)],[c_87,c_84]) ).
tcf(c_435,plain,
! [X0: $i,X1: $i] :
( ( X0 = i2 )
| ( store(store(a_426,X0,X1),i2,e_427) = store(a_428,X0,X1) ) ),
inference(superposition,[status(thm)],[c_91,c_84]) ).
tcf(c_448,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X1 = X3 )
| ( select(store(store(X0,X1,X2),X3,X4),X1) = X2 ) ),
inference(superposition,[status(thm)],[c_84,c_80]) ).
tcf(c_546,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_424,X0) = select(a_426,X0) ) ),
inference(superposition,[status(thm)],[c_303,c_81]) ).
tcf(c_547,plain,
! [X0: $i] : store(a_424,i2,X0) = store(a_426,i2,X0),
inference(superposition,[status(thm)],[c_303,c_83]) ).
tcf(c_549,plain,
! [X0: $i,X1: $i] :
( ( X0 = i2 )
| ( store(store(a_424,X0,X1),i2,e_421) = store(a_426,X0,X1) ) ),
inference(superposition,[status(thm)],[c_303,c_84]) ).
tcf(c_556,plain,
store(a_428,i0,e_421) = a_430,
inference(light_normalisation,[status(thm)],[c_305,c_302]) ).
tcf(c_571,plain,
! [X0: $i] : store(a_436,i0,X0) = store(a_438,i0,X0),
inference(superposition,[status(thm)],[c_307,c_83]) ).
tcf(c_711,plain,
store(a_422,i3,select(a_420,i3)) = a_420,
inference(superposition,[status(thm)],[c_325,c_82]) ).
tcf(c_827,plain,
store(a_432,i0,select(a_431,i0)) = a_431,
inference(superposition,[status(thm)],[c_329,c_82]) ).
tcf(c_837,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( select(a_431,X0) = select(a_432,X0) ) ),
inference(superposition,[status(thm)],[c_827,c_81]) ).
tcf(c_886,plain,
store(a_436,i2,select(a_434,i2)) = a_434,
inference(superposition,[status(thm)],[c_331,c_82]) ).
tcf(c_923,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( select(a_434,X0) = select(a_436,X0) ) ),
inference(superposition,[status(thm)],[c_886,c_81]) ).
tcf(c_944,plain,
store(a_426,i2,select(a_424,i2)) = a_424,
inference(superposition,[status(thm)],[c_547,c_82]) ).
tcf(c_1302,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( store(a_424,X0,select(a_426,X0)) = a_424 ) ),
inference(superposition,[status(thm)],[c_546,c_82]) ).
tcf(c_1421,plain,
! [X0: $i] :
( ( X0 = i0 )
| ( store(a_431,X0,select(a_432,X0)) = a_431 ) ),
inference(superposition,[status(thm)],[c_837,c_82]) ).
tcf(c_1422,plain,
( ( i0 = i3 )
| ( select(a_432,i3) = e_421 ) ),
inference(superposition,[status(thm)],[c_837,c_296]) ).
tcf(c_1426,plain,
( ( e_421 = e_435 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_1422,c_107]) ).
tcf(c_1440,plain,
( ( i0 = i3 )
| ( store(a_436,i2,e_421) = a_436 ) ),
inference(superposition,[status(thm)],[c_1426,c_340]) ).
tcf(c_1442,plain,
( ( i0 = i3 )
| ( store(a_436,i0,e_421) = a_438 ) ),
inference(superposition,[status(thm)],[c_1426,c_307]) ).
tcf(c_1524,plain,
! [X0: $i] :
( ( X0 = i2 )
| ( store(a_434,X0,select(a_436,X0)) = a_434 ) ),
inference(superposition,[status(thm)],[c_923,c_82]) ).
tcf(c_2197,plain,
( ( i0 = i2 )
| ( store(a_424,i0,e_427) = a_424 ) ),
inference(superposition,[status(thm)],[c_104,c_1302]) ).
tcf(c_2220,plain,
( ( i0 = i2 )
| ( select(a_424,i0) = e_427 ) ),
inference(superposition,[status(thm)],[c_2197,c_80]) ).
tcf(c_2464,plain,
( ( i0 = i2 )
| ( store(a_431,i2,e_433) = a_431 ) ),
inference(superposition,[status(thm)],[c_106,c_1421]) ).
tcf(c_2511,plain,
( ( i0 = i2 )
| ( select(a_431,i2) = e_433 ) ),
inference(superposition,[status(thm)],[c_2464,c_80]) ).
tcf(c_2557,plain,
( ( i0 = i2 )
| ( store(a_434,i0,e_439) = a_434 ) ),
inference(superposition,[status(thm)],[c_109,c_1524]) ).
tcf(c_2579,plain,
( ( i0 = i2 )
| ( select(a_434,i0) = e_439 ) ),
inference(superposition,[status(thm)],[c_2557,c_80]) ).
tcf(c_4502,plain,
! [X0: $i,X1: $i] :
( ( X0 = i2 )
| ( select(store(a_422,X0,X1),i2) = e_423 ) ),
inference(superposition,[status(thm)],[c_312,c_448]) ).
tcf(c_6304,plain,
( ( i0 = i3 )
| ( store(a_420,i3,e_421) = store(a_431,i0,e_419) ) ),
inference(superposition,[status(thm)],[c_93,c_433]) ).
tcf(c_6417,plain,
( ( a_422 = a_432 )
| ( i0 = i3 ) ),
inference(demodulation,[status(thm)],[c_6304,c_325,c_329,c_338,c_339]) ).
tcf(c_6443,plain,
( ( i0 = i3 )
| ( store(a_422,i3,e_433) = a_434 ) ),
inference(superposition,[status(thm)],[c_6417,c_95]) ).
tcf(c_6445,plain,
( ( i0 = i3 )
| ( select(a_422,i2) = e_433 ) ),
inference(superposition,[status(thm)],[c_6417,c_106]) ).
tcf(c_6446,plain,
( ( e_423 = e_433 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_6445,c_102]) ).
tcf(c_6712,plain,
( ( i0 = i3 )
| ( store(a_422,i3,e_423) = a_434 ) ),
inference(superposition,[status(thm)],[c_6446,c_6443]) ).
tcf(c_6725,plain,
( ( a_424 = a_434 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_6712,c_89]) ).
tcf(c_7118,plain,
! [X0: $i] :
( ( i0 = i3 )
| ( store(a_424,i2,X0) = store(a_436,i2,X0) ) ),
inference(superposition,[status(thm)],[c_6725,c_331]) ).
tcf(c_7125,plain,
! [X0: $i] :
( ( i0 = i3 )
| ( store(a_426,i2,X0) = store(a_436,i2,X0) ) ),
inference(light_normalisation,[status(thm)],[c_7118,c_547]) ).
tcf(c_8003,plain,
( ( i0 = i3 )
| ( store(a_426,i2,e_421) = a_436 ) ),
inference(superposition,[status(thm)],[c_7125,c_1440]) ).
tcf(c_8006,plain,
( ( a_426 = a_436 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_8003,c_403]) ).
tcf(c_8100,plain,
( ( i0 = i3 )
| ( store(a_426,i0,e_421) = a_438 ) ),
inference(superposition,[status(thm)],[c_8006,c_1442]) ).
tcf(c_8108,plain,
( ( i0 = i3 )
| ( select(a_426,i0) = e_439 ) ),
inference(superposition,[status(thm)],[c_8006,c_109]) ).
tcf(c_8109,plain,
( ( e_427 = e_439 )
| ( i0 = i3 ) ),
inference(light_normalisation,[status(thm)],[c_8108,c_104]) ).
tcf(c_8222,plain,
( ( i0 = i3 )
| ( store(a_438,i2,e_427) = a_440 ) ),
inference(superposition,[status(thm)],[c_8109,c_98]) ).
tcf(c_8300,plain,
( ( i0 = i2 )
| ( i0 = i3 )
| ( store(a_428,i0,e_421) = store(a_438,i2,e_427) ) ),
inference(superposition,[status(thm)],[c_8100,c_435]) ).
tcf(c_8309,plain,
( ( i0 = i2 )
| ( i0 = i3 )
| ( store(a_438,i2,e_427) = a_430 ) ),
inference(light_normalisation,[status(thm)],[c_8300,c_556]) ).
tcf(c_11652,plain,
( ( a_430 = a_440 )
| ( i0 = i2 )
| ( i0 = i3 ) ),
inference(superposition,[status(thm)],[c_8309,c_8222]) ).
tcf(c_11653,plain,
( ( i0 = i2 )
| ( i0 = i3 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_11652,c_192]) ).
tcf(c_11970,plain,
! [X0: $i] :
( ( i0 = i2 )
| ( store(a_418,i0,X0) = store(a_431,i0,X0) ) ),
inference(superposition,[status(thm)],[c_11653,c_328]) ).
tcf(c_11971,plain,
! [X0: $i] :
( ( i0 = i2 )
| ( store(a_422,i0,X0) = store(a_424,i0,X0) ) ),
inference(superposition,[status(thm)],[c_11653,c_326]) ).
tcf(c_11972,plain,
( ( i0 = i2 )
| ( store(a_422,i0,select(a_420,i0)) = a_420 ) ),
inference(superposition,[status(thm)],[c_11653,c_711]) ).
tcf(c_11974,plain,
( ( i0 = i2 )
| ( store(a_422,i0,e_421) = a_422 ) ),
inference(superposition,[status(thm)],[c_11653,c_338]) ).
tcf(c_11977,plain,
( ( i0 = i2 )
| ( select(a_434,i0) = e_433 ) ),
inference(superposition,[status(thm)],[c_11653,c_298]) ).
tcf(c_11978,plain,
( ( i0 = i2 )
| ( select(a_431,i0) = e_421 ) ),
inference(superposition,[status(thm)],[c_11653,c_296]) ).
tcf(c_11979,plain,
( ( i0 = i2 )
| ( select(a_424,i0) = e_423 ) ),
inference(superposition,[status(thm)],[c_11653,c_292]) ).
tcf(c_11981,plain,
( ( i0 = i2 )
| ( store(a_432,i0,e_433) = a_434 ) ),
inference(superposition,[status(thm)],[c_11653,c_95]) ).
tcf(c_11982,plain,
( ( i0 = i2 )
| ( store(a_418,i0,e_421) = a_431 ) ),
inference(superposition,[status(thm)],[c_11653,c_93]) ).
tcf(c_11983,plain,
( ( i0 = i2 )
| ( store(a_422,i0,e_423) = a_424 ) ),
inference(superposition,[status(thm)],[c_11653,c_89]) ).
tcf(c_11985,plain,
( ( i0 = i2 )
| ( select(a_418,i0) = e_419 ) ),
inference(superposition,[status(thm)],[c_11653,c_100]) ).
tcf(c_11986,plain,
( ( e_419 = e_421 )
| ( i0 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_11985,c_101]) ).
tcf(c_12002,plain,
( ( i0 = i2 )
| ( a_418 = a_431 ) ),
inference(light_normalisation,[status(thm)],[c_11982,c_311]) ).
tcf(c_12014,plain,
( ( i0 = i2 )
| ( store(a_422,i0,e_419) = a_420 ) ),
inference(light_normalisation,[status(thm)],[c_11972,c_290]) ).
tcf(c_12022,plain,
! [X0: $i] :
( ( i0 = i2 )
| ( store(a_418,i0,X0) = store(a_432,i0,X0) ) ),
inference(light_normalisation,[status(thm)],[c_11970,c_329]) ).
tcf(c_12250,plain,
( ( i0 = i2 )
| ( store(a_428,i0,e_419) = a_430 ) ),
inference(superposition,[status(thm)],[c_11986,c_556]) ).
tcf(c_12426,plain,
( ( i0 = i2 )
| ( select(a_418,i2) = e_433 ) ),
inference(superposition,[status(thm)],[c_12002,c_2511]) ).
tcf(c_12473,plain,
( ( e_433 = e_439 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_11977,c_2579]) ).
tcf(c_12511,plain,
( ( i0 = i2 )
| ( store(a_432,i0,e_421) = a_431 ) ),
inference(superposition,[status(thm)],[c_11978,c_827]) ).
tcf(c_12531,plain,
( ( e_423 = e_427 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_11979,c_2220]) ).
tcf(c_12570,plain,
( ( i0 = i2 )
| ( store(a_422,i0,e_419) = a_422 ) ),
inference(superposition,[status(thm)],[c_11986,c_11974]) ).
tcf(c_12740,plain,
( ( i0 = i2 )
| ( select(a_424,i2) = e_423 ) ),
inference(superposition,[status(thm)],[c_11983,c_4502]) ).
tcf(c_13017,plain,
( ( i0 = i2 )
| ( store(a_438,i2,e_433) = a_440 ) ),
inference(superposition,[status(thm)],[c_12473,c_98]) ).
tcf(c_13140,plain,
( ( i0 = i2 )
| ( store(a_426,i2,e_423) = a_428 ) ),
inference(superposition,[status(thm)],[c_12531,c_91]) ).
tcf(c_13267,plain,
! [X0: $i] :
( ( i0 = i2 )
| ( store(store(a_422,i0,X0),i2,e_421) = store(a_426,i0,X0) ) ),
inference(superposition,[status(thm)],[c_11971,c_549]) ).
tcf(c_13649,plain,
( ( i0 = i2 )
| ( store(a_426,i2,e_423) = a_424 ) ),
inference(superposition,[status(thm)],[c_12740,c_944]) ).
tcf(c_13698,plain,
( ( i0 = i2 )
| ( select(a_420,i2) = e_423 ) ),
inference(superposition,[status(thm)],[c_12014,c_4502]) ).
tcf(c_14324,plain,
( ( i0 = i2 )
| ( select(a_418,i2) = e_423 ) ),
inference(superposition,[status(thm)],[c_13698,c_358]) ).
tcf(c_14338,plain,
( ( e_423 = e_433 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_14324,c_12426]) ).
tcf(c_14347,plain,
( ( i0 = i2 )
| ( store(a_438,i2,e_423) = a_440 ) ),
inference(superposition,[status(thm)],[c_14338,c_13017]) ).
tcf(c_14365,plain,
( ( i0 = i2 )
| ( store(a_432,i3,e_423) = a_434 ) ),
inference(superposition,[status(thm)],[c_14338,c_95]) ).
tcf(c_15472,plain,
( ( i0 = i2 )
| ( store(a_432,i0,e_419) = a_431 ) ),
inference(superposition,[status(thm)],[c_11986,c_12511]) ).
tcf(c_15488,plain,
( ( a_431 = a_432 )
| ( i0 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_15472,c_339]) ).
tcf(c_15628,plain,
( ( i0 = i2 )
| ( a_420 = a_422 ) ),
inference(superposition,[status(thm)],[c_12570,c_12014]) ).
tcf(c_15958,plain,
( ( i0 = i2 )
| ( select(a_432,i3) = e_421 ) ),
inference(superposition,[status(thm)],[c_15488,c_296]) ).
tcf(c_15961,plain,
( ( e_421 = e_435 )
| ( i0 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_15958,c_107]) ).
tcf(c_16622,plain,
( ( i0 = i2 )
| ( store(a_418,i0,e_419) = a_432 ) ),
inference(superposition,[status(thm)],[c_12022,c_339]) ).
tcf(c_16639,plain,
( ( i0 = i2 )
| ( a_420 = a_432 ) ),
inference(light_normalisation,[status(thm)],[c_16622,c_87]) ).
tcf(c_17349,plain,
( ( i0 = i2 )
| ( store(a_436,i2,e_421) = a_436 ) ),
inference(superposition,[status(thm)],[c_15961,c_340]) ).
tcf(c_17351,plain,
( ( i0 = i2 )
| ( store(a_436,i0,e_421) = a_438 ) ),
inference(superposition,[status(thm)],[c_15961,c_307]) ).
tcf(c_17513,plain,
( ( a_422 = a_432 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_16639,c_15628]) ).
tcf(c_17732,plain,
( ( i0 = i2 )
| ( store(a_422,i3,e_423) = a_434 ) ),
inference(superposition,[status(thm)],[c_17513,c_14365]) ).
tcf(c_17737,plain,
( ( i0 = i2 )
| ( store(a_422,i0,e_433) = a_434 ) ),
inference(superposition,[status(thm)],[c_17513,c_11981]) ).
tcf(c_17777,plain,
( ( a_424 = a_434 )
| ( i0 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_17732,c_89]) ).
tcf(c_18430,plain,
( ( i0 = i2 )
| ( select(a_424,i0) = e_433 ) ),
inference(superposition,[status(thm)],[c_17777,c_11977]) ).
tcf(c_18609,plain,
( ( e_427 = e_433 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_18430,c_2220]) ).
tcf(c_19357,plain,
( ( i0 = i2 )
| ( store(a_422,i0,e_427) = a_434 ) ),
inference(superposition,[status(thm)],[c_18609,c_17737]) ).
tcf(c_22734,plain,
( ( i0 = i2 )
| ( store(a_422,i2,e_421) = store(a_426,i0,e_421) ) ),
inference(superposition,[status(thm)],[c_11974,c_13267]) ).
tcf(c_25067,plain,
( ( a_424 = a_428 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_13649,c_13140]) ).
tcf(c_25085,plain,
( ( i0 = i2 )
| ( store(a_424,i0,e_419) = a_430 ) ),
inference(superposition,[status(thm)],[c_25067,c_12250]) ).
tcf(c_38621,plain,
( ( i0 = i2 )
| ( store(a_426,i0,e_427) = store(a_434,i2,e_421) ) ),
inference(superposition,[status(thm)],[c_19357,c_13267]) ).
tcf(c_38627,plain,
( ( i0 = i2 )
| ( store(a_434,i2,e_421) = a_426 ) ),
inference(light_normalisation,[status(thm)],[c_38621,c_313]) ).
tcf(c_42780,plain,
( ( i0 = i2 )
| ( store(a_422,i0,e_419) = a_430 ) ),
inference(superposition,[status(thm)],[c_25085,c_11971]) ).
tcf(c_42868,plain,
( ( a_422 = a_430 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_42780,c_12570]) ).
tcf(c_53398,plain,
( ( i0 = i2 )
| ( store(a_436,i2,e_421) = a_426 ) ),
inference(demodulation,[status(thm)],[c_38627,c_331]) ).
tcf(c_53432,plain,
( ( a_426 = a_436 )
| ( i0 = i2 ) ),
inference(superposition,[status(thm)],[c_53398,c_17349]) ).
tcf(c_53496,plain,
( ( i0 = i2 )
| ( store(a_426,i0,e_421) = a_438 ) ),
inference(superposition,[status(thm)],[c_53432,c_17351]) ).
tcf(c_64358,plain,
( ( i0 = i2 )
| ( store(a_422,i2,e_421) = a_438 ) ),
inference(superposition,[status(thm)],[c_53496,c_22734]) ).
tcf(c_64416,plain,
! [X0: $i] :
( ( i0 = i2 )
| ( store(a_422,i2,X0) = store(a_438,i2,X0) ) ),
inference(superposition,[status(thm)],[c_64358,c_83]) ).
tcf(c_65010,plain,
( ( i0 = i2 )
| ( store(a_422,i2,e_423) = a_440 ) ),
inference(superposition,[status(thm)],[c_64416,c_14347]) ).
tcf(c_65011,plain,
( ( a_422 = a_440 )
| ( i0 = i2 ) ),
inference(light_normalisation,[status(thm)],[c_65010,c_312]) ).
tcf(c_65418,plain,
( ( i0 = i2 )
| ( a_422 != a_430 ) ),
inference(superposition,[status(thm)],[c_65011,c_192]) ).
tcf(c_65779,plain,
i0 = i2,
inference(global_subsumption_just,[status(thm)],[c_65418,c_42868,c_65418]) ).
tcf(c_66337,plain,
( ( a_426 = a_436 )
| ( i3 = i2 ) ),
inference(demodulation,[status(thm)],[c_8006,c_65779]) ).
tcf(c_66437,plain,
! [X0: $i] : store(a_436,i2,X0) = store(a_438,i2,X0),
inference(demodulation,[status(thm)],[c_571,c_65779]) ).
tcf(c_66440,plain,
! [X0: $i] : store(a_431,i2,X0) = store(a_432,i2,X0),
inference(demodulation,[status(thm)],[c_329,c_65779]) ).
tcf(c_66441,plain,
! [X0: $i] : store(a_418,i2,X0) = store(a_420,i2,X0),
inference(demodulation,[status(thm)],[c_324,c_65779]) ).
tcf(c_66442,plain,
store(a_432,i2,e_419) = a_432,
inference(demodulation,[status(thm)],[c_339,c_65779]) ).
tcf(c_66444,plain,
store(a_426,i2,e_427) = a_426,
inference(demodulation,[status(thm)],[c_313,c_65779]) ).
tcf(c_66445,plain,
store(a_418,i2,e_421) = a_418,
inference(demodulation,[status(thm)],[c_311,c_65779]) ).
tcf(c_66447,plain,
store(a_428,i2,e_421) = a_430,
inference(demodulation,[status(thm)],[c_556,c_65779]) ).
tcf(c_66449,plain,
select(a_432,i2) = e_419,
inference(demodulation,[status(thm)],[c_297,c_65779]) ).
tcf(c_66453,plain,
select(a_436,i2) = e_439,
inference(demodulation,[status(thm)],[c_109,c_65779]) ).
tcf(c_66455,plain,
select(a_418,i2) = e_421,
inference(demodulation,[status(thm)],[c_101,c_65779]) ).
tcf(c_66457,plain,
e_435 = e_439,
inference(light_normalisation,[status(thm)],[c_66453,c_299]) ).
tcf(c_66816,plain,
store(a_436,i2,e_439) = a_440,
inference(demodulation,[status(thm)],[c_98,c_66437]) ).
tcf(c_66840,plain,
a_426 = a_428,
inference(demodulation,[status(thm)],[c_91,c_66444]) ).
tcf(c_66996,plain,
a_426 = a_430,
inference(light_normalisation,[status(thm)],[c_66447,c_403,c_66840]) ).
tcf(c_66998,plain,
a_426 != a_440,
inference(demodulation,[status(thm)],[c_192,c_66996]) ).
tcf(c_67177,plain,
a_436 = a_440,
inference(light_normalisation,[status(thm)],[c_66816,c_340,c_66457]) ).
tcf(c_67179,plain,
a_426 != a_436,
inference(demodulation,[status(thm)],[c_66998,c_67177]) ).
tcf(c_67184,plain,
i3 = i2,
inference(backward_subsumption_resolution,[status(thm)],[c_66337,c_67179]) ).
tcf(c_67214,plain,
! [X0: $i] : store(a_432,i2,X0) = store(a_434,i2,X0),
inference(demodulation,[status(thm)],[c_330,c_67184]) ).
tcf(c_67215,plain,
! [X0: $i] : store(a_418,i2,X0) = store(a_431,i2,X0),
inference(demodulation,[status(thm)],[c_328,c_67184]) ).
tcf(c_67218,plain,
! [X0: $i] : store(a_420,i2,X0) = store(a_422,i2,X0),
inference(demodulation,[status(thm)],[c_325,c_67184]) ).
tcf(c_67226,plain,
store(a_422,i2,e_423) = a_424,
inference(demodulation,[status(thm)],[c_89,c_67184]) ).
tcf(c_67227,plain,
select(a_432,i2) = e_435,
inference(demodulation,[status(thm)],[c_107,c_67184]) ).
tcf(c_67228,plain,
select(a_418,i2) = e_419,
inference(demodulation,[status(thm)],[c_100,c_67184]) ).
tcf(c_67229,plain,
e_419 = e_421,
inference(demodulation,[status(thm)],[c_66455,c_67228]) ).
tcf(c_67230,plain,
store(a_418,i2,e_419) = a_418,
inference(demodulation,[status(thm)],[c_66445,c_67229]) ).
tcf(c_67235,plain,
store(a_426,i2,e_419) = a_426,
inference(demodulation,[status(thm)],[c_403,c_67229]) ).
tcf(c_67247,plain,
e_419 = e_435,
inference(light_normalisation,[status(thm)],[c_67227,c_66449]) ).
tcf(c_67251,plain,
store(a_436,i2,e_419) = a_436,
inference(demodulation,[status(thm)],[c_340,c_67247]) ).
tcf(c_67258,plain,
a_422 = a_424,
inference(light_normalisation,[status(thm)],[c_67226,c_312]) ).
tcf(c_67264,plain,
! [X0: $i] : store(a_422,i2,X0) = store(a_426,i2,X0),
inference(demodulation,[status(thm)],[c_547,c_67258]) ).
tcf(c_67283,plain,
! [X0: $i] : store(a_418,i2,X0) = store(a_422,i2,X0),
inference(light_normalisation,[status(thm)],[c_67218,c_66441]) ).
tcf(c_67284,plain,
! [X0: $i] : store(a_432,i2,X0) = store(a_436,i2,X0),
inference(demodulation,[status(thm)],[c_331,c_67214]) ).
tcf(c_67381,plain,
! [X0: $i] : store(a_418,i2,X0) = store(a_432,i2,X0),
inference(light_normalisation,[status(thm)],[c_66440,c_67215]) ).
tcf(c_67382,plain,
store(a_418,i2,e_419) = a_432,
inference(demodulation,[status(thm)],[c_66442,c_67381]) ).
tcf(c_67383,plain,
a_418 = a_432,
inference(light_normalisation,[status(thm)],[c_67382,c_67230]) ).
tcf(c_67661,plain,
a_418 = a_426,
inference(demodulation,[status(thm)],[c_67235,c_67230,c_67264,c_67283]) ).
tcf(c_67664,plain,
a_418 != a_436,
inference(demodulation,[status(thm)],[c_67179,c_67661]) ).
tcf(c_67696,plain,
a_418 = a_436,
inference(demodulation,[status(thm)],[c_67251,c_67230,c_67284,c_67383]) ).
tcf(c_67697,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_67696,c_67664]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV540-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n007.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 : Thu Sep 24 20:20:54 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 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.13/0.44
% 0.13/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.44
% 0.13/0.44 % Detected problem language: tptp
% 0.13/0.46 % Proving...
% 33.92/6.49 % SZS status Started for theBenchmark.p
% 33.92/6.49 % SZS status Unsatisfiable for theBenchmark.p
% 33.92/6.49
% 33.92/6.49 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 33.92/6.49
% 33.92/6.49 % ------ iProver source info
% 33.92/6.49
% 33.92/6.49 % git: date: 2026-07-19 20:42:38 +0200
% 33.92/6.49 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 33.92/6.49 % git: non_committed_changes: false
% 33.92/6.49
% 33.92/6.49 % ------ Parsing...% successful
% 33.92/6.49
% 33.92/6.49
% 33.92/6.49 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 33.92/6.49
% 33.92/6.49 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 33.92/6.49
% 33.92/6.49 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 33.92/6.49
% 33.92/6.49 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 33.92/6.49 % ------ Proving...
% 33.92/6.49 % ------ Problem Properties
% 33.92/6.49
% 33.92/6.49 %
% 33.92/6.49 % clauses 31
% 33.92/6.49 % conjectures 1
% 33.92/6.49 % EPR 1
% 33.92/6.49 % Horn 29
% 33.92/6.49 % unary 29
% 33.92/6.49 % binary 2
% 33.92/6.49 % lits 33
% 33.92/6.49 % lits eq 33
% 33.92/6.49 % fd_pure 0
% 33.92/6.49 % fd_pseudo 0
% 33.92/6.49 % fd_cond 0
% 33.92/6.49 % fd_pseudo_cond 2
% 33.92/6.49 % AC symbols 0
% 33.92/6.49
% 33.92/6.49 % ------ Schedule dynamic 5 is on
% 33.92/6.49
% 33.92/6.49 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 33.92/6.49
% 33.92/6.49
% 33.92/6.49 % ------
% 33.92/6.49 % Current options:
% 33.92/6.49 % ------
% 33.92/6.49
% 33.92/6.49
% 33.92/6.49 %
% 33.92/6.49
% 33.92/6.49 % ------ Proving...
% 33.92/6.49 %
% 33.92/6.49
% 33.92/6.49 % SZS status Unsatisfiable for theBenchmark.p
% 33.92/6.49
% 33.92/6.49 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 40.03/6.50
% 40.03/6.50
%------------------------------------------------------------------------------