%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV558-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 : n013.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:18:33 PM UTC 2026
% Result : Unsatisfiable 2.82s 1.05s
% Output : Refutation 3.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 32
% Syntax : Number of formulae : 203 ( 56 unt; 10 def)
% Number of atoms : 435 ( 192 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 421 ( 189 ~; 222 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 11 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 22 con; 0-3 aty)
% Number of variables : 27 ( 0 sgn 27 !; 0 ?)
% 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(f6,axiom,
a_17 = store(a1,i1,e_16),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f7,axiom,
a_19 = store(a2,i1,e_18),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp1) ).
fof(f8,axiom,
a_21 = store(a_17,i2,e_20),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp2) ).
fof(f9,axiom,
a_23 = store(a_19,i2,e_22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp3) ).
fof(f10,axiom,
a_25 = store(a_21,i3,e_24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp4) ).
fof(f11,axiom,
a_27 = store(a_23,i3,e_26),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp5) ).
fof(f12,axiom,
a_29 = store(a_25,i4,e_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp6) ).
fof(f13,axiom,
a_31 = store(a_27,i4,e_30),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp7) ).
fof(f14,axiom,
e_16 = select(a2,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp8) ).
fof(f15,axiom,
e_18 = select(a1,i1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp9) ).
fof(f16,axiom,
e_20 = select(a_19,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp10) ).
fof(f17,axiom,
e_22 = select(a_17,i2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp11) ).
fof(f18,axiom,
e_24 = select(a_23,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp12) ).
fof(f19,axiom,
e_26 = select(a_21,i3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp13) ).
fof(f20,axiom,
e_28 = select(a_27,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp14) ).
fof(f21,axiom,
e_30 = select(a_25,i4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp15) ).
fof(f22,axiom,
a_29 = a_31,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp16) ).
fof(f23,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f24,plain,
a2 = store(a2,i1,e_16),
inference(superposition,[],[f3,f14]) ).
fof(f25,plain,
a1 = store(a1,i1,e_18),
inference(superposition,[],[f3,f15]) ).
fof(f26,plain,
a_19 = store(a_19,i2,e_20),
inference(superposition,[],[f3,f16]) ).
fof(f27,plain,
a_17 = store(a_17,i2,e_22),
inference(superposition,[],[f3,f17]) ).
fof(f28,plain,
a_23 = store(a_23,i3,e_24),
inference(superposition,[],[f3,f18]) ).
fof(f29,plain,
a_21 = store(a_21,i3,e_26),
inference(superposition,[],[f3,f19]) ).
fof(f31,plain,
a_25 = store(a_25,i4,e_30),
inference(superposition,[],[f3,f21]) ).
fof(f32,plain,
e_16 = select(a_17,i1),
inference(superposition,[],[f1,f6]) ).
fof(f38,plain,
e_18 = select(a_19,i1),
inference(superposition,[],[f1,f7]) ).
fof(f43,plain,
e_20 = select(a_21,i2),
inference(superposition,[],[f1,f8]) ).
fof(f44,plain,
! [X0] :
( select(a_17,X0) = select(a_21,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f8]) ).
fof(f51,plain,
e_22 = select(a_23,i2),
inference(superposition,[],[f1,f9]) ).
fof(f52,plain,
! [X0] :
( select(a_19,X0) = select(a_23,X0)
| i2 = X0 ),
inference(superposition,[],[f2,f9]) ).
fof(f56,plain,
e_24 = select(a_25,i3),
inference(superposition,[],[f1,f10]) ).
fof(f57,plain,
! [X0] :
( select(a_21,X0) = select(a_25,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f10]) ).
fof(f64,plain,
e_26 = select(a_27,i3),
inference(superposition,[],[f1,f11]) ).
fof(f65,plain,
! [X0] :
( select(a_23,X0) = select(a_27,X0)
| i3 = X0 ),
inference(superposition,[],[f2,f11]) ).
fof(f69,plain,
( e_26 = select(a_17,i3)
| i2 = i3 ),
inference(superposition,[],[f44,f19]) ).
fof(f73,definition,
( spl0_1
<=> i2 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f74,plain,
( i2 = i3
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f73]) ).
fof(f76,definition,
( spl0_2
<=> e_26 = select(a_17,i3) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f77,plain,
( e_26 = select(a_17,i3)
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f76]) ).
fof(f79,plain,
( spl0_1
| spl0_2 ),
inference(avatar_split_clause,[],[f69,f76,f73]) ).
fof(f80,plain,
e_28 = select(a_29,i4),
inference(superposition,[],[f1,f12]) ).
fof(f92,definition,
( spl0_3
<=> e_24 = select(a_19,i3) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f93,plain,
( e_24 = select(a_19,i3)
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f96,plain,
a_29 = store(a_27,i4,e_30),
inference(forward_demodulation,[],[f13,f22]) ).
fof(f99,plain,
( e_24 = select(a_23,i2)
| ~ spl0_1 ),
inference(superposition,[],[f18,f74]) ).
fof(f100,plain,
( e_26 = select(a_21,i2)
| ~ spl0_1 ),
inference(superposition,[],[f19,f74]) ).
fof(f101,plain,
( e_24 = select(a_25,i2)
| ~ spl0_1 ),
inference(superposition,[],[f56,f74]) ).
fof(f102,plain,
( e_26 = select(a_27,i2)
| ~ spl0_1 ),
inference(superposition,[],[f64,f74]) ).
fof(f105,plain,
( e_20 = e_26
| ~ spl0_1 ),
inference(forward_demodulation,[],[f100,f43]) ).
fof(f106,plain,
( e_22 = e_24
| ~ spl0_1 ),
inference(forward_demodulation,[],[f99,f51]) ).
fof(f111,plain,
e_30 = select(a_29,i4),
inference(superposition,[],[f1,f96]) ).
fof(f112,plain,
! [X0] :
( select(a_27,X0) = select(a_29,X0)
| i4 = X0 ),
inference(superposition,[],[f2,f96]) ).
fof(f113,plain,
! [X0] : store(a_29,i4,X0) = store(a_27,i4,X0),
inference(superposition,[],[f4,f96]) ).
fof(f116,plain,
e_28 = e_30,
inference(forward_demodulation,[],[f111,f80]) ).
fof(f125,plain,
( e_22 = select(a_25,i2)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f101,f106]) ).
fof(f143,definition,
( spl0_4
<=> i2 = i4 ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f144,plain,
( i2 = i4
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f143]) ).
fof(f151,plain,
( e_28 = select(a_29,i2)
| ~ spl0_4 ),
inference(superposition,[],[f80,f144]) ).
fof(f154,plain,
( e_28 = select(a_27,i2)
| ~ spl0_4 ),
inference(superposition,[],[f20,f144]) ).
fof(f219,plain,
a_25 = store(a_25,i4,e_28),
inference(forward_demodulation,[],[f31,f116]) ).
fof(f220,plain,
a_25 = a_29,
inference(forward_demodulation,[],[f219,f12]) ).
fof(f271,definition,
( spl0_7
<=> e_16 = e_18 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f272,plain,
( e_16 = e_18
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f286,plain,
( e_24 = select(a_19,i3)
| i2 = i3 ),
inference(superposition,[],[f52,f18]) ).
fof(f289,plain,
( e_20 = select(a_27,i2)
| ~ spl0_1 ),
inference(forward_demodulation,[],[f102,f105]) ).
fof(f294,plain,
( e_28 = select(a_25,i2)
| ~ spl0_4 ),
inference(forward_demodulation,[],[f151,f220]) ).
fof(f295,plain,
( e_22 = e_28
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f294,f125]) ).
fof(f304,plain,
( e_22 = select(a_27,i2)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f154,f295]) ).
fof(f309,plain,
( e_20 = e_22
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f304,f289]) ).
fof(f321,plain,
( a_17 = store(a_17,i2,e_20)
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f27,f309]) ).
fof(f322,plain,
( a_23 = store(a_19,i2,e_20)
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f9,f309]) ).
fof(f323,plain,
( a_19 = a_23
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f322,f26]) ).
fof(f324,plain,
( a_17 = a_21
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f321,f8]) ).
fof(f326,plain,
( a_27 = store(a_19,i3,e_26)
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f11,f323]) ).
fof(f331,plain,
( a_27 = store(a_19,i3,e_20)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f326,f105]) ).
fof(f334,plain,
( a_27 = store(a_19,i2,e_20)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f331,f74]) ).
fof(f336,plain,
( a_19 = a_27
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f334,f26]) ).
fof(f337,plain,
( a_25 = store(a_17,i3,e_24)
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f10,f324]) ).
fof(f342,plain,
( a_25 = store(a_17,i3,e_22)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f337,f106]) ).
fof(f344,plain,
( a_25 = store(a_17,i3,e_20)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f342,f309]) ).
fof(f346,plain,
( store(a_17,i2,e_20) = a_25
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f344,f74]) ).
fof(f347,plain,
( a_21 = a_25
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f346,f8]) ).
fof(f348,plain,
( a_17 = a_25
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f347,f324]) ).
fof(f354,plain,
( a_29 = store(a_19,i4,e_30)
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f96,f336]) ).
fof(f358,plain,
( a_29 = store(a_19,i4,e_28)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f354,f116]) ).
fof(f361,plain,
( a_29 = store(a_19,i4,e_22)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f358,f295]) ).
fof(f364,plain,
( a_29 = store(a_19,i4,e_20)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f361,f309]) ).
fof(f366,plain,
( a_29 = store(a_19,i2,e_20)
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f364,f144]) ).
fof(f367,plain,
( a_19 = a_29
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f366,f26]) ).
fof(f368,plain,
( a_19 = a_25
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f367,f220]) ).
fof(f385,plain,
( a_17 = a_19
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f368,f348]) ).
fof(f393,plain,
( e_18 = select(a_17,i1)
| ~ spl0_1
| ~ spl0_4 ),
inference(superposition,[],[f38,f385]) ).
fof(f396,plain,
( e_16 = e_18
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_demodulation,[],[f393,f32]) ).
fof(f399,plain,
( spl0_7
| ~ spl0_1
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f396,f143,f73,f271]) ).
fof(f401,plain,
! [X0] :
( select(a_25,X0) = select(a_27,X0)
| i4 = X0 ),
inference(forward_demodulation,[],[f112,f220]) ).
fof(f424,plain,
( a1 = store(a1,i1,e_16)
| ~ spl0_7 ),
inference(superposition,[],[f25,f272]) ).
fof(f425,plain,
( a_19 = store(a2,i1,e_16)
| ~ spl0_7 ),
inference(superposition,[],[f7,f272]) ).
fof(f426,plain,
( a_19 = a2
| ~ spl0_7 ),
inference(forward_demodulation,[],[f425,f24]) ).
fof(f427,plain,
( a_17 = a1
| ~ spl0_7 ),
inference(forward_demodulation,[],[f424,f6]) ).
fof(f463,plain,
( a1 != a_19
| ~ spl0_7 ),
inference(superposition,[],[f23,f426]) ).
fof(f470,plain,
( a_17 != a_19
| ~ spl0_7 ),
inference(superposition,[],[f463,f427]) ).
fof(f546,plain,
( $false
| ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(forward_subsumption_resolution,[],[f385,f470]) ).
fof(f547,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(avatar_contradiction_clause,[],[f546]) ).
fof(f549,plain,
( spl0_1
| spl0_3 ),
inference(avatar_split_clause,[],[f286,f92,f73]) ).
fof(f554,definition,
( spl0_9
<=> e_24 = e_26 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f555,plain,
( e_24 = e_26
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f554]) ).
fof(f558,plain,
( e_30 = select(a_21,i4)
| i3 = i4 ),
inference(superposition,[],[f57,f21]) ).
fof(f562,plain,
( e_30 = select(a_21,i2)
| i3 = i4
| ~ spl0_4 ),
inference(forward_demodulation,[],[f558,f144]) ).
fof(f564,plain,
( e_20 = e_30
| i3 = i4
| ~ spl0_4 ),
inference(forward_demodulation,[],[f562,f43]) ).
fof(f566,plain,
( e_20 = e_28
| i3 = i4
| ~ spl0_4 ),
inference(forward_demodulation,[],[f564,f116]) ).
fof(f568,plain,
( i2 = i3
| e_20 = e_28
| ~ spl0_4 ),
inference(forward_demodulation,[],[f566,f144]) ).
fof(f570,definition,
( spl0_10
<=> e_20 = e_28 ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f571,plain,
( e_20 = e_28
| ~ spl0_10 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f573,plain,
( spl0_10
| spl0_1
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f568,f143,f73,f570]) ).
fof(f577,plain,
( a_27 = store(a_23,i3,e_24)
| ~ spl0_9 ),
inference(superposition,[],[f11,f555]) ).
fof(f578,plain,
( a_23 = a_27
| ~ spl0_9 ),
inference(forward_demodulation,[],[f577,f28]) ).
fof(f582,plain,
( e_28 = select(a_23,i4)
| i3 = i4 ),
inference(superposition,[],[f65,f20]) ).
fof(f586,plain,
( e_28 = select(a_23,i2)
| i3 = i4
| ~ spl0_4 ),
inference(forward_demodulation,[],[f582,f144]) ).
fof(f588,plain,
( e_22 = e_28
| i3 = i4
| ~ spl0_4 ),
inference(forward_demodulation,[],[f586,f51]) ).
fof(f590,plain,
( e_20 = e_22
| i3 = i4
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_demodulation,[],[f588,f571]) ).
fof(f592,plain,
( i2 = i3
| e_20 = e_22
| ~ spl0_4
| ~ spl0_10 ),
inference(forward_demodulation,[],[f590,f144]) ).
fof(f594,definition,
( spl0_11
<=> e_20 = e_22 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f595,plain,
( e_20 = e_22
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f597,plain,
( spl0_11
| spl0_1
| ~ spl0_4
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f592,f570,f143,f73,f594]) ).
fof(f598,plain,
( a_17 = store(a_17,i2,e_20)
| ~ spl0_11 ),
inference(superposition,[],[f27,f595]) ).
fof(f599,plain,
( a_23 = store(a_19,i2,e_20)
| ~ spl0_11 ),
inference(superposition,[],[f9,f595]) ).
fof(f600,plain,
( a_19 = a_23
| ~ spl0_11 ),
inference(forward_demodulation,[],[f599,f26]) ).
fof(f601,plain,
( a_17 = a_21
| ~ spl0_11 ),
inference(forward_demodulation,[],[f598,f8]) ).
fof(f602,plain,
( a_21 = store(a_21,i3,e_24)
| ~ spl0_9 ),
inference(forward_demodulation,[],[f29,f555]) ).
fof(f603,plain,
( a_21 = a_25
| ~ spl0_9 ),
inference(forward_demodulation,[],[f602,f10]) ).
fof(f630,plain,
( e_24 = select(a_19,i3)
| ~ spl0_11 ),
inference(superposition,[],[f18,f600]) ).
fof(f634,plain,
( spl0_3
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f630,f594,f92]) ).
fof(f650,plain,
( e_24 = select(a_17,i3)
| ~ spl0_2
| ~ spl0_9 ),
inference(forward_demodulation,[],[f77,f555]) ).
fof(f661,definition,
( spl0_12
<=> e_24 = select(a_17,i3) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f662,plain,
( e_24 = select(a_17,i3)
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f661]) ).
fof(f668,plain,
( spl0_12
| ~ spl0_2
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f650,f554,f76,f661]) ).
fof(f734,definition,
( spl0_13
<=> i1 = i3 ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f735,plain,
( i1 = i3
| ~ spl0_13 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f752,plain,
( ! [X0] :
( select(a_23,X0) = select(a_25,X0)
| i4 = X0 )
| ~ spl0_9 ),
inference(forward_demodulation,[],[f401,f578]) ).
fof(f766,plain,
( ! [X0] :
( select(a_21,X0) = select(a_23,X0)
| i4 = X0 )
| ~ spl0_9 ),
inference(forward_demodulation,[],[f752,f603]) ).
fof(f999,plain,
( e_24 = select(a_19,i1)
| ~ spl0_3
| ~ spl0_13 ),
inference(superposition,[],[f93,f735]) ).
fof(f1000,plain,
( e_24 = select(a_17,i1)
| ~ spl0_12
| ~ spl0_13 ),
inference(superposition,[],[f662,f735]) ).
fof(f1001,plain,
( e_16 = e_24
| ~ spl0_12
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1000,f32]) ).
fof(f1002,plain,
( e_18 = e_24
| ~ spl0_3
| ~ spl0_13 ),
inference(forward_demodulation,[],[f999,f38]) ).
fof(f1018,plain,
( e_16 = e_18
| ~ spl0_3
| ~ spl0_12
| ~ spl0_13 ),
inference(forward_demodulation,[],[f1002,f1001]) ).
fof(f1019,plain,
( spl0_7
| ~ spl0_3
| ~ spl0_12
| ~ spl0_13 ),
inference(avatar_split_clause,[],[f1018,f734,f661,f92,f271]) ).
fof(f1171,plain,
( e_22 = select(a_21,i2)
| i2 = i4
| ~ spl0_9 ),
inference(superposition,[],[f766,f51]) ).
fof(f1181,plain,
( e_20 = e_22
| i2 = i4
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1171,f43]) ).
fof(f1208,plain,
( spl0_4
| spl0_11
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f1181,f554,f594,f143]) ).
fof(f1216,plain,
! [X0] : store(a_25,i4,X0) = store(a_27,i4,X0),
inference(forward_demodulation,[],[f113,f220]) ).
fof(f1486,plain,
a_27 = store(a_25,i4,select(a_27,i4)),
inference(superposition,[],[f3,f1216]) ).
fof(f1487,plain,
a_27 = store(a_25,i4,e_28),
inference(forward_demodulation,[],[f1486,f20]) ).
fof(f1492,plain,
a_27 = a_29,
inference(forward_demodulation,[],[f1487,f12]) ).
fof(f1494,plain,
a_25 = a_27,
inference(forward_demodulation,[],[f1492,f220]) ).
fof(f1564,plain,
e_26 = select(a_25,i3),
inference(superposition,[],[f64,f1494]) ).
fof(f1565,plain,
! [X0] :
( select(a_23,X0) = select(a_25,X0)
| i3 = X0 ),
inference(superposition,[],[f65,f1494]) ).
fof(f1572,plain,
e_24 = e_26,
inference(forward_demodulation,[],[f1564,f56]) ).
fof(f1585,plain,
( ! [X0] :
( select(a_19,X0) = select(a_25,X0)
| i3 = X0 )
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1565,f600]) ).
fof(f1596,plain,
( ! [X0] :
( select(a_19,X0) = select(a_21,X0)
| i3 = X0 )
| ~ spl0_11 ),
inference(backward_subsumption_demodulation,[],[f57,f1585]) ).
fof(f1600,plain,
( ! [X0] :
( select(a_17,X0) = select(a_19,X0)
| i3 = X0 )
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1596,f601]) ).
fof(f1603,plain,
( e_18 = select(a_17,i1)
| i1 = i3
| ~ spl0_11 ),
inference(superposition,[],[f1600,f38]) ).
fof(f1614,plain,
( e_16 = e_18
| i1 = i3
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1603,f32]) ).
fof(f1616,plain,
( spl0_13
| spl0_7
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1614,f594,f271,f734]) ).
fof(f1632,plain,
spl0_9,
inference(avatar_split_clause,[],[f1572,f554]) ).
fof(f1654,plain,
( a_17 = a_25
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f603,f601]) ).
fof(f1660,plain,
( e_24 = select(a_17,i3)
| ~ spl0_9
| ~ spl0_11 ),
inference(superposition,[],[f56,f1654]) ).
fof(f1663,plain,
( spl0_12
| ~ spl0_9
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1660,f594,f554,f661]) ).
fof(f1675,plain,
( a_27 = store(a_23,i3,e_24)
| ~ spl0_9 ),
inference(superposition,[],[f11,f555]) ).
fof(f1676,plain,
( a_23 = a_27
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1675,f28]) ).
fof(f1678,plain,
( a_23 = a_25
| ~ spl0_9 ),
inference(forward_demodulation,[],[f1676,f1494]) ).
fof(f1680,plain,
( a_17 = a_23
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1678,f1654]) ).
fof(f1681,plain,
( a_17 = a_19
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_demodulation,[],[f1680,f600]) ).
fof(f1682,plain,
( $false
| ~ spl0_7
| ~ spl0_9
| ~ spl0_11 ),
inference(forward_subsumption_resolution,[],[f1681,f470]) ).
fof(f1683,plain,
( ~ spl0_7
| ~ spl0_9
| ~ spl0_11 ),
inference(avatar_contradiction_clause,[],[f1682]) ).
cnf(s2,plain,
( spl0_1
| spl0_2 ),
inference(sat_conversion,[],[f79]) ).
cnf(s9,plain,
( ~ spl0_1
| ~ spl0_4
| spl0_7 ),
inference(sat_conversion,[],[f399]) ).
cnf(s15,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_7 ),
inference(sat_conversion,[],[f547]) ).
cnf(s17,plain,
( spl0_1
| spl0_3 ),
inference(sat_conversion,[],[f549]) ).
cnf(s21,plain,
( spl0_1
| ~ spl0_4
| spl0_10 ),
inference(sat_conversion,[],[f573]) ).
cnf(s23,plain,
( spl0_1
| ~ spl0_4
| ~ spl0_10
| spl0_11 ),
inference(sat_conversion,[],[f597]) ).
cnf(s24,plain,
( spl0_3
| ~ spl0_11 ),
inference(sat_conversion,[],[f634]) ).
cnf(s27,plain,
( ~ spl0_2
| ~ spl0_9
| spl0_12 ),
inference(sat_conversion,[],[f668]) ).
cnf(s55,plain,
( ~ spl0_3
| spl0_7
| ~ spl0_12
| ~ spl0_13 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s76,plain,
( spl0_4
| ~ spl0_9
| spl0_11 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s110,plain,
( spl0_7
| ~ spl0_11
| spl0_13 ),
inference(sat_conversion,[],[f1616]) ).
cnf(s116,plain,
spl0_9,
inference(sat_conversion,[],[f1632]) ).
cnf(s123,plain,
( ~ spl0_9
| ~ spl0_11
| spl0_12 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s124,plain,
( ~ spl0_7
| ~ spl0_9
| ~ spl0_11 ),
inference(sat_conversion,[],[f1683]) ).
cnf(s125,plain,
( spl0_4
| spl0_11 ),
inference(rat,[],[s76,s116]) ).
cnf(s147,plain,
( ~ spl0_2
| spl0_12 ),
inference(rat,[],[s27,s116]) ).
cnf(s150,plain,
( ~ spl0_11
| spl0_1 ),
inference(rat,[],[s55,s110,s124,s17,s147,s2,s116]) ).
cnf(s151,plain,
spl0_1,
inference(rat,[],[s23,s21,s125,s150]) ).
cnf(s152,plain,
( ~ spl0_11
| ~ spl0_3 ),
inference(rat,[],[s55,s110,s124,s123,s116]) ).
cnf(s153,plain,
~ spl0_4,
inference(rat,[],[s9,s15,s151]) ).
cnf(s155,plain,
spl0_11,
inference(rat,[],[s125,s153]) ).
cnf(s161,plain,
spl0_3,
inference(rat,[],[s24,s155]) ).
cnf(s166,plain,
$false,
inference(rat,[],[s152,s161,s155]) ).
fof(f1684,plain,
$false,
inference(avatar_sat_refutation,[],[s166]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV558-1.004 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n013.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 11:45:37 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 Running first-order theorem proving
% 0.08/0.20 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
% 2.82/1.05 % (1124103)Input is clausal, will run a generic CNF schedule.
% 2.82/1.05 % (1124112)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2836182416:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.82/1.05 % (1124113)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1959868950:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.82/1.05 % (1124109)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=804342881:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.82/1.05 % (1124114)dis-21_1_sil=8000:lcm=predicate:random_seed=433935688: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)
% 2.82/1.05 % (1124108)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=4127686000:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.82/1.05 % (1124111)lrs+10_1_sil=8000:sp=occurrence:random_seed=2089798257:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.82/1.05 % (1124110)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3088014855:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.82/1.05 % (1124114)Refutation not found, incomplete strategy
% 2.82/1.05 % (1124114)------------------------------
% 2.82/1.05 % (1124114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.05 % (1124114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.05 % (1124114)CaDiCaL version: 2.1.3
% 2.82/1.05 % (1124114)Termination reason: Refutation not found, incomplete strategy
% 2.82/1.05 % (1124114)Time elapsed: 0.001 s
% 2.82/1.05 % (1124114)Peak memory usage: 88 MB
% 2.82/1.05 % (1124114)Instructions burned: 1 (million)
% 2.82/1.05 % (1124112)Instruction limit reached!
% 2.82/1.05 % (1124112)------------------------------
% 2.82/1.05 % (1124112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.05 % (1124112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.05 % (1124112)CaDiCaL version: 2.1.3
% 2.82/1.05 % (1124112)Termination reason: Instruction limit
% 2.82/1.05 % (1124112)Termination phase: Saturation
% 2.82/1.05 % (1124112)Time elapsed: 0.032 s
% 2.82/1.05 % (1124112)Peak memory usage: 88 MB
% 2.82/1.05 % (1124112)Instructions burned: 114 (million)
% 2.82/1.05 % (1124111)Instruction limit reached!
% 2.82/1.05 % (1124111)------------------------------
% 2.82/1.05 % (1124111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.05 % (1124111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.05 % (1124111)CaDiCaL version: 2.1.3
% 2.82/1.05 % (1124111)Termination reason: Instruction limit
% 2.82/1.05 % (1124111)Termination phase: Saturation
% 2.82/1.05 % (1124111)Time elapsed: 0.057 s
% 2.82/1.05 % (1124111)Peak memory usage: 89 MB
% 2.82/1.05 % (1124111)Instructions burned: 108 (million)
% 2.82/1.05 % (1124122)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=3052314719:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 2.82/1.05 % (1124113)Instruction limit reached!
% 2.82/1.05 % (1124113)------------------------------
% 2.82/1.05 % (1124113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.82/1.05 % (1124113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.82/1.05 % (1124113)CaDiCaL version: 2.1.3
% 2.82/1.05 % (1124113)Termination reason: Instruction limit
% 2.82/1.05 % (1124113)Termination phase: Saturation
% 2.82/1.05 % (1124113)Time elapsed: 0.104 s
% 2.82/1.05 % (1124113)Peak memory usage: 89 MB
% 2.82/1.05 % (1124113)Instructions burned: 181 (million)
% 2.82/1.05 % (1124122)First to succeed.
% 2.82/1.05 % (1124122)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1124103"
% 2.82/1.05 % (1124123)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4216542502: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)
% 2.82/1.05 % (1124125)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3042017752:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 2.82/1.05 % (1124114)------------------------------
% 2.82/1.05 % (1124114)------------------------------
% 2.82/1.05 % (1124122)Refutation found. Thanks to Tanya!
% 2.82/1.05 % SZS status Unsatisfiable for theBenchmark
% 2.82/1.05 % SZS output start Proof for theBenchmark
% See solution above
% 3.56/1.25 % (1124122)------------------------------
% 3.56/1.25 % (1124122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.56/1.25 % (1124122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.56/1.25 % (1124122)CaDiCaL version: 2.1.3
% 3.56/1.25 % (1124122)Termination reason: Refutation
% 3.56/1.25 % (1124122)Time elapsed: 0.020 s
% 3.56/1.25 % (1124122)Peak memory usage: 90 MB
% 3.56/1.25 % (1124122)Instructions burned: 57 (million)
% 3.56/1.25 % (1124122)------------------------------
% 3.56/1.25 % (1124122)------------------------------
% 3.56/1.25 % (1124103)Success in time 0.416 s
% 3.56/1.25 % Vampire exiting
%------------------------------------------------------------------------------