%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV557-1.007 : 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:18:32 PM UTC 2026
% Result : Unsatisfiable 5.31s 1.54s
% Output : Refutation 6.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 92
% Syntax : Number of formulae : 331 ( 153 unt; 87 def)
% Number of atoms : 596 ( 223 equ)
% Maximal formula atoms : 44 ( 1 avg)
% Number of connectives : 474 ( 209 ~; 206 |; 0 &)
% ( 59 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 45 ( 2 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of predicates : 61 ( 59 usr; 60 prp; 0-2 aty)
% Number of functors : 39 ( 39 usr; 37 con; 0-3 aty)
% Number of variables : 5 ( 0 sgn 5 !; 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(f6,negated_conjecture,
store(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7)) = store(store(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6)),i7,select(store(store(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5)),i6,select(store(store(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4,select(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4)),i5,select(store(store(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3,select(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3)),i4,select(store(store(store(a2,i1,select(a1,i1)),i2,select(store(a1,i1,select(a2,i1)),i2)),i3,select(store(store(a1,i1,select(a2,i1)),i2,select(store(a2,i1,select(a1,i1)),i2)),i3)),i4)),i5)),i6)),i7)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',hyp0) ).
fof(f7,negated_conjecture,
a1 != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
fof(f8,definition,
sF0 = select(a2,i1),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f9,plain,
select(a2,i1) = sF0,
inference(reorient_equations,[],[f8]) ).
fof(f10,definition,
sF1 = store(a1,i1,sF0),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f11,plain,
store(a1,i1,sF0) = sF1,
inference(reorient_equations,[],[f10]) ).
fof(f12,definition,
sF2 = select(a1,i1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f13,plain,
select(a1,i1) = sF2,
inference(reorient_equations,[],[f12]) ).
fof(f14,definition,
sF3 = store(a2,i1,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f15,plain,
store(a2,i1,sF2) = sF3,
inference(reorient_equations,[],[f14]) ).
fof(f16,definition,
sF4 = select(sF3,i2),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f17,plain,
select(sF3,i2) = sF4,
inference(reorient_equations,[],[f16]) ).
fof(f18,definition,
sF5 = store(sF1,i2,sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f19,plain,
store(sF1,i2,sF4) = sF5,
inference(reorient_equations,[],[f18]) ).
fof(f20,definition,
sF6 = select(sF1,i2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f21,plain,
select(sF1,i2) = sF6,
inference(reorient_equations,[],[f20]) ).
fof(f22,definition,
sF7 = store(sF3,i2,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f23,plain,
store(sF3,i2,sF6) = sF7,
inference(reorient_equations,[],[f22]) ).
fof(f24,definition,
sF8 = select(sF7,i3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f25,plain,
select(sF7,i3) = sF8,
inference(reorient_equations,[],[f24]) ).
fof(f26,definition,
sF9 = store(sF5,i3,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f27,plain,
store(sF5,i3,sF8) = sF9,
inference(reorient_equations,[],[f26]) ).
fof(f28,definition,
sF10 = select(sF5,i3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f29,plain,
select(sF5,i3) = sF10,
inference(reorient_equations,[],[f28]) ).
fof(f30,definition,
sF11 = store(sF7,i3,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f31,plain,
store(sF7,i3,sF10) = sF11,
inference(reorient_equations,[],[f30]) ).
fof(f32,definition,
sF12 = select(sF11,i4),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f33,plain,
select(sF11,i4) = sF12,
inference(reorient_equations,[],[f32]) ).
fof(f34,definition,
sF13 = store(sF9,i4,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f35,plain,
store(sF9,i4,sF12) = sF13,
inference(reorient_equations,[],[f34]) ).
fof(f36,definition,
sF14 = select(sF9,i4),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f37,plain,
select(sF9,i4) = sF14,
inference(reorient_equations,[],[f36]) ).
fof(f38,definition,
sF15 = store(sF11,i4,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f39,plain,
store(sF11,i4,sF14) = sF15,
inference(reorient_equations,[],[f38]) ).
fof(f40,definition,
sF16 = select(sF15,i5),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f41,plain,
select(sF15,i5) = sF16,
inference(reorient_equations,[],[f40]) ).
fof(f42,definition,
sF17 = store(sF13,i5,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f43,plain,
store(sF13,i5,sF16) = sF17,
inference(reorient_equations,[],[f42]) ).
fof(f44,definition,
sF18 = select(sF13,i5),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f45,plain,
select(sF13,i5) = sF18,
inference(reorient_equations,[],[f44]) ).
fof(f46,definition,
sF19 = store(sF15,i5,sF18),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f47,plain,
store(sF15,i5,sF18) = sF19,
inference(reorient_equations,[],[f46]) ).
fof(f48,definition,
sF20 = select(sF19,i6),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f49,plain,
select(sF19,i6) = sF20,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF21 = store(sF17,i6,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f51,plain,
store(sF17,i6,sF20) = sF21,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF22 = select(sF17,i6),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f53,plain,
select(sF17,i6) = sF22,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF23 = store(sF19,i6,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f55,plain,
store(sF19,i6,sF22) = sF23,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF24 = select(sF23,i7),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f57,plain,
select(sF23,i7) = sF24,
inference(reorient_equations,[],[f56]) ).
fof(f58,definition,
sF25 = store(sF21,i7,sF24),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f59,plain,
store(sF21,i7,sF24) = sF25,
inference(reorient_equations,[],[f58]) ).
fof(f60,definition,
sF26 = select(sF21,i7),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f61,plain,
select(sF21,i7) = sF26,
inference(reorient_equations,[],[f60]) ).
fof(f62,definition,
sF27 = store(sF23,i7,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f63,plain,
store(sF23,i7,sF26) = sF27,
inference(reorient_equations,[],[f62]) ).
fof(f64,plain,
sF25 = sF27,
inference(definition_folding,[],[f6,f63,f61,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f59,f57,f55,f53,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f51,f49,f47,f45,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f43,f41,f39,f37,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f35,f33,f31,f29,f19,f17,f15,f13,f11,f9,f23,f21,f11,f9,f15,f13,f27,f25,f23,f21,f11,f9,f15,f13,f19,f17,f15,f13,f11,f9]) ).
fof(f66,definition,
( spl28_1
<=> a1 = a2 ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
fof(f69,plain,
~ spl28_1,
inference(avatar_split_clause,[],[f7,f66]) ).
fof(f71,definition,
( spl28_2
<=> sF25 = sF27 ),
introduced(definition,[new_symbols(definition,[spl28_2])],[avatar_definition]) ).
fof(f73,plain,
( sF25 = sF27
| ~ spl28_2 ),
inference(avatar_component_clause,[],[f71]) ).
fof(f74,plain,
spl28_2,
inference(avatar_split_clause,[],[f64,f71]) ).
fof(f76,definition,
( spl28_3
<=> select(a2,i1) = sF0 ),
introduced(definition,[new_symbols(definition,[spl28_3])],[avatar_definition]) ).
fof(f78,plain,
( select(a2,i1) = sF0
| ~ spl28_3 ),
inference(avatar_component_clause,[],[f76]) ).
fof(f79,plain,
spl28_3,
inference(avatar_split_clause,[],[f9,f76]) ).
fof(f81,definition,
( spl28_4
<=> store(a1,i1,sF0) = sF1 ),
introduced(definition,[new_symbols(definition,[spl28_4])],[avatar_definition]) ).
fof(f83,plain,
( store(a1,i1,sF0) = sF1
| ~ spl28_4 ),
inference(avatar_component_clause,[],[f81]) ).
fof(f84,plain,
spl28_4,
inference(avatar_split_clause,[],[f11,f81]) ).
fof(f86,definition,
( spl28_5
<=> select(a1,i1) = sF2 ),
introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition]) ).
fof(f88,plain,
( select(a1,i1) = sF2
| ~ spl28_5 ),
inference(avatar_component_clause,[],[f86]) ).
fof(f89,plain,
spl28_5,
inference(avatar_split_clause,[],[f13,f86]) ).
fof(f91,definition,
( spl28_6
<=> store(a2,i1,sF2) = sF3 ),
introduced(definition,[new_symbols(definition,[spl28_6])],[avatar_definition]) ).
fof(f93,plain,
( store(a2,i1,sF2) = sF3
| ~ spl28_6 ),
inference(avatar_component_clause,[],[f91]) ).
fof(f94,plain,
spl28_6,
inference(avatar_split_clause,[],[f15,f91]) ).
fof(f96,definition,
( spl28_7
<=> select(sF3,i2) = sF4 ),
introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition]) ).
fof(f98,plain,
( select(sF3,i2) = sF4
| ~ spl28_7 ),
inference(avatar_component_clause,[],[f96]) ).
fof(f99,plain,
spl28_7,
inference(avatar_split_clause,[],[f17,f96]) ).
fof(f101,definition,
( spl28_8
<=> store(sF1,i2,sF4) = sF5 ),
introduced(definition,[new_symbols(definition,[spl28_8])],[avatar_definition]) ).
fof(f103,plain,
( store(sF1,i2,sF4) = sF5
| ~ spl28_8 ),
inference(avatar_component_clause,[],[f101]) ).
fof(f104,plain,
spl28_8,
inference(avatar_split_clause,[],[f19,f101]) ).
fof(f106,definition,
( spl28_9
<=> select(sF1,i2) = sF6 ),
introduced(definition,[new_symbols(definition,[spl28_9])],[avatar_definition]) ).
fof(f108,plain,
( select(sF1,i2) = sF6
| ~ spl28_9 ),
inference(avatar_component_clause,[],[f106]) ).
fof(f109,plain,
spl28_9,
inference(avatar_split_clause,[],[f21,f106]) ).
fof(f111,definition,
( spl28_10
<=> store(sF3,i2,sF6) = sF7 ),
introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition]) ).
fof(f113,plain,
( store(sF3,i2,sF6) = sF7
| ~ spl28_10 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
spl28_10,
inference(avatar_split_clause,[],[f23,f111]) ).
fof(f116,definition,
( spl28_11
<=> select(sF7,i3) = sF8 ),
introduced(definition,[new_symbols(definition,[spl28_11])],[avatar_definition]) ).
fof(f118,plain,
( select(sF7,i3) = sF8
| ~ spl28_11 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f119,plain,
spl28_11,
inference(avatar_split_clause,[],[f25,f116]) ).
fof(f121,definition,
( spl28_12
<=> store(sF5,i3,sF8) = sF9 ),
introduced(definition,[new_symbols(definition,[spl28_12])],[avatar_definition]) ).
fof(f123,plain,
( store(sF5,i3,sF8) = sF9
| ~ spl28_12 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f124,plain,
spl28_12,
inference(avatar_split_clause,[],[f27,f121]) ).
fof(f126,definition,
( spl28_13
<=> select(sF5,i3) = sF10 ),
introduced(definition,[new_symbols(definition,[spl28_13])],[avatar_definition]) ).
fof(f128,plain,
( select(sF5,i3) = sF10
| ~ spl28_13 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f129,plain,
spl28_13,
inference(avatar_split_clause,[],[f29,f126]) ).
fof(f131,definition,
( spl28_14
<=> store(sF7,i3,sF10) = sF11 ),
introduced(definition,[new_symbols(definition,[spl28_14])],[avatar_definition]) ).
fof(f133,plain,
( store(sF7,i3,sF10) = sF11
| ~ spl28_14 ),
inference(avatar_component_clause,[],[f131]) ).
fof(f134,plain,
spl28_14,
inference(avatar_split_clause,[],[f31,f131]) ).
fof(f136,definition,
( spl28_15
<=> select(sF11,i4) = sF12 ),
introduced(definition,[new_symbols(definition,[spl28_15])],[avatar_definition]) ).
fof(f138,plain,
( select(sF11,i4) = sF12
| ~ spl28_15 ),
inference(avatar_component_clause,[],[f136]) ).
fof(f139,plain,
spl28_15,
inference(avatar_split_clause,[],[f33,f136]) ).
fof(f141,definition,
( spl28_16
<=> store(sF9,i4,sF12) = sF13 ),
introduced(definition,[new_symbols(definition,[spl28_16])],[avatar_definition]) ).
fof(f143,plain,
( store(sF9,i4,sF12) = sF13
| ~ spl28_16 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f144,plain,
spl28_16,
inference(avatar_split_clause,[],[f35,f141]) ).
fof(f146,definition,
( spl28_17
<=> select(sF9,i4) = sF14 ),
introduced(definition,[new_symbols(definition,[spl28_17])],[avatar_definition]) ).
fof(f148,plain,
( select(sF9,i4) = sF14
| ~ spl28_17 ),
inference(avatar_component_clause,[],[f146]) ).
fof(f149,plain,
spl28_17,
inference(avatar_split_clause,[],[f37,f146]) ).
fof(f151,definition,
( spl28_18
<=> store(sF11,i4,sF14) = sF15 ),
introduced(definition,[new_symbols(definition,[spl28_18])],[avatar_definition]) ).
fof(f153,plain,
( store(sF11,i4,sF14) = sF15
| ~ spl28_18 ),
inference(avatar_component_clause,[],[f151]) ).
fof(f154,plain,
spl28_18,
inference(avatar_split_clause,[],[f39,f151]) ).
fof(f156,definition,
( spl28_19
<=> select(sF15,i5) = sF16 ),
introduced(definition,[new_symbols(definition,[spl28_19])],[avatar_definition]) ).
fof(f158,plain,
( select(sF15,i5) = sF16
| ~ spl28_19 ),
inference(avatar_component_clause,[],[f156]) ).
fof(f159,plain,
spl28_19,
inference(avatar_split_clause,[],[f41,f156]) ).
fof(f161,definition,
( spl28_20
<=> store(sF13,i5,sF16) = sF17 ),
introduced(definition,[new_symbols(definition,[spl28_20])],[avatar_definition]) ).
fof(f163,plain,
( store(sF13,i5,sF16) = sF17
| ~ spl28_20 ),
inference(avatar_component_clause,[],[f161]) ).
fof(f164,plain,
spl28_20,
inference(avatar_split_clause,[],[f43,f161]) ).
fof(f166,definition,
( spl28_21
<=> select(sF13,i5) = sF18 ),
introduced(definition,[new_symbols(definition,[spl28_21])],[avatar_definition]) ).
fof(f168,plain,
( select(sF13,i5) = sF18
| ~ spl28_21 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,plain,
spl28_21,
inference(avatar_split_clause,[],[f45,f166]) ).
fof(f171,definition,
( spl28_22
<=> store(sF15,i5,sF18) = sF19 ),
introduced(definition,[new_symbols(definition,[spl28_22])],[avatar_definition]) ).
fof(f173,plain,
( store(sF15,i5,sF18) = sF19
| ~ spl28_22 ),
inference(avatar_component_clause,[],[f171]) ).
fof(f174,plain,
spl28_22,
inference(avatar_split_clause,[],[f47,f171]) ).
fof(f176,definition,
( spl28_23
<=> select(sF19,i6) = sF20 ),
introduced(definition,[new_symbols(definition,[spl28_23])],[avatar_definition]) ).
fof(f178,plain,
( select(sF19,i6) = sF20
| ~ spl28_23 ),
inference(avatar_component_clause,[],[f176]) ).
fof(f179,plain,
spl28_23,
inference(avatar_split_clause,[],[f49,f176]) ).
fof(f181,definition,
( spl28_24
<=> store(sF17,i6,sF20) = sF21 ),
introduced(definition,[new_symbols(definition,[spl28_24])],[avatar_definition]) ).
fof(f183,plain,
( store(sF17,i6,sF20) = sF21
| ~ spl28_24 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f184,plain,
spl28_24,
inference(avatar_split_clause,[],[f51,f181]) ).
fof(f186,definition,
( spl28_25
<=> select(sF17,i6) = sF22 ),
introduced(definition,[new_symbols(definition,[spl28_25])],[avatar_definition]) ).
fof(f188,plain,
( select(sF17,i6) = sF22
| ~ spl28_25 ),
inference(avatar_component_clause,[],[f186]) ).
fof(f189,plain,
spl28_25,
inference(avatar_split_clause,[],[f53,f186]) ).
fof(f191,definition,
( spl28_26
<=> store(sF19,i6,sF22) = sF23 ),
introduced(definition,[new_symbols(definition,[spl28_26])],[avatar_definition]) ).
fof(f193,plain,
( store(sF19,i6,sF22) = sF23
| ~ spl28_26 ),
inference(avatar_component_clause,[],[f191]) ).
fof(f194,plain,
spl28_26,
inference(avatar_split_clause,[],[f55,f191]) ).
fof(f196,definition,
( spl28_27
<=> select(sF23,i7) = sF24 ),
introduced(definition,[new_symbols(definition,[spl28_27])],[avatar_definition]) ).
fof(f198,plain,
( select(sF23,i7) = sF24
| ~ spl28_27 ),
inference(avatar_component_clause,[],[f196]) ).
fof(f199,plain,
spl28_27,
inference(avatar_split_clause,[],[f57,f196]) ).
fof(f201,definition,
( spl28_28
<=> store(sF21,i7,sF24) = sF25 ),
introduced(definition,[new_symbols(definition,[spl28_28])],[avatar_definition]) ).
fof(f203,plain,
( store(sF21,i7,sF24) = sF25
| ~ spl28_28 ),
inference(avatar_component_clause,[],[f201]) ).
fof(f204,plain,
spl28_28,
inference(avatar_split_clause,[],[f59,f201]) ).
fof(f206,definition,
( spl28_29
<=> select(sF21,i7) = sF26 ),
introduced(definition,[new_symbols(definition,[spl28_29])],[avatar_definition]) ).
fof(f208,plain,
( select(sF21,i7) = sF26
| ~ spl28_29 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f209,plain,
spl28_29,
inference(avatar_split_clause,[],[f61,f206]) ).
fof(f211,definition,
( spl28_30
<=> store(sF23,i7,sF26) = sF27 ),
introduced(definition,[new_symbols(definition,[spl28_30])],[avatar_definition]) ).
fof(f213,plain,
( store(sF23,i7,sF26) = sF27
| ~ spl28_30 ),
inference(avatar_component_clause,[],[f211]) ).
fof(f214,plain,
spl28_30,
inference(avatar_split_clause,[],[f63,f211]) ).
fof(f215,plain,
( sF25 = store(sF23,i7,sF26)
| ~ spl28_2
| ~ spl28_30 ),
inference(forward_demodulation,[],[f213,f73]) ).
fof(f217,definition,
( spl28_31
<=> sF25 = store(sF23,i7,sF26) ),
introduced(definition,[new_symbols(definition,[spl28_31])],[avatar_definition]) ).
fof(f219,plain,
( sF25 = store(sF23,i7,sF26)
| ~ spl28_31 ),
inference(avatar_component_clause,[],[f217]) ).
fof(f220,plain,
( spl28_31
| ~ spl28_2
| ~ spl28_30 ),
inference(avatar_split_clause,[],[f215,f211,f71,f217]) ).
fof(f221,plain,
( sF0 = select(sF1,i1)
| ~ spl28_4 ),
inference(superposition,[],[f1,f83]) ).
fof(f222,plain,
( sF2 = select(sF3,i1)
| ~ spl28_6 ),
inference(superposition,[],[f1,f93]) ).
fof(f223,plain,
( sF4 = select(sF5,i2)
| ~ spl28_8 ),
inference(superposition,[],[f1,f103]) ).
fof(f224,plain,
( sF6 = select(sF7,i2)
| ~ spl28_10 ),
inference(superposition,[],[f1,f113]) ).
fof(f225,plain,
( sF8 = select(sF9,i3)
| ~ spl28_12 ),
inference(superposition,[],[f1,f123]) ).
fof(f226,plain,
( sF10 = select(sF11,i3)
| ~ spl28_14 ),
inference(superposition,[],[f1,f133]) ).
fof(f227,plain,
( sF12 = select(sF13,i4)
| ~ spl28_16 ),
inference(superposition,[],[f1,f143]) ).
fof(f228,plain,
( sF14 = select(sF15,i4)
| ~ spl28_18 ),
inference(superposition,[],[f1,f153]) ).
fof(f229,plain,
( sF16 = select(sF17,i5)
| ~ spl28_20 ),
inference(superposition,[],[f1,f163]) ).
fof(f230,plain,
( sF18 = select(sF19,i5)
| ~ spl28_22 ),
inference(superposition,[],[f1,f173]) ).
fof(f231,plain,
( sF20 = select(sF21,i6)
| ~ spl28_24 ),
inference(superposition,[],[f1,f183]) ).
fof(f232,plain,
( sF22 = select(sF23,i6)
| ~ spl28_26 ),
inference(superposition,[],[f1,f193]) ).
fof(f233,plain,
( sF24 = select(sF25,i7)
| ~ spl28_28 ),
inference(superposition,[],[f1,f203]) ).
fof(f234,plain,
( sF26 = select(sF25,i7)
| ~ spl28_31 ),
inference(superposition,[],[f1,f219]) ).
fof(f236,definition,
( spl28_32
<=> sF26 = select(sF25,i7) ),
introduced(definition,[new_symbols(definition,[spl28_32])],[avatar_definition]) ).
fof(f239,plain,
( spl28_32
| ~ spl28_31 ),
inference(avatar_split_clause,[],[f234,f217,f236]) ).
fof(f241,definition,
( spl28_33
<=> sF24 = select(sF25,i7) ),
introduced(definition,[new_symbols(definition,[spl28_33])],[avatar_definition]) ).
fof(f244,plain,
( spl28_33
| ~ spl28_28 ),
inference(avatar_split_clause,[],[f233,f201,f241]) ).
fof(f246,definition,
( spl28_34
<=> sF22 = select(sF23,i6) ),
introduced(definition,[new_symbols(definition,[spl28_34])],[avatar_definition]) ).
fof(f249,plain,
( spl28_34
| ~ spl28_26 ),
inference(avatar_split_clause,[],[f232,f191,f246]) ).
fof(f251,definition,
( spl28_35
<=> sF20 = select(sF21,i6) ),
introduced(definition,[new_symbols(definition,[spl28_35])],[avatar_definition]) ).
fof(f254,plain,
( spl28_35
| ~ spl28_24 ),
inference(avatar_split_clause,[],[f231,f181,f251]) ).
fof(f256,definition,
( spl28_36
<=> sF18 = select(sF19,i5) ),
introduced(definition,[new_symbols(definition,[spl28_36])],[avatar_definition]) ).
fof(f259,plain,
( spl28_36
| ~ spl28_22 ),
inference(avatar_split_clause,[],[f230,f171,f256]) ).
fof(f261,definition,
( spl28_37
<=> sF16 = select(sF17,i5) ),
introduced(definition,[new_symbols(definition,[spl28_37])],[avatar_definition]) ).
fof(f264,plain,
( spl28_37
| ~ spl28_20 ),
inference(avatar_split_clause,[],[f229,f161,f261]) ).
fof(f266,definition,
( spl28_38
<=> sF14 = select(sF15,i4) ),
introduced(definition,[new_symbols(definition,[spl28_38])],[avatar_definition]) ).
fof(f269,plain,
( spl28_38
| ~ spl28_18 ),
inference(avatar_split_clause,[],[f228,f151,f266]) ).
fof(f271,definition,
( spl28_39
<=> sF12 = select(sF13,i4) ),
introduced(definition,[new_symbols(definition,[spl28_39])],[avatar_definition]) ).
fof(f274,plain,
( spl28_39
| ~ spl28_16 ),
inference(avatar_split_clause,[],[f227,f141,f271]) ).
fof(f276,definition,
( spl28_40
<=> sF10 = select(sF11,i3) ),
introduced(definition,[new_symbols(definition,[spl28_40])],[avatar_definition]) ).
fof(f279,plain,
( spl28_40
| ~ spl28_14 ),
inference(avatar_split_clause,[],[f226,f131,f276]) ).
fof(f281,definition,
( spl28_41
<=> sF8 = select(sF9,i3) ),
introduced(definition,[new_symbols(definition,[spl28_41])],[avatar_definition]) ).
fof(f284,plain,
( spl28_41
| ~ spl28_12 ),
inference(avatar_split_clause,[],[f225,f121,f281]) ).
fof(f286,definition,
( spl28_42
<=> sF6 = select(sF7,i2) ),
introduced(definition,[new_symbols(definition,[spl28_42])],[avatar_definition]) ).
fof(f289,plain,
( spl28_42
| ~ spl28_10 ),
inference(avatar_split_clause,[],[f224,f111,f286]) ).
fof(f291,definition,
( spl28_43
<=> sF4 = select(sF5,i2) ),
introduced(definition,[new_symbols(definition,[spl28_43])],[avatar_definition]) ).
fof(f294,plain,
( spl28_43
| ~ spl28_8 ),
inference(avatar_split_clause,[],[f223,f101,f291]) ).
fof(f296,definition,
( spl28_44
<=> sF2 = select(sF3,i1) ),
introduced(definition,[new_symbols(definition,[spl28_44])],[avatar_definition]) ).
fof(f299,plain,
( spl28_44
| ~ spl28_6 ),
inference(avatar_split_clause,[],[f222,f91,f296]) ).
fof(f301,definition,
( spl28_45
<=> sF0 = select(sF1,i1) ),
introduced(definition,[new_symbols(definition,[spl28_45])],[avatar_definition]) ).
fof(f304,plain,
( spl28_45
| ~ spl28_4 ),
inference(avatar_split_clause,[],[f221,f81,f301]) ).
fof(f306,plain,
( a2 = store(a2,i1,sF0)
| ~ spl28_3 ),
inference(superposition,[],[f3,f78]) ).
fof(f307,plain,
( a1 = store(a1,i1,sF2)
| ~ spl28_5 ),
inference(superposition,[],[f3,f88]) ).
fof(f308,plain,
( sF3 = store(sF3,i2,sF4)
| ~ spl28_7 ),
inference(superposition,[],[f3,f98]) ).
fof(f309,plain,
( sF1 = store(sF1,i2,sF6)
| ~ spl28_9 ),
inference(superposition,[],[f3,f108]) ).
fof(f310,plain,
( sF7 = store(sF7,i3,sF8)
| ~ spl28_11 ),
inference(superposition,[],[f3,f118]) ).
fof(f311,plain,
( sF5 = store(sF5,i3,sF10)
| ~ spl28_13 ),
inference(superposition,[],[f3,f128]) ).
fof(f312,plain,
( sF11 = store(sF11,i4,sF12)
| ~ spl28_15 ),
inference(superposition,[],[f3,f138]) ).
fof(f313,plain,
( sF9 = store(sF9,i4,sF14)
| ~ spl28_17 ),
inference(superposition,[],[f3,f148]) ).
fof(f314,plain,
( sF15 = store(sF15,i5,sF16)
| ~ spl28_19 ),
inference(superposition,[],[f3,f158]) ).
fof(f315,plain,
( sF13 = store(sF13,i5,sF18)
| ~ spl28_21 ),
inference(superposition,[],[f3,f168]) ).
fof(f316,plain,
( sF19 = store(sF19,i6,sF20)
| ~ spl28_23 ),
inference(superposition,[],[f3,f178]) ).
fof(f317,plain,
( sF17 = store(sF17,i6,sF22)
| ~ spl28_25 ),
inference(superposition,[],[f3,f188]) ).
fof(f318,plain,
( sF23 = store(sF23,i7,sF24)
| ~ spl28_27 ),
inference(superposition,[],[f3,f198]) ).
fof(f319,plain,
( sF21 = store(sF21,i7,sF26)
| ~ spl28_29 ),
inference(superposition,[],[f3,f208]) ).
fof(f321,definition,
( spl28_46
<=> sF21 = store(sF21,i7,sF26) ),
introduced(definition,[new_symbols(definition,[spl28_46])],[avatar_definition]) ).
fof(f324,plain,
( spl28_46
| ~ spl28_29 ),
inference(avatar_split_clause,[],[f319,f206,f321]) ).
fof(f326,definition,
( spl28_47
<=> sF23 = store(sF23,i7,sF24) ),
introduced(definition,[new_symbols(definition,[spl28_47])],[avatar_definition]) ).
fof(f329,plain,
( spl28_47
| ~ spl28_27 ),
inference(avatar_split_clause,[],[f318,f196,f326]) ).
fof(f331,definition,
( spl28_48
<=> sF17 = store(sF17,i6,sF22) ),
introduced(definition,[new_symbols(definition,[spl28_48])],[avatar_definition]) ).
fof(f334,plain,
( spl28_48
| ~ spl28_25 ),
inference(avatar_split_clause,[],[f317,f186,f331]) ).
fof(f336,definition,
( spl28_49
<=> sF19 = store(sF19,i6,sF20) ),
introduced(definition,[new_symbols(definition,[spl28_49])],[avatar_definition]) ).
fof(f339,plain,
( spl28_49
| ~ spl28_23 ),
inference(avatar_split_clause,[],[f316,f176,f336]) ).
fof(f341,definition,
( spl28_50
<=> sF13 = store(sF13,i5,sF18) ),
introduced(definition,[new_symbols(definition,[spl28_50])],[avatar_definition]) ).
fof(f344,plain,
( spl28_50
| ~ spl28_21 ),
inference(avatar_split_clause,[],[f315,f166,f341]) ).
fof(f346,definition,
( spl28_51
<=> sF15 = store(sF15,i5,sF16) ),
introduced(definition,[new_symbols(definition,[spl28_51])],[avatar_definition]) ).
fof(f349,plain,
( spl28_51
| ~ spl28_19 ),
inference(avatar_split_clause,[],[f314,f156,f346]) ).
fof(f351,definition,
( spl28_52
<=> sF9 = store(sF9,i4,sF14) ),
introduced(definition,[new_symbols(definition,[spl28_52])],[avatar_definition]) ).
fof(f354,plain,
( spl28_52
| ~ spl28_17 ),
inference(avatar_split_clause,[],[f313,f146,f351]) ).
fof(f356,definition,
( spl28_53
<=> sF11 = store(sF11,i4,sF12) ),
introduced(definition,[new_symbols(definition,[spl28_53])],[avatar_definition]) ).
fof(f359,plain,
( spl28_53
| ~ spl28_15 ),
inference(avatar_split_clause,[],[f312,f136,f356]) ).
fof(f361,definition,
( spl28_54
<=> sF5 = store(sF5,i3,sF10) ),
introduced(definition,[new_symbols(definition,[spl28_54])],[avatar_definition]) ).
fof(f364,plain,
( spl28_54
| ~ spl28_13 ),
inference(avatar_split_clause,[],[f311,f126,f361]) ).
fof(f366,definition,
( spl28_55
<=> sF7 = store(sF7,i3,sF8) ),
introduced(definition,[new_symbols(definition,[spl28_55])],[avatar_definition]) ).
fof(f369,plain,
( spl28_55
| ~ spl28_11 ),
inference(avatar_split_clause,[],[f310,f116,f366]) ).
fof(f371,definition,
( spl28_56
<=> sF1 = store(sF1,i2,sF6) ),
introduced(definition,[new_symbols(definition,[spl28_56])],[avatar_definition]) ).
fof(f374,plain,
( spl28_56
| ~ spl28_9 ),
inference(avatar_split_clause,[],[f309,f106,f371]) ).
fof(f376,definition,
( spl28_57
<=> sF3 = store(sF3,i2,sF4) ),
introduced(definition,[new_symbols(definition,[spl28_57])],[avatar_definition]) ).
fof(f379,plain,
( spl28_57
| ~ spl28_7 ),
inference(avatar_split_clause,[],[f308,f96,f376]) ).
fof(f381,definition,
( spl28_58
<=> a1 = store(a1,i1,sF2) ),
introduced(definition,[new_symbols(definition,[spl28_58])],[avatar_definition]) ).
fof(f384,plain,
( spl28_58
| ~ spl28_5 ),
inference(avatar_split_clause,[],[f307,f86,f381]) ).
fof(f386,definition,
( spl28_59
<=> a2 = store(a2,i1,sF0) ),
introduced(definition,[new_symbols(definition,[spl28_59])],[avatar_definition]) ).
fof(f389,plain,
( spl28_59
| ~ spl28_3 ),
inference(avatar_split_clause,[],[f306,f76,f386]) ).
fof(f390,plain,
( sF24 != select(sF25,i7)
| sF26 != select(sF25,i7)
| sF20 != select(sF21,i6)
| sF22 != select(sF23,i6)
| sF16 != select(sF17,i5)
| sF18 != select(sF19,i5)
| sF12 != select(sF13,i4)
| sF14 != select(sF15,i4)
| sF8 != select(sF9,i3)
| sF10 != select(sF11,i3)
| sF4 != select(sF5,i2)
| sF6 != select(sF7,i2)
| sF0 != select(sF1,i1)
| sF2 != select(sF3,i1)
| a1 != store(a1,i1,sF2)
| a2 != store(a2,i1,sF0)
| store(a1,i1,sF0) != sF1
| sF1 != store(sF1,i2,sF6)
| store(a2,i1,sF2) != sF3
| sF3 != store(sF3,i2,sF4)
| store(sF1,i2,sF4) != sF5
| sF5 != store(sF5,i3,sF10)
| store(sF3,i2,sF6) != sF7
| sF7 != store(sF7,i3,sF8)
| store(sF5,i3,sF8) != sF9
| sF9 != store(sF9,i4,sF14)
| store(sF7,i3,sF10) != sF11
| sF11 != store(sF11,i4,sF12)
| store(sF9,i4,sF12) != sF13
| sF13 != store(sF13,i5,sF18)
| store(sF11,i4,sF14) != sF15
| sF15 != store(sF15,i5,sF16)
| store(sF13,i5,sF16) != sF17
| sF17 != store(sF17,i6,sF22)
| store(sF15,i5,sF18) != sF19
| sF19 != store(sF19,i6,sF20)
| store(sF17,i6,sF20) != sF21
| sF21 != store(sF21,i7,sF26)
| store(sF19,i6,sF22) != sF23
| sF23 != store(sF23,i7,sF24)
| store(sF21,i7,sF24) != sF25
| sF25 != sF27
| store(sF23,i7,sF26) != sF27
| a1 = a2 ),
introduced(definition,[],[theory_tautology_sat_conflict]) ).
cnf(s1,plain,
~ spl28_1,
inference(sat_conversion,[],[f69]) ).
cnf(s2,plain,
spl28_2,
inference(sat_conversion,[],[f74]) ).
cnf(s3,plain,
spl28_3,
inference(sat_conversion,[],[f79]) ).
cnf(s4,plain,
spl28_4,
inference(sat_conversion,[],[f84]) ).
cnf(s5,plain,
spl28_5,
inference(sat_conversion,[],[f89]) ).
cnf(s6,plain,
spl28_6,
inference(sat_conversion,[],[f94]) ).
cnf(s7,plain,
spl28_7,
inference(sat_conversion,[],[f99]) ).
cnf(s8,plain,
spl28_8,
inference(sat_conversion,[],[f104]) ).
cnf(s9,plain,
spl28_9,
inference(sat_conversion,[],[f109]) ).
cnf(s10,plain,
spl28_10,
inference(sat_conversion,[],[f114]) ).
cnf(s11,plain,
spl28_11,
inference(sat_conversion,[],[f119]) ).
cnf(s12,plain,
spl28_12,
inference(sat_conversion,[],[f124]) ).
cnf(s13,plain,
spl28_13,
inference(sat_conversion,[],[f129]) ).
cnf(s14,plain,
spl28_14,
inference(sat_conversion,[],[f134]) ).
cnf(s15,plain,
spl28_15,
inference(sat_conversion,[],[f139]) ).
cnf(s16,plain,
spl28_16,
inference(sat_conversion,[],[f144]) ).
cnf(s17,plain,
spl28_17,
inference(sat_conversion,[],[f149]) ).
cnf(s18,plain,
spl28_18,
inference(sat_conversion,[],[f154]) ).
cnf(s19,plain,
spl28_19,
inference(sat_conversion,[],[f159]) ).
cnf(s20,plain,
spl28_20,
inference(sat_conversion,[],[f164]) ).
cnf(s21,plain,
spl28_21,
inference(sat_conversion,[],[f169]) ).
cnf(s22,plain,
spl28_22,
inference(sat_conversion,[],[f174]) ).
cnf(s23,plain,
spl28_23,
inference(sat_conversion,[],[f179]) ).
cnf(s24,plain,
spl28_24,
inference(sat_conversion,[],[f184]) ).
cnf(s25,plain,
spl28_25,
inference(sat_conversion,[],[f189]) ).
cnf(s26,plain,
spl28_26,
inference(sat_conversion,[],[f194]) ).
cnf(s27,plain,
spl28_27,
inference(sat_conversion,[],[f199]) ).
cnf(s28,plain,
spl28_28,
inference(sat_conversion,[],[f204]) ).
cnf(s29,plain,
spl28_29,
inference(sat_conversion,[],[f209]) ).
cnf(s30,plain,
spl28_30,
inference(sat_conversion,[],[f214]) ).
cnf(s31,plain,
( ~ spl28_2
| ~ spl28_30
| spl28_31 ),
inference(sat_conversion,[],[f220]) ).
cnf(s32,plain,
( ~ spl28_31
| spl28_32 ),
inference(sat_conversion,[],[f239]) ).
cnf(s33,plain,
( ~ spl28_28
| spl28_33 ),
inference(sat_conversion,[],[f244]) ).
cnf(s34,plain,
( ~ spl28_26
| spl28_34 ),
inference(sat_conversion,[],[f249]) ).
cnf(s35,plain,
( ~ spl28_24
| spl28_35 ),
inference(sat_conversion,[],[f254]) ).
cnf(s36,plain,
( ~ spl28_22
| spl28_36 ),
inference(sat_conversion,[],[f259]) ).
cnf(s37,plain,
( ~ spl28_20
| spl28_37 ),
inference(sat_conversion,[],[f264]) ).
cnf(s38,plain,
( ~ spl28_18
| spl28_38 ),
inference(sat_conversion,[],[f269]) ).
cnf(s39,plain,
( ~ spl28_16
| spl28_39 ),
inference(sat_conversion,[],[f274]) ).
cnf(s40,plain,
( ~ spl28_14
| spl28_40 ),
inference(sat_conversion,[],[f279]) ).
cnf(s41,plain,
( ~ spl28_12
| spl28_41 ),
inference(sat_conversion,[],[f284]) ).
cnf(s42,plain,
( ~ spl28_10
| spl28_42 ),
inference(sat_conversion,[],[f289]) ).
cnf(s43,plain,
( ~ spl28_8
| spl28_43 ),
inference(sat_conversion,[],[f294]) ).
cnf(s44,plain,
( ~ spl28_6
| spl28_44 ),
inference(sat_conversion,[],[f299]) ).
cnf(s45,plain,
( ~ spl28_4
| spl28_45 ),
inference(sat_conversion,[],[f304]) ).
cnf(s46,plain,
( ~ spl28_29
| spl28_46 ),
inference(sat_conversion,[],[f324]) ).
cnf(s47,plain,
( ~ spl28_27
| spl28_47 ),
inference(sat_conversion,[],[f329]) ).
cnf(s48,plain,
( ~ spl28_25
| spl28_48 ),
inference(sat_conversion,[],[f334]) ).
cnf(s49,plain,
( ~ spl28_23
| spl28_49 ),
inference(sat_conversion,[],[f339]) ).
cnf(s50,plain,
( ~ spl28_21
| spl28_50 ),
inference(sat_conversion,[],[f344]) ).
cnf(s51,plain,
( ~ spl28_19
| spl28_51 ),
inference(sat_conversion,[],[f349]) ).
cnf(s52,plain,
( ~ spl28_17
| spl28_52 ),
inference(sat_conversion,[],[f354]) ).
cnf(s53,plain,
( ~ spl28_15
| spl28_53 ),
inference(sat_conversion,[],[f359]) ).
cnf(s54,plain,
( ~ spl28_13
| spl28_54 ),
inference(sat_conversion,[],[f364]) ).
cnf(s55,plain,
( ~ spl28_11
| spl28_55 ),
inference(sat_conversion,[],[f369]) ).
cnf(s56,plain,
( ~ spl28_9
| spl28_56 ),
inference(sat_conversion,[],[f374]) ).
cnf(s57,plain,
( ~ spl28_7
| spl28_57 ),
inference(sat_conversion,[],[f379]) ).
cnf(s58,plain,
( ~ spl28_5
| spl28_58 ),
inference(sat_conversion,[],[f384]) ).
cnf(s59,plain,
( ~ spl28_3
| spl28_59 ),
inference(sat_conversion,[],[f389]) ).
cnf(s60,plain,
( spl28_1
| ~ spl28_2
| ~ spl28_4
| ~ spl28_6
| ~ spl28_8
| ~ spl28_10
| ~ spl28_12
| ~ spl28_14
| ~ spl28_16
| ~ spl28_18
| ~ spl28_20
| ~ spl28_22
| ~ spl28_24
| ~ spl28_26
| ~ spl28_28
| ~ spl28_30
| ~ spl28_32
| ~ spl28_33
| ~ spl28_34
| ~ spl28_35
| ~ spl28_36
| ~ spl28_37
| ~ spl28_38
| ~ spl28_39
| ~ spl28_40
| ~ spl28_41
| ~ spl28_42
| ~ spl28_43
| ~ spl28_44
| ~ spl28_45
| ~ spl28_46
| ~ spl28_47
| ~ spl28_48
| ~ spl28_49
| ~ spl28_50
| ~ spl28_51
| ~ spl28_52
| ~ spl28_53
| ~ spl28_54
| ~ spl28_55
| ~ spl28_56
| ~ spl28_57
| ~ spl28_58
| ~ spl28_59 ),
inference(sat_conversion,[],[f390]) ).
cnf(s61,plain,
spl28_46,
inference(rat,[],[s46,s29]) ).
cnf(s62,plain,
spl28_33,
inference(rat,[],[s33,s28]) ).
cnf(s63,plain,
spl28_47,
inference(rat,[],[s47,s27]) ).
cnf(s64,plain,
spl28_34,
inference(rat,[],[s34,s26]) ).
cnf(s65,plain,
spl28_48,
inference(rat,[],[s48,s25]) ).
cnf(s66,plain,
spl28_35,
inference(rat,[],[s35,s24]) ).
cnf(s67,plain,
spl28_49,
inference(rat,[],[s49,s23]) ).
cnf(s68,plain,
spl28_36,
inference(rat,[],[s36,s22]) ).
cnf(s69,plain,
spl28_50,
inference(rat,[],[s50,s21]) ).
cnf(s70,plain,
spl28_37,
inference(rat,[],[s37,s20]) ).
cnf(s71,plain,
spl28_51,
inference(rat,[],[s51,s19]) ).
cnf(s72,plain,
spl28_38,
inference(rat,[],[s38,s18]) ).
cnf(s73,plain,
spl28_52,
inference(rat,[],[s52,s17]) ).
cnf(s74,plain,
spl28_39,
inference(rat,[],[s39,s16]) ).
cnf(s75,plain,
spl28_53,
inference(rat,[],[s53,s15]) ).
cnf(s76,plain,
spl28_40,
inference(rat,[],[s40,s14]) ).
cnf(s77,plain,
spl28_54,
inference(rat,[],[s54,s13]) ).
cnf(s78,plain,
spl28_41,
inference(rat,[],[s41,s12]) ).
cnf(s79,plain,
spl28_55,
inference(rat,[],[s55,s11]) ).
cnf(s80,plain,
spl28_42,
inference(rat,[],[s42,s10]) ).
cnf(s81,plain,
spl28_56,
inference(rat,[],[s56,s9]) ).
cnf(s82,plain,
spl28_43,
inference(rat,[],[s43,s8]) ).
cnf(s83,plain,
spl28_57,
inference(rat,[],[s57,s7]) ).
cnf(s84,plain,
spl28_44,
inference(rat,[],[s44,s6]) ).
cnf(s85,plain,
spl28_58,
inference(rat,[],[s58,s5]) ).
cnf(s86,plain,
spl28_45,
inference(rat,[],[s45,s4]) ).
cnf(s87,plain,
spl28_59,
inference(rat,[],[s59,s3]) ).
cnf(s88,plain,
spl28_31,
inference(rat,[],[s31,s30,s2]) ).
cnf(s89,plain,
spl28_32,
inference(rat,[],[s32,s88]) ).
cnf(s90,plain,
spl28_1,
inference(rat,[],[s60,s87,s85,s83,s81,s79,s77,s75,s73,s71,s69,s67,s65,s63,s61,s86,s84,s82,s80,s78,s76,s74,s72,s70,s68,s66,s64,s62,s2,s30,s28,s26,s24,s22,s20,s18,s16,s14,s12,s10,s8,s6,s4,s89]) ).
cnf(s91,plain,
$false,
inference(rat,[],[s1,s90]) ).
fof(f391,plain,
$false,
inference(avatar_sat_refutation,[],[s91]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV557-1.007 : 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.20 % Computer : n005.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 11:45:46 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.24 Running first-order theorem proving
% 0.09/0.24 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.31/1.54 % (736438)Input is clausal, will run a generic CNF schedule.
% 5.31/1.54 % (736447)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1474714961:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.31/1.54 % (736447)Instruction limit reached!
% 5.31/1.54 % (736447)------------------------------
% 5.31/1.54 % (736447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736447)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736447)Termination reason: Instruction limit
% 5.31/1.54 % (736447)Termination phase: Saturation
% 5.31/1.54 % (736447)Time elapsed: 0.025 s
% 5.31/1.54 % (736447)Peak memory usage: 88 MB
% 5.31/1.54 % (736447)Instructions burned: 118 (million)
% 5.31/1.54 % (736443)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=3234768110:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.31/1.54 % (736446)lrs+10_1_sil=8000:sp=occurrence:random_seed=1190575710:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.31/1.54 % (736445)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2123669946:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.31/1.54 % (736444)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=337747129:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.31/1.54 % (736448)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3176445949:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.31/1.54 % (736449)dis-21_1_sil=8000:lcm=predicate:random_seed=3189277782: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.31/1.54 % (736449)Refutation not found, incomplete strategy
% 5.31/1.54 % (736449)------------------------------
% 5.31/1.54 % (736449)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736449)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736449)Termination reason: Refutation not found, incomplete strategy
% 5.31/1.54 % (736449)Time elapsed: 0.002 s
% 5.31/1.54 % (736449)Peak memory usage: 87 MB
% 5.31/1.54 % (736449)Instructions burned: 3 (million)
% 5.31/1.54 % (736446)Instruction limit reached!
% 5.31/1.54 % (736446)------------------------------
% 5.31/1.54 % (736446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736446)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736446)Termination reason: Instruction limit
% 5.31/1.54 % (736446)Termination phase: Saturation
% 5.31/1.54 % (736446)Time elapsed: 0.047 s
% 5.31/1.54 % (736446)Peak memory usage: 88 MB
% 5.31/1.54 % (736446)Instructions burned: 109 (million)
% 5.31/1.54 % (736448)Instruction limit reached!
% 5.31/1.54 % (736448)------------------------------
% 5.31/1.54 % (736448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736448)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736448)Termination reason: Instruction limit
% 5.31/1.54 % (736448)Termination phase: Saturation
% 5.31/1.54 % (736448)Time elapsed: 0.081 s
% 5.31/1.54 % (736448)Peak memory usage: 88 MB
% 5.31/1.54 % (736448)Instructions burned: 182 (million)
% 5.31/1.54 % (736451)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=344467659:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.31/1.54 % (736451)Instruction limit reached!
% 5.31/1.54 % (736451)------------------------------
% 5.31/1.54 % (736451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736451)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736451)Termination reason: Instruction limit
% 5.31/1.54 % (736451)Termination phase: Saturation
% 5.31/1.54 % (736451)Time elapsed: 0.033 s
% 5.31/1.54 % (736451)Peak memory usage: 88 MB
% 5.31/1.54 % (736451)Instructions burned: 143 (million)
% 5.31/1.54 % (736458)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=415344223: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.31/1.54 % (736459)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3929393043:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.31/1.54 % (736449)------------------------------
% 5.31/1.54 % (736449)------------------------------
% 5.31/1.54 % (736458)Instruction limit reached!
% 5.31/1.54 % (736458)------------------------------
% 5.31/1.54 % (736458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736458)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736458)Termination reason: Instruction limit
% 5.31/1.54 % (736458)Termination phase: Saturation
% 5.31/1.54 % (736458)Time elapsed: 0.076 s
% 5.31/1.54 % (736458)Peak memory usage: 88 MB
% 5.31/1.54 % (736458)Instructions burned: 190 (million)
% 5.31/1.54 % (736461)lrs+10_64_to=lpo:sil=8000:random_seed=1812688622:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 5.31/1.54 % (736461)Instruction limit reached!
% 5.31/1.54 % (736461)------------------------------
% 5.31/1.54 % (736461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736461)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736461)Termination reason: Instruction limit
% 5.31/1.54 % (736461)Termination phase: Saturation
% 5.31/1.54 % (736461)Time elapsed: 0.038 s
% 5.31/1.54 % (736461)Peak memory usage: 88 MB
% 5.31/1.54 % (736461)Instructions burned: 129 (million)
% 5.31/1.54 % (736459)Instruction limit reached!
% 5.31/1.54 % (736459)------------------------------
% 5.31/1.54 % (736459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736459)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736459)Termination reason: Instruction limit
% 5.31/1.54 % (736459)Termination phase: Saturation
% 5.31/1.54 % (736459)Time elapsed: 0.091 s
% 5.31/1.54 % (736459)Peak memory usage: 89 MB
% 5.31/1.54 % (736459)Instructions burned: 220 (million)
% 5.31/1.54 % (736465)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2387550919:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 5.31/1.54 % (736464)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=650655119:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.31/1.54 % (736465)First to succeed.
% 5.31/1.54 % (736465)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-736438"
% 5.31/1.54 % (736467)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2491089233:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 5.31/1.54 % (736468)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=878765298:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 5.31/1.54 % (736464)Instruction limit reached!
% 5.31/1.54 % (736464)------------------------------
% 5.31/1.54 % (736464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736464)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736464)Termination reason: Instruction limit
% 5.31/1.54 % (736464)Termination phase: Saturation
% 5.31/1.54 % (736464)Time elapsed: 0.081 s
% 5.31/1.54 % (736464)Peak memory usage: 89 MB
% 5.31/1.54 % (736464)Instructions burned: 195 (million)
% 5.31/1.54 % (736468)Instruction limit reached!
% 5.31/1.54 % (736468)------------------------------
% 5.31/1.54 % (736468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.31/1.54 % (736468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.31/1.54 % (736468)CaDiCaL version: 2.1.3
% 5.31/1.54 % (736468)Termination reason: Instruction limit
% 5.31/1.54 % (736468)Termination phase: Saturation
% 5.31/1.54 % (736468)Time elapsed: 0.049 s
% 5.31/1.54 % (736468)Peak memory usage: 88 MB
% 5.31/1.54 % (736468)Instructions burned: 107 (million)
% 5.31/1.54 % (736473)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3478855082:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 5.31/1.54 % (736465)Refutation found. Thanks to Tanya!
% 5.31/1.54 % SZS status Unsatisfiable for theBenchmark
% 5.31/1.54 % SZS output start Proof for theBenchmark
% See solution above
% 6.73/1.74 % (736465)------------------------------
% 6.73/1.74 % (736465)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.73/1.74 % (736465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.73/1.74 % (736465)CaDiCaL version: 2.1.3
% 6.73/1.74 % (736465)Termination reason: Refutation
% 6.73/1.74 % (736465)Time elapsed: 0.011 s
% 6.73/1.74 % (736465)Peak memory usage: 89 MB
% 6.73/1.74 % (736465)Instructions burned: 18 (million)
% 6.73/1.74 % (736465)------------------------------
% 6.73/1.74 % (736465)------------------------------
% 6.73/1.74 % (736438)Success in time 0.861 s
% 6.73/1.74 % Vampire exiting
%------------------------------------------------------------------------------