%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW643_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:31:01 PM UTC 2026
% Result : Theorem 9.18s 2.21s
% Output : Refutation 10.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 35
% Syntax : Number of formulae : 304 ( 63 unt; 0 typ; 24 def)
% Number of atoms : 1298 ( 385 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1588 ( 594 ~; 837 |; 98 &)
% ( 25 <=>; 33 =>; 0 <=; 1 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 119 ( 68 atm; 0 fun; 0 num; 51 var)
% Number of types : 7 ( 5 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 15 usr; 13 prp; 0-3 aty)
% Number of functors : 50 ( 50 usr; 27 con; 0-5 aty)
% Number of variables : 173 ( 0 sgn 142 !; 31 ?; 173 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(type_def_9,type,
list_int: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
list: ty > ty ).
tff(func_def_13,type,
nil: ty > uni ).
tff(func_def_14,type,
cons: ( ty * uni * uni ) > uni ).
tff(func_def_15,type,
match_list1: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_16,type,
cons_proj_11: ( ty * uni ) > uni ).
tff(func_def_17,type,
cons_proj_21: ( ty * uni ) > uni ).
tff(func_def_18,type,
t2tb: list_int > uni ).
tff(func_def_19,type,
tb2t: uni > list_int ).
tff(func_def_20,type,
t2tb1: $int > uni ).
tff(func_def_21,type,
tb2t1: uni > $int ).
tff(func_def_22,type,
infix_plpl: ( ty * uni * uni ) > uni ).
tff(func_def_23,type,
length1: ( ty * uni ) > $int ).
tff(func_def_27,type,
sK0: ( uni * uni * ty ) > uni ).
tff(func_def_28,type,
sK1: ( uni * uni * ty ) > uni ).
tff(func_def_29,type,
sK2: ( $int * list_int ) > $int ).
tff(func_def_30,type,
sK3: list_int ).
tff(func_def_31,type,
sK4: $int ).
tff(func_def_32,type,
sK5: $int ).
tff(func_def_33,type,
sK6: list_int ).
tff(func_def_34,type,
sK7: $int ).
tff(func_def_35,type,
sK8: list_int ).
tff(func_def_36,type,
sK9: bool1 ).
tff(func_def_37,type,
sK10: list_int > $int ).
tff(func_def_38,type,
sK11: list_int > $int ).
tff(func_def_39,type,
sK12: list_int > list_int ).
tff(func_def_40,type,
sK13: list_int > $int ).
tff(func_def_41,type,
sK14: ( list_int * list_int ) > $int ).
tff(func_def_42,type,
sK15: ( list_int * list_int ) > $int ).
tff(func_def_43,type,
sF16: uni ).
tff(func_def_44,type,
sF17: list_int ).
tff(func_def_45,type,
sF18: uni ).
tff(func_def_46,type,
sF19: uni ).
tff(func_def_47,type,
sF20: uni ).
tff(func_def_48,type,
sF21: uni ).
tff(func_def_49,type,
sF22: uni ).
tff(func_def_50,type,
sF23: uni ).
tff(func_def_51,type,
sF24: list_int ).
tff(func_def_52,type,
sF25: uni ).
tff(func_def_53,type,
sF26: uni ).
tff(func_def_54,type,
sF27: list_int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
mem: ( ty * uni * uni ) > $o ).
tff(pred_def_4,type,
sorted1: list_int > $o ).
tff(f14,axiom,
! [X1: uni,X2: uni,X0: ty] : ( nil(X0) != cons(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nil_Cons1) ).
tff(f18,axiom,
! [X2: uni,X0: ty,X1: uni] : ( cons_proj_21(X0,cons(X0,X1,X2)) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cons_proj_2_def1) ).
tff(f20,axiom,
! [X1: uni,X0: ty] :
( sort1(X0,X1)
=> ( ! [X3: uni,X2: uni] :
( sort1(X0,X2)
=> ( ( mem(X0,X1,X3)
| ( X1 = X2 ) )
<=> mem(X0,X1,cons(X0,X2,X3)) ) )
& ~ mem(X0,X1,nil(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mem_def) ).
tff(f22,axiom,
! [X0: list_int] : ( tb2t(t2tb(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL) ).
tff(f23,axiom,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR) ).
tff(f25,axiom,
! [X0: $int] : sort1(int,t2tb1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2tb_sort1) ).
tff(f26,axiom,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeL1) ).
tff(f27,axiom,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',bridgeR1) ).
tff(f31,axiom,
! [X0: $int,X1: list_int] :
( sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1))))
<=> ( ! [X2: $int] :
( mem(int,t2tb1(X2),t2tb(X1))
=> $lesseq(X0,X2) )
& sorted1(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sorted_mem) ).
tff(f44,conjecture,
! [X1: list_int,X0: $int] :
( sorted1(X1)
=> ( ( ( X1 = tb2t(nil(int)) )
=> ~ mem(int,t2tb1(X0),t2tb(X1)) )
& ! [X2: $int,X3: list_int] :
( ( X1 = tb2t(cons(int,t2tb1(X2),t2tb(X3))) )
=> ( ( ( X0 != X2 )
=> ( ( ~ $less(X2,X0)
=> ~ mem(int,t2tb1(X0),t2tb(X1)) )
& ( $less(X2,X0)
=> ( ! [X6: bool1] :
( ( ( X6 = true1 )
<=> mem(int,t2tb1(X0),t2tb(X3)) )
=> ( ( X6 = true1 )
<=> mem(int,t2tb1(X0),t2tb(X1)) ) )
& ( X1 != tb2t(nil(int)) )
& ! [X5: list_int,X4: $int] :
( ( X1 = tb2t(cons(int,t2tb1(X4),t2tb(X5))) )
=> ( X5 = X3 ) )
& sorted1(X3) ) ) ) )
& ( ( X0 = X2 )
=> mem(int,t2tb1(X0),t2tb(X1)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_find) ).
tff(f45,negated_conjecture,
~ ! [X1: list_int,X0: $int] :
( sorted1(X1)
=> ( ( ( X1 = tb2t(nil(int)) )
=> ~ mem(int,t2tb1(X0),t2tb(X1)) )
& ! [X2: $int,X3: list_int] :
( ( X1 = tb2t(cons(int,t2tb1(X2),t2tb(X3))) )
=> ( ( ( X0 != X2 )
=> ( ( ~ $less(X2,X0)
=> ~ mem(int,t2tb1(X0),t2tb(X1)) )
& ( $less(X2,X0)
=> ( ! [X6: bool1] :
( ( ( X6 = true1 )
<=> mem(int,t2tb1(X0),t2tb(X3)) )
=> ( ( X6 = true1 )
<=> mem(int,t2tb1(X0),t2tb(X1)) ) )
& ( X1 != tb2t(nil(int)) )
& ! [X5: list_int,X4: $int] :
( ( X1 = tb2t(cons(int,t2tb1(X4),t2tb(X5))) )
=> ( X5 = X3 ) )
& sorted1(X3) ) ) ) )
& ( ( X0 = X2 )
=> mem(int,t2tb1(X0),t2tb(X1)) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f44]) ).
tff(f49,plain,
! [X1: list_int,X0: $int] :
( sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1))))
<=> ( ! [X2: $int] :
( mem(int,t2tb1(X2),t2tb(X1))
=> ~ $less(X2,X0) )
& sorted1(X1) ) ),
inference(theory_normalization,[],[f31]) ).
tff(f59,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,X0)
| ( X0 = X1 ) ),
introduced(definition,[],[tha_order_totality]) ).
tff(f73,plain,
~ ! [X0: list_int,X1: $int] :
( sorted1(X0)
=> ( ! [X3: list_int,X2: $int] :
( ( tb2t(cons(int,t2tb1(X2),t2tb(X3))) = X0 )
=> ( ( ( X1 = X2 )
=> mem(int,t2tb1(X1),t2tb(X0)) )
& ( ( X1 != X2 )
=> ( ( $less(X2,X1)
=> ( ! [X6: $int,X5: list_int] :
( ( tb2t(cons(int,t2tb1(X6),t2tb(X5))) = X0 )
=> ( X5 = X3 ) )
& ! [X4: bool1] :
( ( mem(int,t2tb1(X1),t2tb(X3))
<=> ( true1 = X4 ) )
=> ( mem(int,t2tb1(X1),t2tb(X0))
<=> ( true1 = X4 ) ) )
& ( tb2t(nil(int)) != X0 )
& sorted1(X3) ) )
& ( ~ $less(X2,X1)
=> ~ mem(int,t2tb1(X1),t2tb(X0)) ) ) ) ) )
& ( ( tb2t(nil(int)) = X0 )
=> ~ mem(int,t2tb1(X1),t2tb(X0)) ) ) ),
inference(rectify,[],[f45]) ).
tff(f77,plain,
! [X0: uni,X2: uni,X1: ty] : ( cons_proj_21(X1,cons(X1,X2,X0)) = X0 ),
inference(rectify,[],[f18]) ).
tff(f83,plain,
! [X0: uni,X1: ty] :
( sort1(X1,X0)
=> ( ~ mem(X1,X0,nil(X1))
& ! [X3: uni,X2: uni] :
( sort1(X1,X3)
=> ( mem(X1,X0,cons(X1,X3,X2))
<=> ( ( X0 = X3 )
| mem(X1,X0,X2) ) ) ) ) ),
inference(rectify,[],[f20]) ).
tff(f98,plain,
! [X0: $int,X1: list_int] :
( ( sorted1(X1)
& ! [X2: $int] :
( ~ $less(X2,X0)
| ~ mem(int,t2tb1(X2),t2tb(X1)) ) )
<=> sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) ),
inference(ennf_transformation,[],[f49]) ).
tff(f99,plain,
! [X1: ty,X0: uni] :
( ~ sort1(X1,X0)
| ( ! [X3: uni,X2: uni] :
( ( mem(X1,X0,cons(X1,X3,X2))
<=> ( ( X0 = X3 )
| mem(X1,X0,X2) ) )
| ~ sort1(X1,X3) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(ennf_transformation,[],[f83]) ).
tff(f104,plain,
? [X0: list_int,X1: $int] :
( sorted1(X0)
& ( ( ( tb2t(nil(int)) = X0 )
& mem(int,t2tb1(X1),t2tb(X0)) )
| ? [X2: $int,X3: list_int] :
( ( ( ~ mem(int,t2tb1(X1),t2tb(X0))
& ( X1 = X2 ) )
| ( ( ( $less(X2,X1)
& ( ? [X6: $int,X5: list_int] :
( ( X3 != X5 )
& ( tb2t(cons(int,t2tb1(X6),t2tb(X5))) = X0 ) )
| ? [X4: bool1] :
( ( mem(int,t2tb1(X1),t2tb(X0))
<~> ( true1 = X4 ) )
& ( mem(int,t2tb1(X1),t2tb(X3))
<=> ( true1 = X4 ) ) )
| ~ sorted1(X3)
| ( tb2t(nil(int)) = X0 ) ) )
| ( ~ $less(X2,X1)
& mem(int,t2tb1(X1),t2tb(X0)) ) )
& ( X1 != X2 ) ) )
& ( tb2t(cons(int,t2tb1(X2),t2tb(X3))) = X0 ) ) ) ),
inference(ennf_transformation,[],[f73]) ).
tff(f122,plain,
! [X0: $int,X1: list_int] :
( ( ( sorted1(X1)
& ! [X2: $int] :
( ~ $less(X2,X0)
| ~ mem(int,t2tb1(X2),t2tb(X1)) ) )
| ~ sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) )
& ( sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1))))
| ~ sorted1(X1)
| ? [X2: $int] :
( $less(X2,X0)
& mem(int,t2tb1(X2),t2tb(X1)) ) ) ),
inference(nnf_transformation,[],[f98]) ).
tff(f123,plain,
! [X0: $int,X1: list_int] :
( ( ( sorted1(X1)
& ! [X2: $int] :
( ~ $less(X2,X0)
| ~ mem(int,t2tb1(X2),t2tb(X1)) ) )
| ~ sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) )
& ( sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1))))
| ~ sorted1(X1)
| ? [X2: $int] :
( $less(X2,X0)
& mem(int,t2tb1(X2),t2tb(X1)) ) ) ),
inference(flattening,[],[f122]) ).
tff(f124,plain,
! [X0: $int,X1: list_int] :
( ( ( sorted1(X1)
& ! [X2: $int] :
( ~ $less(X2,X0)
| ~ mem(int,t2tb1(X2),t2tb(X1)) ) )
| ~ sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) )
& ( sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1))))
| ~ sorted1(X1)
| ? [X3: $int] :
( $less(X3,X0)
& mem(int,t2tb1(X3),t2tb(X1)) ) ) ),
inference(rectify,[],[f123]) ).
tff(f125,plain,
! [X0: $int,X1: list_int] :
( ( ( sorted1(X1)
& ! [X2: $int] :
( ~ $less(X2,X0)
| ~ mem(int,t2tb1(X2),t2tb(X1)) ) )
| ~ sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) )
& ( sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1))))
| ~ sorted1(X1)
| ( $less(sK2(X0,X1),X0)
& mem(int,t2tb1(sK2(X0,X1)),t2tb(X1)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X3,sK2(X0,X1))],[f124]) ).
tff(f126,plain,
! [X1: ty,X0: uni] :
( ~ sort1(X1,X0)
| ( ! [X3: uni,X2: uni] :
( ( ( mem(X1,X0,cons(X1,X3,X2))
| ( ( X0 != X3 )
& ~ mem(X1,X0,X2) ) )
& ( ( X0 = X3 )
| mem(X1,X0,X2)
| ~ mem(X1,X0,cons(X1,X3,X2)) ) )
| ~ sort1(X1,X3) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(nnf_transformation,[],[f99]) ).
tff(f127,plain,
! [X1: ty,X0: uni] :
( ~ sort1(X1,X0)
| ( ! [X3: uni,X2: uni] :
( ( ( mem(X1,X0,cons(X1,X3,X2))
| ( ( X0 != X3 )
& ~ mem(X1,X0,X2) ) )
& ( ( X0 = X3 )
| mem(X1,X0,X2)
| ~ mem(X1,X0,cons(X1,X3,X2)) ) )
| ~ sort1(X1,X3) )
& ~ mem(X1,X0,nil(X1)) ) ),
inference(flattening,[],[f126]) ).
tff(f128,plain,
! [X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| ( ! [X2: uni,X3: uni] :
( ( ( mem(X0,X1,cons(X0,X2,X3))
| ( ( X1 != X2 )
& ~ mem(X0,X1,X3) ) )
& ( ( X1 = X2 )
| mem(X0,X1,X3)
| ~ mem(X0,X1,cons(X0,X2,X3)) ) )
| ~ sort1(X0,X2) )
& ~ mem(X0,X1,nil(X0)) ) ),
inference(rectify,[],[f127]) ).
tff(f135,plain,
? [X0: list_int,X1: $int] :
( sorted1(X0)
& ( ( ( tb2t(nil(int)) = X0 )
& mem(int,t2tb1(X1),t2tb(X0)) )
| ? [X2: $int,X3: list_int] :
( ( ( ~ mem(int,t2tb1(X1),t2tb(X0))
& ( X1 = X2 ) )
| ( ( ( $less(X2,X1)
& ( ? [X6: $int,X5: list_int] :
( ( X3 != X5 )
& ( tb2t(cons(int,t2tb1(X6),t2tb(X5))) = X0 ) )
| ? [X4: bool1] :
( ( ( true1 != X4 )
| ~ mem(int,t2tb1(X1),t2tb(X0)) )
& ( ( true1 = X4 )
| mem(int,t2tb1(X1),t2tb(X0)) )
& ( mem(int,t2tb1(X1),t2tb(X3))
| ( true1 != X4 ) )
& ( ( true1 = X4 )
| ~ mem(int,t2tb1(X1),t2tb(X3)) ) )
| ~ sorted1(X3)
| ( tb2t(nil(int)) = X0 ) ) )
| ( ~ $less(X2,X1)
& mem(int,t2tb1(X1),t2tb(X0)) ) )
& ( X1 != X2 ) ) )
& ( tb2t(cons(int,t2tb1(X2),t2tb(X3))) = X0 ) ) ) ),
inference(nnf_transformation,[],[f104]) ).
tff(f136,plain,
? [X0: list_int,X1: $int] :
( sorted1(X0)
& ( ( ( tb2t(nil(int)) = X0 )
& mem(int,t2tb1(X1),t2tb(X0)) )
| ? [X2: $int,X3: list_int] :
( ( ( ~ mem(int,t2tb1(X1),t2tb(X0))
& ( X1 = X2 ) )
| ( ( ( $less(X2,X1)
& ( ? [X6: $int,X5: list_int] :
( ( X3 != X5 )
& ( tb2t(cons(int,t2tb1(X6),t2tb(X5))) = X0 ) )
| ? [X4: bool1] :
( ( ( true1 != X4 )
| ~ mem(int,t2tb1(X1),t2tb(X0)) )
& ( ( true1 = X4 )
| mem(int,t2tb1(X1),t2tb(X0)) )
& ( mem(int,t2tb1(X1),t2tb(X3))
| ( true1 != X4 ) )
& ( ( true1 = X4 )
| ~ mem(int,t2tb1(X1),t2tb(X3)) ) )
| ~ sorted1(X3)
| ( tb2t(nil(int)) = X0 ) ) )
| ( ~ $less(X2,X1)
& mem(int,t2tb1(X1),t2tb(X0)) ) )
& ( X1 != X2 ) ) )
& ( tb2t(cons(int,t2tb1(X2),t2tb(X3))) = X0 ) ) ) ),
inference(flattening,[],[f135]) ).
tff(f137,plain,
? [X0: list_int,X1: $int] :
( sorted1(X0)
& ( ( ( tb2t(nil(int)) = X0 )
& mem(int,t2tb1(X1),t2tb(X0)) )
| ? [X2: $int,X3: list_int] :
( ( ( ~ mem(int,t2tb1(X1),t2tb(X0))
& ( X1 = X2 ) )
| ( ( ( $less(X2,X1)
& ( ? [X4: $int,X5: list_int] :
( ( X3 != X5 )
& ( tb2t(cons(int,t2tb1(X4),t2tb(X5))) = X0 ) )
| ? [X6: bool1] :
( ( ( true1 != X6 )
| ~ mem(int,t2tb1(X1),t2tb(X0)) )
& ( ( true1 = X6 )
| mem(int,t2tb1(X1),t2tb(X0)) )
& ( mem(int,t2tb1(X1),t2tb(X3))
| ( true1 != X6 ) )
& ( ( true1 = X6 )
| ~ mem(int,t2tb1(X1),t2tb(X3)) ) )
| ~ sorted1(X3)
| ( tb2t(nil(int)) = X0 ) ) )
| ( ~ $less(X2,X1)
& mem(int,t2tb1(X1),t2tb(X0)) ) )
& ( X1 != X2 ) ) )
& ( tb2t(cons(int,t2tb1(X2),t2tb(X3))) = X0 ) ) ) ),
inference(rectify,[],[f136]) ).
tff(f138,plain,
( sorted1(sK3)
& ( ( ( tb2t(nil(int)) = sK3 )
& mem(int,t2tb1(sK4),t2tb(sK3)) )
| ( ( ( ~ mem(int,t2tb1(sK4),t2tb(sK3))
& ( sK5 = sK4 ) )
| ( ( ( $less(sK5,sK4)
& ( ( ( sK8 != sK6 )
& ( sK3 = tb2t(cons(int,t2tb1(sK7),t2tb(sK8))) ) )
| ( ( ( true1 != sK9 )
| ~ mem(int,t2tb1(sK4),t2tb(sK3)) )
& ( ( true1 = sK9 )
| mem(int,t2tb1(sK4),t2tb(sK3)) )
& ( mem(int,t2tb1(sK4),t2tb(sK6))
| ( true1 != sK9 ) )
& ( ( true1 = sK9 )
| ~ mem(int,t2tb1(sK4),t2tb(sK6)) ) )
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 ) ) )
| ( ~ $less(sK5,sK4)
& mem(int,t2tb1(sK4),t2tb(sK3)) ) )
& ( sK5 != sK4 ) ) )
& ( sK3 = tb2t(cons(int,t2tb1(sK5),t2tb(sK6))) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6,sK7,sK8,sK9]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6),skolemize(X4,sK7),skolemize(X5,sK8),skolemize(X6,sK9)],[f137]) ).
tff(f141,plain,
! [X0: uni,X1: uni,X2: ty] : ( nil(X2) != cons(X2,X0,X1) ),
inference(rectify,[],[f14]) ).
tff(f149,plain,
! [X0: uni,X1: uni,X2: ty] : ( cons_proj_21(X2,cons(X2,X1,X0)) = X0 ),
inference(rectify,[],[f77]) ).
tff(f156,plain,
! [X0: $int] : ( tb2t1(t2tb1(X0)) = X0 ),
inference(cnf_transformation,[],[f26]) ).
tff(f161,plain,
! [X0: list_int] : ( tb2t(t2tb(X0)) = X0 ),
inference(cnf_transformation,[],[f22]) ).
tff(f163,plain,
! [X0: uni] : ( t2tb1(tb2t1(X0)) = X0 ),
inference(cnf_transformation,[],[f27]) ).
tff(f176,plain,
! [X2: $int,X0: $int,X1: list_int] :
( ~ $less(X2,X0)
| ~ mem(int,t2tb1(X2),t2tb(X1))
| ~ sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) ),
inference(cnf_transformation,[],[f125]) ).
tff(f177,plain,
! [X0: $int,X1: list_int] :
( sorted1(X1)
| ~ sorted1(tb2t(cons(int,t2tb1(X0),t2tb(X1)))) ),
inference(cnf_transformation,[],[f125]) ).
tff(f178,plain,
! [X0: ty,X1: uni] :
( ~ mem(X0,X1,nil(X0))
| ~ sort1(X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
tff(f179,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ mem(X0,X1,cons(X0,X2,X3))
| ( X1 = X2 )
| ~ sort1(X0,X2)
| mem(X0,X1,X3)
| ~ sort1(X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
tff(f180,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ mem(X0,X1,X3)
| mem(X0,X1,cons(X0,X2,X3))
| ~ sort1(X0,X1)
| ~ sort1(X0,X2) ),
inference(cnf_transformation,[],[f128]) ).
tff(f181,plain,
! [X2: uni,X3: uni,X0: ty,X1: uni] :
( ~ sort1(X0,X1)
| mem(X0,X1,cons(X0,X2,X3))
| ( X1 != X2 )
| ~ sort1(X0,X2) ),
inference(cnf_transformation,[],[f128]) ).
tff(f191,plain,
( mem(int,t2tb1(sK4),t2tb(sK3))
| ( sK3 = tb2t(cons(int,t2tb1(sK5),t2tb(sK6))) ) ),
inference(cnf_transformation,[],[f138]) ).
tff(f197,plain,
( mem(int,t2tb1(sK4),t2tb(sK3))
| ( sK5 = sK4 )
| ( sK3 = tb2t(cons(int,t2tb1(sK7),t2tb(sK8))) )
| ( true1 = sK9 )
| mem(int,t2tb1(sK4),t2tb(sK3))
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| mem(int,t2tb1(sK4),t2tb(sK3)) ),
inference(cnf_transformation,[],[f138]) ).
tff(f203,plain,
( mem(int,t2tb1(sK4),t2tb(sK3))
| ( sK5 = sK4 )
| ( sK8 != sK6 )
| mem(int,t2tb1(sK4),t2tb(sK6))
| ( true1 != sK9 )
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| mem(int,t2tb1(sK4),t2tb(sK3)) ),
inference(cnf_transformation,[],[f138]) ).
tff(f205,plain,
( mem(int,t2tb1(sK4),t2tb(sK3))
| ( sK5 = sK4 )
| ( sK8 != sK6 )
| ( true1 = sK9 )
| mem(int,t2tb1(sK4),t2tb(sK3))
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| mem(int,t2tb1(sK4),t2tb(sK3)) ),
inference(cnf_transformation,[],[f138]) ).
tff(f230,plain,
( ( tb2t(nil(int)) = sK3 )
| ( sK3 = tb2t(cons(int,t2tb1(sK5),t2tb(sK6))) ) ),
inference(cnf_transformation,[],[f138]) ).
tff(f233,plain,
( ( tb2t(nil(int)) = sK3 )
| ( sK5 = sK4 )
| ( sK3 = tb2t(cons(int,t2tb1(sK7),t2tb(sK8))) )
| ( true1 = sK9 )
| ~ mem(int,t2tb1(sK4),t2tb(sK6))
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| ~ $less(sK5,sK4) ),
inference(cnf_transformation,[],[f138]) ).
tff(f234,plain,
( ( tb2t(nil(int)) = sK3 )
| ( sK5 = sK4 )
| ( sK3 = tb2t(cons(int,t2tb1(sK7),t2tb(sK8))) )
| mem(int,t2tb1(sK4),t2tb(sK6))
| ( true1 != sK9 )
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| mem(int,t2tb1(sK4),t2tb(sK3)) ),
inference(cnf_transformation,[],[f138]) ).
tff(f241,plain,
( ( tb2t(nil(int)) = sK3 )
| ( sK5 = sK4 )
| ( sK8 != sK6 )
| ( true1 = sK9 )
| ~ mem(int,t2tb1(sK4),t2tb(sK6))
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| ~ $less(sK5,sK4) ),
inference(cnf_transformation,[],[f138]) ).
tff(f250,plain,
( ( tb2t(nil(int)) = sK3 )
| ~ mem(int,t2tb1(sK4),t2tb(sK3))
| ( sK5 != sK4 ) ),
inference(cnf_transformation,[],[f138]) ).
tff(f258,plain,
( ( tb2t(nil(int)) = sK3 )
| ~ mem(int,t2tb1(sK4),t2tb(sK3))
| ( sK3 = tb2t(cons(int,t2tb1(sK7),t2tb(sK8))) )
| ( true1 != sK9 )
| ~ mem(int,t2tb1(sK4),t2tb(sK3))
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| ~ $less(sK5,sK4) ),
inference(cnf_transformation,[],[f138]) ).
tff(f266,plain,
( ( tb2t(nil(int)) = sK3 )
| ~ mem(int,t2tb1(sK4),t2tb(sK3))
| ( sK8 != sK6 )
| ( true1 != sK9 )
| ~ mem(int,t2tb1(sK4),t2tb(sK3))
| ~ sorted1(sK6)
| ( tb2t(nil(int)) = sK3 )
| ~ $less(sK5,sK4) ),
inference(cnf_transformation,[],[f138]) ).
tff(f269,plain,
sorted1(sK3),
inference(cnf_transformation,[],[f138]) ).
tff(f275,plain,
! [X2: ty,X0: uni,X1: uni] : ( nil(X2) != cons(X2,X0,X1) ),
inference(cnf_transformation,[],[f141]) ).
tff(f286,plain,
! [X2: ty,X0: uni,X1: uni] : ( cons_proj_21(X2,cons(X2,X1,X0)) = X0 ),
inference(cnf_transformation,[],[f149]) ).
tff(f293,plain,
! [X0: uni] : ( t2tb(tb2t(X0)) = X0 ),
inference(cnf_transformation,[],[f23]) ).
tff(f294,plain,
! [X0: $int] : sort1(int,t2tb1(X0)),
inference(cnf_transformation,[],[f25]) ).
tff(f298,plain,
! [X2: uni,X3: uni,X0: ty] :
( ~ sort1(X0,X2)
| mem(X0,X2,cons(X0,X2,X3))
| ~ sort1(X0,X2) ),
inference(equality_resolution,[],[f181]) ).
tff(f300,definition,
sF16 = nil(int),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f301,plain,
nil(int) = sF16,
inference(reorient_equations,[],[f300]) ).
tff(f302,definition,
sF17 = tb2t(sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f303,definition,
sF18 = t2tb1(sK4),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f304,plain,
t2tb1(sK4) = sF18,
inference(reorient_equations,[],[f303]) ).
tff(f305,definition,
sF19 = t2tb(sK3),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f308,plain,
( ( sK8 != sK6 )
| ( true1 != sK9 )
| ~ mem(int,sF18,sF19)
| ~ $less(sK5,sK4)
| ( sF17 = sK3 )
| ~ sorted1(sK6)
| ~ mem(int,sF18,sF19)
| ( sF17 = sK3 ) ),
inference(definition_folding,[],[f266,f302,f301,f305,f304,f305,f304,f302,f301]) ).
tff(f312,definition,
sF20 = t2tb(sK6),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f313,plain,
t2tb(sK6) = sF20,
inference(reorient_equations,[],[f312]) ).
tff(f318,definition,
sF21 = t2tb1(sK7),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f319,plain,
t2tb1(sK7) = sF21,
inference(reorient_equations,[],[f318]) ).
tff(f320,definition,
sF22 = t2tb(sK8),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f321,definition,
sF23 = cons(int,sF21,sF22),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f322,definition,
sF24 = tb2t(sF23),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f323,plain,
tb2t(sF23) = sF24,
inference(reorient_equations,[],[f322]) ).
tff(f324,plain,
( ~ mem(int,sF18,sF19)
| ( true1 != sK9 )
| ~ $less(sK5,sK4)
| ( sF17 = sK3 )
| ( sK3 = sF24 )
| ( sF17 = sK3 )
| ~ mem(int,sF18,sF19)
| ~ sorted1(sK6) ),
inference(definition_folding,[],[f258,f302,f301,f305,f304,f323,f321,f320,f319,f305,f304,f302,f301]) ).
tff(f332,plain,
( ~ mem(int,sF18,sF19)
| ( sK5 != sK4 )
| ( sF17 = sK3 ) ),
inference(definition_folding,[],[f250,f305,f304,f302,f301]) ).
tff(f341,plain,
( ( true1 = sK9 )
| ~ $less(sK5,sK4)
| ~ sorted1(sK6)
| ( sK8 != sK6 )
| ~ mem(int,sF18,sF20)
| ( sF17 = sK3 )
| ( sK5 = sK4 )
| ( sF17 = sK3 ) ),
inference(definition_folding,[],[f241,f302,f301,f313,f304,f302,f301]) ).
tff(f348,plain,
( ( sF17 = sK3 )
| ~ sorted1(sK6)
| ( sK3 = sF24 )
| mem(int,sF18,sF20)
| mem(int,sF18,sF19)
| ( true1 != sK9 )
| ( sF17 = sK3 )
| ( sK5 = sK4 ) ),
inference(definition_folding,[],[f234,f305,f304,f302,f301,f313,f304,f323,f321,f320,f319,f302,f301]) ).
tff(f349,plain,
( ~ sorted1(sK6)
| ( sK5 = sK4 )
| ~ $less(sK5,sK4)
| ~ mem(int,sF18,sF20)
| ( sK3 = sF24 )
| ( sF17 = sK3 )
| ( true1 = sK9 )
| ( sF17 = sK3 ) ),
inference(definition_folding,[],[f233,f302,f301,f313,f304,f323,f321,f320,f319,f302,f301]) ).
tff(f352,definition,
sF25 = t2tb1(sK5),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f353,plain,
t2tb1(sK5) = sF25,
inference(reorient_equations,[],[f352]) ).
tff(f354,definition,
sF26 = cons(int,sF25,sF20),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f355,plain,
cons(int,sF25,sF20) = sF26,
inference(reorient_equations,[],[f354]) ).
tff(f356,definition,
sF27 = tb2t(sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f357,plain,
( ( sF17 = sK3 )
| ( sK3 = sF27 ) ),
inference(definition_folding,[],[f230,f356,f355,f313,f353,f302,f301]) ).
tff(f382,plain,
( mem(int,sF18,sF19)
| ~ sorted1(sK6)
| ( sK8 != sK6 )
| ( sF17 = sK3 )
| ( true1 = sK9 )
| ( sK5 = sK4 )
| mem(int,sF18,sF19)
| mem(int,sF18,sF19) ),
inference(definition_folding,[],[f205,f305,f304,f302,f301,f305,f304,f305,f304]) ).
tff(f384,plain,
( ( sK8 != sK6 )
| mem(int,sF18,sF19)
| mem(int,sF18,sF19)
| ( true1 != sK9 )
| ( sK5 = sK4 )
| ( sF17 = sK3 )
| mem(int,sF18,sF20)
| ~ sorted1(sK6) ),
inference(definition_folding,[],[f203,f305,f304,f302,f301,f313,f304,f305,f304]) ).
tff(f390,plain,
( ( true1 = sK9 )
| ~ sorted1(sK6)
| ( sK3 = sF24 )
| mem(int,sF18,sF19)
| mem(int,sF18,sF19)
| ( sK5 = sK4 )
| mem(int,sF18,sF19)
| ( sF17 = sK3 ) ),
inference(definition_folding,[],[f197,f305,f304,f302,f301,f305,f304,f323,f321,f320,f319,f305,f304]) ).
tff(f396,plain,
( ( sK3 = sF27 )
| mem(int,sF18,sF19) ),
inference(definition_folding,[],[f191,f356,f355,f313,f353,f305,f304]) ).
tff(f398,plain,
( ( sF17 = sK3 )
| ( sK5 = sK4 )
| ~ sorted1(sK6)
| ( sK3 = sF24 )
| ( true1 = sK9 )
| mem(int,sF18,sF19) ),
inference(duplicate_literal_removal,[],[f390]) ).
tff(f399,plain,
( ( sK8 != sK6 )
| mem(int,sF18,sF19)
| ( true1 = sK9 )
| ( sF17 = sK3 )
| ( sK5 = sK4 )
| ~ sorted1(sK6) ),
inference(duplicate_literal_removal,[],[f382]) ).
tff(f407,plain,
( ( true1 != sK9 )
| ( sK5 = sK4 )
| mem(int,sF18,sF20)
| ( sF17 = sK3 )
| mem(int,sF18,sF19)
| ~ sorted1(sK6)
| ( sK3 = sF24 ) ),
inference(duplicate_literal_removal,[],[f348]) ).
tff(f410,plain,
! [X2: uni,X3: uni,X0: ty] :
( mem(X0,X2,cons(X0,X2,X3))
| ~ sort1(X0,X2) ),
inference(duplicate_literal_removal,[],[f298]) ).
tff(f414,plain,
( ~ $less(sK5,sK4)
| ( sF17 = sK3 )
| ( sK3 = sF24 )
| ~ sorted1(sK6)
| ( sK5 = sK4 )
| ~ mem(int,sF18,sF20)
| ( true1 = sK9 ) ),
inference(duplicate_literal_removal,[],[f349]) ).
tff(f415,plain,
( ( sK8 != sK6 )
| ( sF17 = sK3 )
| ~ mem(int,sF18,sF19)
| ~ sorted1(sK6)
| ( true1 != sK9 )
| ~ $less(sK5,sK4) ),
inference(duplicate_literal_removal,[],[f308]) ).
tff(f421,plain,
( ~ $less(sK5,sK4)
| ( true1 != sK9 )
| ~ mem(int,sF18,sF19)
| ( sF17 = sK3 )
| ( sK3 = sF24 )
| ~ sorted1(sK6) ),
inference(duplicate_literal_removal,[],[f324]) ).
tff(f437,plain,
( mem(int,sF18,sF19)
| ( true1 != sK9 )
| ( sK5 = sK4 )
| mem(int,sF18,sF20)
| ( sF17 = sK3 )
| ( sK8 != sK6 )
| ~ sorted1(sK6) ),
inference(duplicate_literal_removal,[],[f384]) ).
tff(f448,plain,
( ( sK8 != sK6 )
| ~ mem(int,sF18,sF20)
| ( true1 = sK9 )
| ( sF17 = sK3 )
| ~ sorted1(sK6)
| ( sK5 = sK4 )
| ~ $less(sK5,sK4) ),
inference(duplicate_literal_removal,[],[f341]) ).
tff(f455,definition,
( spl28_1
<=> ( sK3 = sF27 ) ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
tff(f457,plain,
( ( sK3 = sF27 )
| ~ spl28_1 ),
inference(avatar_component_clause,[],[f455]) ).
tff(f459,definition,
( spl28_2
<=> ( sF17 = sK3 ) ),
introduced(definition,[new_symbols(definition,[spl28_2])],[avatar_definition]) ).
tff(f460,plain,
( ( sF17 != sK3 )
| spl28_2 ),
inference(avatar_component_clause,[],[f459]) ).
tff(f461,plain,
( ( sF17 = sK3 )
| ~ spl28_2 ),
inference(avatar_component_clause,[],[f459]) ).
tff(f462,plain,
( spl28_1
| spl28_2 ),
inference(avatar_split_clause,[],[f357,f459,f455]) ).
tff(f465,definition,
( spl28_3
<=> mem(int,sF18,sF19) ),
introduced(definition,[new_symbols(definition,[spl28_3])],[avatar_definition]) ).
tff(f467,plain,
( mem(int,sF18,sF19)
| ~ spl28_3 ),
inference(avatar_component_clause,[],[f465]) ).
tff(f468,plain,
( spl28_1
| spl28_3 ),
inference(avatar_split_clause,[],[f396,f465,f455]) ).
tff(f472,plain,
( ( sK3 = tb2t(sF16) )
| ~ spl28_2 ),
inference(forward_demodulation,[],[f302,f461]) ).
tff(f474,plain,
sort1(int,sF18),
inference(superposition,[],[f294,f304]) ).
tff(f476,plain,
sort1(int,sF25),
inference(superposition,[],[f294,f353]) ).
tff(f477,plain,
( ( sK3 = tb2t(sF26) )
| ~ spl28_1 ),
inference(forward_demodulation,[],[f356,f457]) ).
tff(f479,definition,
( spl28_4
<=> $less(sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl28_4])],[avatar_definition]) ).
tff(f480,plain,
( ~ $less(sK5,sK4)
| spl28_4 ),
inference(avatar_component_clause,[],[f479]) ).
tff(f481,plain,
( $less(sK5,sK4)
| ~ spl28_4 ),
inference(avatar_component_clause,[],[f479]) ).
tff(f483,definition,
( spl28_5
<=> ( sK5 = sK4 ) ),
introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition]) ).
tff(f484,plain,
( ( sK5 != sK4 )
| spl28_5 ),
inference(avatar_component_clause,[],[f483]) ).
tff(f485,plain,
( ( sK5 = sK4 )
| ~ spl28_5 ),
inference(avatar_component_clause,[],[f483]) ).
tff(f487,plain,
sK4 = tb2t1(sF18),
inference(superposition,[],[f156,f304]) ).
tff(f489,plain,
sK5 = tb2t1(sF25),
inference(superposition,[],[f156,f353]) ).
tff(f491,plain,
sK6 = tb2t(sF20),
inference(superposition,[],[f161,f313]) ).
tff(f492,plain,
tb2t(sF22) = sK8,
inference(superposition,[],[f161,f320]) ).
tff(f495,plain,
! [X0: uni] : sort1(int,X0),
inference(superposition,[],[f294,f163]) ).
tff(f501,plain,
( ( sF16 = t2tb(sK3) )
| ~ spl28_2 ),
inference(superposition,[],[f293,f472]) ).
tff(f502,plain,
t2tb(sF24) = sF23,
inference(superposition,[],[f293,f323]) ).
tff(f503,plain,
( ( sF26 = t2tb(sK3) )
| ~ spl28_1 ),
inference(superposition,[],[f293,f477]) ).
tff(f505,plain,
( ( sF16 = sF19 )
| ~ spl28_2 ),
inference(superposition,[],[f501,f305]) ).
tff(f509,plain,
( mem(int,sF18,sF16)
| ~ spl28_2
| ~ spl28_3 ),
inference(superposition,[],[f467,f505]) ).
tff(f514,plain,
( ( sF16 = sF26 )
| ~ spl28_1
| ~ spl28_2 ),
inference(superposition,[],[f503,f501]) ).
tff(f515,plain,
( ( sF19 = sF26 )
| ~ spl28_1 ),
inference(superposition,[],[f503,f305]) ).
tff(f527,plain,
nil(int) != sF26,
inference(superposition,[],[f275,f355]) ).
tff(f528,plain,
sF16 != sF26,
inference(forward_demodulation,[],[f527,f301]) ).
tff(f530,plain,
( $false
| ~ spl28_1
| ~ spl28_2 ),
inference(forward_subsumption_resolution,[],[f528,f514]) ).
tff(f531,plain,
( ~ spl28_1
| ~ spl28_2 ),
inference(avatar_contradiction_clause,[],[f530]) ).
tff(f533,plain,
sF26 = t2tb(sF27),
inference(superposition,[],[f293,f356]) ).
tff(f543,plain,
! [X0: uni] :
( ~ mem(int,X0,sF16)
| ~ sort1(int,X0) ),
inference(superposition,[],[f178,f301]) ).
tff(f544,plain,
! [X0: uni] : ~ mem(int,X0,sF16),
inference(forward_subsumption_resolution,[],[f543,f495]) ).
tff(f545,plain,
cons_proj_21(int,sF23) = sF22,
inference(superposition,[],[f286,f321]) ).
tff(f546,plain,
cons_proj_21(int,sF26) = sF20,
inference(superposition,[],[f286,f355]) ).
tff(f562,plain,
( ~ sort1(int,sF25)
| mem(int,sF25,sF26) ),
inference(superposition,[],[f410,f355]) ).
tff(f564,plain,
mem(int,sF25,sF26),
inference(forward_subsumption_resolution,[],[f562,f476]) ).
tff(f567,plain,
( $false
| ~ spl28_2
| ~ spl28_3 ),
inference(resolution,[],[f544,f509]) ).
tff(f568,plain,
( ~ spl28_2
| ~ spl28_3 ),
inference(avatar_contradiction_clause,[],[f567]) ).
tff(f569,plain,
( ( sF26 = t2tb(sK3) )
| ~ spl28_1 ),
inference(superposition,[],[f533,f457]) ).
tff(f572,plain,
( ( sK5 != sK4 )
| ~ mem(int,sF18,sF19)
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f332,f460]) ).
tff(f573,plain,
( ~ mem(int,sF18,sF26)
| ( sK5 != sK4 )
| ~ spl28_1
| spl28_2 ),
inference(forward_demodulation,[],[f572,f515]) ).
tff(f575,definition,
( spl28_6
<=> mem(int,sF18,sF26) ),
introduced(definition,[new_symbols(definition,[spl28_6])],[avatar_definition]) ).
tff(f576,plain,
( mem(int,sF18,sF26)
| ~ spl28_6 ),
inference(avatar_component_clause,[],[f575]) ).
tff(f577,plain,
( ~ mem(int,sF18,sF26)
| spl28_6 ),
inference(avatar_component_clause,[],[f575]) ).
tff(f578,plain,
( ~ spl28_6
| ~ spl28_5
| ~ spl28_1
| spl28_2 ),
inference(avatar_split_clause,[],[f573,f459,f455,f483,f575]) ).
tff(f586,plain,
( mem(int,sF18,sF19)
| ~ sorted1(sK6)
| ( sK3 = sF24 )
| ( sK5 = sK4 )
| ( true1 = sK9 )
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f398,f460]) ).
tff(f587,plain,
( ~ sorted1(sK6)
| mem(int,sF18,sF19)
| ( true1 = sK9 )
| ( sK3 = sF24 )
| spl28_2
| spl28_5 ),
inference(forward_subsumption_resolution,[],[f586,f484]) ).
tff(f588,plain,
( mem(int,sF18,sF26)
| ( true1 = sK9 )
| ~ sorted1(sK6)
| ( sK3 = sF24 )
| ~ spl28_1
| spl28_2
| spl28_5 ),
inference(forward_demodulation,[],[f587,f515]) ).
tff(f590,definition,
( spl28_7
<=> ( sK3 = sF24 ) ),
introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition]) ).
tff(f591,plain,
( ( sK3 != sF24 )
| spl28_7 ),
inference(avatar_component_clause,[],[f590]) ).
tff(f592,plain,
( ( sK3 = sF24 )
| ~ spl28_7 ),
inference(avatar_component_clause,[],[f590]) ).
tff(f594,definition,
( spl28_8
<=> sorted1(sK6) ),
introduced(definition,[new_symbols(definition,[spl28_8])],[avatar_definition]) ).
tff(f595,plain,
( sorted1(sK6)
| ~ spl28_8 ),
inference(avatar_component_clause,[],[f594]) ).
tff(f596,plain,
( ~ sorted1(sK6)
| spl28_8 ),
inference(avatar_component_clause,[],[f594]) ).
tff(f598,definition,
( spl28_9
<=> ( true1 = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl28_9])],[avatar_definition]) ).
tff(f599,plain,
( ( true1 != sK9 )
| spl28_9 ),
inference(avatar_component_clause,[],[f598]) ).
tff(f600,plain,
( ( true1 = sK9 )
| ~ spl28_9 ),
inference(avatar_component_clause,[],[f598]) ).
tff(f601,plain,
( spl28_7
| spl28_6
| ~ spl28_8
| spl28_9
| ~ spl28_1
| spl28_2
| spl28_5 ),
inference(avatar_split_clause,[],[f588,f483,f459,f455,f598,f594,f575,f590]) ).
tff(f604,plain,
( ! [X0: $int] : ~ sorted1(tb2t(cons(int,t2tb1(X0),t2tb(sK6))))
| spl28_8 ),
inference(resolution,[],[f596,f177]) ).
tff(f607,plain,
( ! [X0: $int] : ~ sorted1(tb2t(cons(int,t2tb1(X0),sF20)))
| spl28_8 ),
inference(forward_demodulation,[],[f604,f313]) ).
tff(f673,plain,
( ~ sorted1(tb2t(cons(int,sF25,sF20)))
| spl28_8 ),
inference(superposition,[],[f607,f353]) ).
tff(f675,plain,
( ~ sorted1(tb2t(sF26))
| spl28_8 ),
inference(forward_demodulation,[],[f673,f355]) ).
tff(f679,plain,
( ~ sorted1(sF27)
| spl28_8 ),
inference(forward_demodulation,[],[f675,f356]) ).
tff(f680,plain,
( ~ sorted1(sK3)
| ~ spl28_1
| spl28_8 ),
inference(forward_demodulation,[],[f679,f457]) ).
tff(f681,plain,
( $false
| ~ spl28_1
| spl28_8 ),
inference(forward_subsumption_resolution,[],[f680,f269]) ).
tff(f682,plain,
( ~ spl28_1
| spl28_8 ),
inference(avatar_contradiction_clause,[],[f681]) ).
tff(f687,plain,
( ~ mem(int,sF18,sF20)
| ( sK5 = sK4 )
| ~ $less(sK5,sK4)
| ( sK8 != sK6 )
| ~ sorted1(sK6)
| ( true1 = sK9 )
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f448,f460]) ).
tff(f689,plain,
( ( true1 != sK9 )
| mem(int,sF18,sF19)
| ~ sorted1(sK6)
| ( sK8 != sK6 )
| ( sK5 = sK4 )
| mem(int,sF18,sF20)
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f437,f460]) ).
tff(f700,plain,
( ~ mem(int,sF18,sF19)
| ~ $less(sK5,sK4)
| ( sK8 != sK6 )
| ~ sorted1(sK6)
| ( true1 != sK9 )
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f415,f460]) ).
tff(f704,plain,
( mem(int,sF18,sF19)
| mem(int,sF18,sF20)
| ( true1 != sK9 )
| ~ sorted1(sK6)
| ( sK5 = sK4 )
| ( sK3 = sF24 )
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f407,f460]) ).
tff(f709,plain,
( mem(int,sF18,sF19)
| ( true1 = sK9 )
| ( sK8 != sK6 )
| ( sK5 = sK4 )
| ~ sorted1(sK6)
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f399,f460]) ).
tff(f719,plain,
( ( sK5 = sK4 )
| ( true1 != sK9 )
| ( sK8 != sK6 )
| ~ sorted1(sK6)
| mem(int,sF18,sF26)
| mem(int,sF18,sF20)
| ~ spl28_1
| spl28_2 ),
inference(forward_demodulation,[],[f689,f515]) ).
tff(f734,plain,
( ( sK5 = sK4 )
| ~ sorted1(sK6)
| ( true1 != sK9 )
| mem(int,sF18,sF20)
| mem(int,sF18,sF26)
| ( sK3 = sF24 )
| ~ spl28_1
| spl28_2 ),
inference(forward_demodulation,[],[f704,f515]) ).
tff(f739,plain,
( ~ sorted1(sK6)
| ( sK8 != sK6 )
| ( sK5 = sK4 )
| mem(int,sF18,sF26)
| ( true1 = sK9 )
| ~ spl28_1
| spl28_2 ),
inference(forward_demodulation,[],[f709,f515]) ).
tff(f760,plain,
( ( t2tb1(sK4) = sF25 )
| ~ spl28_5 ),
inference(superposition,[],[f353,f485]) ).
tff(f768,plain,
( ~ mem(int,sF18,sF19)
| ~ $less(sK5,sK4)
| ( true1 != sK9 )
| ( sK8 != sK6 )
| spl28_2
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f700,f595]) ).
tff(f769,plain,
( ~ mem(int,sF18,sF19)
| ~ sorted1(sK6)
| ( true1 != sK9 )
| ( sK3 = sF24 )
| ~ $less(sK5,sK4)
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f421,f460]) ).
tff(f774,plain,
( ~ mem(int,sF18,sF26)
| ~ $less(sK5,sK4)
| ( sK8 != sK6 )
| ( true1 != sK9 )
| ~ spl28_1
| spl28_2
| ~ spl28_8 ),
inference(forward_demodulation,[],[f768,f515]) ).
tff(f775,plain,
( ~ mem(int,sF18,sF19)
| ( true1 != sK9 )
| ( sK3 = sF24 )
| ~ $less(sK5,sK4)
| spl28_2
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f769,f595]) ).
tff(f781,plain,
( ( true1 != sK9 )
| ~ $less(sK5,sK4)
| ~ mem(int,sF18,sF26)
| ( sK3 = sF24 )
| ~ spl28_1
| spl28_2
| ~ spl28_8 ),
inference(forward_demodulation,[],[f775,f515]) ).
tff(f786,plain,
( ( sF25 = sF18 )
| ~ spl28_5 ),
inference(superposition,[],[f760,f304]) ).
tff(f791,plain,
( ~ mem(int,sF25,sF26)
| ~ spl28_5
| spl28_6 ),
inference(superposition,[],[f577,f786]) ).
tff(f844,plain,
! [X2: $int,X0: $int,X1: list_int] :
( $less(X2,X0)
| ~ sorted1(tb2t(cons(int,t2tb1(X2),t2tb(X1))))
| ~ mem(int,t2tb1(X0),t2tb(X1))
| ( X0 = X2 ) ),
inference(resolution,[],[f176,f59]) ).
tff(f846,plain,
( $false
| ~ spl28_5
| spl28_6 ),
inference(forward_subsumption_resolution,[],[f564,f791]) ).
tff(f847,plain,
( ~ spl28_5
| spl28_6 ),
inference(avatar_contradiction_clause,[],[f846]) ).
tff(f857,plain,
( mem(int,sF18,sF26)
| ( true1 != sK9 )
| mem(int,sF18,sF20)
| ( sK5 = sK4 )
| ( sK8 != sK6 )
| ~ spl28_1
| spl28_2
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f719,f595]) ).
tff(f858,plain,
( ( true1 = sK9 )
| ( sK3 = sF24 )
| ~ mem(int,sF18,sF20)
| ~ sorted1(sK6)
| ( sK5 = sK4 )
| ~ $less(sK5,sK4)
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f414,f460]) ).
tff(f862,plain,
( ( sK8 != sK6 )
| ( sK5 = sK4 )
| ( true1 = sK9 )
| ~ $less(sK5,sK4)
| ~ mem(int,sF18,sF20)
| spl28_2
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f687,f595]) ).
tff(f864,plain,
( ( sK5 = sK4 )
| ( true1 != sK9 )
| mem(int,sF18,sF26)
| mem(int,sF18,sF20)
| ( sK3 = sF24 )
| ~ spl28_1
| spl28_2
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f734,f595]) ).
tff(f875,plain,
( ( sK5 = sK4 )
| ( true1 = sK9 )
| mem(int,sF18,sF26)
| ( sK8 != sK6 )
| ~ spl28_1
| spl28_2
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f739,f595]) ).
tff(f885,plain,
( mem(int,sF18,sF20)
| ( sK8 != sK6 )
| ( sK5 = sK4 )
| ( true1 != sK9 )
| ~ spl28_1
| spl28_2
| spl28_6
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f857,f577]) ).
tff(f886,plain,
( ( sK3 = sF24 )
| ( true1 = sK9 )
| ~ mem(int,sF18,sF20)
| ( sK5 = sK4 )
| ~ $less(sK5,sK4)
| spl28_2
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f858,f595]) ).
tff(f891,plain,
( ( true1 != sK9 )
| mem(int,sF18,sF20)
| ( sK3 = sF24 )
| ( sK5 = sK4 )
| ~ spl28_1
| spl28_2
| spl28_6
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f864,f577]) ).
tff(f901,plain,
( ( sK8 != sK6 )
| ( true1 = sK9 )
| ( sK5 = sK4 )
| ~ spl28_1
| spl28_2
| spl28_6
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f875,f577]) ).
tff(f935,plain,
( ( true1 != sK9 )
| mem(int,sF18,sF20)
| ( sK8 != sK6 )
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f885,f484]) ).
tff(f936,plain,
( ( sK8 != sK6 )
| mem(int,sF18,sF20)
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| ~ spl28_9 ),
inference(forward_subsumption_resolution,[],[f935,f600]) ).
tff(f938,definition,
( spl28_10
<=> ( sK8 = sK6 ) ),
introduced(definition,[new_symbols(definition,[spl28_10])],[avatar_definition]) ).
tff(f939,plain,
( ( sK8 = sK6 )
| ~ spl28_10 ),
inference(avatar_component_clause,[],[f938]) ).
tff(f940,plain,
( ( sK8 != sK6 )
| spl28_10 ),
inference(avatar_component_clause,[],[f938]) ).
tff(f942,definition,
( spl28_11
<=> mem(int,sF18,sF20) ),
introduced(definition,[new_symbols(definition,[spl28_11])],[avatar_definition]) ).
tff(f943,plain,
( ~ mem(int,sF18,sF20)
| spl28_11 ),
inference(avatar_component_clause,[],[f942]) ).
tff(f944,plain,
( mem(int,sF18,sF20)
| ~ spl28_11 ),
inference(avatar_component_clause,[],[f942]) ).
tff(f945,plain,
( ~ spl28_10
| spl28_11
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| ~ spl28_9 ),
inference(avatar_split_clause,[],[f936,f598,f594,f575,f483,f459,f455,f942,f938]) ).
tff(f953,plain,
( mem(int,sF18,sF20)
| ( sK3 = sF24 )
| ( sK5 = sK4 )
| ~ spl28_1
| spl28_2
| spl28_6
| ~ spl28_8
| ~ spl28_9 ),
inference(forward_subsumption_resolution,[],[f891,f600]) ).
tff(f954,plain,
( ( sK3 = sF24 )
| mem(int,sF18,sF20)
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| ~ spl28_9 ),
inference(forward_subsumption_resolution,[],[f953,f484]) ).
tff(f955,plain,
( spl28_7
| spl28_11
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| ~ spl28_9 ),
inference(avatar_split_clause,[],[f954,f598,f594,f575,f483,f459,f455,f942,f590]) ).
tff(f964,plain,
( ( sF23 = t2tb(sK3) )
| ~ spl28_7 ),
inference(superposition,[],[f502,f592]) ).
tff(f965,plain,
( ( sF23 = sF26 )
| ~ spl28_1
| ~ spl28_7 ),
inference(superposition,[],[f964,f569]) ).
tff(f1035,plain,
! [X0: uni] :
( ~ mem(int,X0,sF26)
| mem(int,X0,sF20)
| ~ sort1(int,X0)
| ( sF25 = X0 )
| ~ sort1(int,sF25) ),
inference(superposition,[],[f179,f355]) ).
tff(f1039,plain,
! [X0: uni] :
( ~ sort1(int,X0)
| mem(int,X0,sF20)
| ~ mem(int,X0,sF26)
| ( sF25 = X0 ) ),
inference(forward_subsumption_resolution,[],[f1035,f476]) ).
tff(f1042,plain,
! [X0: uni] :
( mem(int,X0,sF20)
| ~ mem(int,X0,sF26)
| ( sF25 = X0 ) ),
inference(forward_subsumption_resolution,[],[f1039,f495]) ).
tff(f1146,plain,
( ( cons_proj_21(int,sF23) = sF20 )
| ~ spl28_1
| ~ spl28_7 ),
inference(forward_demodulation,[],[f546,f965]) ).
tff(f1147,plain,
( ( sF22 = sF20 )
| ~ spl28_1
| ~ spl28_7 ),
inference(forward_demodulation,[],[f1146,f545]) ).
tff(f1149,plain,
( ( tb2t(sF22) = sK6 )
| ~ spl28_1
| ~ spl28_7 ),
inference(superposition,[],[f491,f1147]) ).
tff(f1211,plain,
( ( sK8 = sK6 )
| ~ spl28_1
| ~ spl28_7 ),
inference(superposition,[],[f492,f1149]) ).
tff(f1215,plain,
( $false
| ~ spl28_1
| ~ spl28_7
| spl28_10 ),
inference(forward_subsumption_resolution,[],[f1211,f940]) ).
tff(f1216,plain,
( ~ spl28_1
| ~ spl28_7
| spl28_10 ),
inference(avatar_contradiction_clause,[],[f1215]) ).
tff(f1219,plain,
( ( sK8 != sK6 )
| ( true1 = sK9 )
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f901,f484]) ).
tff(f1220,plain,
( ~ mem(int,sF18,sF20)
| ~ $less(sK5,sK4)
| ( true1 = sK9 )
| ( sK8 != sK6 )
| spl28_2
| spl28_5
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f862,f484]) ).
tff(f1243,plain,
( ( true1 = sK9 )
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| ~ spl28_10 ),
inference(forward_subsumption_resolution,[],[f1219,f939]) ).
tff(f1244,plain,
( $false
| ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| spl28_9
| ~ spl28_10 ),
inference(forward_subsumption_resolution,[],[f1243,f599]) ).
tff(f1245,plain,
( ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| spl28_9
| ~ spl28_10 ),
inference(avatar_contradiction_clause,[],[f1244]) ).
tff(f1308,plain,
( ~ mem(int,sF18,sF26)
| ( true1 != sK9 )
| ~ $less(sK5,sK4)
| ~ spl28_1
| spl28_2
| ~ spl28_8
| ~ spl28_10 ),
inference(forward_subsumption_resolution,[],[f774,f939]) ).
tff(f1357,plain,
( ~ $less(sK5,sK4)
| ~ mem(int,sF18,sF26)
| ~ spl28_1
| spl28_2
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10 ),
inference(forward_subsumption_resolution,[],[f1308,f600]) ).
tff(f1437,definition,
( spl28_12
<=> ( sF25 = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl28_12])],[avatar_definition]) ).
tff(f1438,plain,
( ( sF25 != sF18 )
| spl28_12 ),
inference(avatar_component_clause,[],[f1437]) ).
tff(f1439,plain,
( ( sF25 = sF18 )
| ~ spl28_12 ),
inference(avatar_component_clause,[],[f1437]) ).
tff(f1446,plain,
( ( tb2t1(sF25) = sK4 )
| ~ spl28_12 ),
inference(superposition,[],[f487,f1439]) ).
tff(f1453,plain,
( ( sK5 = sK4 )
| ~ spl28_12 ),
inference(superposition,[],[f1446,f489]) ).
tff(f1458,plain,
( $false
| spl28_5
| ~ spl28_12 ),
inference(forward_subsumption_resolution,[],[f1453,f484]) ).
tff(f1459,plain,
( spl28_5
| ~ spl28_12 ),
inference(avatar_contradiction_clause,[],[f1458]) ).
tff(f3679,plain,
( ~ $less(sK5,sK4)
| ~ spl28_1
| spl28_2
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10 ),
inference(forward_subsumption_resolution,[],[f1357,f576]) ).
tff(f3683,plain,
( ( sK3 = sF24 )
| ( true1 != sK9 )
| ~ $less(sK5,sK4)
| ~ spl28_1
| spl28_2
| ~ spl28_6
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f781,f576]) ).
tff(f3690,plain,
( ( true1 != sK9 )
| ~ $less(sK5,sK4)
| ~ spl28_1
| spl28_2
| ~ spl28_6
| spl28_7
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f3683,f591]) ).
tff(f3694,plain,
( ~ $less(sK5,sK4)
| ~ spl28_1
| spl28_2
| ~ spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_9 ),
inference(forward_subsumption_resolution,[],[f3690,f600]) ).
tff(f3713,plain,
( $false
| ~ spl28_1
| spl28_2
| ~ spl28_4
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10 ),
inference(forward_subsumption_resolution,[],[f3679,f481]) ).
tff(f3714,plain,
( ~ spl28_1
| spl28_2
| ~ spl28_4
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10 ),
inference(avatar_contradiction_clause,[],[f3713]) ).
tff(f3725,plain,
( ~ spl28_4
| ~ spl28_1
| spl28_2
| ~ spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_9 ),
inference(avatar_split_clause,[],[f3694,f598,f594,f590,f575,f459,f455,f479]) ).
tff(f3728,plain,
( ! [X0: list_int] :
( ~ mem(int,t2tb1(sK4),t2tb(X0))
| ~ sorted1(tb2t(cons(int,t2tb1(sK5),t2tb(X0))))
| ( sK5 = sK4 ) )
| spl28_4 ),
inference(resolution,[],[f480,f844]) ).
tff(f3731,plain,
( ! [X0: list_int] :
( ~ mem(int,t2tb1(sK4),t2tb(X0))
| ~ sorted1(tb2t(cons(int,t2tb1(sK5),t2tb(X0)))) )
| spl28_4
| spl28_5 ),
inference(forward_subsumption_resolution,[],[f3728,f484]) ).
tff(f3736,plain,
( ! [X0: list_int] :
( ~ sorted1(tb2t(cons(int,t2tb1(sK5),t2tb(X0))))
| ~ mem(int,sF18,t2tb(X0)) )
| spl28_4
| spl28_5 ),
inference(forward_demodulation,[],[f3731,f304]) ).
tff(f3740,plain,
( ! [X0: list_int] :
( ~ mem(int,sF18,t2tb(X0))
| ~ sorted1(tb2t(cons(int,sF25,t2tb(X0)))) )
| spl28_4
| spl28_5 ),
inference(forward_demodulation,[],[f3736,f353]) ).
tff(f4155,plain,
( ~ sorted1(tb2t(cons(int,sF25,sF20)))
| ~ mem(int,sF18,sF20)
| spl28_4
| spl28_5 ),
inference(superposition,[],[f3740,f313]) ).
tff(f4161,plain,
( ~ mem(int,sF18,sF20)
| ~ sorted1(tb2t(sF26))
| spl28_4
| spl28_5 ),
inference(forward_demodulation,[],[f4155,f355]) ).
tff(f4166,plain,
( ~ mem(int,sF18,sF20)
| ~ sorted1(sF27)
| spl28_4
| spl28_5 ),
inference(forward_demodulation,[],[f4161,f356]) ).
tff(f4168,plain,
( ~ sorted1(sK3)
| ~ mem(int,sF18,sF20)
| ~ spl28_1
| spl28_4
| spl28_5 ),
inference(forward_demodulation,[],[f4166,f457]) ).
tff(f4170,plain,
( ~ mem(int,sF18,sF20)
| ~ spl28_1
| spl28_4
| spl28_5 ),
inference(forward_subsumption_resolution,[],[f4168,f269]) ).
tff(f4173,plain,
( ~ spl28_11
| ~ spl28_1
| spl28_4
| spl28_5 ),
inference(avatar_split_clause,[],[f4170,f483,f479,f455,f942]) ).
tff(f4174,plain,
( ~ mem(int,sF18,sF26)
| ( sF25 = sF18 )
| spl28_11 ),
inference(resolution,[],[f943,f1042]) ).
tff(f4176,plain,
( ( sF25 = sF18 )
| ~ spl28_6
| spl28_11 ),
inference(forward_subsumption_resolution,[],[f4174,f576]) ).
tff(f4177,plain,
( $false
| ~ spl28_6
| spl28_11
| spl28_12 ),
inference(forward_subsumption_resolution,[],[f4176,f1438]) ).
tff(f4178,plain,
( ~ spl28_6
| spl28_11
| spl28_12 ),
inference(avatar_contradiction_clause,[],[f4177]) ).
tff(f4203,plain,
( ! [X0: uni] :
( mem(int,sF18,cons(int,X0,sF20))
| ~ sort1(int,sF18)
| ~ sort1(int,X0) )
| ~ spl28_11 ),
inference(resolution,[],[f944,f180]) ).
tff(f4206,plain,
( ! [X0: uni] :
( mem(int,sF18,cons(int,X0,sF20))
| ~ sort1(int,X0) )
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4203,f474]) ).
tff(f4207,plain,
( ! [X0: uni] : mem(int,sF18,cons(int,X0,sF20))
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4206,f495]) ).
tff(f4252,plain,
( mem(int,sF18,sF26)
| ~ spl28_11 ),
inference(superposition,[],[f4207,f355]) ).
tff(f4254,plain,
( $false
| spl28_6
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4252,f577]) ).
tff(f4255,plain,
( spl28_6
| ~ spl28_11 ),
inference(avatar_contradiction_clause,[],[f4254]) ).
tff(f4258,plain,
( ~ mem(int,sF18,sF20)
| ( true1 = sK9 )
| ( sK5 = sK4 )
| ~ $less(sK5,sK4)
| spl28_2
| spl28_7
| ~ spl28_8 ),
inference(forward_subsumption_resolution,[],[f886,f591]) ).
tff(f4269,plain,
( ( true1 = sK9 )
| ( sK5 = sK4 )
| ~ $less(sK5,sK4)
| spl28_2
| spl28_7
| ~ spl28_8
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4258,f944]) ).
tff(f4279,plain,
( ~ $less(sK5,sK4)
| ( true1 = sK9 )
| spl28_2
| spl28_5
| spl28_7
| ~ spl28_8
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4269,f484]) ).
tff(f4286,plain,
( ( true1 = sK9 )
| spl28_2
| ~ spl28_4
| spl28_5
| spl28_7
| ~ spl28_8
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4279,f481]) ).
tff(f4288,plain,
( $false
| spl28_2
| ~ spl28_4
| spl28_5
| spl28_7
| ~ spl28_8
| spl28_9
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4286,f599]) ).
tff(f4289,plain,
( spl28_2
| ~ spl28_4
| spl28_5
| spl28_7
| ~ spl28_8
| spl28_9
| ~ spl28_11 ),
inference(avatar_contradiction_clause,[],[f4288]) ).
tff(f4301,plain,
( ( true1 = sK9 )
| ( sK8 != sK6 )
| ~ $less(sK5,sK4)
| spl28_2
| spl28_5
| ~ spl28_8
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f1220,f944]) ).
tff(f4316,plain,
( ~ $less(sK5,sK4)
| ( sK8 != sK6 )
| spl28_2
| spl28_5
| ~ spl28_8
| spl28_9
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4301,f599]) ).
tff(f4325,plain,
( ( sK8 != sK6 )
| spl28_2
| ~ spl28_4
| spl28_5
| ~ spl28_8
| spl28_9
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4316,f481]) ).
tff(f4336,plain,
( $false
| spl28_2
| ~ spl28_4
| spl28_5
| ~ spl28_8
| spl28_9
| ~ spl28_10
| ~ spl28_11 ),
inference(forward_subsumption_resolution,[],[f4325,f939]) ).
tff(f4337,plain,
( spl28_2
| ~ spl28_4
| spl28_5
| ~ spl28_8
| spl28_9
| ~ spl28_10
| ~ spl28_11 ),
inference(avatar_contradiction_clause,[],[f4336]) ).
cnf(s1,plain,
( spl28_1
| spl28_2 ),
inference(sat_conversion,[],[f462]) ).
cnf(s2,plain,
( spl28_1
| spl28_3 ),
inference(sat_conversion,[],[f468]) ).
cnf(s4,plain,
( ~ spl28_1
| ~ spl28_2 ),
inference(sat_conversion,[],[f531]) ).
cnf(s5,plain,
( ~ spl28_2
| ~ spl28_3 ),
inference(sat_conversion,[],[f568]) ).
cnf(s6,plain,
( ~ spl28_1
| spl28_2
| ~ spl28_5
| ~ spl28_6 ),
inference(sat_conversion,[],[f578]) ).
cnf(s7,plain,
( ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| spl28_7
| ~ spl28_8
| spl28_9 ),
inference(sat_conversion,[],[f601]) ).
cnf(s8,plain,
( ~ spl28_1
| spl28_8 ),
inference(sat_conversion,[],[f682]) ).
cnf(s10,plain,
( ~ spl28_5
| spl28_6 ),
inference(sat_conversion,[],[f847]) ).
cnf(s11,plain,
( ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10
| spl28_11 ),
inference(sat_conversion,[],[f945]) ).
cnf(s12,plain,
( ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_9
| spl28_11 ),
inference(sat_conversion,[],[f955]) ).
cnf(s14,plain,
( ~ spl28_1
| ~ spl28_7
| spl28_10 ),
inference(sat_conversion,[],[f1216]) ).
cnf(s15,plain,
( ~ spl28_1
| spl28_2
| spl28_5
| spl28_6
| ~ spl28_8
| spl28_9
| ~ spl28_10 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s21,plain,
( spl28_5
| ~ spl28_12 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s27,plain,
( ~ spl28_1
| spl28_2
| ~ spl28_4
| ~ spl28_6
| ~ spl28_8
| ~ spl28_9
| ~ spl28_10 ),
inference(sat_conversion,[],[f3714]) ).
cnf(s28,plain,
( ~ spl28_1
| spl28_2
| ~ spl28_4
| ~ spl28_6
| spl28_7
| ~ spl28_8
| ~ spl28_9 ),
inference(sat_conversion,[],[f3725]) ).
cnf(s29,plain,
( ~ spl28_1
| spl28_4
| spl28_5
| ~ spl28_11 ),
inference(sat_conversion,[],[f4173]) ).
cnf(s30,plain,
( ~ spl28_6
| spl28_11
| spl28_12 ),
inference(sat_conversion,[],[f4178]) ).
cnf(s32,plain,
( spl28_6
| ~ spl28_11 ),
inference(sat_conversion,[],[f4255]) ).
cnf(s33,plain,
( spl28_2
| ~ spl28_4
| spl28_5
| spl28_7
| ~ spl28_8
| spl28_9
| ~ spl28_11 ),
inference(sat_conversion,[],[f4289]) ).
cnf(s34,plain,
( spl28_2
| ~ spl28_4
| spl28_5
| ~ spl28_8
| spl28_9
| ~ spl28_10
| ~ spl28_11 ),
inference(sat_conversion,[],[f4337]) ).
cnf(s35,plain,
spl28_1,
inference(rat,[],[s5,s1,s2]) ).
cnf(s36,plain,
spl28_8,
inference(rat,[],[s8,s35]) ).
cnf(s37,plain,
~ spl28_2,
inference(rat,[],[s4,s35]) ).
cnf(s38,plain,
( spl28_7
| ~ spl28_6 ),
inference(rat,[],[s33,s28,s29,s30,s21,s6,s37,s36,s35]) ).
cnf(s39,plain,
~ spl28_6,
inference(rat,[],[s27,s34,s14,s38,s29,s30,s21,s6,s35,s37,s36]) ).
cnf(s40,plain,
~ spl28_11,
inference(rat,[],[s32,s39]) ).
cnf(s41,plain,
~ spl28_5,
inference(rat,[],[s10,s39]) ).
cnf(s45,plain,
spl28_7,
inference(rat,[],[s7,s12,s35,s39,s37,s36,s41,s40]) ).
cnf(s46,plain,
spl28_10,
inference(rat,[],[s14,s35,s45]) ).
cnf(s47,plain,
spl28_9,
inference(rat,[],[s15,s41,s37,s36,s39,s35,s46]) ).
cnf(s48,plain,
$false,
inference(rat,[],[s11,s40,s41,s37,s36,s39,s35,s46,s47]) ).
tff(f4338,plain,
$false,
inference(avatar_sat_refutation,[],[s48]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW643_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.17 % Computer : n015.cluster.edu
% 0.06/0.17 % Model : x86_64 x86_64
% 0.06/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.17 % Memory : 8046.5625MB
% 0.06/0.17 % OS : Linux 6.8.0-71-generic
% 0.06/0.17 % CPULimit : 300
% 0.06/0.17 % WCLimit : 300
% 0.06/0.17 % DateTime : Mon Sep 28 14:27:02 UTC 2026
% 0.06/0.17 % CPUTime :
% 0.06/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.21 Running first-order theorem proving
% 0.06/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.63/1.20 % (2664762)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.63/1.20 % (2664767)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1811143133:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.63/1.20 % (2664767)Instruction limit reached!
% 3.63/1.20 % (2664767)------------------------------
% 3.63/1.20 % (2664767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (2664767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (2664767)CaDiCaL version: 2.1.3
% 3.63/1.20 % (2664767)Termination reason: Instruction limit
% 3.63/1.20 % (2664767)Termination phase: Saturation
% 3.63/1.20 % (2664767)Time elapsed: 0.020 s
% 3.63/1.20 % (2664767)Peak memory usage: 115 MB
% 3.63/1.20 % (2664767)Instructions burned: 14 (million)
% 3.63/1.20 % (2664771)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3133402334:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.63/1.20 % (2664770)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3732221759:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.63/1.20 % (2664768)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1727597312:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.63/1.20 % (2664769)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3982289204:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.63/1.20 % (2664772)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=566371608:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.63/1.20 % (2664773)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=519264484:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.63/1.20 % (2664771)Instruction limit reached!
% 3.63/1.20 % (2664771)------------------------------
% 3.63/1.20 % (2664771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (2664771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (2664771)CaDiCaL version: 2.1.3
% 3.63/1.20 % (2664771)Termination reason: Instruction limit
% 3.63/1.20 % (2664771)Termination phase: Saturation
% 3.63/1.20 % (2664771)Time elapsed: 0.003 s
% 3.63/1.20 % (2664771)Peak memory usage: 87 MB
% 3.63/1.20 % (2664771)Instructions burned: 5 (million)
% 3.63/1.20 % (2664770)Instruction limit reached!
% 3.63/1.20 % (2664770)------------------------------
% 3.63/1.20 % (2664770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (2664770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (2664770)CaDiCaL version: 2.1.3
% 3.63/1.20 % (2664770)Termination reason: Instruction limit
% 3.63/1.20 % (2664770)Termination phase: Saturation
% 3.63/1.20 % (2664770)Time elapsed: 0.005 s
% 3.63/1.20 % (2664770)Peak memory usage: 88 MB
% 3.63/1.20 % (2664770)Instructions burned: 7 (million)
% 3.63/1.20 % (2664773)Instruction limit reached!
% 3.63/1.20 % (2664773)------------------------------
% 3.63/1.20 % (2664773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (2664773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (2664773)CaDiCaL version: 2.1.3
% 3.63/1.20 % (2664773)Termination reason: Instruction limit
% 3.63/1.20 % (2664773)Termination phase: Saturation
% 3.63/1.20 % (2664773)Time elapsed: 0.045 s
% 3.63/1.20 % (2664773)Peak memory usage: 115 MB
% 3.63/1.20 % (2664773)Instructions burned: 34 (million)
% 3.63/1.20 % (2664772)Instruction limit reached!
% 3.63/1.20 % (2664772)------------------------------
% 3.63/1.20 % (2664772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.63/1.20 % (2664772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.63/1.20 % (2664772)CaDiCaL version: 2.1.3
% 3.63/1.20 % (2664772)Termination reason: Instruction limit
% 3.63/1.20 % (2664772)Termination phase: Saturation
% 3.63/1.20 % (2664772)Time elapsed: 0.056 s
% 3.63/1.20 % (2664772)Peak memory usage: 115 MB
% 3.63/1.20 % (2664772)Instructions burned: 47 (million)
% 3.63/1.20 % (2664775)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3979736117:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.63/1.20 % (2664775)Instruction limit reached!
% 3.63/1.20 % (2664775)------------------------------
% 4.90/1.41 % (2664775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.41 % (2664775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.41 % (2664775)CaDiCaL version: 2.1.3
% 4.90/1.41 % (2664775)Termination reason: Instruction limit
% 4.90/1.41 % (2664775)Termination phase: Saturation
% 4.90/1.41 % (2664775)Time elapsed: 0.006 s
% 4.90/1.41 % (2664775)Peak memory usage: 89 MB
% 4.90/1.41 % (2664775)Instructions burned: 16 (million)
% 4.90/1.41 % (2664782)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=3667485638:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.90/1.41 % (2664783)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1352030302:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.90/1.41 % (2664783)Instruction limit reached!
% 4.90/1.41 % (2664783)------------------------------
% 4.90/1.41 % (2664783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.41 % (2664783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.41 % (2664783)CaDiCaL version: 2.1.3
% 4.90/1.41 % (2664783)Termination reason: Instruction limit
% 4.90/1.41 % (2664783)Termination phase: Saturation
% 4.90/1.41 % (2664783)Time elapsed: 0.010 s
% 4.90/1.41 % (2664783)Peak memory usage: 89 MB
% 4.90/1.41 % (2664783)Instructions burned: 16 (million)
% 4.90/1.41 % (2664769)Instruction limit reached!
% 4.90/1.41 % (2664769)------------------------------
% 4.90/1.41 % (2664769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.41 % (2664769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.41 % (2664769)CaDiCaL version: 2.1.3
% 4.90/1.41 % (2664769)Termination reason: Instruction limit
% 4.90/1.41 % (2664769)Termination phase: Saturation
% 4.90/1.41 % (2664769)Time elapsed: 0.165 s
% 4.90/1.41 % (2664769)Peak memory usage: 119 MB
% 4.90/1.41 % (2664769)Instructions burned: 202 (million)
% 4.90/1.41 % (2664782)Instruction limit reached!
% 4.90/1.41 % (2664782)------------------------------
% 4.90/1.41 % (2664782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.41 % (2664782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.41 % (2664782)CaDiCaL version: 2.1.3
% 4.90/1.41 % (2664782)Termination reason: Instruction limit
% 4.90/1.41 % (2664782)Termination phase: Saturation
% 4.90/1.41 % (2664782)Time elapsed: 0.021 s
% 4.90/1.41 % (2664782)Peak memory usage: 88 MB
% 4.90/1.41 % (2664782)Instructions burned: 30 (million)
% 4.90/1.41 % (2664785)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=624940941:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.90/1.41 % (2664784)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=49579413:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.90/1.41 % (2664787)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1249556307:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.90/1.41 % (2664768)Instruction limit reached!
% 4.90/1.41 % (2664768)------------------------------
% 4.90/1.41 % (2664768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.41 % (2664768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.41 % (2664768)CaDiCaL version: 2.1.3
% 4.90/1.41 % (2664768)Termination reason: Instruction limit
% 4.90/1.41 % (2664768)Termination phase: Saturation
% 4.90/1.41 % (2664768)Time elapsed: 0.211 s
% 4.90/1.41 % (2664768)Peak memory usage: 117 MB
% 4.90/1.41 % (2664768)Instructions burned: 308 (million)
% 4.90/1.41 % (2664784)Instruction limit reached!
% 4.90/1.41 % (2664784)------------------------------
% 4.90/1.41 % (2664784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.90/1.41 % (2664784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.90/1.41 % (2664784)CaDiCaL version: 2.1.3
% 4.90/1.41 % (2664784)Termination reason: Instruction limit
% 4.90/1.41 % (2664784)Termination phase: Saturation
% 4.90/1.41 % (2664784)Time elapsed: 0.019 s
% 4.90/1.41 % (2664784)Peak memory usage: 89 MB
% 4.90/1.41 % (2664784)Instructions burned: 24 (million)
% 4.90/1.41 % (2664785)Instruction limit reached!
% 4.90/1.41 % (2664785)------------------------------
% 4.90/1.41 % (2664785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.57 % (2664785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.57 % (2664785)CaDiCaL version: 2.1.3
% 5.77/1.57 % (2664785)Termination reason: Instruction limit
% 5.77/1.57 % (2664785)Termination phase: Saturation
% 5.77/1.57 % (2664785)Time elapsed: 0.020 s
% 5.77/1.57 % (2664785)Peak memory usage: 89 MB
% 5.77/1.57 % (2664785)Instructions burned: 27 (million)
% 5.77/1.57 % (2664787)Instruction limit reached!
% 5.77/1.57 % (2664787)------------------------------
% 5.77/1.57 % (2664787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.57 % (2664787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.57 % (2664787)CaDiCaL version: 2.1.3
% 5.77/1.57 % (2664787)Termination reason: Instruction limit
% 5.77/1.57 % (2664787)Termination phase: Saturation
% 5.77/1.57 % (2664787)Time elapsed: 0.025 s
% 5.77/1.57 % (2664787)Peak memory usage: 89 MB
% 5.77/1.57 % (2664787)Instructions burned: 88 (million)
% 5.77/1.57 % (2664790)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3960845521:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.77/1.57 % (2664791)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3593404431:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.77/1.57 % (2664790)Instruction limit reached!
% 5.77/1.57 % (2664790)------------------------------
% 5.77/1.57 % (2664790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.57 % (2664790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.57 % (2664790)CaDiCaL version: 2.1.3
% 5.77/1.57 % (2664790)Termination reason: Instruction limit
% 5.77/1.57 % (2664790)Termination phase: Preprocessing 3
% 5.77/1.57 % (2664790)Time elapsed: 0.002 s
% 5.77/1.57 % (2664790)Peak memory usage: 86 MB
% 5.77/1.57 % (2664790)Instructions burned: 2 (million)
% 5.77/1.57 % (2664792)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2995063528:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.77/1.57 % (2664792)Instruction limit reached!
% 5.77/1.57 % (2664792)------------------------------
% 5.77/1.57 % (2664792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.57 % (2664792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.57 % (2664792)CaDiCaL version: 2.1.3
% 5.77/1.57 % (2664792)Termination reason: Instruction limit
% 5.77/1.57 % (2664792)Termination phase: Equality proxy
% 5.77/1.57 % (2664792)Time elapsed: 0.003 s
% 5.77/1.57 % (2664792)Peak memory usage: 86 MB
% 5.77/1.57 % (2664792)Instructions burned: 4 (million)
% 5.77/1.57 % (2664798)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=1220402555:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.77/1.57 % (2664797)lrs+10_1_thi=all:si=on:fd=off:random_seed=3431904566:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.77/1.57 % (2664796)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3199196386:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.77/1.57 % (2664798)Instruction limit reached!
% 5.77/1.57 % (2664798)------------------------------
% 5.77/1.57 % (2664798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.57 % (2664798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.57 % (2664798)CaDiCaL version: 2.1.3
% 5.77/1.57 % (2664798)Termination reason: Instruction limit
% 5.77/1.57 % (2664798)Termination phase: Saturation
% 5.77/1.57 % (2664798)Time elapsed: 0.005 s
% 5.77/1.57 % (2664798)Peak memory usage: 87 MB
% 5.77/1.57 % (2664798)Instructions burned: 9 (million)
% 5.77/1.57 % (2664799)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=564983958:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.77/1.57 % (2664799)Instruction limit reached!
% 5.77/1.57 % (2664799)------------------------------
% 5.77/1.57 % (2664799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.77/1.57 % (2664799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.77/1.57 % (2664799)CaDiCaL version: 2.1.3
% 5.77/1.57 % (2664799)Termination reason: Instruction limit
% 5.77/1.57 % (2664799)Termination phase: Saturation
% 7.20/1.77 % (2664799)Time elapsed: 0.002 s
% 7.20/1.77 % (2664799)Peak memory usage: 88 MB
% 7.20/1.77 % (2664799)Instructions burned: 4 (million)
% 7.20/1.77 % (2664797)Instruction limit reached!
% 7.20/1.77 % (2664797)------------------------------
% 7.20/1.77 % (2664797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.77 % (2664797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.77 % (2664797)CaDiCaL version: 2.1.3
% 7.20/1.77 % (2664797)Termination reason: Instruction limit
% 7.20/1.77 % (2664797)Termination phase: Saturation
% 7.20/1.77 % (2664797)Time elapsed: 0.062 s
% 7.20/1.77 % (2664797)Peak memory usage: 118 MB
% 7.20/1.77 % (2664797)Instructions burned: 53 (million)
% 7.20/1.77 % (2664796)Instruction limit reached!
% 7.20/1.77 % (2664796)------------------------------
% 7.20/1.77 % (2664796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.77 % (2664796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.77 % (2664796)CaDiCaL version: 2.1.3
% 7.20/1.77 % (2664796)Termination reason: Instruction limit
% 7.20/1.77 % (2664796)Termination phase: Saturation
% 7.20/1.77 % (2664796)Time elapsed: 0.092 s
% 7.20/1.77 % (2664796)Peak memory usage: 134 MB
% 7.20/1.77 % (2664796)Instructions burned: 67 (million)
% 7.20/1.77 % (2664791)Instruction limit reached!
% 7.20/1.77 % (2664791)------------------------------
% 7.20/1.77 % (2664791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.77 % (2664791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.77 % (2664791)CaDiCaL version: 2.1.3
% 7.20/1.77 % (2664791)Termination reason: Instruction limit
% 7.20/1.77 % (2664791)Termination phase: Saturation
% 7.20/1.77 % (2664791)Time elapsed: 0.132 s
% 7.20/1.77 % (2664791)Peak memory usage: 91 MB
% 7.20/1.77 % (2664791)Instructions burned: 181 (million)
% 7.20/1.77 % (2664802)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=4146107913:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.20/1.77 % (2664802)Instruction limit reached!
% 7.20/1.77 % (2664802)------------------------------
% 7.20/1.77 % (2664802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.77 % (2664802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.77 % (2664802)CaDiCaL version: 2.1.3
% 7.20/1.77 % (2664802)Termination reason: Instruction limit
% 7.20/1.77 % (2664802)Termination phase: Preprocessing 3
% 7.20/1.77 % (2664802)Time elapsed: 0.002 s
% 7.20/1.77 % (2664802)Peak memory usage: 86 MB
% 7.20/1.77 % (2664802)Instructions burned: 2 (million)
% 7.20/1.77 % (2664804)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1543401290:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.20/1.77 % (2664810)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=251092433:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.20/1.77 % (2664808)dis+10_1_si=on:random_seed=2492272222:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.20/1.77 % (2664810)Instruction limit reached!
% 7.20/1.77 % (2664810)------------------------------
% 7.20/1.77 % (2664810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.77 % (2664810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.77 % (2664810)CaDiCaL version: 2.1.3
% 7.20/1.77 % (2664810)Termination reason: Instruction limit
% 7.20/1.77 % (2664810)Termination phase: Saturation
% 7.20/1.77 % (2664810)Time elapsed: 0.009 s
% 7.20/1.77 % (2664810)Peak memory usage: 89 MB
% 7.20/1.77 % (2664810)Instructions burned: 27 (million)
% 7.20/1.77 % (2664808)Instruction limit reached!
% 7.20/1.77 % (2664808)------------------------------
% 7.20/1.77 % (2664808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.20/1.77 % (2664808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.20/1.77 % (2664808)CaDiCaL version: 2.1.3
% 7.20/1.77 % (2664808)Termination reason: Instruction limit
% 7.20/1.77 % (2664808)Termination phase: Saturation
% 7.20/1.77 % (2664808)Time elapsed: 0.007 s
% 7.20/1.77 % (2664808)Peak memory usage: 88 MB
% 7.20/1.77 % (2664808)Instructions burned: 11 (million)
% 7.20/1.77 % (2664811)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1471020008:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 7.20/1.77 % (2664811)Instruction limit reached!
% 9.18/2.21 % (2664811)------------------------------
% 9.18/2.21 % (2664811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664811)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664811)Termination reason: Instruction limit
% 9.18/2.21 % (2664811)Termination phase: Saturation
% 9.18/2.21 % (2664811)Time elapsed: 0.027 s
% 9.18/2.21 % (2664811)Peak memory usage: 89 MB
% 9.18/2.21 % (2664811)Instructions burned: 35 (million)
% 9.18/2.21 % (2664804)Instruction limit reached!
% 9.18/2.21 % (2664804)------------------------------
% 9.18/2.21 % (2664804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664804)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664804)Termination reason: Instruction limit
% 9.18/2.21 % (2664804)Termination phase: Saturation
% 9.18/2.21 % (2664804)Time elapsed: 0.114 s
% 9.18/2.21 % (2664804)Peak memory usage: 117 MB
% 9.18/2.21 % (2664804)Instructions burned: 128 (million)
% 9.18/2.21 % (2664812)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=3899276173:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 9.18/2.21 % (2664813)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=432779650:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 9.18/2.21 % (2664812)Instruction limit reached!
% 9.18/2.21 % (2664812)------------------------------
% 9.18/2.21 % (2664812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664812)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664812)Termination reason: Instruction limit
% 9.18/2.21 % (2664812)Termination phase: Clausification
% 9.18/2.21 % (2664812)Time elapsed: 0.002 s
% 9.18/2.21 % (2664812)Peak memory usage: 86 MB
% 9.18/2.21 % (2664812)Instructions burned: 2 (million)
% 9.18/2.21 % (2664819)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1777701870:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 9.18/2.21 % (2664815)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1016498683:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 9.18/2.21 % (2664813)Instruction limit reached!
% 9.18/2.21 % (2664813)------------------------------
% 9.18/2.21 % (2664813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664813)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664813)Termination reason: Instruction limit
% 9.18/2.21 % (2664813)Termination phase: Saturation
% 9.18/2.21 % (2664813)Time elapsed: 0.006 s
% 9.18/2.21 % (2664813)Peak memory usage: 88 MB
% 9.18/2.21 % (2664813)Instructions burned: 8 (million)
% 9.18/2.21 % (2664819)Instruction limit reached!
% 9.18/2.21 % (2664819)------------------------------
% 9.18/2.21 % (2664819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664819)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664819)Termination reason: Instruction limit
% 9.18/2.21 % (2664819)Termination phase: Saturation
% 9.18/2.21 % (2664819)Time elapsed: 0.018 s
% 9.18/2.21 % (2664819)Peak memory usage: 112 MB
% 9.18/2.21 % (2664819)Instructions burned: 14 (million)
% 9.18/2.21 % (2664820)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3950283059:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 9.18/2.21 % (2664830)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1698709437:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 9.18/2.21 % (2664826)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3945243168:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 9.18/2.21 % (2664822)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2836387444:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 9.18/2.21 % (2664829)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=4284734231:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 9.18/2.21 % (2664828)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=2256834763:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 9.18/2.21 % (2664822)Instruction limit reached!
% 9.18/2.21 % (2664822)------------------------------
% 9.18/2.21 % (2664822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664822)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664822)Termination reason: Instruction limit
% 9.18/2.21 % (2664822)Termination phase: Saturation
% 9.18/2.21 % (2664822)Time elapsed: 0.008 s
% 9.18/2.21 % (2664822)Peak memory usage: 88 MB
% 9.18/2.21 % (2664822)Instructions burned: 11 (million)
% 9.18/2.21 % (2664828)Instruction limit reached!
% 9.18/2.21 % (2664828)------------------------------
% 9.18/2.21 % (2664828)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664828)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664828)Termination reason: Instruction limit
% 9.18/2.21 % (2664828)Termination phase: Saturation
% 9.18/2.21 % (2664828)Time elapsed: 0.040 s
% 9.18/2.21 % (2664828)Peak memory usage: 89 MB
% 9.18/2.21 % (2664828)Instructions burned: 76 (million)
% 9.18/2.21 % (2664830)Instruction limit reached!
% 9.18/2.21 % (2664830)------------------------------
% 9.18/2.21 % (2664830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664830)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664830)Termination reason: Instruction limit
% 9.18/2.21 % (2664830)Termination phase: Saturation
% 9.18/2.21 % (2664830)Time elapsed: 0.059 s
% 9.18/2.21 % (2664830)Peak memory usage: 117 MB
% 9.18/2.21 % (2664830)Instructions burned: 132 (million)
% 9.18/2.21 % (2664820)Instruction limit reached!
% 9.18/2.21 % (2664820)------------------------------
% 9.18/2.21 % (2664820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664820)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664820)Termination reason: Instruction limit
% 9.18/2.21 % (2664820)Termination phase: Saturation
% 9.18/2.21 % (2664820)Time elapsed: 0.159 s
% 9.18/2.21 % (2664820)Peak memory usage: 117 MB
% 9.18/2.21 % (2664820)Instructions burned: 226 (million)
% 9.18/2.21 % (2664815)Instruction limit reached!
% 9.18/2.21 % (2664815)------------------------------
% 9.18/2.21 % (2664815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664815)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664815)Termination reason: Instruction limit
% 9.18/2.21 % (2664815)Termination phase: Saturation
% 9.18/2.21 % (2664815)Time elapsed: 0.203 s
% 9.18/2.21 % (2664815)Peak memory usage: 91 MB
% 9.18/2.21 % (2664815)Instructions burned: 370 (million)
% 9.18/2.21 % (2664826)Instruction limit reached!
% 9.18/2.21 % (2664826)------------------------------
% 9.18/2.21 % (2664826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664826)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664826)Termination reason: Instruction limit
% 9.18/2.21 % (2664826)Termination phase: Saturation
% 9.18/2.21 % (2664826)Time elapsed: 0.095 s
% 9.18/2.21 % (2664826)Peak memory usage: 133 MB
% 9.18/2.21 % (2664826)Instructions burned: 71 (million)
% 9.18/2.21 % (2664829)First to succeed.
% 9.18/2.21 % (2664829)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2664762"
% 9.18/2.21 % (2664839)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1618555010:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 9.18/2.21 % (2664837)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2171944597:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 9.18/2.21 % (2664838)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3441123079:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 9.18/2.21 % (2664840)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1299183684:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 9.18/2.21 % (2664841)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=2328355023:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 9.18/2.21 % (2664842)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=1031455205:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 9.18/2.21 % (2664838)Instruction limit reached!
% 9.18/2.21 % (2664838)------------------------------
% 9.18/2.21 % (2664838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664838)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664838)Termination reason: Instruction limit
% 9.18/2.21 % (2664838)Termination phase: Saturation
% 9.18/2.21 % (2664838)Time elapsed: 0.069 s
% 9.18/2.21 % (2664838)Peak memory usage: 134 MB
% 9.18/2.21 % (2664838)Instructions burned: 40 (million)
% 9.18/2.21 % (2664839)Instruction limit reached!
% 9.18/2.21 % (2664839)------------------------------
% 9.18/2.21 % (2664839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664839)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664839)Termination reason: Instruction limit
% 9.18/2.21 % (2664839)Termination phase: Saturation
% 9.18/2.21 % (2664839)Time elapsed: 0.110 s
% 9.18/2.21 % (2664839)Peak memory usage: 91 MB
% 9.18/2.21 % (2664839)Instructions burned: 308 (million)
% 9.18/2.21 % (2664837)Instruction limit reached!
% 9.18/2.21 % (2664837)------------------------------
% 9.18/2.21 % (2664837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664837)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664837)Termination reason: Instruction limit
% 9.18/2.21 % (2664837)Termination phase: Saturation
% 9.18/2.21 % (2664837)Time elapsed: 0.135 s
% 9.18/2.21 % (2664837)Peak memory usage: 134 MB
% 9.18/2.21 % (2664837)Instructions burned: 131 (million)
% 9.18/2.21 % (2664841)Instruction limit reached!
% 9.18/2.21 % (2664841)------------------------------
% 9.18/2.21 % (2664841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664841)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664841)Termination reason: Instruction limit
% 9.18/2.21 % (2664841)Termination phase: Saturation
% 9.18/2.21 % (2664841)Time elapsed: 0.107 s
% 9.18/2.21 % (2664841)Peak memory usage: 117 MB
% 9.18/2.21 % (2664841)Instructions burned: 132 (million)
% 9.18/2.21 % (2664840)Refutation not found, SMT solver inside AVATAR returned Unknown
% 9.18/2.21 % (2664840)------------------------------
% 9.18/2.21 % (2664840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.18/2.21 % (2664840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.18/2.21 % (2664840)CaDiCaL version: 2.1.3
% 9.18/2.21 % (2664840)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 9.18/2.21 % (2664840)Time elapsed: 0.186 s
% 9.18/2.21 % (2664840)Peak memory usage: 136 MB
% 9.18/2.21 % (2664840)Instructions burned: 178 (million)
% 9.18/2.21 % (2664840)------------------------------
% 9.18/2.21 % (2664840)------------------------------
% 9.18/2.21 % (2664829)Refutation found. Thanks to Tanya!
% 9.18/2.21 % SZS status Theorem for theBenchmark
% 9.18/2.21 % SZS output start Proof for theBenchmark
% See solution above
% 10.13/2.42 % (2664829)------------------------------
% 10.13/2.42 % (2664829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.13/2.42 % (2664829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.13/2.42 % (2664829)CaDiCaL version: 2.1.3
% 10.13/2.42 % (2664829)Termination reason: Refutation
% 10.13/2.42 % (2664829)Time elapsed: 0.129 s
% 10.13/2.42 % (2664829)Peak memory usage: 92 MB
% 10.13/2.42 % (2664829)Instructions burned: 197 (million)
% 10.13/2.42 % (2664829)------------------------------
% 10.13/2.42 % (2664829)------------------------------
% 10.13/2.42 % (2664762)Success in time 1.558 s
% 10.13/2.42 % Vampire exiting
%------------------------------------------------------------------------------