%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW666_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 : n004.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:05 PM UTC 2026
% Result : Theorem 10.17s 2.33s
% Output : Refutation 11.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 25
% Syntax : Number of formulae : 94 ( 21 unt; 0 typ; 22 def)
% Number of atoms : 561 ( 168 equ)
% Maximal formula atoms : 54 ( 5 avg)
% Number of connectives : 631 ( 164 ~; 74 |; 282 &)
% ( 29 <=>; 82 =>; 0 <=; 0 <~>)
% Maximal formula depth : 65 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number arithmetic : 1098 ( 284 atm; 0 fun; 766 num; 48 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 : 33 ( 29 usr; 23 prp; 0-2 aty)
% Number of functors : 57 ( 46 usr; 29 con; 0-5 aty)
% Number of variables : 121 ( 95 !; 26 ?; 121 :)
% 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,
map_int_int: $tType ).
tff(type_def_10,type,
array_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,
map: ( ty * ty ) > ty ).
tff(func_def_13,type,
get: ( ty * ty * uni * uni ) > uni ).
tff(func_def_14,type,
set: ( ty * ty * uni * uni * uni ) > uni ).
tff(func_def_15,type,
const: ( ty * ty * uni ) > uni ).
tff(func_def_16,type,
array: ty > ty ).
tff(func_def_17,type,
mk_array1: ( ty * $int * uni ) > uni ).
tff(func_def_18,type,
length1: ( ty * uni ) > $int ).
tff(func_def_19,type,
elts: ( ty * uni ) > uni ).
tff(func_def_20,type,
get2: ( ty * uni * $int ) > uni ).
tff(func_def_21,type,
t2tb: $int > uni ).
tff(func_def_22,type,
tb2t: uni > $int ).
tff(func_def_23,type,
set2: ( ty * uni * $int * uni ) > uni ).
tff(func_def_24,type,
make1: ( ty * $int * uni ) > uni ).
tff(func_def_25,type,
t2tb1: map_int_int > uni ).
tff(func_def_26,type,
tb2t1: uni > map_int_int ).
tff(func_def_27,type,
occ1: ( ty * uni * uni * $int * $int ) > $int ).
tff(func_def_31,type,
t2tb2: array_int > uni ).
tff(func_def_32,type,
tb2t2: uni > array_int ).
tff(func_def_43,type,
sK0: ( ty * $int * uni * uni * $int ) > $int ).
tff(func_def_44,type,
sK1: map_int_int ).
tff(func_def_45,type,
sK2: map_int_int ).
tff(func_def_46,type,
sK3: map_int_int ).
tff(func_def_47,type,
sK4: map_int_int ).
tff(func_def_48,type,
sK5: map_int_int ).
tff(func_def_49,type,
sK6: map_int_int ).
tff(func_def_50,type,
sK7: map_int_int ).
tff(func_def_51,type,
sK8: map_int_int ).
tff(func_def_52,type,
sK9: map_int_int ).
tff(func_def_53,type,
sK10: map_int_int ).
tff(func_def_54,type,
sK11: ( uni * uni * ty * $int * $int ) > $int ).
tff(func_def_55,type,
sK12: ( map_int_int * $int ) > $int ).
tff(func_def_56,type,
sK13: ( $int * map_int_int ) > $int ).
tff(func_def_57,type,
sK14: ( $int * ty * uni * uni * $int ) > $int ).
tff(func_def_58,type,
sK15: ( $int * map_int_int ) > $int ).
tff(func_def_59,type,
sK16: ( $int * map_int_int ) > $int ).
tff(func_def_60,type,
sK17: ( $int * map_int_int * $int ) > $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(pred_def_3,type,
injective2: ( map_int_int * $int ) > $o ).
tff(pred_def_5,type,
surjective2: ( map_int_int * $int ) > $o ).
tff(pred_def_6,type,
range2: ( map_int_int * $int ) > $o ).
tff(pred_def_7,type,
injective3: ( array_int * $int ) > $o ).
tff(pred_def_8,type,
surjective3: ( array_int * $int ) > $o ).
tff(pred_def_9,type,
range3: ( array_int * $int ) > $o ).
tff(f32,axiom,
! [X0: map_int_int,X1: $int] :
( injective2(X0,X1)
<=> ! [X3: $int,X2: $int] :
( ( $lesseq(0,X2)
& $less(X2,X1) )
=> ( ( $less(X3,X1)
& $lesseq(0,X3) )
=> ( ( X2 != X3 )
=> ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) != tb2t(get(int,int,t2tb1(X0),t2tb(X3))) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',injective_def) ).
tff(f34,axiom,
! [X0: map_int_int,X1: $int] :
( range2(X0,X1)
<=> ! [X2: $int] :
( ( $less(X2,X1)
& $lesseq(0,X2) )
=> ( $lesseq(0,tb2t(get(int,int,t2tb1(X0),t2tb(X2))))
& $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',range_def) ).
tff(f52,conjecture,
( $lesseq(0,10)
=> ( $lesseq(0,10)
=> ( ( $lesseq(0,0)
& $less(0,10) )
=> ! [X0: map_int_int] :
( ( ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(9))) )
& $lesseq(0,10) )
=> ( ( $lesseq(0,1)
& $less(1,10) )
=> ! [X1: map_int_int] :
( ( ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(1),t2tb(3))) )
& $lesseq(0,10) )
=> ( ( $lesseq(0,2)
& $less(2,10) )
=> ! [X2: map_int_int] :
( ( ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(2),t2tb(8))) )
& $lesseq(0,10) )
=> ( ( $lesseq(0,3)
& $less(3,10) )
=> ! [X3: map_int_int] :
( ( ( X3 = tb2t1(set(int,int,t2tb1(X2),t2tb(3),t2tb(2))) )
& $lesseq(0,10) )
=> ( ( $less(4,10)
& $lesseq(0,4) )
=> ! [X4: map_int_int] :
( ( $lesseq(0,10)
& ( X4 = tb2t1(set(int,int,t2tb1(X3),t2tb(4),t2tb(7))) ) )
=> ( ( $less(5,10)
& $lesseq(0,5) )
=> ! [X5: map_int_int] :
( ( ( X5 = tb2t1(set(int,int,t2tb1(X4),t2tb(5),t2tb(4))) )
& $lesseq(0,10) )
=> ( ( $less(6,10)
& $lesseq(0,6) )
=> ! [X6: map_int_int] :
( ( $lesseq(0,10)
& ( X6 = tb2t1(set(int,int,t2tb1(X5),t2tb(6),t2tb(0))) ) )
=> ( ( $less(7,10)
& $lesseq(0,7) )
=> ! [X7: map_int_int] :
( ( $lesseq(0,10)
& ( X7 = tb2t1(set(int,int,t2tb1(X6),t2tb(7),t2tb(1))) ) )
=> ( ( $lesseq(0,8)
& $less(8,10) )
=> ! [X8: map_int_int] :
( ( ( X8 = tb2t1(set(int,int,t2tb1(X7),t2tb(8),t2tb(5))) )
& $lesseq(0,10) )
=> ( ( $less(9,10)
& $lesseq(0,9) )
=> ! [X9: map_int_int] :
( ( $lesseq(0,10)
& ( X9 = tb2t1(set(int,int,t2tb1(X8),t2tb(9),t2tb(6))) ) )
=> ( ( ( tb2t(get(int,int,t2tb1(X9),t2tb(6))) = 0 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(3))) = 2 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(7))) = 1 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(2))) = 8 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(4))) = 7 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(5))) = 4 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(9))) = 6 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(1))) = 3 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(8))) = 5 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 9 ) )
=> ( range2(X9,10)
& injective2(X9,10) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wP_parameter_test) ).
tff(f53,negated_conjecture,
~ ( $lesseq(0,10)
=> ( $lesseq(0,10)
=> ( ( $lesseq(0,0)
& $less(0,10) )
=> ! [X0: map_int_int] :
( ( ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(9))) )
& $lesseq(0,10) )
=> ( ( $lesseq(0,1)
& $less(1,10) )
=> ! [X1: map_int_int] :
( ( ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(1),t2tb(3))) )
& $lesseq(0,10) )
=> ( ( $lesseq(0,2)
& $less(2,10) )
=> ! [X2: map_int_int] :
( ( ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(2),t2tb(8))) )
& $lesseq(0,10) )
=> ( ( $lesseq(0,3)
& $less(3,10) )
=> ! [X3: map_int_int] :
( ( ( X3 = tb2t1(set(int,int,t2tb1(X2),t2tb(3),t2tb(2))) )
& $lesseq(0,10) )
=> ( ( $less(4,10)
& $lesseq(0,4) )
=> ! [X4: map_int_int] :
( ( $lesseq(0,10)
& ( X4 = tb2t1(set(int,int,t2tb1(X3),t2tb(4),t2tb(7))) ) )
=> ( ( $less(5,10)
& $lesseq(0,5) )
=> ! [X5: map_int_int] :
( ( ( X5 = tb2t1(set(int,int,t2tb1(X4),t2tb(5),t2tb(4))) )
& $lesseq(0,10) )
=> ( ( $less(6,10)
& $lesseq(0,6) )
=> ! [X6: map_int_int] :
( ( $lesseq(0,10)
& ( X6 = tb2t1(set(int,int,t2tb1(X5),t2tb(6),t2tb(0))) ) )
=> ( ( $less(7,10)
& $lesseq(0,7) )
=> ! [X7: map_int_int] :
( ( $lesseq(0,10)
& ( X7 = tb2t1(set(int,int,t2tb1(X6),t2tb(7),t2tb(1))) ) )
=> ( ( $lesseq(0,8)
& $less(8,10) )
=> ! [X8: map_int_int] :
( ( ( X8 = tb2t1(set(int,int,t2tb1(X7),t2tb(8),t2tb(5))) )
& $lesseq(0,10) )
=> ( ( $less(9,10)
& $lesseq(0,9) )
=> ! [X9: map_int_int] :
( ( $lesseq(0,10)
& ( X9 = tb2t1(set(int,int,t2tb1(X8),t2tb(9),t2tb(6))) ) )
=> ( ( ( tb2t(get(int,int,t2tb1(X9),t2tb(6))) = 0 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(3))) = 2 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(7))) = 1 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(2))) = 8 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(4))) = 7 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(5))) = 4 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(9))) = 6 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(1))) = 3 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(8))) = 5 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 9 ) )
=> ( range2(X9,10)
& injective2(X9,10) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f52]) ).
tff(f59,plain,
~ ( ~ $less(10,0)
=> ( ~ $less(10,0)
=> ( ( ~ $less(0,0)
& $less(0,10) )
=> ! [X0: map_int_int] :
( ( ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(9))) )
& ~ $less(10,0) )
=> ( ( $less(1,10)
& ~ $less(1,0) )
=> ! [X1: map_int_int] :
( ( ~ $less(10,0)
& ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(1),t2tb(3))) ) )
=> ( ( ~ $less(2,0)
& $less(2,10) )
=> ! [X2: map_int_int] :
( ( ~ $less(10,0)
& ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(2),t2tb(8))) ) )
=> ( ( $less(3,10)
& ~ $less(3,0) )
=> ! [X3: map_int_int] :
( ( ( X3 = tb2t1(set(int,int,t2tb1(X2),t2tb(3),t2tb(2))) )
& ~ $less(10,0) )
=> ( ( $less(4,10)
& ~ $less(4,0) )
=> ! [X4: map_int_int] :
( ( ~ $less(10,0)
& ( X4 = tb2t1(set(int,int,t2tb1(X3),t2tb(4),t2tb(7))) ) )
=> ( ( ~ $less(5,0)
& $less(5,10) )
=> ! [X5: map_int_int] :
( ( ( X5 = tb2t1(set(int,int,t2tb1(X4),t2tb(5),t2tb(4))) )
& ~ $less(10,0) )
=> ( ( $less(6,10)
& ~ $less(6,0) )
=> ! [X6: map_int_int] :
( ( ( X6 = tb2t1(set(int,int,t2tb1(X5),t2tb(6),t2tb(0))) )
& ~ $less(10,0) )
=> ( ( $less(7,10)
& ~ $less(7,0) )
=> ! [X7: map_int_int] :
( ( ~ $less(10,0)
& ( X7 = tb2t1(set(int,int,t2tb1(X6),t2tb(7),t2tb(1))) ) )
=> ( ( ~ $less(8,0)
& $less(8,10) )
=> ! [X8: map_int_int] :
( ( ~ $less(10,0)
& ( X8 = tb2t1(set(int,int,t2tb1(X7),t2tb(8),t2tb(5))) ) )
=> ( ( ~ $less(9,0)
& $less(9,10) )
=> ! [X9: map_int_int] :
( ( ~ $less(10,0)
& ( X9 = tb2t1(set(int,int,t2tb1(X8),t2tb(9),t2tb(6))) ) )
=> ( ( ( tb2t(get(int,int,t2tb1(X9),t2tb(6))) = 0 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(3))) = 2 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(7))) = 1 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(2))) = 8 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(4))) = 7 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(5))) = 4 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(9))) = 6 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(1))) = 3 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(8))) = 5 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 9 ) )
=> ( range2(X9,10)
& injective2(X9,10) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(theory_normalization,[],[f53]) ).
tff(f62,plain,
! [X1: $int,X0: map_int_int] :
( range2(X0,X1)
<=> ! [X2: $int] :
( ( ~ $less(X2,0)
& $less(X2,X1) )
=> ( $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),X1)
& ~ $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),0) ) ) ),
inference(theory_normalization,[],[f34]) ).
tff(f67,plain,
! [X0: map_int_int,X1: $int] :
( injective2(X0,X1)
<=> ! [X3: $int,X2: $int] :
( ( ~ $less(X2,0)
& $less(X2,X1) )
=> ( ( $less(X3,X1)
& ~ $less(X3,0) )
=> ( ( X2 != X3 )
=> ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) != tb2t(get(int,int,t2tb1(X0),t2tb(X3))) ) ) ) ) ),
inference(theory_normalization,[],[f32]) ).
tff(f113,plain,
! [X0: map_int_int,X1: $int] :
( ! [X3: $int,X2: $int] :
( ( ~ $less(X3,0)
& $less(X3,X1) )
=> ( ( ~ $less(X2,0)
& $less(X2,X1) )
=> ( ( X2 != X3 )
=> ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) != tb2t(get(int,int,t2tb1(X0),t2tb(X3))) ) ) ) )
<=> injective2(X0,X1) ),
inference(rectify,[],[f67]) ).
tff(f117,plain,
! [X1: $int,X0: map_int_int] :
( ! [X2: $int] :
( ( ~ $less(X2,0)
& $less(X2,X1) )
=> ( $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),X1)
& ~ $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),0) ) )
=> range2(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f62]) ).
tff(f120,plain,
! [X1: $int,X0: map_int_int] :
( range2(X0,X1)
| ? [X2: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),X1)
| $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),0) )
& ~ $less(X2,0)
& $less(X2,X1) ) ),
inference(ennf_transformation,[],[f117]) ).
tff(f121,plain,
! [X0: map_int_int,X1: $int] :
( ? [X2: $int] :
( ( ~ $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),X1)
| $less(tb2t(get(int,int,t2tb1(X0),t2tb(X2))),0) )
& $less(X2,X1)
& ~ $less(X2,0) )
| range2(X0,X1) ),
inference(flattening,[],[f120]) ).
tff(f136,plain,
! [X0: map_int_int,X1: $int] :
( ! [X3: $int,X2: $int] :
( ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) != tb2t(get(int,int,t2tb1(X0),t2tb(X3))) )
| ( X2 = X3 )
| $less(X2,0)
| ~ $less(X2,X1)
| $less(X3,0)
| ~ $less(X3,X1) )
<=> injective2(X0,X1) ),
inference(ennf_transformation,[],[f113]) ).
tff(f137,plain,
! [X1: $int,X0: map_int_int] :
( ! [X2: $int,X3: $int] :
( $less(X3,0)
| ~ $less(X2,X1)
| ~ $less(X3,X1)
| ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) != tb2t(get(int,int,t2tb1(X0),t2tb(X3))) )
| ( X2 = X3 )
| $less(X2,0) )
<=> injective2(X0,X1) ),
inference(flattening,[],[f136]) ).
tff(f145,plain,
( ? [X0: map_int_int] :
( ? [X1: map_int_int] :
( ? [X2: map_int_int] :
( ? [X3: map_int_int] :
( ? [X4: map_int_int] :
( ? [X5: map_int_int] :
( ? [X6: map_int_int] :
( ? [X7: map_int_int] :
( ? [X8: map_int_int] :
( ? [X9: map_int_int] :
( ( ~ range2(X9,10)
| ~ injective2(X9,10) )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(6))) = 0 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(3))) = 2 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(7))) = 1 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(2))) = 8 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(4))) = 7 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(5))) = 4 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(9))) = 6 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(1))) = 3 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(8))) = 5 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 9 )
& ~ $less(10,0)
& ( X9 = tb2t1(set(int,int,t2tb1(X8),t2tb(9),t2tb(6))) ) )
& ~ $less(9,0)
& $less(9,10)
& ~ $less(10,0)
& ( X8 = tb2t1(set(int,int,t2tb1(X7),t2tb(8),t2tb(5))) ) )
& ~ $less(8,0)
& $less(8,10)
& ~ $less(10,0)
& ( X7 = tb2t1(set(int,int,t2tb1(X6),t2tb(7),t2tb(1))) ) )
& $less(7,10)
& ~ $less(7,0)
& ( X6 = tb2t1(set(int,int,t2tb1(X5),t2tb(6),t2tb(0))) )
& ~ $less(10,0) )
& $less(6,10)
& ~ $less(6,0)
& ( X5 = tb2t1(set(int,int,t2tb1(X4),t2tb(5),t2tb(4))) )
& ~ $less(10,0) )
& ~ $less(5,0)
& $less(5,10)
& ~ $less(10,0)
& ( X4 = tb2t1(set(int,int,t2tb1(X3),t2tb(4),t2tb(7))) ) )
& $less(4,10)
& ~ $less(4,0)
& ( X3 = tb2t1(set(int,int,t2tb1(X2),t2tb(3),t2tb(2))) )
& ~ $less(10,0) )
& $less(3,10)
& ~ $less(3,0)
& ~ $less(10,0)
& ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(2),t2tb(8))) ) )
& ~ $less(2,0)
& $less(2,10)
& ~ $less(10,0)
& ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(1),t2tb(3))) ) )
& $less(1,10)
& ~ $less(1,0)
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(9))) )
& ~ $less(10,0) )
& ~ $less(0,0)
& $less(0,10)
& ~ $less(10,0)
& ~ $less(10,0) ),
inference(ennf_transformation,[],[f59]) ).
tff(f146,plain,
( ? [X0: map_int_int] :
( ? [X1: map_int_int] :
( ~ $less(2,0)
& ( X1 = tb2t1(set(int,int,t2tb1(X0),t2tb(1),t2tb(3))) )
& ? [X2: map_int_int] :
( ? [X3: map_int_int] :
( ~ $less(10,0)
& $less(4,10)
& ~ $less(4,0)
& ( X3 = tb2t1(set(int,int,t2tb1(X2),t2tb(3),t2tb(2))) )
& ? [X4: map_int_int] :
( ( X4 = tb2t1(set(int,int,t2tb1(X3),t2tb(4),t2tb(7))) )
& ~ $less(10,0)
& $less(5,10)
& ~ $less(5,0)
& ? [X5: map_int_int] :
( ~ $less(6,0)
& ( X5 = tb2t1(set(int,int,t2tb1(X4),t2tb(5),t2tb(4))) )
& ~ $less(10,0)
& $less(6,10)
& ? [X6: map_int_int] :
( ~ $less(7,0)
& ~ $less(10,0)
& $less(7,10)
& ( X6 = tb2t1(set(int,int,t2tb1(X5),t2tb(6),t2tb(0))) )
& ? [X7: map_int_int] :
( ? [X8: map_int_int] :
( $less(9,10)
& ( X8 = tb2t1(set(int,int,t2tb1(X7),t2tb(8),t2tb(5))) )
& ? [X9: map_int_int] :
( ( tb2t(get(int,int,t2tb1(X9),t2tb(2))) = 8 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(8))) = 5 )
& ( ~ range2(X9,10)
| ~ injective2(X9,10) )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(3))) = 2 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(7))) = 1 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(0))) = 9 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(5))) = 4 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(6))) = 0 )
& ( X9 = tb2t1(set(int,int,t2tb1(X8),t2tb(9),t2tb(6))) )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(9))) = 6 )
& ( tb2t(get(int,int,t2tb1(X9),t2tb(4))) = 7 )
& ~ $less(10,0)
& ( tb2t(get(int,int,t2tb1(X9),t2tb(1))) = 3 ) )
& ~ $less(9,0)
& ~ $less(10,0) )
& ~ $less(10,0)
& ~ $less(8,0)
& ( X7 = tb2t1(set(int,int,t2tb1(X6),t2tb(7),t2tb(1))) )
& $less(8,10) ) ) ) ) )
& ~ $less(10,0)
& $less(3,10)
& ( X2 = tb2t1(set(int,int,t2tb1(X1),t2tb(2),t2tb(8))) )
& ~ $less(3,0) )
& $less(2,10)
& ~ $less(10,0) )
& ( X0 = tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(9))) )
& ~ $less(10,0)
& $less(1,10)
& ~ $less(1,0) )
& ~ $less(10,0)
& $less(0,10)
& ~ $less(10,0)
& ~ $less(0,0) ),
inference(flattening,[],[f145]) ).
tff(f169,plain,
( ~ $less(2,0)
& ( sK2 = tb2t1(set(int,int,t2tb1(sK1),t2tb(1),t2tb(3))) )
& ~ $less(10,0)
& $less(4,10)
& ~ $less(4,0)
& ( tb2t1(set(int,int,t2tb1(sK3),t2tb(3),t2tb(2))) = sK4 )
& ( sK5 = tb2t1(set(int,int,t2tb1(sK4),t2tb(4),t2tb(7))) )
& ~ $less(10,0)
& $less(5,10)
& ~ $less(5,0)
& ~ $less(6,0)
& ( sK6 = tb2t1(set(int,int,t2tb1(sK5),t2tb(5),t2tb(4))) )
& ~ $less(10,0)
& $less(6,10)
& ~ $less(7,0)
& ~ $less(10,0)
& $less(7,10)
& ( tb2t1(set(int,int,t2tb1(sK6),t2tb(6),t2tb(0))) = sK7 )
& $less(9,10)
& ( tb2t1(set(int,int,t2tb1(sK8),t2tb(8),t2tb(5))) = sK9 )
& ( 8 = tb2t(get(int,int,t2tb1(sK10),t2tb(2))) )
& ( 5 = tb2t(get(int,int,t2tb1(sK10),t2tb(8))) )
& ( ~ range2(sK10,10)
| ~ injective2(sK10,10) )
& ( 2 = tb2t(get(int,int,t2tb1(sK10),t2tb(3))) )
& ( 1 = tb2t(get(int,int,t2tb1(sK10),t2tb(7))) )
& ( 9 = tb2t(get(int,int,t2tb1(sK10),t2tb(0))) )
& ( 4 = tb2t(get(int,int,t2tb1(sK10),t2tb(5))) )
& ( 0 = tb2t(get(int,int,t2tb1(sK10),t2tb(6))) )
& ( sK10 = tb2t1(set(int,int,t2tb1(sK9),t2tb(9),t2tb(6))) )
& ( 6 = tb2t(get(int,int,t2tb1(sK10),t2tb(9))) )
& ( 7 = tb2t(get(int,int,t2tb1(sK10),t2tb(4))) )
& ~ $less(10,0)
& ( 3 = tb2t(get(int,int,t2tb1(sK10),t2tb(1))) )
& ~ $less(9,0)
& ~ $less(10,0)
& ~ $less(10,0)
& ~ $less(8,0)
& ( tb2t1(set(int,int,t2tb1(sK7),t2tb(7),t2tb(1))) = sK8 )
& $less(8,10)
& ~ $less(10,0)
& $less(3,10)
& ( sK3 = tb2t1(set(int,int,t2tb1(sK2),t2tb(2),t2tb(8))) )
& ~ $less(3,0)
& $less(2,10)
& ~ $less(10,0)
& ( tb2t1(set(int,int,const(int,int,t2tb(0)),t2tb(0),t2tb(9))) = sK1 )
& ~ $less(10,0)
& $less(1,10)
& ~ $less(1,0)
& ~ $less(10,0)
& $less(0,10)
& ~ $less(10,0)
& ~ $less(0,0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10]),skolemize(X0,sK1),skolemize(X1,sK2),skolemize(X2,sK3),skolemize(X3,sK4),skolemize(X4,sK5),skolemize(X5,sK6),skolemize(X6,sK7),skolemize(X7,sK8),skolemize(X8,sK9),skolemize(X9,sK10)],[f146]) ).
tff(f176,plain,
! [X0: map_int_int,X1: $int] :
( ( ( ~ $less(tb2t(get(int,int,t2tb1(X0),t2tb(sK12(X0,X1)))),X1)
| $less(tb2t(get(int,int,t2tb1(X0),t2tb(sK12(X0,X1)))),0) )
& $less(sK12(X0,X1),X1)
& ~ $less(sK12(X0,X1),0) )
| range2(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(X2,sK12(X0,X1))],[f121]) ).
tff(f188,plain,
! [X1: $int,X0: map_int_int] :
( ( ! [X2: $int,X3: $int] :
( $less(X3,0)
| ~ $less(X2,X1)
| ~ $less(X3,X1)
| ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) != tb2t(get(int,int,t2tb1(X0),t2tb(X3))) )
| ( X2 = X3 )
| $less(X2,0) )
| ~ injective2(X0,X1) )
& ( injective2(X0,X1)
| ? [X2: $int,X3: $int] :
( ~ $less(X3,0)
& $less(X2,X1)
& $less(X3,X1)
& ( tb2t(get(int,int,t2tb1(X0),t2tb(X2))) = tb2t(get(int,int,t2tb1(X0),t2tb(X3))) )
& ( X2 != X3 )
& ~ $less(X2,0) ) ) ),
inference(nnf_transformation,[],[f137]) ).
tff(f189,plain,
! [X0: $int,X1: map_int_int] :
( ( ! [X2: $int,X3: $int] :
( $less(X3,0)
| ~ $less(X2,X0)
| ~ $less(X3,X0)
| ( tb2t(get(int,int,t2tb1(X1),t2tb(X2))) != tb2t(get(int,int,t2tb1(X1),t2tb(X3))) )
| ( X2 = X3 )
| $less(X2,0) )
| ~ injective2(X1,X0) )
& ( injective2(X1,X0)
| ? [X4: $int,X5: $int] :
( ~ $less(X5,0)
& $less(X4,X0)
& $less(X5,X0)
& ( tb2t(get(int,int,t2tb1(X1),t2tb(X5))) = tb2t(get(int,int,t2tb1(X1),t2tb(X4))) )
& ( X4 != X5 )
& ~ $less(X4,0) ) ) ),
inference(rectify,[],[f188]) ).
tff(f190,plain,
! [X0: $int,X1: map_int_int] :
( ( ! [X2: $int,X3: $int] :
( $less(X3,0)
| ~ $less(X2,X0)
| ~ $less(X3,X0)
| ( tb2t(get(int,int,t2tb1(X1),t2tb(X2))) != tb2t(get(int,int,t2tb1(X1),t2tb(X3))) )
| ( X2 = X3 )
| $less(X2,0) )
| ~ injective2(X1,X0) )
& ( injective2(X1,X0)
| ( ~ $less(sK16(X0,X1),0)
& $less(sK15(X0,X1),X0)
& $less(sK16(X0,X1),X0)
& ( tb2t(get(int,int,t2tb1(X1),t2tb(sK16(X0,X1)))) = tb2t(get(int,int,t2tb1(X1),t2tb(sK15(X0,X1)))) )
& ( sK16(X0,X1) != sK15(X0,X1) )
& ~ $less(sK15(X0,X1),0) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15,sK16]),skolemize(X4,sK15(X0,X1)),skolemize(X5,sK16(X0,X1))],[f189]) ).
tff(f237,plain,
3 = tb2t(get(int,int,t2tb1(sK10),t2tb(1))),
inference(cnf_transformation,[],[f169]) ).
tff(f239,plain,
7 = tb2t(get(int,int,t2tb1(sK10),t2tb(4))),
inference(cnf_transformation,[],[f169]) ).
tff(f240,plain,
6 = tb2t(get(int,int,t2tb1(sK10),t2tb(9))),
inference(cnf_transformation,[],[f169]) ).
tff(f242,plain,
0 = tb2t(get(int,int,t2tb1(sK10),t2tb(6))),
inference(cnf_transformation,[],[f169]) ).
tff(f243,plain,
4 = tb2t(get(int,int,t2tb1(sK10),t2tb(5))),
inference(cnf_transformation,[],[f169]) ).
tff(f244,plain,
9 = tb2t(get(int,int,t2tb1(sK10),t2tb(0))),
inference(cnf_transformation,[],[f169]) ).
tff(f245,plain,
1 = tb2t(get(int,int,t2tb1(sK10),t2tb(7))),
inference(cnf_transformation,[],[f169]) ).
tff(f246,plain,
2 = tb2t(get(int,int,t2tb1(sK10),t2tb(3))),
inference(cnf_transformation,[],[f169]) ).
tff(f247,plain,
( ~ range2(sK10,10)
| ~ injective2(sK10,10) ),
inference(cnf_transformation,[],[f169]) ).
tff(f248,plain,
5 = tb2t(get(int,int,t2tb1(sK10),t2tb(8))),
inference(cnf_transformation,[],[f169]) ).
tff(f249,plain,
8 = tb2t(get(int,int,t2tb1(sK10),t2tb(2))),
inference(cnf_transformation,[],[f169]) ).
tff(f280,plain,
! [X0: map_int_int,X1: $int] :
( range2(X0,X1)
| ~ $less(sK12(X0,X1),0) ),
inference(cnf_transformation,[],[f176]) ).
tff(f281,plain,
! [X0: map_int_int,X1: $int] :
( range2(X0,X1)
| $less(sK12(X0,X1),X1) ),
inference(cnf_transformation,[],[f176]) ).
tff(f282,plain,
! [X0: map_int_int,X1: $int] :
( range2(X0,X1)
| ~ $less(tb2t(get(int,int,t2tb1(X0),t2tb(sK12(X0,X1)))),X1)
| $less(tb2t(get(int,int,t2tb1(X0),t2tb(sK12(X0,X1)))),0) ),
inference(cnf_transformation,[],[f176]) ).
tff(f299,plain,
! [X0: $int,X1: map_int_int] :
( injective2(X1,X0)
| ~ $less(sK15(X0,X1),0) ),
inference(cnf_transformation,[],[f190]) ).
tff(f300,plain,
! [X0: $int,X1: map_int_int] :
( injective2(X1,X0)
| ( sK16(X0,X1) != sK15(X0,X1) ) ),
inference(cnf_transformation,[],[f190]) ).
tff(f301,plain,
! [X0: $int,X1: map_int_int] :
( injective2(X1,X0)
| ( tb2t(get(int,int,t2tb1(X1),t2tb(sK16(X0,X1)))) = tb2t(get(int,int,t2tb1(X1),t2tb(sK15(X0,X1)))) ) ),
inference(cnf_transformation,[],[f190]) ).
tff(f302,plain,
! [X0: $int,X1: map_int_int] :
( injective2(X1,X0)
| $less(sK16(X0,X1),X0) ),
inference(cnf_transformation,[],[f190]) ).
tff(f303,plain,
! [X0: $int,X1: map_int_int] :
( injective2(X1,X0)
| $less(sK15(X0,X1),X0) ),
inference(cnf_transformation,[],[f190]) ).
tff(f304,plain,
! [X0: $int,X1: map_int_int] :
( injective2(X1,X0)
| ~ $less(sK16(X0,X1),0) ),
inference(cnf_transformation,[],[f190]) ).
tff(f341,definition,
( spl18_5
<=> ( 5 = tb2t(get(int,int,t2tb1(sK10),t2tb(8))) ) ),
introduced(definition,[new_symbols(definition,[spl18_5])],[avatar_definition]) ).
tff(f344,plain,
spl18_5,
inference(avatar_split_clause,[],[f248,f341]) ).
tff(f356,definition,
( spl18_8
<=> ( 1 = tb2t(get(int,int,t2tb1(sK10),t2tb(7))) ) ),
introduced(definition,[new_symbols(definition,[spl18_8])],[avatar_definition]) ).
tff(f359,plain,
spl18_8,
inference(avatar_split_clause,[],[f245,f356]) ).
tff(f361,definition,
( spl18_9
<=> ( 9 = tb2t(get(int,int,t2tb1(sK10),t2tb(0))) ) ),
introduced(definition,[new_symbols(definition,[spl18_9])],[avatar_definition]) ).
tff(f364,plain,
spl18_9,
inference(avatar_split_clause,[],[f244,f361]) ).
tff(f366,definition,
( spl18_10
<=> ( 8 = tb2t(get(int,int,t2tb1(sK10),t2tb(2))) ) ),
introduced(definition,[new_symbols(definition,[spl18_10])],[avatar_definition]) ).
tff(f369,plain,
spl18_10,
inference(avatar_split_clause,[],[f249,f366]) ).
tff(f371,definition,
( spl18_11
<=> ( 7 = tb2t(get(int,int,t2tb1(sK10),t2tb(4))) ) ),
introduced(definition,[new_symbols(definition,[spl18_11])],[avatar_definition]) ).
tff(f374,plain,
spl18_11,
inference(avatar_split_clause,[],[f239,f371]) ).
tff(f381,definition,
( spl18_13
<=> ( 0 = tb2t(get(int,int,t2tb1(sK10),t2tb(6))) ) ),
introduced(definition,[new_symbols(definition,[spl18_13])],[avatar_definition]) ).
tff(f384,plain,
spl18_13,
inference(avatar_split_clause,[],[f242,f381]) ).
tff(f386,definition,
( spl18_14
<=> ( 3 = tb2t(get(int,int,t2tb1(sK10),t2tb(1))) ) ),
introduced(definition,[new_symbols(definition,[spl18_14])],[avatar_definition]) ).
tff(f389,plain,
spl18_14,
inference(avatar_split_clause,[],[f237,f386]) ).
tff(f391,definition,
( spl18_15
<=> ( 6 = tb2t(get(int,int,t2tb1(sK10),t2tb(9))) ) ),
introduced(definition,[new_symbols(definition,[spl18_15])],[avatar_definition]) ).
tff(f394,plain,
spl18_15,
inference(avatar_split_clause,[],[f240,f391]) ).
tff(f396,definition,
( spl18_16
<=> ( 4 = tb2t(get(int,int,t2tb1(sK10),t2tb(5))) ) ),
introduced(definition,[new_symbols(definition,[spl18_16])],[avatar_definition]) ).
tff(f399,plain,
spl18_16,
inference(avatar_split_clause,[],[f243,f396]) ).
tff(f416,definition,
( spl18_20
<=> injective2(sK10,10) ),
introduced(definition,[new_symbols(definition,[spl18_20])],[avatar_definition]) ).
tff(f418,plain,
( ~ injective2(sK10,10)
| spl18_20 ),
inference(avatar_component_clause,[],[f416]) ).
tff(f420,definition,
( spl18_21
<=> range2(sK10,10) ),
introduced(definition,[new_symbols(definition,[spl18_21])],[avatar_definition]) ).
tff(f422,plain,
( ~ range2(sK10,10)
| spl18_21 ),
inference(avatar_component_clause,[],[f420]) ).
tff(f423,plain,
( ~ spl18_20
| ~ spl18_21 ),
inference(avatar_split_clause,[],[f247,f420,f416]) ).
tff(f425,definition,
( spl18_22
<=> ( 2 = tb2t(get(int,int,t2tb1(sK10),t2tb(3))) ) ),
introduced(definition,[new_symbols(definition,[spl18_22])],[avatar_definition]) ).
tff(f428,plain,
spl18_22,
inference(avatar_split_clause,[],[f246,f425]) ).
tff(f568,plain,
( ~ $less(sK12(sK10,10),0)
| spl18_21 ),
inference(resolution,[],[f280,f422]) ).
tff(f570,definition,
( spl18_44
<=> $less(sK12(sK10,10),0) ),
introduced(definition,[new_symbols(definition,[spl18_44])],[avatar_definition]) ).
tff(f573,plain,
( ~ spl18_44
| spl18_21 ),
inference(avatar_split_clause,[],[f568,f420,f570]) ).
tff(f574,plain,
( $less(sK12(sK10,10),10)
| spl18_21 ),
inference(unit_resulting_resolution,[],[f281,f422]) ).
tff(f577,definition,
( spl18_45
<=> $less(sK12(sK10,10),10) ),
introduced(definition,[new_symbols(definition,[spl18_45])],[avatar_definition]) ).
tff(f580,plain,
( spl18_45
| spl18_21 ),
inference(avatar_split_clause,[],[f574,f420,f577]) ).
tff(f625,plain,
( ( sK15(10,sK10) != sK16(10,sK10) )
| spl18_20 ),
inference(unit_resulting_resolution,[],[f300,f418]) ).
tff(f627,plain,
( $less(sK15(10,sK10),10)
| spl18_20 ),
inference(unit_resulting_resolution,[],[f303,f418]) ).
tff(f631,plain,
( ~ $less(sK16(10,sK10),0)
| spl18_20 ),
inference(resolution,[],[f418,f304]) ).
tff(f633,plain,
( $less(sK16(10,sK10),10)
| spl18_20 ),
inference(resolution,[],[f418,f302]) ).
tff(f634,plain,
( ~ $less(sK15(10,sK10),0)
| spl18_20 ),
inference(resolution,[],[f418,f299]) ).
tff(f636,definition,
( spl18_49
<=> $less(sK16(10,sK10),0) ),
introduced(definition,[new_symbols(definition,[spl18_49])],[avatar_definition]) ).
tff(f639,plain,
( ~ spl18_49
| spl18_20 ),
inference(avatar_split_clause,[],[f631,f416,f636]) ).
tff(f641,definition,
( spl18_50
<=> $less(sK15(10,sK10),0) ),
introduced(definition,[new_symbols(definition,[spl18_50])],[avatar_definition]) ).
tff(f644,plain,
( ~ spl18_50
| spl18_20 ),
inference(avatar_split_clause,[],[f634,f416,f641]) ).
tff(f646,definition,
( spl18_51
<=> $less(sK15(10,sK10),10) ),
introduced(definition,[new_symbols(definition,[spl18_51])],[avatar_definition]) ).
tff(f649,plain,
( spl18_51
| spl18_20 ),
inference(avatar_split_clause,[],[f627,f416,f646]) ).
tff(f651,definition,
( spl18_52
<=> ( sK15(10,sK10) = sK16(10,sK10) ) ),
introduced(definition,[new_symbols(definition,[spl18_52])],[avatar_definition]) ).
tff(f654,plain,
( ~ spl18_52
| spl18_20 ),
inference(avatar_split_clause,[],[f625,f416,f651]) ).
tff(f656,definition,
( spl18_53
<=> $less(sK16(10,sK10),10) ),
introduced(definition,[new_symbols(definition,[spl18_53])],[avatar_definition]) ).
tff(f659,plain,
( spl18_53
| spl18_20 ),
inference(avatar_split_clause,[],[f633,f416,f656]) ).
tff(f1063,plain,
( $less(tb2t(get(int,int,t2tb1(sK10),t2tb(sK12(sK10,10)))),0)
| ~ $less(tb2t(get(int,int,t2tb1(sK10),t2tb(sK12(sK10,10)))),10)
| spl18_21 ),
inference(resolution,[],[f282,f422]) ).
tff(f1065,definition,
( spl18_56
<=> $less(tb2t(get(int,int,t2tb1(sK10),t2tb(sK12(sK10,10)))),0) ),
introduced(definition,[new_symbols(definition,[spl18_56])],[avatar_definition]) ).
tff(f1069,definition,
( spl18_57
<=> $less(tb2t(get(int,int,t2tb1(sK10),t2tb(sK12(sK10,10)))),10) ),
introduced(definition,[new_symbols(definition,[spl18_57])],[avatar_definition]) ).
tff(f1072,plain,
( spl18_56
| ~ spl18_57
| spl18_21 ),
inference(avatar_split_clause,[],[f1063,f420,f1069,f1065]) ).
tff(f1078,plain,
( ( tb2t(get(int,int,t2tb1(sK10),t2tb(sK16(10,sK10)))) = tb2t(get(int,int,t2tb1(sK10),t2tb(sK15(10,sK10)))) )
| spl18_20 ),
inference(unit_resulting_resolution,[],[f301,f418]) ).
tff(f1090,definition,
( spl18_58
<=> ( tb2t(get(int,int,t2tb1(sK10),t2tb(sK16(10,sK10)))) = tb2t(get(int,int,t2tb1(sK10),t2tb(sK15(10,sK10)))) ) ),
introduced(definition,[new_symbols(definition,[spl18_58])],[avatar_definition]) ).
tff(f1093,plain,
( spl18_58
| spl18_20 ),
inference(avatar_split_clause,[],[f1078,f416,f1090]) ).
tff(f1094,plain,
$false,
inference(avatar_smt_refutation,[],[f1093,f1072,f659,f654,f649,f644,f639,f580,f573,f428,f423,f399,f394,f389,f384,f374,f369,f364,f359,f344]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW666_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n004.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:24:37 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.39/1.65 % (385630)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.39/1.65 % (385774)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1895038678:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.39/1.65 % (385774)Instruction limit reached!
% 5.39/1.65 % (385774)------------------------------
% 5.39/1.65 % (385774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.65 % (385774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.65 % (385774)CaDiCaL version: 2.1.3
% 5.39/1.65 % (385774)Termination reason: Instruction limit
% 5.39/1.65 % (385774)Termination phase: Saturation
% 5.39/1.65 % (385774)Time elapsed: 0.018 s
% 5.39/1.65 % (385774)Peak memory usage: 112 MB
% 5.39/1.65 % (385774)Instructions burned: 14 (million)
% 5.39/1.65 % (385778)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2829928822:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.39/1.65 % (385779)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3387254907:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.39/1.65 % (385776)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1543467166:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.39/1.65 % (385777)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=650969521:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.39/1.65 % (385779)Instruction limit reached!
% 5.39/1.65 % (385779)------------------------------
% 5.39/1.65 % (385779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.65 % (385779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.65 % (385779)CaDiCaL version: 2.1.3
% 5.39/1.65 % (385779)Termination reason: Instruction limit
% 5.39/1.65 % (385779)Termination phase: Property scanning
% 5.39/1.65 % (385779)Time elapsed: 0.005 s
% 5.39/1.65 % (385779)Peak memory usage: 86 MB
% 5.39/1.65 % (385779)Instructions burned: 5 (million)
% 5.39/1.65 % (385778)Instruction limit reached!
% 5.39/1.65 % (385778)------------------------------
% 5.39/1.65 % (385778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.65 % (385778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.65 % (385778)CaDiCaL version: 2.1.3
% 5.39/1.65 % (385778)Termination reason: Instruction limit
% 5.39/1.65 % (385778)Termination phase: Saturation
% 5.39/1.65 % (385778)Time elapsed: 0.007 s
% 5.39/1.65 % (385778)Peak memory usage: 86 MB
% 5.39/1.65 % (385778)Instructions burned: 7 (million)
% 5.39/1.65 % (385782)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3937019409:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.39/1.65 % (385780)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2800666635:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.39/1.65 % (385782)Instruction limit reached!
% 5.39/1.65 % (385782)------------------------------
% 5.39/1.65 % (385782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.65 % (385782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.65 % (385782)CaDiCaL version: 2.1.3
% 5.39/1.65 % (385782)Termination reason: Instruction limit
% 5.39/1.65 % (385782)Termination phase: Saturation
% 5.39/1.65 % (385782)Time elapsed: 0.065 s
% 5.39/1.65 % (385782)Peak memory usage: 116 MB
% 5.39/1.65 % (385782)Instructions burned: 34 (million)
% 5.39/1.65 % (385780)Instruction limit reached!
% 5.39/1.65 % (385780)------------------------------
% 5.39/1.65 % (385780)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.39/1.65 % (385780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.65 % (385780)CaDiCaL version: 2.1.3
% 5.39/1.65 % (385780)Termination reason: Instruction limit
% 5.39/1.65 % (385780)Termination phase: Saturation
% 5.39/1.65 % (385780)Time elapsed: 0.077 s
% 5.39/1.65 % (385780)Peak memory usage: 115 MB
% 5.39/1.65 % (385780)Instructions burned: 46 (million)
% 5.39/1.65 % (385787)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2719479687:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 5.39/1.65 % (385787)Instruction limit reached!
% 5.39/1.65 % (385787)------------------------------
% 5.39/1.65 % (385787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.86 % (385787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.86 % (385787)CaDiCaL version: 2.1.3
% 7.06/1.86 % (385787)Termination reason: Instruction limit
% 7.06/1.86 % (385787)Termination phase: Saturation
% 7.06/1.86 % (385787)Time elapsed: 0.016 s
% 7.06/1.86 % (385787)Peak memory usage: 89 MB
% 7.06/1.86 % (385787)Instructions burned: 14 (million)
% 7.06/1.86 % (385794)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=4270058547:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 7.06/1.86 % (385794)Instruction limit reached!
% 7.06/1.86 % (385794)------------------------------
% 7.06/1.86 % (385794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.86 % (385794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.86 % (385794)CaDiCaL version: 2.1.3
% 7.06/1.86 % (385794)Termination reason: Instruction limit
% 7.06/1.86 % (385794)Termination phase: Saturation
% 7.06/1.86 % (385794)Time elapsed: 0.019 s
% 7.06/1.86 % (385794)Peak memory usage: 89 MB
% 7.06/1.86 % (385794)Instructions burned: 30 (million)
% 7.06/1.86 % (385777)Instruction limit reached!
% 7.06/1.86 % (385777)------------------------------
% 7.06/1.86 % (385777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.86 % (385777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.86 % (385777)CaDiCaL version: 2.1.3
% 7.06/1.86 % (385777)Termination reason: Instruction limit
% 7.06/1.86 % (385777)Termination phase: Saturation
% 7.06/1.86 % (385777)Time elapsed: 0.243 s
% 7.06/1.86 % (385777)Peak memory usage: 118 MB
% 7.06/1.86 % (385777)Instructions burned: 201 (million)
% 7.06/1.86 % (385795)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=639374147:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 7.06/1.86 % (385776)Instruction limit reached!
% 7.06/1.86 % (385776)------------------------------
% 7.06/1.86 % (385776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.86 % (385776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.86 % (385776)CaDiCaL version: 2.1.3
% 7.06/1.86 % (385776)Termination reason: Instruction limit
% 7.06/1.86 % (385776)Termination phase: Saturation
% 7.06/1.86 % (385776)Time elapsed: 0.296 s
% 7.06/1.86 % (385776)Peak memory usage: 117 MB
% 7.06/1.86 % (385776)Instructions burned: 307 (million)
% 7.06/1.86 % (385795)Instruction limit reached!
% 7.06/1.86 % (385795)------------------------------
% 7.06/1.86 % (385795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.86 % (385795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.86 % (385795)CaDiCaL version: 2.1.3
% 7.06/1.86 % (385795)Termination reason: Instruction limit
% 7.06/1.86 % (385795)Termination phase: Saturation
% 7.06/1.86 % (385795)Time elapsed: 0.018 s
% 7.06/1.86 % (385795)Peak memory usage: 89 MB
% 7.06/1.86 % (385795)Instructions burned: 16 (million)
% 7.06/1.86 % (385803)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2923116077:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 7.06/1.86 % (385803)Instruction limit reached!
% 7.06/1.86 % (385803)------------------------------
% 7.06/1.86 % (385803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.86 % (385803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.06/1.86 % (385803)CaDiCaL version: 2.1.3
% 7.06/1.86 % (385803)Termination reason: Instruction limit
% 7.06/1.86 % (385803)Termination phase: Saturation
% 7.06/1.86 % (385803)Time elapsed: 0.029 s
% 7.06/1.86 % (385803)Peak memory usage: 89 MB
% 7.06/1.86 % (385803)Instructions burned: 24 (million)
% 7.06/1.86 % (385804)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=309132281:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 7.06/1.86 % (385810)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=3726145476:i=181:rtra=on:ss=axioms:ev=cautious_2995 on theBenchmark for (2995ds/181Mi)
% 7.06/1.86 % (385804)Instruction limit reached!
% 7.06/1.86 % (385804)------------------------------
% 7.06/1.86 % (385804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.06/1.86 % (385804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.48/2.21 % (385804)CaDiCaL version: 2.1.3
% 10.48/2.21 % (385804)Termination reason: Instruction limit
% 10.48/2.21 % (385804)Termination phase: Saturation
% 10.48/2.21 % (385804)Time elapsed: 0.030 s
% 10.48/2.21 % (385804)Peak memory usage: 89 MB
% 10.48/2.21 % (385804)Instructions burned: 27 (million)
% 10.48/2.21 % (385806)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=810080249:i=85:gtgl=4:rtra=on:gtg=exists_sym_2995 on theBenchmark for (2995ds/85Mi)
% 10.48/2.21 % (385808)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=576076840:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 10.48/2.21 % (385808)Instruction limit reached!
% 10.48/2.21 % (385808)------------------------------
% 10.48/2.21 % (385808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.48/2.21 % (385808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.48/2.21 % (385808)CaDiCaL version: 2.1.3
% 10.48/2.21 % (385808)Termination reason: Instruction limit
% 10.48/2.21 % (385808)Termination phase: Unused predicate definition removal
% 10.48/2.21 % (385808)Time elapsed: 0.003 s
% 10.48/2.21 % (385808)Peak memory usage: 85 MB
% 10.48/2.21 % (385808)Instructions burned: 2 (million)
% 10.48/2.21 % (385806)Instruction limit reached!
% 10.48/2.21 % (385806)------------------------------
% 10.48/2.21 % (385806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.48/2.21 % (385806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.48/2.21 % (385806)CaDiCaL version: 2.1.3
% 10.48/2.21 % (385806)Termination reason: Instruction limit
% 10.48/2.21 % (385806)Termination phase: Saturation
% 10.48/2.21 % (385806)Time elapsed: 0.070 s
% 10.48/2.21 % (385806)Peak memory usage: 89 MB
% 10.48/2.21 % (385806)Instructions burned: 85 (million)
% 10.48/2.21 % (385810)Instruction limit reached!
% 10.48/2.21 % (385810)------------------------------
% 10.48/2.21 % (385810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.48/2.21 % (385810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.48/2.21 % (385810)CaDiCaL version: 2.1.3
% 10.48/2.21 % (385810)Termination reason: Instruction limit
% 10.48/2.21 % (385810)Termination phase: Saturation
% 10.48/2.21 % (385810)Time elapsed: 0.111 s
% 10.48/2.21 % (385810)Peak memory usage: 92 MB
% 10.48/2.21 % (385810)Instructions burned: 181 (million)
% 10.48/2.21 % (385814)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1219926572:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 10.48/2.21 % (385813)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3918563741:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 10.48/2.21 % (385813)Instruction limit reached!
% 10.48/2.21 % (385813)------------------------------
% 10.48/2.21 % (385813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.48/2.21 % (385813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.48/2.21 % (385813)CaDiCaL version: 2.1.3
% 10.48/2.21 % (385813)Termination reason: Instruction limit
% 10.48/2.21 % (385813)Termination phase: Preprocessing 3
% 10.48/2.21 % (385813)Time elapsed: 0.005 s
% 10.48/2.21 % (385813)Peak memory usage: 86 MB
% 10.48/2.21 % (385813)Instructions burned: 4 (million)
% 10.48/2.21 % (385816)lrs+10_1_thi=all:si=on:fd=off:random_seed=712284096:i=53:rtra=on:gtg=all_2993 on theBenchmark for (2993ds/53Mi)
% 10.48/2.21 % (385814)Instruction limit reached!
% 10.48/2.21 % (385814)------------------------------
% 10.48/2.21 % (385814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.48/2.21 % (385814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.48/2.21 % (385814)CaDiCaL version: 2.1.3
% 10.48/2.21 % (385814)Termination reason: Instruction limit
% 10.48/2.21 % (385814)Termination phase: Saturation
% 10.48/2.21 % (385814)Time elapsed: 0.125 s
% 10.48/2.21 % (385814)Peak memory usage: 134 MB
% 10.48/2.21 % (385814)Instructions burned: 66 (million)
% 10.48/2.21 % (385829)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3626417691:i=2:doe=on:canc=force:asg=cautious:rtra=on_2992 on theBenchmark for (2992ds/2Mi)
% 10.48/2.21 % (385829)Instruction limit reached!
% 10.48/2.21 % (385829)------------------------------
% 10.48/2.21 % (385829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.48/2.21 % (385829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385829)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385829)Termination reason: Instruction limit
% 10.17/2.33 % (385829)Termination phase: Preprocessing 3
% 10.17/2.33 % (385829)Time elapsed: 0.002 s
% 10.17/2.33 % (385829)Peak memory usage: 86 MB
% 10.17/2.33 % (385829)Instructions burned: 3 (million)
% 10.17/2.33 % (385820)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=1446139841:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2993 on theBenchmark for (2993ds/8Mi)
% 10.17/2.33 % (385820)Instruction limit reached!
% 10.17/2.33 % (385820)------------------------------
% 10.17/2.33 % (385820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385820)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385820)Termination reason: Instruction limit
% 10.17/2.33 % (385820)Termination phase: Property scanning
% 10.17/2.33 % (385820)Time elapsed: 0.009 s
% 10.17/2.33 % (385820)Peak memory usage: 87 MB
% 10.17/2.33 % (385820)Instructions burned: 9 (million)
% 10.17/2.33 % (385816)Instruction limit reached!
% 10.17/2.33 % (385816)------------------------------
% 10.17/2.33 % (385816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385816)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385816)Termination reason: Instruction limit
% 10.17/2.33 % (385816)Termination phase: Saturation
% 10.17/2.33 % (385816)Time elapsed: 0.097 s
% 10.17/2.33 % (385816)Peak memory usage: 116 MB
% 10.17/2.33 % (385816)Instructions burned: 53 (million)
% 10.17/2.33 % (385827)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1486252159:st=3:i=2:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/2Mi)
% 10.17/2.33 % (385827)Instruction limit reached!
% 10.17/2.33 % (385827)------------------------------
% 10.17/2.33 % (385827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385827)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385827)Termination reason: Instruction limit
% 10.17/2.33 % (385827)Termination phase: Preprocessing 2
% 10.17/2.33 % (385827)Time elapsed: 0.003 s
% 10.17/2.33 % (385827)Peak memory usage: 86 MB
% 10.17/2.33 % (385827)Instructions burned: 2 (million)
% 10.17/2.33 % (385831)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=547844386:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 10.17/2.33 % (385835)dis+10_1_si=on:random_seed=1720549450:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.17/2.33 % (385835)Instruction limit reached!
% 10.17/2.33 % (385835)------------------------------
% 10.17/2.33 % (385835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385835)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385835)Termination reason: Instruction limit
% 10.17/2.33 % (385835)Termination phase: Saturation
% 10.17/2.33 % (385835)Time elapsed: 0.012 s
% 10.17/2.33 % (385835)Peak memory usage: 88 MB
% 10.17/2.33 % (385835)Instructions burned: 10 (million)
% 10.17/2.33 % (385837)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=281362827:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 10.17/2.33 % (385837)Instruction limit reached!
% 10.17/2.33 % (385837)------------------------------
% 10.17/2.33 % (385837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385837)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385837)Termination reason: Instruction limit
% 10.17/2.33 % (385837)Termination phase: Saturation
% 10.17/2.33 % (385837)Time elapsed: 0.028 s
% 10.17/2.33 % (385837)Peak memory usage: 89 MB
% 10.17/2.33 % (385837)Instructions burned: 27 (million)
% 10.17/2.33 % (385840)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2082711796: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_2990 on theBenchmark for (2990ds/35Mi)
% 10.17/2.33 % (385840)Instruction limit reached!
% 10.17/2.33 % (385840)------------------------------
% 10.17/2.33 % (385840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385840)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385840)Termination reason: Instruction limit
% 10.17/2.33 % (385840)Termination phase: Saturation
% 10.17/2.33 % (385840)Time elapsed: 0.022 s
% 10.17/2.33 % (385840)Peak memory usage: 89 MB
% 10.17/2.33 % (385840)Instructions burned: 35 (million)
% 10.17/2.33 % (385831)First to succeed.
% 10.17/2.33 % (385831)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-385630"
% 10.17/2.33 % (385841)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1397475445:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 10.17/2.33 % (385841)Instruction limit reached!
% 10.17/2.33 % (385841)------------------------------
% 10.17/2.33 % (385841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385841)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385841)Termination reason: Instruction limit
% 10.17/2.33 % (385841)Termination phase: Unused predicate definition removal
% 10.17/2.33 % (385841)Time elapsed: 0.003 s
% 10.17/2.33 % (385841)Peak memory usage: 86 MB
% 10.17/2.33 % (385841)Instructions burned: 2 (million)
% 10.17/2.33 % (385844)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2014800648:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 10.17/2.33 % (385843)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2912584415:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 10.17/2.33 % (385843)Instruction limit reached!
% 10.17/2.33 % (385843)------------------------------
% 10.17/2.33 % (385843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385843)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385843)Termination reason: Instruction limit
% 10.17/2.33 % (385843)Termination phase: Saturation
% 10.17/2.33 % (385843)Time elapsed: 0.009 s
% 10.17/2.33 % (385843)Peak memory usage: 88 MB
% 10.17/2.33 % (385843)Instructions burned: 8 (million)
% 10.17/2.33 % (385850)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3826933071:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 10.17/2.33 % (385850)Instruction limit reached!
% 10.17/2.33 % (385850)------------------------------
% 10.17/2.33 % (385850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385850)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385850)Termination reason: Instruction limit
% 10.17/2.33 % (385850)Termination phase: Saturation
% 10.17/2.33 % (385850)Time elapsed: 0.041 s
% 10.17/2.33 % (385850)Peak memory usage: 111 MB
% 10.17/2.33 % (385850)Instructions burned: 13 (million)
% 10.17/2.33 % (385855)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=35080768:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 10.17/2.33 % (385853)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=4030796619:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 10.17/2.33 % (385855)Instruction limit reached!
% 10.17/2.33 % (385855)------------------------------
% 10.17/2.33 % (385855)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385855)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385855)Termination reason: Instruction limit
% 10.17/2.33 % (385855)Termination phase: Saturation
% 10.17/2.33 % (385855)Time elapsed: 0.007 s
% 10.17/2.33 % (385855)Peak memory usage: 88 MB
% 10.17/2.33 % (385855)Instructions burned: 11 (million)
% 10.17/2.33 % (385857)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1267690883:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 10.17/2.33 % (385862)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=1644975442:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 10.17/2.33 % (385860)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=3574189189:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 10.17/2.33 % (385844)Instruction limit reached!
% 10.17/2.33 % (385844)------------------------------
% 10.17/2.33 % (385844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385844)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385844)Termination reason: Instruction limit
% 10.17/2.33 % (385844)Termination phase: Saturation
% 10.17/2.33 % (385844)Time elapsed: 0.320 s
% 10.17/2.33 % (385844)Peak memory usage: 92 MB
% 10.17/2.33 % (385844)Instructions burned: 370 (million)
% 10.17/2.33 % (385860)Instruction limit reached!
% 10.17/2.33 % (385860)------------------------------
% 10.17/2.33 % (385860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.17/2.33 % (385860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.17/2.33 % (385860)CaDiCaL version: 2.1.3
% 10.17/2.33 % (385860)Termination reason: Instruction limit
% 10.17/2.33 % (385860)Termination phase: Saturation
% 10.17/2.33 % (385860)Time elapsed: 0.084 s
% 10.17/2.33 % (385860)Peak memory usage: 90 MB
% 10.17/2.33 % (385860)Instructions burned: 76 (million)
% 10.17/2.33 % (385831)Refutation found. Thanks to Tanya!
% 10.17/2.33 % SZS status Theorem for theBenchmark
% 10.17/2.33 % SZS output start Proof for theBenchmark
% See solution above
% 11.82/2.57 % (385831)------------------------------
% 11.82/2.57 % (385831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.82/2.57 % (385831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.82/2.57 % (385831)CaDiCaL version: 2.1.3
% 11.82/2.57 % (385831)Termination reason: Refutation
% 11.82/2.57 % (385831)Time elapsed: 0.174 s
% 11.82/2.57 % (385831)Peak memory usage: 118 MB
% 11.82/2.57 % (385831)Instructions burned: 124 (million)
% 11.82/2.57 % (385831)------------------------------
% 11.82/2.57 % (385831)------------------------------
% 11.82/2.57 % (385630)Success in time 1.582 s
% 11.82/2.57 % Vampire exiting
%------------------------------------------------------------------------------