%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV540-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 : Thu Sep 24 02:48:37 PM UTC 2026
% Result : Unsatisfiable 3.74s 0.97s
% Output : CNFRefutation 3.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 72
% Syntax : Number of formulae : 411 ( 110 unt; 42 def)
% Number of atoms : 772 ( 431 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 583 ( 222 ~; 319 |; 0 &)
% ( 42 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 44 ( 42 usr; 43 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 30 con; 0-3 aty)
% Number of variables : 388 ( 388 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,I,E] : select(store(A,I,E),I) = E,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [I,J,A,E] :
( select(store(A,I,E),J) = select(A,J)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A,I] : store(A,I,select(A,I)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A,I,E,F] : store(store(A,I,E),I,F) = store(A,I,F),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [I,J,A,E,F] :
( store(store(A,I,E),J,F) = store(store(A,J,F),I,E)
| I = J ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,hypothesis,
a_417 = store(a1,i1,e_416),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,hypothesis,
a_418 = store(a_417,i1,e_416),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,hypothesis,
a_420 = store(a_418,i0,e_419),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,hypothesis,
a_422 = store(a_420,i3,e_421),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,hypothesis,
a_424 = store(a_422,i3,e_423),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,hypothesis,
a_426 = store(a_424,i2,e_425),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,hypothesis,
a_428 = store(a_426,i2,e_427),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,hypothesis,
a_430 = store(a_428,i0,e_429),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,hypothesis,
a_431 = store(a_418,i3,e_421),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,hypothesis,
a_432 = store(a_431,i0,e_419),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
a_434 = store(a_432,i3,e_433),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,hypothesis,
a_436 = store(a_434,i2,e_435),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,hypothesis,
a_438 = store(a_436,i0,e_437),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,hypothesis,
a_440 = store(a_438,i2,e_439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,hypothesis,
e_419 = select(a_418,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,hypothesis,
e_421 = select(a_418,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,hypothesis,
e_423 = select(a_422,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,hypothesis,
e_425 = select(a_422,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,hypothesis,
e_427 = select(a_426,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,hypothesis,
e_429 = select(a_426,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
e_433 = select(a_432,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
e_435 = select(a_432,i3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
e_437 = select(a_436,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
e_439 = select(a_436,i0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
a_430 != a_440,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,plain,
! [X0,X1,X2] : select(store(X0,X1,X2),X1) = X2,
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f33,plain,
! [I,J] :
( ! [A,E] : select(store(A,I,E),J) = select(A,J)
| I = J ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f34,plain,
! [X0,X1,X2,X3] :
( select(store(X2,X0,X3),X1) = select(X2,X1)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [X0,X1] : store(X0,X1,select(X0,X1)) = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f36,plain,
! [X0,X1,X2,X3] : store(store(X0,X1,X2),X1,X3) = store(X0,X1,X3),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f37,plain,
! [I,J] :
( ! [A,E,F] : store(store(A,I,E),J,F) = store(store(A,J,F),I,E)
| I = J ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f38,plain,
! [X0,X1,X2,X3,X4] :
( store(store(X2,X0,X3),X1,X4) = store(store(X2,X1,X4),X0,X3)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f39,plain,
a_417 = store(a1,i1,e_416),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f40,plain,
a_418 = store(a_417,i1,e_416),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f41,plain,
a_420 = store(a_418,i0,e_419),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f42,plain,
a_422 = store(a_420,i3,e_421),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f43,plain,
a_424 = store(a_422,i3,e_423),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f44,plain,
a_426 = store(a_424,i2,e_425),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f45,plain,
a_428 = store(a_426,i2,e_427),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f46,plain,
a_430 = store(a_428,i0,e_429),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f47,plain,
a_431 = store(a_418,i3,e_421),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f48,plain,
a_432 = store(a_431,i0,e_419),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f49,plain,
a_434 = store(a_432,i3,e_433),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f50,plain,
a_436 = store(a_434,i2,e_435),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f51,plain,
a_438 = store(a_436,i0,e_437),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f52,plain,
a_440 = store(a_438,i2,e_439),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f54,plain,
e_419 = select(a_418,i3),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f55,plain,
e_421 = select(a_418,i0),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f56,plain,
e_423 = select(a_422,i2),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f57,plain,
e_425 = select(a_422,i3),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f58,plain,
e_427 = select(a_426,i0),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f59,plain,
e_429 = select(a_426,i2),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f60,plain,
e_433 = select(a_432,i2),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f61,plain,
e_435 = select(a_432,i3),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f62,plain,
e_437 = select(a_436,i2),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f63,plain,
e_439 = select(a_436,i0),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f64,plain,
a_430 != a_440,
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f69,plain,
! [X0] :
( select(a_430,X0) = select(a_428,X0)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f46,f34]) ).
fof(f73,definition,
( sQ0_spl
<=> i2 = i2 ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f81,plain,
store(a_436,i0,e_439) = a_436,
inference(paramodulation,[status(thm)],[f63,f35]) ).
fof(f84,plain,
store(a_432,i2,e_433) = a_432,
inference(paramodulation,[status(thm)],[f60,f35]) ).
fof(f88,plain,
store(a_422,i2,e_423) = a_422,
inference(paramodulation,[status(thm)],[f56,f35]) ).
fof(f89,plain,
store(a_418,i0,e_421) = a_418,
inference(paramodulation,[status(thm)],[f55,f35]) ).
fof(f90,plain,
store(a_418,i3,e_419) = a_418,
inference(paramodulation,[status(thm)],[f54,f35]) ).
fof(f95,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| store(store(X0,X1,X2),X3,select(X0,X3)) = store(X0,X1,X2) ),
inference(paramodulation,[status(thm)],[f34,f35]) ).
fof(f100,plain,
select(a_417,i1) = e_416,
inference(paramodulation,[status(thm)],[f39,f32]) ).
fof(f104,plain,
! [X0] : store(a_440,i2,X0) = store(a_438,i2,X0),
inference(paramodulation,[status(thm)],[f52,f36]) ).
fof(f105,plain,
! [X0] : store(a_430,i0,X0) = store(a_428,i0,X0),
inference(paramodulation,[status(thm)],[f46,f36]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( store(X2,X0,X3) = store(store(X2,X1,select(store(X2,X0,X3),X1)),X0,X3)
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f35,f38]) ).
fof(f115,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( X0 = X4
| store(store(store(X2,X0,X3),X4,X5),X1,X6) = store(store(store(X2,X4,X5),X1,X6),X0,X3)
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f38,f38]) ).
fof(f117,plain,
! [X0,X1,X2,X3,X4,X5] :
( store(store(X2,X0,X3),X1,X4) = store(store(store(X2,X0,X5),X1,X4),X0,X3)
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f36,f38]) ).
fof(f119,plain,
! [X0,X1] :
( store(a_440,X0,X1) = store(store(a_438,X0,X1),i2,e_439)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f52,f38]) ).
fof(f120,plain,
! [X0,X1] :
( store(a_430,X0,X1) = store(store(a_428,X0,X1),i0,e_429)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f46,f38]) ).
fof(f137,plain,
! [X0,X1,X2,X3,X4] :
( X3 = X1
| select(store(store(X0,X1,X2),X3,X4),X1) = X2 ),
inference(paramodulation,[status(thm)],[f38,f32]) ).
fof(f141,plain,
! [X0,X1,X2,X3,X4,X5] :
( X0 = X4
| select(store(store(X2,X0,X3),X4,X5),X1) = select(store(X2,X4,X5),X1)
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f38,f34]) ).
fof(f142,plain,
! [X0,X1,X2,X3,X4] :
( X1 = X3
| select(store(store(X0,X1,X2),X3,X4),X1) = X2 ),
inference(paramodulation,[status(thm)],[f38,f32]) ).
fof(f160,plain,
! [X0] :
( i0 = X0
| store(a_430,X0,select(a_428,X0)) = a_430 ),
inference(paramodulation,[status(thm)],[f69,f35]) ).
fof(f172,plain,
! [X0,X1,X2] :
( store(store(a_440,X0,X1),i2,X2) = store(store(a_438,i2,X2),X0,X1)
| X0 = i2 ),
inference(paramodulation,[status(thm)],[f104,f38]) ).
fof(f183,plain,
! [X0,X1,X2] :
( store(store(a_430,X0,X1),i0,X2) = store(store(a_428,i0,X2),X0,X1)
| X0 = i0 ),
inference(paramodulation,[status(thm)],[f105,f38]) ).
fof(f255,plain,
! [X0,X1] :
( i2 = X0
| select(store(a_440,X0,X1),i2) = e_439 ),
inference(paramodulation,[status(thm)],[f119,f32]) ).
fof(f278,plain,
! [X0,X1] :
( i0 = X0
| select(store(a_430,X0,X1),i0) = e_429 ),
inference(paramodulation,[status(thm)],[f120,f32]) ).
fof(f289,plain,
store(a_417,i1,e_416) = a_417,
inference(paramodulation,[status(thm)],[f100,f35]) ).
fof(f290,plain,
a_418 = a_417,
inference(forward_demodulation,[status(thm)],[f40,f289]) ).
fof(f292,plain,
e_421 = select(a_417,i0),
inference(backward_demodulation,[status(thm)],[f290,f55]) ).
fof(f293,plain,
e_419 = select(a_417,i3),
inference(backward_demodulation,[status(thm)],[f290,f54]) ).
fof(f297,plain,
a_420 = store(a_417,i0,e_419),
inference(forward_demodulation,[status(thm)],[f290,f41]) ).
fof(f298,plain,
! [X0,X1] :
( store(store(a_417,X0,X1),i0,e_419) = store(a_420,X0,X1)
| X0 = i0 ),
inference(paramodulation,[status(thm)],[f297,f38]) ).
fof(f308,plain,
select(a_422,i3) = e_421,
inference(paramodulation,[status(thm)],[f42,f32]) ).
fof(f309,plain,
e_425 = e_421,
inference(forward_demodulation,[status(thm)],[f57,f308]) ).
fof(f310,plain,
e_421 = select(a_422,i3),
inference(backward_demodulation,[status(thm)],[f309,f57]) ).
fof(f316,plain,
a_426 = store(a_424,i2,e_421),
inference(forward_demodulation,[status(thm)],[f309,f44]) ).
fof(f321,plain,
select(a_426,i2) = e_421,
inference(paramodulation,[status(thm)],[f316,f32]) ).
fof(f322,plain,
e_429 = e_421,
inference(forward_demodulation,[status(thm)],[f59,f321]) ).
fof(f327,plain,
select(a_428,i2) = e_427,
inference(paramodulation,[status(thm)],[f45,f32]) ).
fof(f332,plain,
! [X0] :
( i2 = X0
| select(a_440,i2) = e_439 ),
inference(paramodulation,[status(thm)],[f35,f255]) ).
fof(f336,definition,
( sQ12_spl
<=> select(a_440,i2) = e_439 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f339,definition,
! [X0] :
( sQ13_spl
<=> ( X0 = i2
| i2 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f340,plain,
! [X0] :
( ~ sQ13_spl
| X0 = i2
| i2 = X0 ),
inference(component_clause,[status(thm)],[f339]) ).
fof(f352,definition,
! [X0] :
( sQ16_spl
<=> i2 = X0 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f353,plain,
! [X0] :
( ~ sQ16_spl
| i2 = X0 ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f355,plain,
( sQ16_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f332,f336,f352]) ).
fof(f362,plain,
! [X0] :
( i0 = X0
| select(a_430,i0) = e_429 ),
inference(paramodulation,[status(thm)],[f35,f278]) ).
fof(f366,definition,
( sQ17_spl
<=> select(a_430,i0) = e_429 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f382,definition,
! [X0] :
( sQ21_spl
<=> i0 = X0 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f383,plain,
! [X0] :
( ~ sQ21_spl
| i0 = X0 ),
inference(component_clause,[status(thm)],[f382]) ).
fof(f385,plain,
( sQ21_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f362,f366,f382]) ).
fof(f403,plain,
! [X0,X1,X2] :
( X1 = i2
| select(store(store(a_438,i2,X0),X1,X2),i2) = X0 ),
inference(paramodulation,[status(thm)],[f172,f32]) ).
fof(f417,plain,
! [X0,X1] :
( i2 = i2
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f32,f403]) ).
fof(f422,plain,
! [X0,X1] :
( X1 = i2
| select(store(a_438,i2,X0),i2) = X0 ),
inference(paramodulation,[status(thm)],[f35,f403]) ).
fof(f428,definition,
! [X0] :
( sQ24_spl
<=> select(store(a_438,i2,X0),i2) = X0 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f432,definition,
! [X0,X1] :
( sQ25_spl
<=> X0 = X1 ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f433,plain,
! [X0,X1] :
( ~ sQ25_spl
| X0 = X1 ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f435,plain,
( sQ0_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f417,f432,f73]) ).
fof(f444,plain,
( sQ16_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f422,f428,f352]) ).
fof(f546,plain,
e_421 = select(a_426,i2),
inference(backward_demodulation,[status(thm)],[f322,f59]) ).
fof(f548,plain,
a_430 = store(a_428,i0,e_421),
inference(backward_demodulation,[status(thm)],[f322,f46]) ).
fof(f551,plain,
( i0 = i2
| store(a_430,i2,e_427) = a_430 ),
inference(paramodulation,[status(thm)],[f327,f160]) ).
fof(f553,definition,
( sQ34_spl
<=> store(a_430,i2,e_427) = a_430 ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f554,plain,
( ~ sQ34_spl
| store(a_430,i2,e_427) = a_430 ),
inference(component_clause,[status(thm)],[f553]) ).
fof(f556,definition,
( sQ35_spl
<=> i0 = i2 ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f557,plain,
( ~ sQ35_spl
| i0 = i2 ),
inference(component_clause,[status(thm)],[f556]) ).
fof(f558,plain,
( sQ35_spl
| i0 != i2 ),
inference(component_clause,[status(thm)],[f556]) ).
fof(f559,plain,
( sQ35_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f551,f553,f556]) ).
fof(f570,plain,
a_431 = store(a_417,i3,e_421),
inference(forward_demodulation,[status(thm)],[f290,f47]) ).
fof(f581,plain,
select(a_432,i0) = e_419,
inference(paramodulation,[status(thm)],[f48,f32]) ).
fof(f591,plain,
select(a_436,i2) = e_435,
inference(paramodulation,[status(thm)],[f50,f32]) ).
fof(f592,plain,
e_437 = e_435,
inference(forward_demodulation,[status(thm)],[f62,f591]) ).
fof(f597,plain,
select(a_438,i0) = e_437,
inference(paramodulation,[status(thm)],[f51,f32]) ).
fof(f604,plain,
! [X0] :
( ~ sQ34_spl
| store(a_430,i0,X0) = store(store(a_428,i0,X0),i2,e_427)
| i2 = i0 ),
inference(paramodulation,[status(thm)],[f554,f183]) ).
fof(f609,plain,
( ~ sQ34_spl
| select(a_430,i2) = e_427 ),
inference(paramodulation,[status(thm)],[f554,f32]) ).
fof(f610,definition,
! [X0] :
( sQ37_spl
<=> store(a_430,i0,X0) = store(store(a_428,i0,X0),i2,e_427) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f613,plain,
( ~ sQ34_spl
| sQ37_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f604,f556,f610,f553]) ).
fof(f614,plain,
( ~ sQ35_spl
| a_436 = store(a_434,i0,e_435) ),
inference(backward_demodulation,[status(thm)],[f557,f50]) ).
fof(f615,plain,
( ~ sQ35_spl
| e_421 = select(a_426,i0) ),
inference(backward_demodulation,[status(thm)],[f557,f546]) ).
fof(f616,plain,
( ~ sQ35_spl
| select(a_428,i0) = e_427 ),
inference(backward_demodulation,[status(thm)],[f557,f327]) ).
fof(f621,plain,
( ~ sQ35_spl
| a_428 = store(a_426,i0,e_427) ),
inference(backward_demodulation,[status(thm)],[f557,f45]) ).
fof(f622,plain,
( ~ sQ35_spl
| a_426 = store(a_424,i0,e_421) ),
inference(backward_demodulation,[status(thm)],[f557,f316]) ).
fof(f627,plain,
( ~ sQ35_spl
| e_437 = select(a_436,i0) ),
inference(backward_demodulation,[status(thm)],[f557,f62]) ).
fof(f628,plain,
( ~ sQ35_spl
| e_433 = select(a_432,i0) ),
inference(backward_demodulation,[status(thm)],[f557,f60]) ).
fof(f632,plain,
( ~ sQ35_spl
| a_440 = store(a_438,i0,e_439) ),
inference(backward_demodulation,[status(thm)],[f557,f52]) ).
fof(f633,plain,
( ~ sQ35_spl
| e_421 = e_427 ),
inference(forward_demodulation,[status(thm)],[f58,f615]) ).
fof(f643,plain,
( ~ sQ35_spl
| e_437 = e_439 ),
inference(forward_demodulation,[status(thm)],[f63,f627]) ).
fof(f648,plain,
( ~ sQ35_spl
| select(a_436,i0) = e_435 ),
inference(paramodulation,[status(thm)],[f614,f32]) ).
fof(f649,plain,
( ~ sQ35_spl
| e_439 = e_435 ),
inference(forward_demodulation,[status(thm)],[f63,f648]) ).
fof(f650,plain,
( ~ sQ35_spl
| e_421 = select(a_426,i0) ),
inference(backward_demodulation,[status(thm)],[f633,f58]) ).
fof(f652,plain,
( ~ sQ35_spl
| e_435 = e_439 ),
inference(backward_demodulation,[status(thm)],[f654,f643]) ).
fof(f653,plain,
( ~ sQ35_spl
| a_438 = store(a_436,i0,e_435) ),
inference(backward_demodulation,[status(thm)],[f654,f51]) ).
fof(f654,plain,
( ~ sQ35_spl
| e_437 = e_435 ),
inference(forward_demodulation,[status(thm)],[f643,f649]) ).
fof(f655,plain,
( ~ sQ35_spl
| select(a_428,i0) = e_421 ),
inference(forward_demodulation,[status(thm)],[f633,f616]) ).
fof(f657,plain,
( ~ sQ35_spl
| store(a_428,i0,e_421) = a_428 ),
inference(paramodulation,[status(thm)],[f655,f35]) ).
fof(f662,plain,
( ~ sQ35_spl
| a_430 = a_428 ),
inference(forward_demodulation,[status(thm)],[f548,f657]) ).
fof(f670,plain,
( ~ sQ35_spl
| a_428 != a_440 ),
inference(backward_demodulation,[status(thm)],[f662,f64]) ).
fof(f672,plain,
( ~ sQ35_spl
| a_428 = store(a_426,i0,e_421) ),
inference(forward_demodulation,[status(thm)],[f633,f621]) ).
fof(f685,plain,
( ~ sQ35_spl
| select(a_438,i0) = e_435 ),
inference(forward_demodulation,[status(thm)],[f654,f597]) ).
fof(f686,plain,
( ~ sQ35_spl
| store(a_438,i0,e_435) = a_438 ),
inference(paramodulation,[status(thm)],[f685,f35]) ).
fof(f688,plain,
( ~ sQ35_spl
| a_434 = store(a_432,i3,e_419) ),
inference(backward_demodulation,[status(thm)],[f689,f49]) ).
fof(f689,plain,
( ~ sQ35_spl
| e_433 = e_419 ),
inference(forward_demodulation,[status(thm)],[f581,f628]) ).
fof(f693,plain,
( ~ sQ35_spl
| store(a_426,i0,e_421) = a_426 ),
inference(paramodulation,[status(thm)],[f650,f35]) ).
fof(f694,plain,
( ~ sQ35_spl
| a_428 = a_426 ),
inference(forward_demodulation,[status(thm)],[f672,f693]) ).
fof(f700,plain,
( ~ sQ35_spl
| a_440 = store(a_438,i0,e_435) ),
inference(forward_demodulation,[status(thm)],[f652,f632]) ).
fof(f708,plain,
( ~ sQ35_spl
| a_426 != a_440 ),
inference(backward_demodulation,[status(thm)],[f694,f670]) ).
fof(f710,plain,
( ~ sQ35_spl
| a_430 = a_426 ),
inference(backward_demodulation,[status(thm)],[f694,f662]) ).
fof(f727,plain,
( ~ sQ35_spl
| a_426 != a_438 ),
inference(backward_demodulation,[status(thm)],[f730,f708]) ).
fof(f730,plain,
( ~ sQ35_spl
| a_440 = a_438 ),
inference(forward_demodulation,[status(thm)],[f700,f686]) ).
fof(f736,plain,
( ~ sQ35_spl
| store(a_436,i0,e_435) = a_436 ),
inference(forward_demodulation,[status(thm)],[f652,f81]) ).
fof(f737,plain,
( ~ sQ35_spl
| a_426 != a_436 ),
inference(backward_demodulation,[status(thm)],[f741,f727]) ).
fof(f738,plain,
( ~ sQ35_spl
| a_440 = a_436 ),
inference(backward_demodulation,[status(thm)],[f741,f730]) ).
fof(f741,plain,
( ~ sQ35_spl
| a_438 = a_436 ),
inference(forward_demodulation,[status(thm)],[f653,f736]) ).
fof(f754,plain,
( ~ sQ35_spl
| store(a_432,i0,e_433) = a_432 ),
inference(forward_demodulation,[status(thm)],[f557,f84]) ).
fof(f755,plain,
( ~ sQ35_spl
| store(a_432,i0,e_419) = a_432 ),
inference(forward_demodulation,[status(thm)],[f689,f754]) ).
fof(f772,plain,
( ~ sQ35_spl
| store(a_422,i0,e_423) = a_422 ),
inference(forward_demodulation,[status(thm)],[f557,f88]) ).
fof(f832,plain,
store(a_417,i0,e_421) = a_418,
inference(forward_demodulation,[status(thm)],[f290,f89]) ).
fof(f833,plain,
store(a_417,i0,e_421) = a_417,
inference(forward_demodulation,[status(thm)],[f290,f832]) ).
fof(f839,plain,
store(a_417,i3,e_419) = a_418,
inference(forward_demodulation,[status(thm)],[f290,f90]) ).
fof(f840,plain,
store(a_417,i3,e_419) = a_417,
inference(forward_demodulation,[status(thm)],[f290,f839]) ).
fof(f1053,definition,
( sQ50_spl
<=> i3 = i0 ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f1054,plain,
( ~ sQ50_spl
| i3 = i0 ),
inference(component_clause,[status(thm)],[f1053]) ).
fof(f1055,plain,
( sQ50_spl
| i3 != i0 ),
inference(component_clause,[status(thm)],[f1053]) ).
fof(f1066,plain,
( ~ sQ50_spl
| store(a_417,i0,e_419) = a_417 ),
inference(backward_demodulation,[status(thm)],[f1054,f840]) ).
fof(f1069,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_434 = store(a_432,i0,e_419) ),
inference(backward_demodulation,[status(thm)],[f1054,f688]) ).
fof(f1072,plain,
( ~ sQ50_spl
| a_431 = store(a_417,i0,e_421) ),
inference(backward_demodulation,[status(thm)],[f1054,f570]) ).
fof(f1075,plain,
( ~ sQ50_spl
| a_424 = store(a_422,i0,e_423) ),
inference(backward_demodulation,[status(thm)],[f1054,f43]) ).
fof(f1076,plain,
( ~ sQ50_spl
| a_422 = store(a_420,i0,e_421) ),
inference(backward_demodulation,[status(thm)],[f1054,f42]) ).
fof(f1077,plain,
( ~ sQ50_spl
| e_419 = select(a_417,i0) ),
inference(backward_demodulation,[status(thm)],[f1054,f293]) ).
fof(f1078,plain,
( ~ sQ50_spl
| e_435 = select(a_432,i0) ),
inference(backward_demodulation,[status(thm)],[f1054,f61]) ).
fof(f1080,plain,
( ~ sQ50_spl
| a_420 = a_417 ),
inference(forward_demodulation,[status(thm)],[f297,f1066]) ).
fof(f1081,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_434 = a_432 ),
inference(forward_demodulation,[status(thm)],[f755,f1069]) ).
fof(f1082,plain,
( ~ sQ50_spl
| a_431 = a_417 ),
inference(forward_demodulation,[status(thm)],[f833,f1072]) ).
fof(f1084,plain,
( ~ sQ50_spl
| ~ sQ35_spl
| a_424 = a_422 ),
inference(forward_demodulation,[status(thm)],[f772,f1075]) ).
fof(f1085,plain,
( ~ sQ50_spl
| e_419 = e_421 ),
inference(forward_demodulation,[status(thm)],[f292,f1077]) ).
fof(f1086,plain,
( ~ sQ50_spl
| e_435 = e_419 ),
inference(forward_demodulation,[status(thm)],[f581,f1078]) ).
fof(f1089,plain,
( ~ sQ50_spl
| a_417 = store(a_417,i0,e_419) ),
inference(backward_demodulation,[status(thm)],[f1080,f297]) ).
fof(f1095,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_436 = store(a_432,i0,e_435) ),
inference(backward_demodulation,[status(thm)],[f1081,f614]) ).
fof(f1096,plain,
( ~ sQ50_spl
| a_432 = store(a_417,i0,e_419) ),
inference(backward_demodulation,[status(thm)],[f1082,f48]) ).
fof(f1101,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_426 = store(a_422,i0,e_421) ),
inference(backward_demodulation,[status(thm)],[f1084,f622]) ).
fof(f1114,plain,
( ~ sQ50_spl
| a_422 = store(a_417,i0,e_421) ),
inference(forward_demodulation,[status(thm)],[f1080,f1076]) ).
fof(f1115,plain,
( ~ sQ50_spl
| a_422 = store(a_417,i0,e_419) ),
inference(forward_demodulation,[status(thm)],[f1085,f1114]) ).
fof(f1121,plain,
( ~ sQ50_spl
| select(a_422,i0) = e_419 ),
inference(paramodulation,[status(thm)],[f1115,f32]) ).
fof(f1123,plain,
( ~ sQ50_spl
| a_417 = store(a_417,i0,e_419) ),
inference(backward_demodulation,[status(thm)],[f1125,f1115]) ).
fof(f1125,plain,
( ~ sQ50_spl
| a_417 = a_422 ),
inference(forward_demodulation,[status(thm)],[f1115,f1089]) ).
fof(f1126,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_436 = store(a_432,i0,e_419) ),
inference(forward_demodulation,[status(thm)],[f1086,f1095]) ).
fof(f1128,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_426 != a_432 ),
inference(backward_demodulation,[status(thm)],[f1130,f737]) ).
fof(f1130,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_436 = a_432 ),
inference(forward_demodulation,[status(thm)],[f755,f1126]) ).
fof(f1143,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_426 = store(a_417,i0,e_421) ),
inference(forward_demodulation,[status(thm)],[f1125,f1101]) ).
fof(f1144,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_426 = store(a_417,i0,e_419) ),
inference(forward_demodulation,[status(thm)],[f1085,f1143]) ).
fof(f1145,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| a_426 = a_432 ),
inference(forward_demodulation,[status(thm)],[f1096,f1144]) ).
fof(f1146,plain,
( ~ sQ35_spl
| ~ sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1145,f1128]) ).
fof(f1147,plain,
( ~ sQ35_spl
| ~ sQ50_spl ),
inference(contradiction_clause,[status(thm)],[f1146]) ).
fof(f1150,plain,
select(a_438,i0) = e_435,
inference(forward_demodulation,[status(thm)],[f592,f597]) ).
fof(f1152,plain,
store(a_438,i0,e_435) = a_438,
inference(paramodulation,[status(thm)],[f1150,f35]) ).
fof(f1166,plain,
! [X0,X1] :
( store(a_430,X0,X1) = store(store(a_428,X0,X1),i0,e_421)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f548,f38]) ).
fof(f1171,plain,
a_438 = store(a_436,i0,e_435),
inference(forward_demodulation,[status(thm)],[f592,f51]) ).
fof(f1185,plain,
! [X0,X1] :
( store(a_440,X0,X1) = store(store(a_438,X0,X1),i2,e_439)
| i2 = X0 ),
inference(paramodulation,[status(thm)],[f52,f38]) ).
fof(f1211,plain,
( ~ sQ34_spl
| e_427 = select(a_428,i2)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f609,f69]) ).
fof(f1217,definition,
( sQ52_spl
<=> e_427 = select(a_428,i2) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f1218,plain,
( ~ sQ52_spl
| e_427 = select(a_428,i2) ),
inference(component_clause,[status(thm)],[f1217]) ).
fof(f1220,plain,
( ~ sQ34_spl
| sQ52_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f1211,f556,f1217,f553]) ).
fof(f1279,plain,
e_435 = select(a_436,i2),
inference(forward_demodulation,[status(thm)],[f592,f62]) ).
fof(f2047,plain,
( ~ sQ52_spl
| store(a_428,i2,e_427) = a_428 ),
inference(paramodulation,[status(thm)],[f1218,f35]) ).
fof(f2226,plain,
( ~ sQ52_spl
| store(a_430,i2,e_427) = store(a_428,i0,e_421)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f2047,f1166]) ).
fof(f2252,definition,
( sQ60_spl
<=> store(a_430,i2,e_427) = store(a_428,i0,e_421) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f2255,plain,
( ~ sQ52_spl
| sQ60_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f2226,f556,f2252,f1217]) ).
fof(f2283,plain,
( store(a_440,i0,e_435) = store(a_438,i2,e_439)
| i2 = i0 ),
inference(paramodulation,[status(thm)],[f1152,f1185]) ).
fof(f2295,definition,
( sQ62_spl
<=> store(a_440,i0,e_435) = store(a_438,i2,e_439) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f2298,plain,
( sQ62_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f2283,f556,f2295]) ).
fof(f2640,definition,
( sQ73_spl
<=> a_426 = a_436 ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f2641,plain,
( ~ sQ73_spl
| a_426 = a_436 ),
inference(component_clause,[status(thm)],[f2640]) ).
fof(f2642,plain,
( sQ73_spl
| a_426 != a_436 ),
inference(component_clause,[status(thm)],[f2640]) ).
fof(f2695,plain,
( ~ sQ73_spl
| ~ sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2641,f737]) ).
fof(f2696,plain,
( ~ sQ73_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f2695]) ).
fof(f2697,plain,
! [X0,X1,X2,X3] : store(store(X0,a_430,X1),a_440,X2) = store(store(store(X0,a_430,X3),a_440,X2),a_430,X1),
inference(resolution,[status(thm)],[f64,f117]) ).
fof(f2699,plain,
! [X0,X1,X2,X3,X4] :
( store(store(X1,a_440,X2),X0,X3) = store(store(store(X1,a_440,X4),X0,X3),a_440,X2)
| a_430 != X0 ),
inference(paramodulation,[status(thm)],[f117,f64]) ).
fof(f2700,plain,
! [X0,X1,X2,X3,X4] :
( store(store(X1,X0,X2),a_440,X3) = store(store(store(X1,X0,X4),a_440,X3),X0,X2)
| a_430 != X0 ),
inference(paramodulation,[status(thm)],[f117,f64]) ).
fof(f2701,plain,
! [X0,X1,X2,X3] : store(store(X0,a_440,X1),a_430,X2) = store(store(store(X0,a_440,X3),a_430,X2),a_440,X1),
inference(destructive_equality_resolution,[status(thm)],[f2699]) ).
fof(f2702,plain,
! [X0,X1,X2,X3] : store(store(X0,a_430,X1),a_440,X2) = store(store(store(X0,a_430,X3),a_440,X2),a_430,X1),
inference(destructive_equality_resolution,[status(thm)],[f2700]) ).
fof(f2705,plain,
! [X0,X1,X2,X3] :
( a_430 = a_430
| a_430 = a_440
| store(store(X0,a_430,X1),a_440,X2) = store(store(store(X0,a_430,X1),a_430,X3),a_440,X2) ),
inference(paramodulation,[status(thm)],[f115,f2697]) ).
fof(f2706,plain,
! [X0,X1,X2] :
( a_430 = a_440
| store(store(X0,a_430,X1),a_440,select(store(store(X0,a_430,X2),a_430,X1),a_440)) = store(store(X0,a_430,X2),a_430,X1) ),
inference(paramodulation,[status(thm)],[f114,f2697]) ).
fof(f2707,plain,
! [X0,X1,X2] :
( a_440 = a_430
| store(store(X0,a_430,select(store(X0,a_430,X1),a_430)),a_440,X2) = store(store(X0,a_430,X1),a_440,X2) ),
inference(paramodulation,[status(thm)],[f95,f2697]) ).
fof(f2708,plain,
! [X0,X1,X2,X3] :
( a_430 = a_440
| store(store(X0,a_430,X1),a_440,X2) = store(store(store(X0,a_430,X3),a_430,X1),a_440,X2) ),
inference(paramodulation,[status(thm)],[f38,f2697]) ).
fof(f2713,plain,
! [X0,X1,X2,X3,X4,X5] :
( a_440 = X1
| a_440 = a_430
| store(store(store(X0,X1,X2),a_430,X3),a_440,X4) = store(store(store(store(X0,a_440,X4),X1,X2),a_430,X5),a_430,X3) ),
inference(paramodulation,[status(thm)],[f115,f2697]) ).
fof(f2715,plain,
! [X0,X1,X2] :
( a_440 = a_430
| store(store(X0,a_430,X1),a_440,X2) = store(store(X0,a_440,X2),a_430,X1) ),
inference(paramodulation,[status(thm)],[f114,f2697]) ).
fof(f2716,plain,
! [X0,X1,X2] :
( a_430 = a_440
| store(store(X0,a_430,X1),a_440,select(X0,a_440)) = store(store(X0,a_430,X2),a_430,X1) ),
inference(paramodulation,[status(thm)],[f95,f2697]) ).
fof(f2736,plain,
! [X0,X1,X2] :
( store(store(X0,a_430,X1),a_430,X2) = store(store(X0,a_430,X2),a_440,select(store(store(X0,a_430,X1),a_430,X2),a_440))
| a_430 = a_440 ),
inference(paramodulation,[status(thm)],[f2697,f114]) ).
fof(f2739,plain,
! [X0,X1,X2,X3,X4,X5] :
( a_440 = a_430
| store(store(store(X1,a_430,X2),a_440,X3),X0,X4) = store(store(store(store(X1,a_430,X5),a_430,X2),X0,X4),a_440,X3)
| a_440 = X0 ),
inference(paramodulation,[status(thm)],[f2697,f115]) ).
fof(f2754,plain,
! [X0,X1,X2] : select(store(store(X0,a_430,X1),a_440,X2),a_430) = X1,
inference(paramodulation,[status(thm)],[f2697,f32]) ).
fof(f2760,definition,
! [X0,X1,X2,X3] :
( sQ83_spl
<=> store(store(X0,a_430,X1),a_440,X2) = store(store(store(X0,a_430,X1),a_430,X3),a_440,X2) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f2761,plain,
! [X0,X1,X2,X3] :
( ~ sQ83_spl
| store(store(X0,a_430,X1),a_440,X2) = store(store(store(X0,a_430,X1),a_430,X3),a_440,X2) ),
inference(component_clause,[status(thm)],[f2760]) ).
fof(f2763,definition,
( sQ84_spl
<=> a_430 = a_440 ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f2764,plain,
( ~ sQ84_spl
| a_430 = a_440 ),
inference(component_clause,[status(thm)],[f2763]) ).
fof(f2766,definition,
( sQ85_spl
<=> a_430 = a_430 ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f2769,plain,
( sQ85_spl
| sQ84_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f2705,f2760,f2763,f2766]) ).
fof(f2770,definition,
! [X0,X1,X2] :
( sQ86_spl
<=> store(store(X0,a_430,X1),a_440,select(store(store(X0,a_430,X2),a_430,X1),a_440)) = store(store(X0,a_430,X2),a_430,X1) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f2773,plain,
( sQ84_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f2706,f2770,f2763]) ).
fof(f2774,definition,
! [X0,X1,X2] :
( sQ87_spl
<=> store(store(X0,a_430,select(store(X0,a_430,X1),a_430)),a_440,X2) = store(store(X0,a_430,X1),a_440,X2) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f2777,plain,
( sQ84_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f2707,f2774,f2763]) ).
fof(f2778,definition,
! [X0,X1,X2,X3] :
( sQ88_spl
<=> store(store(X0,a_430,X1),a_440,X2) = store(store(store(X0,a_430,X3),a_430,X1),a_440,X2) ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f2781,plain,
( sQ84_spl
| sQ88_spl ),
inference(split_clause,[status(thm)],[f2708,f2778,f2763]) ).
fof(f2783,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ89_spl
<=> ( a_440 = X1
| store(store(store(X0,X1,X2),a_430,X3),a_440,X4) = store(store(store(store(X0,a_440,X4),X1,X2),a_430,X5),a_430,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f2786,plain,
( sQ84_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f2713,f2783,f2763]) ).
fof(f2787,definition,
! [X0,X1,X2] :
( sQ90_spl
<=> store(store(X0,a_430,X1),a_440,X2) = store(store(X0,a_440,X2),a_430,X1) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f2790,plain,
( sQ84_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f2715,f2787,f2763]) ).
fof(f2791,definition,
! [X0,X1,X2] :
( sQ91_spl
<=> store(store(X0,a_430,X1),a_440,select(X0,a_440)) = store(store(X0,a_430,X2),a_430,X1) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f2792,plain,
! [X0,X1,X2] :
( ~ sQ91_spl
| store(store(X0,a_430,X1),a_440,select(X0,a_440)) = store(store(X0,a_430,X2),a_430,X1) ),
inference(component_clause,[status(thm)],[f2791]) ).
fof(f2794,plain,
( sQ84_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f2716,f2791,f2763]) ).
fof(f2802,definition,
! [X0,X1,X2] :
( sQ92_spl
<=> store(store(X0,a_430,X1),a_430,X2) = store(store(X0,a_430,X2),a_440,select(store(store(X0,a_430,X1),a_430,X2),a_440)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f2805,plain,
( sQ92_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f2736,f2763,f2802]) ).
fof(f2807,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ93_spl
<=> ( store(store(store(X1,a_430,X2),a_440,X3),X0,X4) = store(store(store(store(X1,a_430,X5),a_430,X2),X0,X4),a_440,X3)
| a_440 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f2810,plain,
( sQ84_spl
| sQ93_spl ),
inference(split_clause,[status(thm)],[f2739,f2807,f2763]) ).
fof(f2818,plain,
( ~ sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2764,f64]) ).
fof(f2819,plain,
~ sQ84_spl,
inference(contradiction_clause,[status(thm)],[f2818]) ).
fof(f2831,plain,
! [X0,X1] :
( ~ sQ91_spl
| store(store(X0,a_430,X1),a_440,select(X0,a_440)) = store(X0,a_430,X1) ),
inference(forward_demodulation,[status(thm)],[f36,f2792]) ).
fof(f2835,plain,
! [X0,X1,X2,X3] :
( ~ sQ83_spl
| store(store(X0,a_430,X1),a_440,X2) = store(store(X0,a_430,X3),a_440,X2) ),
inference(forward_demodulation,[status(thm)],[f36,f2761]) ).
fof(f3059,plain,
! [X0,X1,X2] :
( ~ sQ35_spl
| select(store(store(X0,a_426,X1),a_440,X2),a_430) = X1 ),
inference(forward_demodulation,[status(thm)],[f710,f2754]) ).
fof(f3060,plain,
! [X0,X1,X2] :
( ~ sQ35_spl
| select(store(store(X0,a_426,X1),a_436,X2),a_430) = X1 ),
inference(forward_demodulation,[status(thm)],[f738,f3059]) ).
fof(f3061,plain,
! [X0,X1,X2] :
( ~ sQ35_spl
| select(store(store(X0,a_426,X1),a_436,X2),a_426) = X1 ),
inference(forward_demodulation,[status(thm)],[f710,f3060]) ).
fof(f3083,plain,
! [X0,X1] :
( ~ sQ35_spl
| select(store(X0,a_436,X1),a_426) = select(X0,a_426) ),
inference(paramodulation,[status(thm)],[f35,f3061]) ).
fof(f5463,plain,
! [X0,X1,X2,X3] :
( ~ sQ83_spl
| ~ sQ35_spl
| store(store(X0,a_426,X1),a_440,X2) = store(store(X0,a_430,X3),a_440,X2) ),
inference(forward_demodulation,[status(thm)],[f710,f2835]) ).
fof(f5464,plain,
! [X0,X1,X2,X3] :
( ~ sQ83_spl
| ~ sQ35_spl
| store(store(X0,a_426,X1),a_436,X2) = store(store(X0,a_430,X3),a_440,X2) ),
inference(forward_demodulation,[status(thm)],[f738,f5463]) ).
fof(f5465,plain,
! [X0,X1,X2,X3] :
( ~ sQ83_spl
| ~ sQ35_spl
| store(store(X0,a_426,X1),a_436,X2) = store(store(X0,a_426,X3),a_440,X2) ),
inference(forward_demodulation,[status(thm)],[f710,f5464]) ).
fof(f5466,plain,
! [X0,X1,X2,X3] :
( ~ sQ83_spl
| ~ sQ35_spl
| store(store(X0,a_426,X1),a_436,X2) = store(store(X0,a_426,X3),a_436,X2) ),
inference(forward_demodulation,[status(thm)],[f738,f5465]) ).
fof(f5519,plain,
! [X0,X1,X2,X3] :
( ~ sQ83_spl
| ~ sQ35_spl
| select(store(store(X0,a_426,X1),a_436,X2),a_426) = select(store(X0,a_426,X3),a_426) ),
inference(paramodulation,[status(thm)],[f5466,f3083]) ).
fof(f5570,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ35_spl
| select(store(X0,a_426,X1),a_426) = select(store(X0,a_426,X2),a_426) ),
inference(forward_demodulation,[status(thm)],[f3083,f5519]) ).
fof(f5571,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| ~ sQ35_spl
| X0 = select(store(X1,a_426,X2),a_426) ),
inference(forward_demodulation,[status(thm)],[f32,f5570]) ).
fof(f5572,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ35_spl
| X0 = X1 ),
inference(forward_demodulation,[status(thm)],[f32,f5571]) ).
fof(f5587,plain,
( sQ50_spl
| ~ sQ83_spl
| ~ sQ35_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1055,f5572]) ).
fof(f5590,plain,
( sQ50_spl
| ~ sQ83_spl
| ~ sQ35_spl ),
inference(contradiction_clause,[status(thm)],[f5587]) ).
fof(f5591,plain,
! [X0] :
( ~ sQ13_spl
| i2 = X0 ),
inference(duplicate_literals_removal,[status(thm)],[f340]) ).
fof(f5592,plain,
! [X0,X1] :
( ~ sQ21_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f383,f383]) ).
fof(f5593,plain,
( ~ sQ21_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f64,f5592]) ).
fof(f5594,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f5593]) ).
fof(f5595,plain,
! [X0,X1] :
( ~ sQ16_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f353,f353]) ).
fof(f5596,plain,
( sQ35_spl
| ~ sQ16_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f558,f5595]) ).
fof(f5597,plain,
( sQ35_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f5596]) ).
fof(f5598,plain,
( ~ sQ13_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f5591,f352,f339]) ).
fof(f5619,definition,
! [X0,X1] :
( sQ141_spl
<=> select(X0,a_426) = X1 ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f5620,plain,
! [X0,X1] :
( ~ sQ141_spl
| select(X0,a_426) = X1 ),
inference(component_clause,[status(thm)],[f5619]) ).
fof(f5625,plain,
! [X0,X1] :
( ~ sQ141_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f5620,f5620]) ).
fof(f5647,plain,
( ~ sQ141_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f64,f5625]) ).
fof(f5648,plain,
~ sQ141_spl,
inference(contradiction_clause,[status(thm)],[f5647]) ).
fof(f5659,plain,
( ~ sQ50_spl
| a_432 = store(a_417,i0,e_419) ),
inference(forward_demodulation,[status(thm)],[f1082,f48]) ).
fof(f5684,plain,
! [X0,X1,X2] : select(store(store(X0,a_440,X1),a_430,X2),a_440) = X1,
inference(paramodulation,[status(thm)],[f2701,f32]) ).
fof(f5722,plain,
! [X0,X1] : select(store(X0,a_440,X1),a_430) = select(X0,a_430),
inference(paramodulation,[status(thm)],[f35,f2754]) ).
fof(f5777,plain,
! [X0,X1] : store(store(X0,a_440,X1),a_430,select(X0,a_430)) = store(X0,a_440,X1),
inference(paramodulation,[status(thm)],[f5722,f35]) ).
fof(f5783,plain,
! [X0,X1] : select(store(X0,a_430,X1),a_440) = select(X0,a_440),
inference(paramodulation,[status(thm)],[f35,f5684]) ).
fof(f5793,plain,
! [X0,X1,X2] : store(store(X0,a_430,X1),a_440,select(store(X0,a_430,X2),a_440)) = store(store(X0,a_430,X2),a_430,X1),
inference(paramodulation,[status(thm)],[f35,f2697]) ).
fof(f5804,plain,
! [X0,X1,X2] : store(store(X0,a_430,X1),a_440,select(X0,a_440)) = store(store(X0,a_430,X2),a_430,X1),
inference(forward_demodulation,[status(thm)],[f5783,f5793]) ).
fof(f5805,plain,
! [X0,X1] : store(store(X0,a_430,X1),a_440,select(X0,a_440)) = store(X0,a_430,X1),
inference(forward_demodulation,[status(thm)],[f36,f5804]) ).
fof(f5817,plain,
( ~ sQ50_spl
| select(a_417,i0) = e_419 ),
inference(forward_demodulation,[status(thm)],[f1125,f1121]) ).
fof(f5838,plain,
( ~ sQ50_spl
| e_423 = select(a_417,i2) ),
inference(forward_demodulation,[status(thm)],[f1125,f56]) ).
fof(f5896,plain,
! [X0,X1,X2] :
( ~ sQ91_spl
| store(store(X0,a_430,X1),a_440,select(X0,a_440)) = store(store(X0,a_430,X2),a_430,X1) ),
inference(paramodulation,[status(thm)],[f2831,f2702]) ).
fof(f5900,plain,
! [X0,X1,X2] :
( ~ sQ91_spl
| store(X0,a_430,X1) = store(store(X0,a_430,X2),a_430,X1) ),
inference(forward_demodulation,[status(thm)],[f2831,f5896]) ).
fof(f5910,plain,
( ~ sQ73_spl
| e_439 = select(a_426,i0) ),
inference(forward_demodulation,[status(thm)],[f2641,f63]) ).
fof(f5952,plain,
! [X0] :
( select(X0,a_430) = select(X0,a_430)
| a_440 = a_430 ),
inference(paramodulation,[status(thm)],[f5722,f34]) ).
fof(f5953,plain,
! [X0] :
( select(X0,a_440) = select(X0,a_440)
| a_430 = a_440 ),
inference(paramodulation,[status(thm)],[f5783,f34]) ).
fof(f5964,definition,
! [X0] :
( sQ142_spl
<=> select(X0,a_430) = select(X0,a_430) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f5967,plain,
( sQ142_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f5952,f2763,f5964]) ).
fof(f5968,definition,
! [X0] :
( sQ143_spl
<=> select(X0,a_440) = select(X0,a_440) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f5971,plain,
( sQ143_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f5953,f2763,f5968]) ).
fof(f6001,plain,
( ~ sQ73_spl
| a_438 = store(a_426,i0,e_435) ),
inference(forward_demodulation,[status(thm)],[f2641,f1171]) ).
fof(f6002,plain,
( ~ sQ73_spl
| e_435 = select(a_426,i2) ),
inference(forward_demodulation,[status(thm)],[f2641,f1279]) ).
fof(f6017,plain,
! [X0,X1] :
( ~ sQ73_spl
| store(a_438,X0,X1) = store(store(a_426,X0,X1),i0,e_435)
| i0 = X0 ),
inference(paramodulation,[status(thm)],[f6001,f38]) ).
fof(f6018,plain,
( ~ sQ73_spl
| a_440 = store(a_438,i2,e_427) ),
inference(backward_demodulation,[status(thm)],[f6022,f52]) ).
fof(f6022,plain,
( ~ sQ73_spl
| e_427 = e_439 ),
inference(forward_demodulation,[status(thm)],[f5910,f58]) ).
fof(f6027,plain,
( ~ sQ73_spl
| e_421 = e_435 ),
inference(forward_demodulation,[status(thm)],[f6002,f546]) ).
fof(f7633,plain,
! [X0,X1,X2] :
( X2 = X2
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f32,f137]) ).
fof(f7689,definition,
! [X2] :
( sQ166_spl
<=> X2 = X2 ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f7692,plain,
( sQ166_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f7633,f432,f7689]) ).
fof(f7781,plain,
( ~ sQ50_spl
| a_417 = a_420 ),
inference(forward_demodulation,[status(thm)],[f297,f1123]) ).
fof(f7783,plain,
( ~ sQ50_spl
| e_421 = e_419 ),
inference(forward_demodulation,[status(thm)],[f292,f5817]) ).
fof(f7796,plain,
( ~ sQ50_spl
| a_432 = a_420 ),
inference(forward_demodulation,[status(thm)],[f297,f5659]) ).
fof(f7800,plain,
( ~ sQ25_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f64,f433]) ).
fof(f7802,plain,
~ sQ25_spl,
inference(contradiction_clause,[status(thm)],[f7800]) ).
fof(f7803,plain,
( ~ sQ50_spl
| a_432 = a_417 ),
inference(forward_demodulation,[status(thm)],[f7781,f7796]) ).
fof(f7811,plain,
( ~ sQ50_spl
| a_424 = store(a_417,i0,e_423) ),
inference(forward_demodulation,[status(thm)],[f1125,f1075]) ).
fof(f7822,plain,
( ~ sQ50_spl
| a_434 = store(a_417,i3,e_433) ),
inference(forward_demodulation,[status(thm)],[f7803,f49]) ).
fof(f7823,plain,
( ~ sQ50_spl
| a_434 = store(a_417,i0,e_433) ),
inference(forward_demodulation,[status(thm)],[f1054,f7822]) ).
fof(f7851,plain,
( ~ sQ50_spl
| e_433 = select(a_417,i2) ),
inference(forward_demodulation,[status(thm)],[f7803,f60]) ).
fof(f7853,plain,
( ~ sQ50_spl
| a_434 = store(a_417,i0,e_423) ),
inference(backward_demodulation,[status(thm)],[f7854,f7823]) ).
fof(f7854,plain,
( ~ sQ50_spl
| e_433 = e_423 ),
inference(forward_demodulation,[status(thm)],[f5838,f7851]) ).
fof(f7855,plain,
( ~ sQ50_spl
| a_434 = a_424 ),
inference(forward_demodulation,[status(thm)],[f7811,f7853]) ).
fof(f7863,plain,
( ~ sQ50_spl
| a_426 = store(a_424,i2,e_419) ),
inference(forward_demodulation,[status(thm)],[f7783,f316]) ).
fof(f7869,plain,
! [X0,X1,X2] : store(store(X0,a_440,X1),a_430,select(X0,a_430)) = store(store(X0,a_440,X2),a_440,X1),
inference(paramodulation,[status(thm)],[f5777,f2701]) ).
fof(f7875,plain,
! [X0,X1,X2] : store(X0,a_440,X1) = store(store(X0,a_440,X2),a_440,X1),
inference(forward_demodulation,[status(thm)],[f5777,f7869]) ).
fof(f7934,plain,
! [X0,X1,X2] : store(store(X0,a_430,X1),a_440,X2) = store(store(X0,a_440,X2),a_430,X1),
inference(resolution,[status(thm)],[f38,f64]) ).
fof(f8121,plain,
! [X0,X1,X2,X3] :
( select(store(X1,a_440,X2),X0) = select(store(X1,a_440,X3),X0)
| a_440 = X0 ),
inference(paramodulation,[status(thm)],[f7875,f34]) ).
fof(f8124,plain,
! [X0,X1,X2,X3] :
( ~ sQ91_spl
| select(store(X1,a_430,X2),X0) = select(store(X1,a_430,X3),X0)
| a_430 = X0 ),
inference(paramodulation,[status(thm)],[f5900,f34]) ).
fof(f8557,plain,
! [X0,X1] :
( ~ sQ73_spl
| store(a_438,X0,X1) = store(store(a_426,X0,X1),i0,e_421)
| i0 = X0 ),
inference(forward_demodulation,[status(thm)],[f6027,f6017]) ).
fof(f8567,plain,
( ~ sQ73_spl
| store(a_438,i2,e_427) = store(a_428,i0,e_421)
| i0 = i2 ),
inference(paramodulation,[status(thm)],[f45,f8557]) ).
fof(f8596,definition,
( sQ185_spl
<=> store(a_438,i2,e_427) = store(a_428,i0,e_421) ),
introduced(definition,[new_symbols(definition,[sQ185_spl])],[split_symbol_definition]) ).
fof(f8597,plain,
( ~ sQ185_spl
| store(a_438,i2,e_427) = store(a_428,i0,e_421) ),
inference(component_clause,[status(thm)],[f8596]) ).
fof(f8599,plain,
( ~ sQ73_spl
| sQ185_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f8567,f556,f8596,f2640]) ).
fof(f9207,plain,
! [X0,X1,X2,X3] :
( a_440 = a_430
| select(store(store(X1,a_430,X2),a_440,X3),X0) = select(store(X1,a_430,X2),X0)
| a_440 = X0 ),
inference(paramodulation,[status(thm)],[f7934,f141]) ).
fof(f9208,plain,
! [X0,X1,X2] :
( a_430 = a_440
| select(store(X1,a_430,X2),X0) = select(store(X1,a_440,select(X1,a_440)),X0)
| a_430 = X0 ),
inference(paramodulation,[status(thm)],[f5805,f141]) ).
fof(f9252,definition,
! [X0,X1,X2,X3] :
( sQ187_spl
<=> ( select(store(store(X1,a_430,X2),a_440,X3),X0) = select(store(X1,a_430,X2),X0)
| a_440 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ187_spl])],[split_symbol_definition]) ).
fof(f9255,plain,
( sQ84_spl
| sQ187_spl ),
inference(split_clause,[status(thm)],[f9207,f9252,f2763]) ).
fof(f9256,definition,
! [X0,X1,X2] :
( sQ188_spl
<=> ( select(store(X1,a_430,X2),X0) = select(store(X1,a_440,select(X1,a_440)),X0)
| a_430 = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ188_spl])],[split_symbol_definition]) ).
fof(f9259,plain,
( sQ84_spl
| sQ188_spl ),
inference(split_clause,[status(thm)],[f9208,f9256,f2763]) ).
fof(f9266,plain,
! [X0,X1] :
( a_430 = a_440
| select(store(X0,a_430,X1),a_430) = X1 ),
inference(paramodulation,[status(thm)],[f5722,f142]) ).
fof(f9267,plain,
! [X0,X1] :
( a_440 = a_430
| select(store(X0,a_440,X1),a_440) = X1 ),
inference(paramodulation,[status(thm)],[f5783,f142]) ).
fof(f9273,plain,
! [X0,X1,X2] :
( a_440 = a_430
| select(store(store(X0,a_430,X1),a_440,X2),a_440) = X2 ),
inference(paramodulation,[status(thm)],[f7934,f142]) ).
fof(f9315,definition,
! [X0,X1] :
( sQ189_spl
<=> select(store(X0,a_430,X1),a_430) = X1 ),
introduced(definition,[new_symbols(definition,[sQ189_spl])],[split_symbol_definition]) ).
fof(f9318,plain,
( sQ84_spl
| sQ189_spl ),
inference(split_clause,[status(thm)],[f9266,f9315,f2763]) ).
fof(f9319,definition,
! [X0,X1] :
( sQ190_spl
<=> select(store(X0,a_440,X1),a_440) = X1 ),
introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition]) ).
fof(f9322,plain,
( sQ84_spl
| sQ190_spl ),
inference(split_clause,[status(thm)],[f9267,f9319,f2763]) ).
fof(f9324,definition,
! [X0,X1,X2] :
( sQ191_spl
<=> select(store(store(X0,a_430,X1),a_440,X2),a_440) = X2 ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f9327,plain,
( sQ84_spl
| sQ191_spl ),
inference(split_clause,[status(thm)],[f9273,f9324,f2763]) ).
fof(f9520,plain,
! [X0,X1] :
( select(X0,a_430) = select(store(X0,a_440,X1),a_430)
| a_440 = a_430 ),
inference(paramodulation,[status(thm)],[f5722,f8121]) ).
fof(f9563,definition,
! [X0,X1] :
( sQ192_spl
<=> select(X0,a_430) = select(store(X0,a_440,X1),a_430) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f9566,plain,
( sQ192_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f9520,f2763,f9563]) ).
fof(f9602,plain,
! [X0,X1] :
( ~ sQ91_spl
| select(X0,a_440) = select(store(X0,a_430,X1),a_440)
| a_430 = a_440 ),
inference(paramodulation,[status(thm)],[f5783,f8124]) ).
fof(f9605,plain,
! [X0,X1,X2] :
( ~ sQ91_spl
| X0 = select(store(X1,a_430,X2),a_430)
| a_430 = a_430 ),
inference(paramodulation,[status(thm)],[f32,f8124]) ).
fof(f9635,plain,
! [X0,X1,X2,X3] :
( ~ sQ91_spl
| a_430 = a_440
| store(store(store(X0,a_430,X1),a_430,X2),a_440,select(store(X0,a_430,X3),a_440)) = store(store(X0,a_430,X1),a_430,X2) ),
inference(paramodulation,[status(thm)],[f8124,f5805]) ).
fof(f9645,definition,
! [X0,X1] :
( sQ196_spl
<=> select(X0,a_440) = select(store(X0,a_430,X1),a_440) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f9648,plain,
( ~ sQ91_spl
| sQ196_spl
| sQ84_spl ),
inference(split_clause,[status(thm)],[f9602,f2763,f9645,f2791]) ).
fof(f9651,definition,
! [X0,X1,X2] :
( sQ197_spl
<=> X0 = select(store(X1,a_430,X2),a_430) ),
introduced(definition,[new_symbols(definition,[sQ197_spl])],[split_symbol_definition]) ).
fof(f9654,plain,
( ~ sQ91_spl
| sQ197_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f9605,f2766,f9651,f2791]) ).
fof(f9670,definition,
! [X0,X1,X2,X3] :
( sQ198_spl
<=> store(store(store(X0,a_430,X1),a_430,X2),a_440,select(store(X0,a_430,X3),a_440)) = store(store(X0,a_430,X1),a_430,X2) ),
introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition]) ).
fof(f9673,plain,
( ~ sQ91_spl
| sQ84_spl
| sQ198_spl ),
inference(split_clause,[status(thm)],[f9635,f9670,f2763,f2791]) ).
fof(f9708,plain,
( store(a_431,i0,e_419) = store(a_420,i3,e_421)
| i3 = i0 ),
inference(paramodulation,[status(thm)],[f570,f298]) ).
fof(f9741,definition,
( sQ203_spl
<=> store(a_431,i0,e_419) = store(a_420,i3,e_421) ),
introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition]) ).
fof(f9742,plain,
( ~ sQ203_spl
| store(a_431,i0,e_419) = store(a_420,i3,e_421) ),
inference(component_clause,[status(thm)],[f9741]) ).
fof(f9744,plain,
( sQ203_spl
| sQ50_spl ),
inference(split_clause,[status(thm)],[f9708,f1053,f9741]) ).
fof(f9750,plain,
( ~ sQ203_spl
| a_432 = store(a_420,i3,e_421) ),
inference(forward_demodulation,[status(thm)],[f48,f9742]) ).
fof(f9751,plain,
( ~ sQ203_spl
| a_432 = a_422 ),
inference(forward_demodulation,[status(thm)],[f42,f9750]) ).
fof(f9776,plain,
( ~ sQ203_spl
| a_434 = store(a_422,i3,e_433) ),
inference(backward_demodulation,[status(thm)],[f9751,f49]) ).
fof(f9777,plain,
( ~ sQ203_spl
| e_435 = select(a_422,i3) ),
inference(backward_demodulation,[status(thm)],[f9751,f61]) ).
fof(f9779,plain,
( ~ sQ203_spl
| e_433 = select(a_422,i2) ),
inference(backward_demodulation,[status(thm)],[f9751,f60]) ).
fof(f9784,plain,
( ~ sQ203_spl
| e_435 = e_421 ),
inference(forward_demodulation,[status(thm)],[f310,f9777]) ).
fof(f9785,plain,
( ~ sQ203_spl
| e_433 = e_423 ),
inference(forward_demodulation,[status(thm)],[f56,f9779]) ).
fof(f9791,plain,
( ~ sQ203_spl
| a_436 = store(a_434,i2,e_421) ),
inference(backward_demodulation,[status(thm)],[f9784,f50]) ).
fof(f9895,plain,
( ~ sQ203_spl
| a_434 = store(a_422,i3,e_423) ),
inference(forward_demodulation,[status(thm)],[f9785,f9776]) ).
fof(f9898,plain,
( ~ sQ203_spl
| a_434 = a_424 ),
inference(forward_demodulation,[status(thm)],[f43,f9895]) ).
fof(f9906,plain,
( ~ sQ203_spl
| a_436 = store(a_424,i2,e_421) ),
inference(forward_demodulation,[status(thm)],[f9898,f9791]) ).
fof(f9907,plain,
( ~ sQ203_spl
| a_436 = a_426 ),
inference(forward_demodulation,[status(thm)],[f316,f9906]) ).
fof(f9908,plain,
( ~ sQ203_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f9907,f2642]) ).
fof(f9909,plain,
( ~ sQ203_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f9908]) ).
fof(f9912,plain,
( ~ sQ185_spl
| store(a_438,i2,e_427) = a_430 ),
inference(forward_demodulation,[status(thm)],[f548,f8597]) ).
fof(f10056,plain,
( ~ sQ185_spl
| ~ sQ73_spl
| a_440 = a_430 ),
inference(forward_demodulation,[status(thm)],[f6018,f9912]) ).
fof(f10057,plain,
( ~ sQ185_spl
| ~ sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10056,f64]) ).
fof(f10058,plain,
( ~ sQ185_spl
| ~ sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f10057]) ).
fof(f10333,plain,
( ~ sQ50_spl
| a_436 = store(a_424,i2,e_435) ),
inference(forward_demodulation,[status(thm)],[f7855,f50]) ).
fof(f10334,plain,
( ~ sQ50_spl
| a_436 = store(a_424,i2,e_419) ),
inference(forward_demodulation,[status(thm)],[f1086,f10333]) ).
fof(f10335,plain,
( ~ sQ50_spl
| a_436 = a_426 ),
inference(forward_demodulation,[status(thm)],[f7863,f10334]) ).
fof(f10336,plain,
( ~ sQ50_spl
| sQ73_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f10335,f2642]) ).
fof(f10337,plain,
( ~ sQ50_spl
| sQ73_spl ),
inference(contradiction_clause,[status(thm)],[f10336]) ).
fof(f10338,plain,
$false,
inference(sat_refutation,[status(thm)],[f355,f385,f435,f444,f559,f613,f1147,f1220,f2255,f2298,f2696,f2769,f2773,f2777,f2781,f2786,f2790,f2794,f2805,f2810,f2819,f5590,f5594,f5597,f5598,f5648,f5967,f5971,f7692,f7802,f8599,f9255,f9259,f9318,f9322,f9327,f9566,f9648,f9654,f9673,f9744,f9909,f10058,f10337]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV540-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:04:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 3.74/0.97 % Refutation found
% 3.74/0.97 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.74/0.97 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.01/1.01 % Elapsed time: 0.633880 seconds
% 2.01/1.01 % CPU time: 4.489336 seconds
% 2.01/1.01 % Total memory used: 169.143 MB
% 2.01/1.01 % Net memory used: 153.152 MB
%------------------------------------------------------------------------------