%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW591_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:30:53 PM UTC 2026
% Result : Theorem 5.45s 1.77s
% Output : Refutation 7.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 44
% Syntax : Number of formulae : 189 ( 44 unt; 0 typ; 33 def)
% Number of atoms : 517 ( 206 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 537 ( 209 ~; 223 |; 46 &)
% ( 27 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number arithmetic : 73 ( 16 atm; 0 fun; 16 num; 41 var)
% Number of types : 8 ( 6 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 31 ( 27 usr; 26 prp; 0-2 aty)
% Number of functors : 49 ( 48 usr; 26 con; 0-5 aty)
% Number of variables : 179 ( 163 !; 16 ?; 179 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool: $tType ).
tff(type_def_8,type,
tuple0: $tType ).
tff(type_def_9,type,
map_int_lpoption_intrp: $tType ).
tff(type_def_10,type,
option_int: $tType ).
tff(func_def_0,type,
witness: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool1: ty ).
tff(func_def_4,type,
true: bool ).
tff(func_def_5,type,
false: bool ).
tff(func_def_6,type,
match_bool: ( ty * bool * uni * uni ) > uni ).
tff(func_def_7,type,
tuple01: ty ).
tff(func_def_8,type,
tuple02: tuple0 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_10,type,
option: ty > ty ).
tff(func_def_11,type,
none: ty > uni ).
tff(func_def_12,type,
some: ( ty * uni ) > uni ).
tff(func_def_13,type,
match_option: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_14,type,
some_proj_1: ( ty * uni ) > uni ).
tff(func_def_17,type,
fib: $int > $int ).
tff(func_def_22,type,
ref: ty > ty ).
tff(func_def_23,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_24,type,
contents: ( ty * uni ) > uni ).
tff(func_def_25,type,
map: ( ty * ty ) > ty ).
tff(func_def_26,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_27,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_28,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_29,type,
t2tb: map_int_lpoption_intrp > uni ).
tff(func_def_30,type,
tb2t: uni > map_int_lpoption_intrp ).
tff(func_def_31,type,
t2tb1: option_int > uni ).
tff(func_def_32,type,
tb2t1: uni > option_int ).
tff(func_def_33,type,
t2tb2: $int > uni ).
tff(func_def_34,type,
tb2t2: uni > $int ).
tff(func_def_36,type,
sK0: $int ).
tff(func_def_37,type,
sK1: map_int_lpoption_intrp ).
tff(func_def_38,type,
sK2: map_int_lpoption_intrp ).
tff(func_def_39,type,
sK3: map_int_lpoption_intrp ).
tff(func_def_40,type,
sK4: map_int_lpoption_intrp > $int ).
tff(func_def_41,type,
sK5: map_int_lpoption_intrp > $int ).
tff(func_def_42,type,
sF6: uni ).
tff(func_def_43,type,
sF7: option_int ).
tff(func_def_44,type,
sF8: ty ).
tff(func_def_45,type,
sF9: uni ).
tff(func_def_46,type,
sF10: uni ).
tff(func_def_47,type,
sF11: uni ).
tff(func_def_48,type,
sF12: option_int ).
tff(func_def_49,type,
sF13: $int ).
tff(func_def_50,type,
sF14: uni ).
tff(func_def_51,type,
sF15: uni ).
tff(func_def_52,type,
sF16: uni ).
tff(func_def_53,type,
sF17: uni ).
tff(func_def_54,type,
sF18: map_int_lpoption_intrp ).
tff(pred_def_1,type,
sort: ( ty * uni ) > $o ).
tff(pred_def_3,type,
inv: map_int_lpoption_intrp > $o ).
tff(f15,axiom,
! [X1: uni,X0: ty] :
( sort(X0,X1)
=> ( some_proj_1(X0,some(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',some_proj_1_def) ).
tff(f27,axiom,
! [X4: uni,X2: uni,X1: ty,X5: uni,X3: uni,X0: ty] :
( sort(X1,X5)
=> ( ( X3 = X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = X5 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_eq) ).
tff(f28,axiom,
! [X3: uni,X4: uni,X2: uni,X1: ty,X0: ty] :
( sort(X0,X3)
=> ( sort(X0,X4)
=> ! [X5: uni] :
( ( X3 != X4 )
=> ( get(X1,X0,set(X1,X0,X2,X3,X5),X4) = get(X1,X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',select_neq) ).
tff(f33,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR) ).
tff(f34,axiom,
! [X0: option_int] : sort(option(int),t2tb1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f36,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR1) ).
tff(f37,axiom,
! [X0: $int] : sort(int,t2tb2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2tb_sort2) ).
tff(f38,axiom,
! [X0: $int] : ( tb2t2(t2tb2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeL2) ).
tff(f39,axiom,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',bridgeR2) ).
tff(f40,axiom,
! [X0: map_int_lpoption_intrp] :
( ! [X2: $int,X1: $int] :
( ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X1))) = tb2t1(some(int,t2tb2(X2))) )
=> ( X2 = fib(X1) ) )
<=> inv(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inv_def) ).
tff(f41,conjecture,
! [X1: map_int_lpoption_intrp,X0: $int] :
( ( $lesseq(0,X0)
& inv(X1) )
=> ( ( tb2t1(get(option(int),int,t2tb(X1),t2tb2(X0))) = tb2t1(none(int)) )
=> ( ( $lesseq(0,X0)
& inv(X1) )
=> ! [X2: map_int_lpoption_intrp] :
( inv(X2)
=> ! [X3: map_int_lpoption_intrp] :
( ( X3 = tb2t(set(option(int),int,t2tb(X2),t2tb2(X0),some(int,t2tb2(fib(X0))))) )
=> ( inv(X3)
& ( fib(X0) = fib(X0) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_memo_fibo) ).
tff(f42,negated_conjecture,
~ ! [X1: map_int_lpoption_intrp,X0: $int] :
( ( $lesseq(0,X0)
& inv(X1) )
=> ( ( tb2t1(get(option(int),int,t2tb(X1),t2tb2(X0))) = tb2t1(none(int)) )
=> ( ( $lesseq(0,X0)
& inv(X1) )
=> ! [X2: map_int_lpoption_intrp] :
( inv(X2)
=> ! [X3: map_int_lpoption_intrp] :
( ( X3 = tb2t(set(option(int),int,t2tb(X2),t2tb2(X0),some(int,t2tb2(fib(X0))))) )
=> ( inv(X3)
& ( fib(X0) = fib(X0) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f41]) ).
tff(f45,plain,
~ ! [X1: map_int_lpoption_intrp,X0: $int] :
( ( ~ $less(X0,0)
& inv(X1) )
=> ( ( tb2t1(get(option(int),int,t2tb(X1),t2tb2(X0))) = tb2t1(none(int)) )
=> ( ( ~ $less(X0,0)
& inv(X1) )
=> ! [X2: map_int_lpoption_intrp] :
( inv(X2)
=> ! [X3: map_int_lpoption_intrp] :
( ( X3 = tb2t(set(option(int),int,t2tb(X2),t2tb2(X0),some(int,t2tb2(fib(X0))))) )
=> ( inv(X3)
& ( fib(X0) = fib(X0) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f42]) ).
tff(f56,plain,
! [X3: ty,X4: ty,X1: uni,X2: uni,X0: uni] :
( sort(X4,X0)
=> ( sort(X4,X1)
=> ! [X5: uni] :
( ( X0 != X1 )
=> ( get(X3,X4,X2,X1) = get(X3,X4,set(X3,X4,X2,X0,X5),X1) ) ) ) ),
inference(rectify,[],[f28]) ).
tff(f61,plain,
~ ! [X1: $int,X0: map_int_lpoption_intrp] :
( ( inv(X0)
& ~ $less(X1,0) )
=> ( ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X1))) = tb2t1(none(int)) )
=> ( ( ~ $less(X1,0)
& inv(X0) )
=> ! [X2: map_int_lpoption_intrp] :
( inv(X2)
=> ! [X3: map_int_lpoption_intrp] :
( ( tb2t(set(option(int),int,t2tb(X2),t2tb2(X1),some(int,t2tb2(fib(X1))))) = X3 )
=> ( inv(X3)
& ( fib(X1) = fib(X1) ) ) ) ) ) ) ),
inference(rectify,[],[f45]) ).
tff(f64,plain,
! [X2: ty,X3: uni,X5: ty,X0: uni,X4: uni,X1: uni] :
( sort(X2,X3)
=> ( ( X0 = X4 )
=> ( get(X2,X5,set(X2,X5,X1,X4,X3),X0) = X3 ) ) ),
inference(rectify,[],[f27]) ).
tff(f65,plain,
! [X3: ty,X4: ty,X1: uni,X2: uni,X0: uni] :
( ! [X5: uni] :
( ( X0 = X1 )
| ( get(X3,X4,X2,X1) = get(X3,X4,set(X3,X4,X2,X0,X5),X1) ) )
| ~ sort(X4,X1)
| ~ sort(X4,X0) ),
inference(ennf_transformation,[],[f56]) ).
tff(f66,plain,
! [X2: uni,X0: uni,X1: uni,X3: ty,X4: ty] :
( ~ sort(X4,X0)
| ~ sort(X4,X1)
| ! [X5: uni] :
( ( X0 = X1 )
| ( get(X3,X4,X2,X1) = get(X3,X4,set(X3,X4,X2,X0,X5),X1) ) ) ),
inference(flattening,[],[f65]) ).
tff(f74,plain,
! [X2: ty,X3: uni,X5: ty,X0: uni,X4: uni,X1: uni] :
( ( get(X2,X5,set(X2,X5,X1,X4,X3),X0) = X3 )
| ( X0 != X4 )
| ~ sort(X2,X3) ),
inference(ennf_transformation,[],[f64]) ).
tff(f75,plain,
! [X3: uni,X1: uni,X0: uni,X2: ty,X5: ty,X4: uni] :
( ~ sort(X2,X3)
| ( X0 != X4 )
| ( get(X2,X5,set(X2,X5,X1,X4,X3),X0) = X3 ) ),
inference(flattening,[],[f74]) ).
tff(f76,plain,
? [X1: $int,X0: map_int_lpoption_intrp] :
( ? [X2: map_int_lpoption_intrp] :
( ? [X3: map_int_lpoption_intrp] :
( ( ( fib(X1) != fib(X1) )
| ~ inv(X3) )
& ( tb2t(set(option(int),int,t2tb(X2),t2tb2(X1),some(int,t2tb2(fib(X1))))) = X3 ) )
& inv(X2) )
& ~ $less(X1,0)
& inv(X0)
& ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X1))) = tb2t1(none(int)) )
& inv(X0)
& ~ $less(X1,0) ),
inference(ennf_transformation,[],[f61]) ).
tff(f77,plain,
? [X1: $int,X0: map_int_lpoption_intrp] :
( ~ $less(X1,0)
& inv(X0)
& ~ $less(X1,0)
& ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X1))) = tb2t1(none(int)) )
& ? [X2: map_int_lpoption_intrp] :
( ? [X3: map_int_lpoption_intrp] :
( ( ( fib(X1) != fib(X1) )
| ~ inv(X3) )
& ( tb2t(set(option(int),int,t2tb(X2),t2tb2(X1),some(int,t2tb2(fib(X1))))) = X3 ) )
& inv(X2) )
& inv(X0) ),
inference(flattening,[],[f76]) ).
tff(f82,plain,
! [X0: map_int_lpoption_intrp] :
( inv(X0)
<=> ! [X2: $int,X1: $int] :
( ( X2 = fib(X1) )
| ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X1))) != tb2t1(some(int,t2tb2(X2))) ) ) ),
inference(ennf_transformation,[],[f40]) ).
tff(f83,plain,
! [X1: uni,X0: ty] :
( ~ sort(X0,X1)
| ( some_proj_1(X0,some(X0,X1)) = X1 ) ),
inference(ennf_transformation,[],[f15]) ).
tff(f91,plain,
! [X0: uni,X1: ty] :
( ~ sort(X1,X0)
| ( some_proj_1(X1,some(X1,X0)) = X0 ) ),
inference(rectify,[],[f83]) ).
tff(f93,plain,
? [X0: $int,X1: map_int_lpoption_intrp] :
( ~ $less(X0,0)
& inv(X1)
& ~ $less(X0,0)
& ( tb2t1(get(option(int),int,t2tb(X1),t2tb2(X0))) = tb2t1(none(int)) )
& ? [X2: map_int_lpoption_intrp] :
( ? [X3: map_int_lpoption_intrp] :
( ( ( fib(X0) != fib(X0) )
| ~ inv(X3) )
& ( tb2t(set(option(int),int,t2tb(X2),t2tb2(X0),some(int,t2tb2(fib(X0))))) = X3 ) )
& inv(X2) )
& inv(X1) ),
inference(rectify,[],[f77]) ).
tff(f94,plain,
( ~ $less(sK0,0)
& inv(sK1)
& ~ $less(sK0,0)
& ( tb2t1(none(int)) = tb2t1(get(option(int),int,t2tb(sK1),t2tb2(sK0))) )
& ( ( fib(sK0) != fib(sK0) )
| ~ inv(sK3) )
& ( tb2t(set(option(int),int,t2tb(sK2),t2tb2(sK0),some(int,t2tb2(fib(sK0))))) = sK3 )
& inv(sK2)
& inv(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f93]) ).
tff(f100,plain,
! [X0: uni,X1: uni,X2: uni,X3: ty,X4: ty,X5: uni] :
( ~ sort(X3,X0)
| ( X2 != X5 )
| ( get(X3,X4,set(X3,X4,X1,X5,X0),X2) = X0 ) ),
inference(rectify,[],[f75]) ).
tff(f101,plain,
! [X0: map_int_lpoption_intrp] :
( ( inv(X0)
| ? [X2: $int,X1: $int] :
( ( fib(X1) != X2 )
& ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X1))) = tb2t1(some(int,t2tb2(X2))) ) ) )
& ( ! [X2: $int,X1: $int] :
( ( X2 = fib(X1) )
| ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X1))) != tb2t1(some(int,t2tb2(X2))) ) )
| ~ inv(X0) ) ),
inference(nnf_transformation,[],[f82]) ).
tff(f102,plain,
! [X0: map_int_lpoption_intrp] :
( ( inv(X0)
| ? [X1: $int,X2: $int] :
( ( fib(X2) != X1 )
& ( tb2t1(get(option(int),int,t2tb(X0),t2tb2(X2))) = tb2t1(some(int,t2tb2(X1))) ) ) )
& ( ! [X3: $int,X4: $int] :
( ( fib(X4) = X3 )
| ( tb2t1(some(int,t2tb2(X3))) != tb2t1(get(option(int),int,t2tb(X0),t2tb2(X4))) ) )
| ~ inv(X0) ) ),
inference(rectify,[],[f101]) ).
tff(f103,plain,
! [X0: map_int_lpoption_intrp] :
( ( inv(X0)
| ( ( sK4(X0) != fib(sK5(X0)) )
& ( tb2t1(some(int,t2tb2(sK4(X0)))) = tb2t1(get(option(int),int,t2tb(X0),t2tb2(sK5(X0)))) ) ) )
& ( ! [X3: $int,X4: $int] :
( ( fib(X4) = X3 )
| ( tb2t1(some(int,t2tb2(X3))) != tb2t1(get(option(int),int,t2tb(X0),t2tb2(X4))) ) )
| ~ inv(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X1,sK4(X0)),skolemize(X2,sK5(X0))],[f102]) ).
tff(f108,plain,
! [X0: uni,X1: uni,X2: uni,X3: ty,X4: ty] :
( ~ sort(X4,X1)
| ~ sort(X4,X2)
| ! [X5: uni] :
( ( X1 = X2 )
| ( get(X3,X4,X0,X2) = get(X3,X4,set(X3,X4,X0,X1,X5),X2) ) ) ),
inference(rectify,[],[f66]) ).
tff(f115,plain,
! [X0: option_int] : sort(option(int),t2tb1(X0)),
inference(cnf_transformation,[],[f34]) ).
tff(f116,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f33]) ).
tff(f119,plain,
! [X0: uni] : ( t2tb2(tb2t2(X0)) = X0 ),
inference(cnf_transformation,[],[f39]) ).
tff(f123,plain,
! [X0: uni,X1: ty] :
( ( some_proj_1(X1,some(X1,X0)) = X0 )
| ~ sort(X1,X0) ),
inference(cnf_transformation,[],[f91]) ).
tff(f126,plain,
inv(sK2),
inference(cnf_transformation,[],[f94]) ).
tff(f127,plain,
tb2t(set(option(int),int,t2tb(sK2),t2tb2(sK0),some(int,t2tb2(fib(sK0))))) = sK3,
inference(cnf_transformation,[],[f94]) ).
tff(f128,plain,
( ( fib(sK0) != fib(sK0) )
| ~ inv(sK3) ),
inference(cnf_transformation,[],[f94]) ).
tff(f136,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f36]) ).
tff(f142,plain,
! [X2: uni,X3: ty,X0: uni,X1: uni,X4: ty,X5: uni] :
( ~ sort(X3,X0)
| ( X2 != X5 )
| ( get(X3,X4,set(X3,X4,X1,X5,X0),X2) = X0 ) ),
inference(cnf_transformation,[],[f100]) ).
tff(f143,plain,
! [X3: $int,X0: map_int_lpoption_intrp,X4: $int] :
( ( tb2t1(some(int,t2tb2(X3))) != tb2t1(get(option(int),int,t2tb(X0),t2tb2(X4))) )
| ( fib(X4) = X3 )
| ~ inv(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f144,plain,
! [X0: map_int_lpoption_intrp] :
( ( tb2t1(some(int,t2tb2(sK4(X0)))) = tb2t1(get(option(int),int,t2tb(X0),t2tb2(sK5(X0)))) )
| inv(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f145,plain,
! [X0: map_int_lpoption_intrp] :
( ( sK4(X0) != fib(sK5(X0)) )
| inv(X0) ),
inference(cnf_transformation,[],[f103]) ).
tff(f151,plain,
! [X0: $int] : sort(int,t2tb2(X0)),
inference(cnf_transformation,[],[f37]) ).
tff(f153,plain,
! [X0: $int] : ( tb2t2(t2tb2(X0)) = X0 ),
inference(cnf_transformation,[],[f38]) ).
tff(f158,plain,
! [X2: uni,X3: ty,X0: uni,X1: uni,X4: ty,X5: uni] :
( ( get(X3,X4,X0,X2) = get(X3,X4,set(X3,X4,X0,X1,X5),X2) )
| ~ sort(X4,X2)
| ~ sort(X4,X1)
| ( X1 = X2 ) ),
inference(cnf_transformation,[],[f108]) ).
tff(f159,plain,
! [X3: ty,X0: uni,X1: uni,X4: ty,X5: uni] :
( ( get(X3,X4,set(X3,X4,X1,X5,X0),X5) = X0 )
| ~ sort(X3,X0) ),
inference(equality_resolution,[],[f142]) ).
tff(f164,definition,
sF8 = option(int),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f165,plain,
option(int) = sF8,
inference(reorient_equations,[],[f164]) ).
tff(f167,definition,
sF10 = t2tb2(sK0),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f168,plain,
t2tb2(sK0) = sF10,
inference(reorient_equations,[],[f167]) ).
tff(f173,definition,
sF13 = fib(sK0),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f174,plain,
fib(sK0) = sF13,
inference(reorient_equations,[],[f173]) ).
tff(f175,plain,
( ~ inv(sK3)
| ( sF13 != sF13 ) ),
inference(definition_folding,[],[f128,f174,f174]) ).
tff(f176,definition,
sF14 = t2tb(sK2),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f177,definition,
sF15 = t2tb2(sF13),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f178,plain,
t2tb2(sF13) = sF15,
inference(reorient_equations,[],[f177]) ).
tff(f179,definition,
sF16 = some(int,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f180,plain,
some(int,sF15) = sF16,
inference(reorient_equations,[],[f179]) ).
tff(f181,definition,
sF17 = set(sF8,int,sF14,sF10,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f182,definition,
sF18 = tb2t(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f183,plain,
tb2t(sF17) = sF18,
inference(reorient_equations,[],[f182]) ).
tff(f184,plain,
sK3 = sF18,
inference(definition_folding,[],[f127,f183,f181,f180,f178,f174,f168,f176,f165]) ).
tff(f185,plain,
~ inv(sK3),
inference(trivial_inequality_removal,[],[f175]) ).
tff(f198,definition,
( spl19_3
<=> ( sF17 = set(sF8,int,sF14,sF10,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl19_3])],[avatar_definition]) ).
tff(f200,plain,
( ( sF17 = set(sF8,int,sF14,sF10,sF16) )
| ~ spl19_3 ),
inference(avatar_component_clause,[],[f198]) ).
tff(f201,plain,
spl19_3,
inference(avatar_split_clause,[],[f181,f198]) ).
tff(f218,definition,
( spl19_7
<=> inv(sK3) ),
introduced(definition,[new_symbols(definition,[spl19_7])],[avatar_definition]) ).
tff(f220,plain,
( ~ inv(sK3)
| spl19_7 ),
inference(avatar_component_clause,[],[f218]) ).
tff(f221,plain,
~ spl19_7,
inference(avatar_split_clause,[],[f185,f218]) ).
tff(f228,definition,
( spl19_9
<=> ( option(int) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl19_9])],[avatar_definition]) ).
tff(f230,plain,
( ( option(int) = sF8 )
| ~ spl19_9 ),
inference(avatar_component_clause,[],[f228]) ).
tff(f231,plain,
spl19_9,
inference(avatar_split_clause,[],[f165,f228]) ).
tff(f233,definition,
( spl19_10
<=> ( sK3 = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl19_10])],[avatar_definition]) ).
tff(f235,plain,
( ( sK3 = sF18 )
| ~ spl19_10 ),
inference(avatar_component_clause,[],[f233]) ).
tff(f236,plain,
spl19_10,
inference(avatar_split_clause,[],[f184,f233]) ).
tff(f238,definition,
( spl19_11
<=> ( t2tb2(sK0) = sF10 ) ),
introduced(definition,[new_symbols(definition,[spl19_11])],[avatar_definition]) ).
tff(f240,plain,
( ( t2tb2(sK0) = sF10 )
| ~ spl19_11 ),
inference(avatar_component_clause,[],[f238]) ).
tff(f241,plain,
spl19_11,
inference(avatar_split_clause,[],[f168,f238]) ).
tff(f243,definition,
( spl19_12
<=> inv(sK2) ),
introduced(definition,[new_symbols(definition,[spl19_12])],[avatar_definition]) ).
tff(f245,plain,
( inv(sK2)
| ~ spl19_12 ),
inference(avatar_component_clause,[],[f243]) ).
tff(f246,plain,
spl19_12,
inference(avatar_split_clause,[],[f126,f243]) ).
tff(f263,definition,
( spl19_16
<=> ( some(int,sF15) = sF16 ) ),
introduced(definition,[new_symbols(definition,[spl19_16])],[avatar_definition]) ).
tff(f265,plain,
( ( some(int,sF15) = sF16 )
| ~ spl19_16 ),
inference(avatar_component_clause,[],[f263]) ).
tff(f266,plain,
spl19_16,
inference(avatar_split_clause,[],[f180,f263]) ).
tff(f278,definition,
( spl19_19
<=> ( tb2t(sF17) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl19_19])],[avatar_definition]) ).
tff(f280,plain,
( ( tb2t(sF17) = sF18 )
| ~ spl19_19 ),
inference(avatar_component_clause,[],[f278]) ).
tff(f281,plain,
spl19_19,
inference(avatar_split_clause,[],[f183,f278]) ).
tff(f283,definition,
( spl19_20
<=> ( fib(sK0) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition]) ).
tff(f285,plain,
( ( fib(sK0) = sF13 )
| ~ spl19_20 ),
inference(avatar_component_clause,[],[f283]) ).
tff(f286,plain,
spl19_20,
inference(avatar_split_clause,[],[f174,f283]) ).
tff(f288,definition,
( spl19_21
<=> ( sF14 = t2tb(sK2) ) ),
introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition]) ).
tff(f290,plain,
( ( sF14 = t2tb(sK2) )
| ~ spl19_21 ),
inference(avatar_component_clause,[],[f288]) ).
tff(f291,plain,
spl19_21,
inference(avatar_split_clause,[],[f176,f288]) ).
tff(f293,definition,
( spl19_22
<=> ( t2tb2(sF13) = sF15 ) ),
introduced(definition,[new_symbols(definition,[spl19_22])],[avatar_definition]) ).
tff(f295,plain,
( ( t2tb2(sF13) = sF15 )
| ~ spl19_22 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f296,plain,
spl19_22,
inference(avatar_split_clause,[],[f178,f293]) ).
tff(f297,plain,
( ~ inv(sF18)
| spl19_7
| ~ spl19_10 ),
inference(superposition,[],[f220,f235]) ).
tff(f299,definition,
( spl19_23
<=> inv(sF18) ),
introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition]) ).
tff(f301,plain,
( ~ inv(sF18)
| spl19_23 ),
inference(avatar_component_clause,[],[f299]) ).
tff(f302,plain,
( ~ spl19_23
| spl19_7
| ~ spl19_10 ),
inference(avatar_split_clause,[],[f297,f233,f218,f299]) ).
tff(f324,plain,
( ( sF17 = t2tb(sF18) )
| ~ spl19_19 ),
inference(superposition,[],[f116,f280]) ).
tff(f326,definition,
( spl19_27
<=> ( sF17 = t2tb(sF18) ) ),
introduced(definition,[new_symbols(definition,[spl19_27])],[avatar_definition]) ).
tff(f328,plain,
( ( sF17 = t2tb(sF18) )
| ~ spl19_27 ),
inference(avatar_component_clause,[],[f326]) ).
tff(f329,plain,
( spl19_27
| ~ spl19_19 ),
inference(avatar_split_clause,[],[f324,f278,f326]) ).
tff(f330,plain,
! [X0: uni] : sort(int,X0),
inference(superposition,[],[f151,f119]) ).
tff(f348,plain,
! [X0: uni] : sort(option(int),X0),
inference(superposition,[],[f115,f136]) ).
tff(f369,plain,
( ( tb2t2(sF10) = sK0 )
| ~ spl19_11 ),
inference(superposition,[],[f153,f240]) ).
tff(f371,definition,
( spl19_33
<=> ( tb2t2(sF10) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl19_33])],[avatar_definition]) ).
tff(f373,plain,
( ( tb2t2(sF10) = sK0 )
| ~ spl19_33 ),
inference(avatar_component_clause,[],[f371]) ).
tff(f374,plain,
( spl19_33
| ~ spl19_11 ),
inference(avatar_split_clause,[],[f369,f238,f371]) ).
tff(f381,plain,
( ( some(int,t2tb2(sF13)) = sF16 )
| ~ spl19_16
| ~ spl19_22 ),
inference(forward_demodulation,[],[f265,f295]) ).
tff(f383,definition,
( spl19_35
<=> ( some(int,t2tb2(sF13)) = sF16 ) ),
introduced(definition,[new_symbols(definition,[spl19_35])],[avatar_definition]) ).
tff(f385,plain,
( ( some(int,t2tb2(sF13)) = sF16 )
| ~ spl19_35 ),
inference(avatar_component_clause,[],[f383]) ).
tff(f386,plain,
( spl19_35
| ~ spl19_16
| ~ spl19_22 ),
inference(avatar_split_clause,[],[f381,f293,f263,f383]) ).
tff(f425,plain,
( ( sF17 = set(option(int),int,sF14,sF10,sF16) )
| ~ spl19_3
| ~ spl19_9 ),
inference(forward_demodulation,[],[f200,f230]) ).
tff(f427,definition,
( spl19_41
<=> ( sF17 = set(option(int),int,sF14,sF10,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl19_41])],[avatar_definition]) ).
tff(f429,plain,
( ( sF17 = set(option(int),int,sF14,sF10,sF16) )
| ~ spl19_41 ),
inference(avatar_component_clause,[],[f427]) ).
tff(f430,plain,
( spl19_41
| ~ spl19_3
| ~ spl19_9 ),
inference(avatar_split_clause,[],[f425,f228,f198,f427]) ).
tff(f437,plain,
( ( some_proj_1(int,sF16) = t2tb2(sF13) )
| ~ sort(int,t2tb2(sF13))
| ~ spl19_35 ),
inference(superposition,[],[f123,f385]) ).
tff(f439,plain,
( ( some_proj_1(int,sF16) = t2tb2(sF13) )
| ~ spl19_35 ),
inference(forward_subsumption_resolution,[],[f437,f151]) ).
tff(f441,definition,
( spl19_42
<=> ( some_proj_1(int,sF16) = t2tb2(sF13) ) ),
introduced(definition,[new_symbols(definition,[spl19_42])],[avatar_definition]) ).
tff(f443,plain,
( ( some_proj_1(int,sF16) = t2tb2(sF13) )
| ~ spl19_42 ),
inference(avatar_component_clause,[],[f441]) ).
tff(f444,plain,
( spl19_42
| ~ spl19_35 ),
inference(avatar_split_clause,[],[f439,f383,f441]) ).
tff(f552,plain,
( ~ sort(option(int),sF16)
| ( get(option(int),int,sF17,sF10) = sF16 )
| ~ spl19_41 ),
inference(superposition,[],[f159,f429]) ).
tff(f554,plain,
( ( get(option(int),int,sF17,sF10) = sF16 )
| ~ spl19_41 ),
inference(forward_subsumption_resolution,[],[f552,f348]) ).
tff(f556,definition,
( spl19_43
<=> ( get(option(int),int,sF17,sF10) = sF16 ) ),
introduced(definition,[new_symbols(definition,[spl19_43])],[avatar_definition]) ).
tff(f558,plain,
( ( get(option(int),int,sF17,sF10) = sF16 )
| ~ spl19_43 ),
inference(avatar_component_clause,[],[f556]) ).
tff(f559,plain,
( spl19_43
| ~ spl19_41 ),
inference(avatar_split_clause,[],[f554,f427,f556]) ).
tff(f570,plain,
! [X0: uni] :
( ( tb2t1(get(option(int),int,X0,t2tb2(sK5(tb2t(X0))))) = tb2t1(some(int,t2tb2(sK4(tb2t(X0))))) )
| inv(tb2t(X0)) ),
inference(superposition,[],[f144,f116]) ).
tff(f574,plain,
! [X0: map_int_lpoption_intrp] :
( ( t2tb1(tb2t1(some(int,t2tb2(sK4(X0))))) = get(option(int),int,t2tb(X0),t2tb2(sK5(X0))) )
| inv(X0) ),
inference(superposition,[],[f136,f144]) ).
tff(f576,plain,
! [X0: map_int_lpoption_intrp] :
( ( some(int,t2tb2(sK4(X0))) = get(option(int),int,t2tb(X0),t2tb2(sK5(X0))) )
| inv(X0) ),
inference(forward_demodulation,[],[f574,f136]) ).
tff(f592,plain,
( ! [X0: $int,X1: $int] :
( ( fib(X1) = X0 )
| ~ inv(sK2)
| ( tb2t1(some(int,t2tb2(X0))) != tb2t1(get(option(int),int,sF14,t2tb2(X1))) ) )
| ~ spl19_21 ),
inference(superposition,[],[f143,f290]) ).
tff(f598,plain,
( ! [X0: $int,X1: $int] :
( ( tb2t1(some(int,t2tb2(X0))) != tb2t1(get(option(int),int,sF14,t2tb2(X1))) )
| ( fib(X1) = X0 ) )
| ~ spl19_12
| ~ spl19_21 ),
inference(forward_subsumption_resolution,[],[f592,f245]) ).
tff(f636,definition,
( spl19_49
<=> ( t2tb2(sK5(sF18)) = sF10 ) ),
introduced(definition,[new_symbols(definition,[spl19_49])],[avatar_definition]) ).
tff(f637,plain,
( ( t2tb2(sK5(sF18)) != sF10 )
| spl19_49 ),
inference(avatar_component_clause,[],[f636]) ).
tff(f638,plain,
( ( t2tb2(sK5(sF18)) = sF10 )
| ~ spl19_49 ),
inference(avatar_component_clause,[],[f636]) ).
tff(f651,plain,
( ( sK5(sF18) = tb2t2(sF10) )
| ~ spl19_49 ),
inference(superposition,[],[f153,f638]) ).
tff(f659,plain,
( ( sK5(sF18) = sK0 )
| ~ spl19_33
| ~ spl19_49 ),
inference(forward_demodulation,[],[f651,f373]) ).
tff(f661,definition,
( spl19_51
<=> ( some(int,t2tb2(sK4(sF18))) = sF16 ) ),
introduced(definition,[new_symbols(definition,[spl19_51])],[avatar_definition]) ).
tff(f663,plain,
( ( some(int,t2tb2(sK4(sF18))) = sF16 )
| ~ spl19_51 ),
inference(avatar_component_clause,[],[f661]) ).
tff(f673,definition,
( spl19_53
<=> ( sK5(sF18) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl19_53])],[avatar_definition]) ).
tff(f675,plain,
( ( sK5(sF18) = sK0 )
| ~ spl19_53 ),
inference(avatar_component_clause,[],[f673]) ).
tff(f676,plain,
( spl19_53
| ~ spl19_33
| ~ spl19_49 ),
inference(avatar_split_clause,[],[f659,f636,f371,f673]) ).
tff(f683,plain,
( ( some(int,t2tb2(sK4(sF18))) = get(option(int),int,t2tb(sF18),sF10) )
| inv(sF18)
| ~ spl19_49 ),
inference(superposition,[],[f576,f638]) ).
tff(f686,plain,
( ( some(int,t2tb2(sK4(sF18))) = get(option(int),int,t2tb(sF18),sF10) )
| spl19_23
| ~ spl19_49 ),
inference(forward_subsumption_resolution,[],[f683,f301]) ).
tff(f687,plain,
( ( some(int,t2tb2(sK4(sF18))) = get(option(int),int,sF17,sF10) )
| spl19_23
| ~ spl19_27
| ~ spl19_49 ),
inference(forward_demodulation,[],[f686,f328]) ).
tff(f688,plain,
( ( some(int,t2tb2(sK4(sF18))) = sF16 )
| spl19_23
| ~ spl19_27
| ~ spl19_43
| ~ spl19_49 ),
inference(forward_demodulation,[],[f687,f558]) ).
tff(f689,plain,
( spl19_51
| spl19_23
| ~ spl19_27
| ~ spl19_43
| ~ spl19_49 ),
inference(avatar_split_clause,[],[f688,f636,f556,f326,f299,f661]) ).
tff(f695,plain,
( ( fib(sK0) != sK4(sF18) )
| inv(sF18)
| ~ spl19_53 ),
inference(superposition,[],[f145,f675]) ).
tff(f698,plain,
( ( fib(sK0) != sK4(sF18) )
| spl19_23
| ~ spl19_53 ),
inference(forward_subsumption_resolution,[],[f695,f301]) ).
tff(f703,plain,
( ( sK4(sF18) != sF13 )
| ~ spl19_20
| spl19_23
| ~ spl19_53 ),
inference(forward_demodulation,[],[f698,f285]) ).
tff(f709,definition,
( spl19_54
<=> ( sK4(sF18) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl19_54])],[avatar_definition]) ).
tff(f711,plain,
( ( sK4(sF18) != sF13 )
| spl19_54 ),
inference(avatar_component_clause,[],[f709]) ).
tff(f712,plain,
( ~ spl19_54
| ~ spl19_20
| spl19_23
| ~ spl19_53 ),
inference(avatar_split_clause,[],[f703,f673,f299,f283,f709]) ).
tff(f731,plain,
( ~ sort(int,t2tb2(sK4(sF18)))
| ( some_proj_1(int,sF16) = t2tb2(sK4(sF18)) )
| ~ spl19_51 ),
inference(superposition,[],[f123,f663]) ).
tff(f734,plain,
( ( some_proj_1(int,sF16) = t2tb2(sK4(sF18)) )
| ~ spl19_51 ),
inference(forward_subsumption_resolution,[],[f731,f151]) ).
tff(f736,plain,
( ( t2tb2(sK4(sF18)) = t2tb2(sF13) )
| ~ spl19_42
| ~ spl19_51 ),
inference(forward_demodulation,[],[f734,f443]) ).
tff(f743,definition,
( spl19_56
<=> ( t2tb2(sK4(sF18)) = t2tb2(sF13) ) ),
introduced(definition,[new_symbols(definition,[spl19_56])],[avatar_definition]) ).
tff(f745,plain,
( ( t2tb2(sK4(sF18)) = t2tb2(sF13) )
| ~ spl19_56 ),
inference(avatar_component_clause,[],[f743]) ).
tff(f746,plain,
( spl19_56
| ~ spl19_42
| ~ spl19_51 ),
inference(avatar_split_clause,[],[f736,f661,f441,f743]) ).
tff(f753,plain,
! [X2: uni,X0: uni,X1: uni] :
( inv(tb2t(set(option(int),int,X0,X1,X2)))
| ( tb2t1(get(option(int),int,X0,t2tb2(sK5(tb2t(set(option(int),int,X0,X1,X2)))))) = tb2t1(some(int,t2tb2(sK4(tb2t(set(option(int),int,X0,X1,X2)))))) )
| ( t2tb2(sK5(tb2t(set(option(int),int,X0,X1,X2)))) = X1 )
| ~ sort(int,t2tb2(sK5(tb2t(set(option(int),int,X0,X1,X2)))))
| ~ sort(int,X1) ),
inference(superposition,[],[f570,f158]) ).
tff(f763,plain,
! [X2: uni,X0: uni,X1: uni] :
( ( t2tb2(sK5(tb2t(set(option(int),int,X0,X1,X2)))) = X1 )
| ~ sort(int,X1)
| inv(tb2t(set(option(int),int,X0,X1,X2)))
| ( tb2t1(get(option(int),int,X0,t2tb2(sK5(tb2t(set(option(int),int,X0,X1,X2)))))) = tb2t1(some(int,t2tb2(sK4(tb2t(set(option(int),int,X0,X1,X2)))))) ) ),
inference(forward_subsumption_resolution,[],[f753,f151]) ).
tff(f767,plain,
! [X2: uni,X0: uni,X1: uni] :
( ( tb2t1(get(option(int),int,X0,t2tb2(sK5(tb2t(set(option(int),int,X0,X1,X2)))))) = tb2t1(some(int,t2tb2(sK4(tb2t(set(option(int),int,X0,X1,X2)))))) )
| inv(tb2t(set(option(int),int,X0,X1,X2)))
| ( t2tb2(sK5(tb2t(set(option(int),int,X0,X1,X2)))) = X1 ) ),
inference(forward_subsumption_resolution,[],[f763,f330]) ).
tff(f841,plain,
( ( tb2t2(t2tb2(sF13)) = sK4(sF18) )
| ~ spl19_56 ),
inference(superposition,[],[f153,f745]) ).
tff(f850,plain,
( ( sK4(sF18) = sF13 )
| ~ spl19_56 ),
inference(forward_demodulation,[],[f841,f153]) ).
tff(f853,plain,
( $false
| spl19_54
| ~ spl19_56 ),
inference(forward_subsumption_resolution,[],[f850,f711]) ).
tff(f854,plain,
( spl19_54
| ~ spl19_56 ),
inference(avatar_contradiction_clause,[],[f853]) ).
tff(f1755,definition,
( spl19_108
<=> ! [X0: $int] :
( ( tb2t1(some(int,t2tb2(X0))) != tb2t1(some(int,t2tb2(sK4(sF18)))) )
| ( fib(sK5(sF18)) = X0 ) ) ),
introduced(definition,[new_symbols(definition,[spl19_108])],[avatar_definition]) ).
tff(f1756,plain,
( ! [X0: $int] :
( ( tb2t1(some(int,t2tb2(X0))) != tb2t1(some(int,t2tb2(sK4(sF18)))) )
| ( fib(sK5(sF18)) = X0 ) )
| ~ spl19_108 ),
inference(avatar_component_clause,[],[f1755]) ).
tff(f1803,plain,
( ! [X2: $int,X0: uni,X1: uni] :
( ( tb2t1(some(int,t2tb2(X2))) != tb2t1(some(int,t2tb2(sK4(tb2t(set(option(int),int,sF14,X0,X1)))))) )
| ( fib(sK5(tb2t(set(option(int),int,sF14,X0,X1)))) = X2 )
| ( t2tb2(sK5(tb2t(set(option(int),int,sF14,X0,X1)))) = X0 )
| inv(tb2t(set(option(int),int,sF14,X0,X1))) )
| ~ spl19_12
| ~ spl19_21 ),
inference(superposition,[],[f598,f767]) ).
tff(f1893,plain,
( ( sK4(sF18) = fib(sK5(sF18)) )
| ~ spl19_108 ),
inference(equality_resolution,[],[f1756]) ).
tff(f1899,definition,
( spl19_114
<=> ( sK4(sF18) = fib(sK5(sF18)) ) ),
introduced(definition,[new_symbols(definition,[spl19_114])],[avatar_definition]) ).
tff(f1901,plain,
( ( sK4(sF18) = fib(sK5(sF18)) )
| ~ spl19_114 ),
inference(avatar_component_clause,[],[f1899]) ).
tff(f1902,plain,
( spl19_114
| ~ spl19_108 ),
inference(avatar_split_clause,[],[f1893,f1755,f1899]) ).
tff(f2378,plain,
( ! [X0: $int] :
( ( fib(sK5(tb2t(sF17))) = X0 )
| inv(tb2t(sF17))
| ( t2tb2(sK5(tb2t(sF17))) = sF10 )
| ( tb2t1(some(int,t2tb2(sK4(tb2t(sF17))))) != tb2t1(some(int,t2tb2(X0))) ) )
| ~ spl19_12
| ~ spl19_21
| ~ spl19_41 ),
inference(superposition,[],[f1803,f429]) ).
tff(f2383,plain,
( ! [X0: $int] :
( inv(tb2t(sF17))
| ( tb2t1(some(int,t2tb2(sK4(tb2t(sF17))))) != tb2t1(some(int,t2tb2(X0))) )
| ( fib(sK5(sF18)) = X0 )
| ( t2tb2(sK5(tb2t(sF17))) = sF10 ) )
| ~ spl19_12
| ~ spl19_19
| ~ spl19_21
| ~ spl19_41 ),
inference(forward_demodulation,[],[f2378,f280]) ).
tff(f2385,plain,
( ! [X0: $int] :
( ( t2tb2(sK5(tb2t(sF17))) = sF10 )
| inv(sF18)
| ( tb2t1(some(int,t2tb2(sK4(tb2t(sF17))))) != tb2t1(some(int,t2tb2(X0))) )
| ( fib(sK5(sF18)) = X0 ) )
| ~ spl19_12
| ~ spl19_19
| ~ spl19_21
| ~ spl19_41 ),
inference(forward_demodulation,[],[f2383,f280]) ).
tff(f2386,plain,
( ! [X0: $int] :
( ( tb2t1(some(int,t2tb2(sK4(tb2t(sF17))))) != tb2t1(some(int,t2tb2(X0))) )
| ( fib(sK5(sF18)) = X0 )
| ( t2tb2(sK5(tb2t(sF17))) = sF10 ) )
| ~ spl19_12
| ~ spl19_19
| ~ spl19_21
| spl19_23
| ~ spl19_41 ),
inference(forward_subsumption_resolution,[],[f2385,f301]) ).
tff(f2387,plain,
( ! [X0: $int] :
( ( fib(sK5(sF18)) = X0 )
| ( t2tb2(sK5(tb2t(sF17))) = sF10 )
| ( tb2t1(some(int,t2tb2(X0))) != tb2t1(some(int,t2tb2(sK4(sF18)))) ) )
| ~ spl19_12
| ~ spl19_19
| ~ spl19_21
| spl19_23
| ~ spl19_41 ),
inference(forward_demodulation,[],[f2386,f280]) ).
tff(f2388,plain,
( ! [X0: $int] :
( ( t2tb2(sK5(sF18)) = sF10 )
| ( tb2t1(some(int,t2tb2(X0))) != tb2t1(some(int,t2tb2(sK4(sF18)))) )
| ( fib(sK5(sF18)) = X0 ) )
| ~ spl19_12
| ~ spl19_19
| ~ spl19_21
| spl19_23
| ~ spl19_41 ),
inference(forward_demodulation,[],[f2387,f280]) ).
tff(f2389,plain,
( ! [X0: $int] :
( ( fib(sK5(sF18)) = X0 )
| ( tb2t1(some(int,t2tb2(X0))) != tb2t1(some(int,t2tb2(sK4(sF18)))) ) )
| ~ spl19_12
| ~ spl19_19
| ~ spl19_21
| spl19_23
| ~ spl19_41
| spl19_49 ),
inference(forward_subsumption_resolution,[],[f2388,f637]) ).
tff(f2390,plain,
( spl19_108
| ~ spl19_12
| ~ spl19_19
| ~ spl19_21
| spl19_23
| ~ spl19_41
| spl19_49 ),
inference(avatar_split_clause,[],[f2389,f636,f427,f299,f288,f278,f243,f1755]) ).
tff(f2391,plain,
( ( sK4(sF18) != sK4(sF18) )
| inv(sF18)
| ~ spl19_114 ),
inference(superposition,[],[f145,f1901]) ).
tff(f2392,plain,
( inv(sF18)
| ~ spl19_114 ),
inference(trivial_inequality_removal,[],[f2391]) ).
tff(f2393,plain,
( $false
| spl19_23
| ~ spl19_114 ),
inference(forward_subsumption_resolution,[],[f2392,f301]) ).
tff(f2394,plain,
( spl19_23
| ~ spl19_114 ),
inference(avatar_contradiction_clause,[],[f2393]) ).
tff(f2395,plain,
$false,
inference(avatar_smt_refutation,[],[f2394,f2390,f1902,f854,f746,f712,f689,f676,f559,f444,f430,f386,f374,f329,f302,f296,f291,f286,f281,f266,f246,f241,f236,f231,f221,f201]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW591_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.28 % Computer : n018.cluster.edu
% 0.23/0.28 % Model : x86_64 x86_64
% 0.23/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.28 % Memory : 8046.5625MB
% 0.23/0.28 % OS : Linux 6.8.0-71-generic
% 0.23/0.28 % CPULimit : 300
% 0.23/0.28 % WCLimit : 300
% 0.23/0.28 % DateTime : Mon Sep 28 14:22:25 UTC 2026
% 0.23/0.28 % CPUTime :
% 0.23/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.32 Running first-order theorem proving
% 0.23/0.32 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.45/1.77 % (3419069)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.45/1.77 % (3419074)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1180069157:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.45/1.77 % (3419074)Instruction limit reached!
% 5.45/1.77 % (3419074)------------------------------
% 5.45/1.77 % (3419074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419074)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419074)Termination reason: Instruction limit
% 5.45/1.77 % (3419074)Termination phase: Saturation
% 5.45/1.77 % (3419074)Time elapsed: 0.031 s
% 5.45/1.77 % (3419074)Peak memory usage: 116 MB
% 5.45/1.77 % (3419074)Instructions burned: 12 (million)
% 5.45/1.77 % (3419076)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3859665255:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.45/1.77 % (3419075)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2103362760:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.45/1.77 % (3419078)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1880116737:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.45/1.77 % (3419080)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4125683784:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.45/1.77 % (3419077)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2584271152:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.45/1.77 % (3419079)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3374415069:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.45/1.77 % (3419078)Instruction limit reached!
% 5.45/1.77 % (3419078)------------------------------
% 5.45/1.77 % (3419078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419078)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419078)Termination reason: Instruction limit
% 5.45/1.77 % (3419078)Termination phase: Saturation
% 5.45/1.77 % (3419078)Time elapsed: 0.005 s
% 5.45/1.77 % (3419078)Peak memory usage: 88 MB
% 5.45/1.77 % (3419078)Instructions burned: 4 (million)
% 5.45/1.77 % (3419077)Instruction limit reached!
% 5.45/1.77 % (3419077)------------------------------
% 5.45/1.77 % (3419077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419077)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419077)Termination reason: Instruction limit
% 5.45/1.77 % (3419077)Termination phase: Saturation
% 5.45/1.77 % (3419077)Time elapsed: 0.009 s
% 5.45/1.77 % (3419077)Peak memory usage: 88 MB
% 5.45/1.77 % (3419077)Instructions burned: 7 (million)
% 5.45/1.77 % (3419080)Instruction limit reached!
% 5.45/1.77 % (3419080)------------------------------
% 5.45/1.77 % (3419080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419080)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419080)Termination reason: Instruction limit
% 5.45/1.77 % (3419080)Termination phase: Saturation
% 5.45/1.77 % (3419080)Time elapsed: 0.063 s
% 5.45/1.77 % (3419080)Peak memory usage: 116 MB
% 5.45/1.77 % (3419080)Instructions burned: 33 (million)
% 5.45/1.77 % (3419079)Instruction limit reached!
% 5.45/1.77 % (3419079)------------------------------
% 5.45/1.77 % (3419079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419079)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419079)Termination reason: Instruction limit
% 5.45/1.77 % (3419079)Termination phase: Saturation
% 5.45/1.77 % (3419079)Time elapsed: 0.081 s
% 5.45/1.77 % (3419079)Peak memory usage: 116 MB
% 5.45/1.77 % (3419079)Instructions burned: 46 (million)
% 5.45/1.77 % (3419084)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1402093100:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 5.45/1.77 % (3419084)Instruction limit reached!
% 5.45/1.77 % (3419084)------------------------------
% 5.45/1.77 % (3419084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419084)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419084)Termination reason: Instruction limit
% 5.45/1.77 % (3419084)Termination phase: Saturation
% 5.45/1.77 % (3419084)Time elapsed: 0.010 s
% 5.45/1.77 % (3419084)Peak memory usage: 88 MB
% 5.45/1.77 % (3419084)Instructions burned: 14 (million)
% 5.45/1.77 % (3419091)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=128057857:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 5.45/1.77 % (3419091)Instruction limit reached!
% 5.45/1.77 % (3419091)------------------------------
% 5.45/1.77 % (3419091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419091)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419091)Termination reason: Instruction limit
% 5.45/1.77 % (3419091)Termination phase: Saturation
% 5.45/1.77 % (3419091)Time elapsed: 0.024 s
% 5.45/1.77 % (3419091)Peak memory usage: 89 MB
% 5.45/1.77 % (3419091)Instructions burned: 29 (million)
% 5.45/1.77 % (3419076)Instruction limit reached!
% 5.45/1.77 % (3419076)------------------------------
% 5.45/1.77 % (3419076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419076)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419076)Termination reason: Instruction limit
% 5.45/1.77 % (3419076)Termination phase: Saturation
% 5.45/1.77 % (3419076)Time elapsed: 0.268 s
% 5.45/1.77 % (3419076)Peak memory usage: 119 MB
% 5.45/1.77 % (3419076)Instructions burned: 201 (million)
% 5.45/1.77 % (3419092)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1632083806:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 5.45/1.77 % (3419075)First to succeed.
% 5.45/1.77 % (3419075)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3419069"
% 5.45/1.77 % (3419092)Instruction limit reached!
% 5.45/1.77 % (3419092)------------------------------
% 5.45/1.77 % (3419092)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419092)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419092)Termination reason: Instruction limit
% 5.45/1.77 % (3419092)Termination phase: Saturation
% 5.45/1.77 % (3419092)Time elapsed: 0.019 s
% 5.45/1.77 % (3419092)Peak memory usage: 90 MB
% 5.45/1.77 % (3419092)Instructions burned: 16 (million)
% 5.45/1.77 % (3419093)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3295151544:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 5.45/1.77 % (3419094)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3442847171:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 5.45/1.77 % (3419094)Also succeeded, but the first one will report.
% 5.45/1.77 % (3419093)Instruction limit reached!
% 5.45/1.77 % (3419093)------------------------------
% 5.45/1.77 % (3419093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419093)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419093)Termination reason: Instruction limit
% 5.45/1.77 % (3419093)Termination phase: Saturation
% 5.45/1.77 % (3419093)Time elapsed: 0.029 s
% 5.45/1.77 % (3419093)Peak memory usage: 89 MB
% 5.45/1.77 % (3419093)Instructions burned: 24 (million)
% 5.45/1.77 % (3419098)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=659100759:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 5.45/1.77 % (3419098)Instruction limit reached!
% 5.45/1.77 % (3419098)------------------------------
% 5.45/1.77 % (3419098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419098)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419098)Termination reason: Instruction limit
% 5.45/1.77 % (3419098)Termination phase: Saturation
% 5.45/1.77 % (3419098)Time elapsed: 0.002 s
% 5.45/1.77 % (3419098)Peak memory usage: 88 MB
% 5.45/1.77 % (3419098)Instructions burned: 2 (million)
% 5.45/1.77 % (3419096)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=82801951:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 5.45/1.77 % (3419096)Instruction limit reached!
% 5.45/1.77 % (3419096)------------------------------
% 5.45/1.77 % (3419096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419096)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419096)Termination reason: Instruction limit
% 5.45/1.77 % (3419096)Termination phase: Saturation
% 5.45/1.77 % (3419096)Time elapsed: 0.072 s
% 5.45/1.77 % (3419096)Peak memory usage: 89 MB
% 5.45/1.77 % (3419096)Instructions burned: 85 (million)
% 5.45/1.77 % (3419100)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3790111867:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 5.45/1.77 % (3419101)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=523502393:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 5.45/1.77 % (3419101)Instruction limit reached!
% 5.45/1.77 % (3419101)------------------------------
% 5.45/1.77 % (3419101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.45/1.77 % (3419101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.45/1.77 % (3419101)CaDiCaL version: 2.1.3
% 5.45/1.77 % (3419101)Termination reason: Instruction limit
% 5.45/1.77 % (3419101)Termination phase: Saturation
% 5.45/1.77 % (3419101)Time elapsed: 0.005 s
% 5.45/1.77 % (3419101)Peak memory usage: 88 MB
% 5.45/1.77 % (3419101)Instructions burned: 4 (million)
% 5.45/1.77 % (3419107)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=52646441:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2993 on theBenchmark for (2993ds/66Mi)
% 5.45/1.77 % (3419112)lrs+10_1_thi=all:si=on:fd=off:random_seed=4032423922:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 5.45/1.77 % (3419075)Refutation found. Thanks to Tanya!
% 5.45/1.77 % SZS status Theorem for theBenchmark
% 5.45/1.77 % SZS output start Proof for theBenchmark
% See solution above
% 7.63/2.11 % (3419075)------------------------------
% 7.63/2.11 % (3419075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.63/2.11 % (3419075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.63/2.11 % (3419075)CaDiCaL version: 2.1.3
% 7.63/2.11 % (3419075)Termination reason: Refutation
% 7.63/2.11 % (3419075)Time elapsed: 0.291 s
% 7.63/2.11 % (3419075)Peak memory usage: 118 MB
% 7.63/2.11 % (3419075)Instructions burned: 271 (million)
% 7.63/2.11 % (3419075)------------------------------
% 7.63/2.11 % (3419075)------------------------------
% 7.63/2.11 % (3419069)Success in time 0.956 s
% 7.63/2.11 % Vampire exiting
%------------------------------------------------------------------------------