%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV540-1.004 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 : Tue Sep 29 01:17:33 PM UTC 2026
% Result : Unsatisfiable 5.59s 1.57s
% Output : Refutation 6.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 30
% Syntax : Number of formulae : 193 ( 60 unt; 3 def)
% Number of atoms : 371 ( 179 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 310 ( 132 ~; 175 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 26 con; 0-3 aty)
% Number of variables : 29 ( 0 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : select(store(X0,X1,X2),X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a1) ).
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) ).
fof(f36,plain,
! [X0] : store(a_418,i0,X0) = store(a_420,i0,X0),
inference(superposition,[],[f4,f8]) ).
fof(f39,plain,
! [X0] : store(a_424,i2,X0) = store(a_426,i2,X0),
inference(superposition,[],[f4,f11]) ).
fof(f40,plain,
! [X0] : store(a_426,i2,X0) = store(a_428,i2,X0),
inference(superposition,[],[f4,f12]) ).
fof(f42,plain,
! [X0] : store(a_431,i0,X0) = store(a_432,i0,X0),
inference(superposition,[],[f4,f15]) ).
fof(f43,plain,
! [X0] : store(a_432,i3,X0) = store(a_434,i3,X0),
inference(superposition,[],[f4,f16]) ).
fof(f44,plain,
! [X0] : store(a_434,i2,X0) = store(a_436,i2,X0),
inference(superposition,[],[f4,f17]) ).
fof(f45,plain,
! [X0] : store(a_436,i0,X0) = store(a_438,i0,X0),
inference(superposition,[],[f4,f18]) ).
fof(f53,plain,
e_421 = select(a_422,i3),
inference(superposition,[],[f1,f9]) ).
fof(f55,plain,
e_425 = select(a_426,i2),
inference(superposition,[],[f1,f11]) ).
fof(f58,plain,
e_419 = select(a_432,i0),
inference(superposition,[],[f1,f15]) ).
fof(f60,plain,
e_435 = select(a_436,i2),
inference(superposition,[],[f1,f17]) ).
fof(f63,plain,
e_435 = e_437,
inference(forward_demodulation,[],[f60,f29]) ).
fof(f64,plain,
e_425 = e_429,
inference(forward_demodulation,[],[f55,f26]) ).
fof(f65,plain,
e_421 = e_425,
inference(forward_demodulation,[],[f53,f24]) ).
fof(f66,plain,
a_426 = store(a_424,i2,e_421),
inference(superposition,[],[f11,f65]) ).
fof(f67,plain,
a_426 = store(a_426,i2,e_421),
inference(forward_demodulation,[],[f66,f39]) ).
fof(f68,plain,
a_438 = store(a_436,i0,e_435),
inference(superposition,[],[f18,f63]) ).
fof(f69,plain,
a_430 = store(a_428,i0,e_425),
inference(superposition,[],[f13,f64]) ).
fof(f70,plain,
a_430 = store(a_428,i0,e_421),
inference(forward_demodulation,[],[f69,f65]) ).
fof(f80,plain,
a_418 = store(a_418,i3,e_419),
inference(superposition,[],[f3,f21]) ).
fof(f81,plain,
a_418 = store(a_418,i0,e_421),
inference(superposition,[],[f3,f22]) ).
fof(f82,plain,
a_422 = store(a_422,i2,e_423),
inference(superposition,[],[f3,f23]) ).
fof(f83,plain,
a_422 = store(a_422,i3,e_425),
inference(superposition,[],[f3,f24]) ).
fof(f85,plain,
a_426 = store(a_426,i0,e_427),
inference(superposition,[],[f3,f25]) ).
fof(f86,plain,
a_432 = store(a_432,i2,e_433),
inference(superposition,[],[f3,f27]) ).
fof(f88,plain,
a_436 = store(a_436,i2,e_437),
inference(superposition,[],[f3,f29]) ).
fof(f92,plain,
a_436 = store(a_436,i2,e_435),
inference(forward_demodulation,[],[f88,f63]) ).
fof(f94,plain,
a_422 = store(a_422,i3,e_421),
inference(forward_demodulation,[],[f83,f65]) ).
fof(f154,plain,
! [X0,X1] :
( store(store(a_418,X0,X1),i3,e_421) = store(a_431,X0,X1)
| i3 = X0 ),
inference(superposition,[],[f5,f14]) ).
fof(f161,plain,
! [X0,X1] :
( store(store(a_426,X0,X1),i2,e_427) = store(a_428,X0,X1)
| i2 = X0 ),
inference(superposition,[],[f5,f12]) ).
fof(f232,plain,
a_432 = store(a_432,i0,e_419),
inference(superposition,[],[f15,f42]) ).
fof(f420,definition,
( spl0_1
<=> i0 = i2 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f421,plain,
( i0 != i2
| spl0_1 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f422,plain,
( i0 = i2
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f420]) ).
fof(f452,definition,
( spl0_3
<=> i0 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f453,plain,
( i0 != i3
| spl0_3 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f454,plain,
( i0 = i3
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f461,definition,
( spl0_5
<=> i3 = i2 ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f462,plain,
( i3 != i2
| spl0_5 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f463,plain,
( i3 = i2
| ~ spl0_5 ),
inference(avatar_component_clause,[],[f461]) ).
fof(f472,plain,
( a_424 = store(a_422,i2,e_423)
| ~ spl0_5 ),
inference(superposition,[],[f10,f463]) ).
fof(f477,plain,
( e_435 = select(a_432,i2)
| ~ spl0_5 ),
inference(superposition,[],[f28,f463]) ).
fof(f481,plain,
( ! [X0] : store(a_434,i2,X0) = store(a_432,i2,X0)
| ~ spl0_5 ),
inference(superposition,[],[f43,f463]) ).
fof(f487,plain,
( a_422 = store(a_422,i2,e_421)
| ~ spl0_5 ),
inference(superposition,[],[f94,f463]) ).
fof(f489,plain,
( ! [X0] : store(a_436,i2,X0) = store(a_432,i2,X0)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f481,f44]) ).
fof(f491,plain,
( e_433 = e_435
| ~ spl0_5 ),
inference(forward_demodulation,[],[f477,f27]) ).
fof(f494,plain,
( a_422 = a_424
| ~ spl0_5 ),
inference(forward_demodulation,[],[f472,f82]) ).
fof(f502,plain,
( a_436 = store(a_436,i2,e_433)
| ~ spl0_5 ),
inference(superposition,[],[f92,f491]) ).
fof(f505,plain,
( a_436 = store(a_432,i2,e_433)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f502,f489]) ).
fof(f508,plain,
( a_432 = a_436
| ~ spl0_5 ),
inference(forward_demodulation,[],[f505,f86]) ).
fof(f512,plain,
( e_439 = select(a_432,i0)
| ~ spl0_5 ),
inference(superposition,[],[f30,f508]) ).
fof(f517,plain,
( e_419 = e_439
| ~ spl0_5 ),
inference(forward_demodulation,[],[f512,f58]) ).
fof(f540,plain,
( a_426 = store(a_422,i2,e_425)
| ~ spl0_5 ),
inference(superposition,[],[f11,f494]) ).
fof(f541,plain,
( a_426 = store(a_422,i2,e_421)
| ~ spl0_5 ),
inference(forward_demodulation,[],[f540,f65]) ).
fof(f543,plain,
( a_422 = a_426
| ~ spl0_5 ),
inference(forward_demodulation,[],[f541,f487]) ).
fof(f610,plain,
( store(a_420,i3,e_421) = store(a_431,i0,e_419)
| i0 = i3 ),
inference(superposition,[],[f154,f8]) ).
fof(f636,plain,
( store(a_420,i3,e_421) = store(a_431,i0,e_419)
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f610,f453]) ).
fof(f645,plain,
( store(a_420,i3,e_421) = a_432
| spl0_3 ),
inference(forward_demodulation,[],[f636,f15]) ).
fof(f658,plain,
( a_422 = a_432
| spl0_3 ),
inference(forward_demodulation,[],[f645,f9]) ).
fof(f665,plain,
( e_433 = select(a_422,i2)
| spl0_3 ),
inference(superposition,[],[f27,f658]) ).
fof(f666,plain,
( e_435 = select(a_422,i3)
| spl0_3 ),
inference(superposition,[],[f28,f658]) ).
fof(f672,plain,
( e_425 = e_435
| spl0_3 ),
inference(forward_demodulation,[],[f666,f24]) ).
fof(f673,plain,
( e_423 = e_433
| spl0_3 ),
inference(forward_demodulation,[],[f665,f23]) ).
fof(f674,plain,
( e_421 = e_435
| spl0_3 ),
inference(forward_demodulation,[],[f672,f65]) ).
fof(f683,plain,
( a_434 = store(a_432,i3,e_423)
| spl0_3 ),
inference(superposition,[],[f16,f673]) ).
fof(f684,plain,
( store(a_422,i3,e_423) = a_434
| spl0_3 ),
inference(forward_demodulation,[],[f683,f658]) ).
fof(f687,plain,
( a_424 = a_434
| spl0_3 ),
inference(forward_demodulation,[],[f684,f10]) ).
fof(f692,plain,
( a_436 = store(a_424,i2,e_435)
| spl0_3 ),
inference(superposition,[],[f17,f687]) ).
fof(f693,plain,
( a_436 = store(a_426,i2,e_435)
| spl0_3 ),
inference(forward_demodulation,[],[f692,f39]) ).
fof(f697,plain,
( a_436 = store(a_426,i2,e_421)
| spl0_3 ),
inference(forward_demodulation,[],[f693,f674]) ).
fof(f698,plain,
( a_426 = a_436
| spl0_3 ),
inference(forward_demodulation,[],[f697,f67]) ).
fof(f701,plain,
( e_439 = select(a_426,i0)
| spl0_3 ),
inference(superposition,[],[f30,f698]) ).
fof(f702,plain,
( a_438 = store(a_426,i0,e_435)
| spl0_3 ),
inference(superposition,[],[f68,f698]) ).
fof(f706,plain,
( a_438 = store(a_426,i0,e_421)
| spl0_3 ),
inference(forward_demodulation,[],[f702,f674]) ).
fof(f707,plain,
( e_427 = e_439
| spl0_3 ),
inference(forward_demodulation,[],[f701,f25]) ).
fof(f715,plain,
( a_440 = store(a_438,i2,e_427)
| spl0_3 ),
inference(superposition,[],[f19,f707]) ).
fof(f755,plain,
( store(a_428,i0,e_421) = store(a_438,i2,e_427)
| i0 = i2
| spl0_3 ),
inference(superposition,[],[f161,f706]) ).
fof(f763,plain,
( store(a_428,i0,e_421) = store(a_438,i2,e_427)
| spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f755,f421]) ).
fof(f765,plain,
( a_440 = store(a_428,i0,e_421)
| spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f763,f715]) ).
fof(f766,plain,
( a_430 = a_440
| spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f765,f70]) ).
fof(f767,plain,
( $false
| spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f766,f31]) ).
fof(f768,plain,
( spl0_1
| spl0_3 ),
inference(avatar_contradiction_clause,[],[f767]) ).
fof(f769,plain,
( a_422 = store(a_420,i0,e_421)
| ~ spl0_3 ),
inference(superposition,[],[f9,f454]) ).
fof(f771,plain,
( a_431 = store(a_418,i0,e_421)
| ~ spl0_3 ),
inference(superposition,[],[f14,f454]) ).
fof(f773,plain,
( e_419 = select(a_418,i0)
| ~ spl0_3 ),
inference(superposition,[],[f21,f454]) ).
fof(f775,plain,
( e_435 = select(a_432,i0)
| ~ spl0_3 ),
inference(superposition,[],[f28,f454]) ).
fof(f783,plain,
( a_418 = store(a_418,i0,e_419)
| ~ spl0_3 ),
inference(superposition,[],[f80,f454]) ).
fof(f788,plain,
( i0 != i2
| ~ spl0_3
| spl0_5 ),
inference(superposition,[],[f462,f454]) ).
fof(f789,plain,
( a_418 = a_420
| ~ spl0_3 ),
inference(forward_demodulation,[],[f783,f8]) ).
fof(f793,plain,
( e_419 = e_435
| ~ spl0_3 ),
inference(forward_demodulation,[],[f775,f58]) ).
fof(f795,plain,
( e_419 = e_421
| ~ spl0_3 ),
inference(forward_demodulation,[],[f773,f22]) ).
fof(f796,plain,
( a_418 = a_431
| ~ spl0_3 ),
inference(forward_demodulation,[],[f771,f81]) ).
fof(f797,plain,
( a_422 = store(a_418,i0,e_421)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f769,f36]) ).
fof(f798,plain,
( a_418 = a_422
| ~ spl0_3 ),
inference(forward_demodulation,[],[f797,f81]) ).
fof(f801,plain,
( a_426 = store(a_426,i2,e_419)
| ~ spl0_3 ),
inference(superposition,[],[f67,f795]) ).
fof(f802,plain,
( a_430 = store(a_428,i0,e_419)
| ~ spl0_3 ),
inference(superposition,[],[f70,f795]) ).
fof(f830,plain,
( e_423 = select(a_418,i2)
| ~ spl0_3 ),
inference(superposition,[],[f23,f798]) ).
fof(f831,plain,
( a_424 = store(a_418,i3,e_423)
| ~ spl0_3 ),
inference(superposition,[],[f10,f798]) ).
fof(f832,plain,
( a_424 = store(a_418,i0,e_423)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f831,f454]) ).
fof(f846,plain,
( store(a_418,i0,e_419) = a_432
| ~ spl0_3 ),
inference(superposition,[],[f15,f796]) ).
fof(f847,plain,
( a_420 = a_432
| ~ spl0_3 ),
inference(forward_demodulation,[],[f846,f8]) ).
fof(f849,plain,
( a_418 = a_432
| ~ spl0_3 ),
inference(forward_demodulation,[],[f847,f789]) ).
fof(f850,plain,
( a_434 = store(a_418,i3,e_433)
| ~ spl0_3 ),
inference(superposition,[],[f16,f849]) ).
fof(f851,plain,
( e_433 = select(a_418,i2)
| ~ spl0_3 ),
inference(superposition,[],[f27,f849]) ).
fof(f864,plain,
( e_423 = e_433
| ~ spl0_3 ),
inference(forward_demodulation,[],[f851,f830]) ).
fof(f974,plain,
( a_434 = store(a_418,i0,e_433)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f850,f454]) ).
fof(f977,plain,
( a_434 = store(a_418,i0,e_423)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f974,f864]) ).
fof(f980,plain,
( a_424 = a_434
| ~ spl0_3 ),
inference(forward_demodulation,[],[f977,f832]) ).
fof(f997,plain,
( a_436 = store(a_424,i2,e_435)
| ~ spl0_3 ),
inference(superposition,[],[f17,f980]) ).
fof(f998,plain,
( a_436 = store(a_426,i2,e_435)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f997,f39]) ).
fof(f1002,plain,
( a_436 = store(a_426,i2,e_419)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f998,f793]) ).
fof(f1004,plain,
( a_426 = a_436
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1002,f801]) ).
fof(f1008,plain,
( e_439 = select(a_426,i0)
| ~ spl0_3 ),
inference(superposition,[],[f30,f1004]) ).
fof(f1009,plain,
( a_438 = store(a_426,i0,e_435)
| ~ spl0_3 ),
inference(superposition,[],[f68,f1004]) ).
fof(f1015,plain,
( a_438 = store(a_426,i0,e_419)
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1009,f793]) ).
fof(f1016,plain,
( e_427 = e_439
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1008,f25]) ).
fof(f1026,plain,
( a_440 = store(a_438,i2,e_427)
| ~ spl0_3 ),
inference(superposition,[],[f19,f1016]) ).
fof(f1045,plain,
( store(a_438,i2,e_427) = store(a_428,i0,e_419)
| i0 = i2
| ~ spl0_3 ),
inference(superposition,[],[f161,f1015]) ).
fof(f1053,plain,
( store(a_438,i2,e_427) = store(a_428,i0,e_419)
| spl0_1
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1045,f421]) ).
fof(f1055,plain,
( a_430 = store(a_438,i2,e_427)
| spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1053,f802]) ).
fof(f1056,plain,
( a_430 = a_440
| spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1055,f1026]) ).
fof(f1057,plain,
( $false
| spl0_1
| ~ spl0_3 ),
inference(forward_subsumption_resolution,[],[f1056,f31]) ).
fof(f1058,plain,
( spl0_1
| ~ spl0_3 ),
inference(avatar_contradiction_clause,[],[f1057]) ).
fof(f1059,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| spl0_5 ),
inference(forward_subsumption_resolution,[],[f788,f422]) ).
fof(f1060,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_5 ),
inference(avatar_contradiction_clause,[],[f1059]) ).
fof(f1064,plain,
( a_418 = a_426
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f543,f798]) ).
fof(f1066,plain,
( e_419 = e_427
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f517,f1016]) ).
fof(f1082,plain,
( ! [X0] : store(a_436,i2,X0) = store(a_438,i2,X0)
| ~ spl0_1 ),
inference(superposition,[],[f45,f422]) ).
fof(f1087,plain,
( a_430 = store(a_428,i2,e_421)
| ~ spl0_1 ),
inference(superposition,[],[f70,f422]) ).
fof(f1089,plain,
( a_426 = store(a_426,i2,e_427)
| ~ spl0_1 ),
inference(superposition,[],[f85,f422]) ).
fof(f1091,plain,
( a_432 = store(a_432,i2,e_419)
| ~ spl0_1 ),
inference(superposition,[],[f232,f422]) ).
fof(f1093,plain,
( a_430 = store(a_428,i2,e_419)
| ~ spl0_1
| ~ spl0_3 ),
inference(superposition,[],[f802,f422]) ).
fof(f1094,plain,
( a_438 = store(a_426,i2,e_419)
| ~ spl0_1
| ~ spl0_3 ),
inference(superposition,[],[f1015,f422]) ).
fof(f1095,plain,
( a_426 = a_438
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1094,f801]) ).
fof(f1096,plain,
( a_430 = store(a_426,i2,e_419)
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1093,f40]) ).
fof(f1098,plain,
( a_418 = store(a_418,i2,e_419)
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1091,f849]) ).
fof(f1100,plain,
( a_426 = a_428
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1089,f12]) ).
fof(f1102,plain,
( a_430 = store(a_426,i2,e_421)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1087,f40]) ).
fof(f1117,plain,
( a_418 = a_438
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1095,f1064]) ).
fof(f1118,plain,
( a_426 = a_430
| ~ spl0_1
| ~ spl0_3 ),
inference(forward_demodulation,[],[f1096,f801]) ).
fof(f1121,plain,
( a_426 = a_430
| ~ spl0_1 ),
inference(forward_demodulation,[],[f1102,f67]) ).
fof(f1134,plain,
( a_418 = a_430
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1118,f1064]) ).
fof(f1184,plain,
( a_440 = store(a_418,i2,e_427)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(superposition,[],[f1026,f1117]) ).
fof(f1191,plain,
( a_440 = store(a_418,i2,e_419)
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1184,f1066]) ).
fof(f1195,plain,
( a_418 = a_440
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_demodulation,[],[f1191,f1098]) ).
fof(f1199,plain,
( a_418 != a_430
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(superposition,[],[f31,f1195]) ).
fof(f1200,plain,
( $false
| ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(forward_subsumption_resolution,[],[f1199,f1134]) ).
fof(f1201,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(avatar_contradiction_clause,[],[f1200]) ).
fof(f1210,plain,
( ! [X0] : store(a_426,i2,X0) = store(a_438,i2,X0)
| ~ spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f1082,f698]) ).
fof(f1291,plain,
( a_440 = store(a_438,i2,e_427)
| spl0_3 ),
inference(superposition,[],[f19,f707]) ).
fof(f1292,plain,
( store(a_426,i2,e_427) = a_440
| ~ spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f1291,f1210]) ).
fof(f1294,plain,
( a_428 = a_440
| ~ spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f1292,f12]) ).
fof(f1296,plain,
( a_426 = a_440
| ~ spl0_1
| spl0_3 ),
inference(forward_demodulation,[],[f1294,f1100]) ).
fof(f1299,plain,
( a_426 != a_430
| ~ spl0_1
| spl0_3 ),
inference(superposition,[],[f31,f1296]) ).
fof(f1300,plain,
( $false
| ~ spl0_1
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f1299,f1121]) ).
fof(f1301,plain,
( ~ spl0_1
| spl0_3 ),
inference(avatar_contradiction_clause,[],[f1300]) ).
cnf(s8,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f768]) ).
cnf(s10,plain,
( spl0_1
| ~ spl0_3 ),
inference(sat_conversion,[],[f1058]) ).
cnf(s11,plain,
( ~ spl0_1
| ~ spl0_3
| spl0_5 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s12,plain,
( ~ spl0_1
| ~ spl0_3
| ~ spl0_5 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s13,plain,
( ~ spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f1301]) ).
cnf(s14,plain,
spl0_1,
inference(rat,[],[s8,s10]) ).
cnf(s15,plain,
spl0_3,
inference(rat,[],[s13,s14]) ).
cnf(s16,plain,
~ spl0_5,
inference(rat,[],[s12,s15,s14]) ).
cnf(s17,plain,
$false,
inference(rat,[],[s11,s15,s14,s16]) ).
fof(f1302,plain,
$false,
inference(avatar_sat_refutation,[],[s17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV540-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n005.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 11:38:17 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.59/1.57 % (731576)Input is clausal, will run a generic CNF schedule.
% 5.59/1.57 % (731581)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1872787325:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.59/1.57 % (731586)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=528522417:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.59/1.57 % (731587)dis-21_1_sil=8000:lcm=predicate:random_seed=2595101225:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 5.59/1.57 % (731582)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3702938831:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.59/1.57 % (731585)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3736099897:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.59/1.57 % (731584)lrs+10_1_sil=8000:sp=occurrence:random_seed=1984207471:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.59/1.57 % (731583)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3945283327:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.59/1.57 % (731587)Refutation not found, incomplete strategy
% 5.59/1.57 % (731587)------------------------------
% 5.59/1.57 % (731587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731587)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731587)Termination reason: Refutation not found, incomplete strategy
% 5.59/1.57 % (731587)Time elapsed: 0.001 s
% 5.59/1.57 % (731587)Peak memory usage: 88 MB
% 5.59/1.57 % (731587)Instructions burned: 1 (million)
% 5.59/1.57 % (731584)Instruction limit reached!
% 5.59/1.57 % (731584)------------------------------
% 5.59/1.57 % (731584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731584)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731584)Termination reason: Instruction limit
% 5.59/1.57 % (731584)Termination phase: Saturation
% 5.59/1.57 % (731584)Time elapsed: 0.059 s
% 5.59/1.57 % (731584)Peak memory usage: 89 MB
% 5.59/1.57 % (731584)Instructions burned: 108 (million)
% 5.59/1.57 % (731585)Instruction limit reached!
% 5.59/1.57 % (731585)------------------------------
% 5.59/1.57 % (731585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731585)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731585)Termination reason: Instruction limit
% 5.59/1.57 % (731585)Termination phase: Saturation
% 5.59/1.57 % (731585)Time elapsed: 0.060 s
% 5.59/1.57 % (731585)Peak memory usage: 88 MB
% 5.59/1.57 % (731585)Instructions burned: 115 (million)
% 5.59/1.57 % (731586)Instruction limit reached!
% 5.59/1.57 % (731586)------------------------------
% 5.59/1.57 % (731586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731586)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731586)Termination reason: Instruction limit
% 5.59/1.57 % (731586)Termination phase: Saturation
% 5.59/1.57 % (731586)Time elapsed: 0.101 s
% 5.59/1.57 % (731586)Peak memory usage: 89 MB
% 5.59/1.57 % (731586)Instructions burned: 181 (million)
% 5.59/1.57 % (731596)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=712200365:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 5.59/1.57 % (731595)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1515687799:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.59/1.57 % (731597)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2459709508:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.59/1.57 % (731587)------------------------------
% 5.59/1.57 % (731587)------------------------------
% 5.59/1.57 % (731596)Instruction limit reached!
% 5.59/1.57 % (731596)------------------------------
% 5.59/1.57 % (731596)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731596)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731596)Termination reason: Instruction limit
% 5.59/1.57 % (731596)Termination phase: Saturation
% 5.59/1.57 % (731596)Time elapsed: 0.090 s
% 5.59/1.57 % (731596)Peak memory usage: 89 MB
% 5.59/1.57 % (731596)Instructions burned: 189 (million)
% 5.59/1.57 % (731595)Instruction limit reached!
% 5.59/1.57 % (731595)------------------------------
% 5.59/1.57 % (731595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731595)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731595)Termination reason: Instruction limit
% 5.59/1.57 % (731595)Termination phase: Saturation
% 5.59/1.57 % (731595)Time elapsed: 0.090 s
% 5.59/1.57 % (731595)Peak memory usage: 89 MB
% 5.59/1.57 % (731595)Instructions burned: 143 (million)
% 5.59/1.57 % (731601)lrs+10_64_to=lpo:sil=8000:random_seed=1550137884:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.59/1.57 % (731597)Instruction limit reached!
% 5.59/1.57 % (731597)------------------------------
% 5.59/1.57 % (731597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731597)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731597)Termination reason: Instruction limit
% 5.59/1.57 % (731597)Termination phase: Saturation
% 5.59/1.57 % (731597)Time elapsed: 0.113 s
% 5.59/1.57 % (731597)Peak memory usage: 89 MB
% 5.59/1.57 % (731597)Instructions burned: 219 (million)
% 5.59/1.57 % (731601)Instruction limit reached!
% 5.59/1.57 % (731601)------------------------------
% 5.59/1.57 % (731601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731601)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731601)Termination reason: Instruction limit
% 5.59/1.57 % (731601)Termination phase: Saturation
% 5.59/1.57 % (731601)Time elapsed: 0.032 s
% 5.59/1.57 % (731601)Peak memory usage: 88 MB
% 5.59/1.57 % (731601)Instructions burned: 130 (million)
% 5.59/1.57 % (731602)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=698849839:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.59/1.57 % (731603)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3053439474:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.59/1.57 % (731606)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1029471785:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.59/1.57 % (731605)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=531205705:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 5.59/1.57 % (731581)First to succeed.
% 5.59/1.57 % (731581)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-731576"
% 5.59/1.57 % (731606)Instruction limit reached!
% 5.59/1.57 % (731606)------------------------------
% 5.59/1.57 % (731606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731606)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731606)Termination reason: Instruction limit
% 5.59/1.57 % (731606)Termination phase: Saturation
% 5.59/1.57 % (731606)Time elapsed: 0.030 s
% 5.59/1.57 % (731606)Peak memory usage: 89 MB
% 5.59/1.57 % (731606)Instructions burned: 108 (million)
% 5.59/1.57 % (731603)Instruction limit reached!
% 5.59/1.57 % (731603)------------------------------
% 5.59/1.57 % (731603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731603)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731603)Termination reason: Instruction limit
% 5.59/1.57 % (731603)Termination phase: Saturation
% 5.59/1.57 % (731603)Time elapsed: 0.088 s
% 5.59/1.57 % (731603)Peak memory usage: 89 MB
% 5.59/1.57 % (731603)Instructions burned: 157 (million)
% 5.59/1.57 % (731602)Instruction limit reached!
% 5.59/1.57 % (731602)------------------------------
% 5.59/1.57 % (731602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731602)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731602)Termination reason: Instruction limit
% 5.59/1.57 % (731602)Termination phase: Saturation
% 5.59/1.57 % (731602)Time elapsed: 0.117 s
% 5.59/1.57 % (731602)Peak memory usage: 88 MB
% 5.59/1.57 % (731602)Instructions burned: 195 (million)
% 5.59/1.57 % (731611)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2247607482:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.59/1.57 % (731611)Instruction limit reached!
% 5.59/1.57 % (731611)------------------------------
% 5.59/1.57 % (731611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.59/1.57 % (731611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.59/1.57 % (731611)CaDiCaL version: 2.1.3
% 5.59/1.57 % (731611)Termination reason: Instruction limit
% 5.59/1.57 % (731611)Termination phase: Saturation
% 5.59/1.57 % (731611)Time elapsed: 0.034 s
% 5.59/1.57 % (731611)Peak memory usage: 88 MB
% 5.59/1.57 % (731611)Instructions burned: 108 (million)
% 5.59/1.57 % (731612)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2175419717:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 5.59/1.57 % (731613)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=587721616:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 5.59/1.57 % (731615)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=613686405:i=134:sd=2:doe=on:ss=axioms:sgt=14_2992 on theBenchmark for (2992ds/134Mi)
% 5.59/1.57 % (731581)Refutation found. Thanks to Tanya!
% 5.59/1.57 % SZS status Unsatisfiable for theBenchmark
% 5.59/1.57 % SZS output start Proof for theBenchmark
% See solution above
% 6.91/1.77 % (731581)------------------------------
% 6.91/1.77 % (731581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.91/1.77 % (731581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.91/1.77 % (731581)CaDiCaL version: 2.1.3
% 6.91/1.77 % (731581)Termination reason: Refutation
% 6.91/1.77 % (731581)Time elapsed: 0.514 s
% 6.91/1.77 % (731581)Peak memory usage: 130 MB
% 6.91/1.77 % (731581)Instructions burned: 1097 (million)
% 6.91/1.77 % (731581)------------------------------
% 6.91/1.77 % (731581)------------------------------
% 6.91/1.77 % (731576)Success in time 0.893 s
% 6.91/1.77 % Vampire exiting
%------------------------------------------------------------------------------