%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT329_1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 09:47:46 AM UTC 2026
% Result : Unsatisfiable 25.63s 4.32s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 67
% Syntax : Number of formulae : 227 ( 75 unt; 0 typ; 64 def)
% Number of atoms : 639 ( 197 equ)
% Maximal formula atoms : 19 ( 2 avg)
% Number of connectives : 689 ( 277 ~; 267 |; 89 &)
% ( 45 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 494 ( 206 atm; 72 fun; 118 num; 98 var)
% Number of types : 3 ( 2 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 51 ( 45 usr; 46 prp; 0-2 aty)
% Number of functors : 38 ( 32 usr; 22 con; 0-3 aty)
% Number of variables : 137 ( 116 !; 21 ?; 137 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Array[Int,Int]': $tType ).
tff(type_def_6,type,
'Queue': $tType ).
tff(func_def_0,type,
size: 'Queue' > $int ).
tff(func_def_1,type,
elems: 'Queue' > 'Array[Int,Int]' ).
tff(func_def_2,type,
'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]': ( 'Array[Int,Int]' * $int * $int ) > 'Array[Int,Int]' ).
tff(func_def_3,type,
'const:(Int)>Array[Int,Int]': $int > 'Array[Int,Int]' ).
tff(func_def_4,type,
'select:(Array[Int,Int]*Int)>Int': ( 'Array[Int,Int]' * $int ) > $int ).
tff(func_def_5,type,
key: $int > $int ).
tff(func_def_11,type,
sK0: $int ).
tff(func_def_12,type,
sK1: 'Queue' ).
tff(func_def_13,type,
sK2: 'Array[Int,Int]' > $int ).
tff(func_def_14,type,
sK3: 'Array[Int,Int]' > 'Array[Int,Int]' ).
tff(func_def_15,type,
sK4: 'Array[Int,Int]' > $int ).
tff(func_def_16,type,
sK5: ( 'Array[Int,Int]' * 'Array[Int,Int]' ) > $int ).
tff(func_def_17,type,
sF6: 'Array[Int,Int]' ).
tff(func_def_18,type,
sF7: $int ).
tff(func_def_19,type,
sF8: $int ).
tff(func_def_20,type,
sF9: 'Array[Int,Int]' ).
tff(func_def_21,type,
sF10: $int ).
tff(func_def_22,type,
sF11: $int ).
tff(func_def_23,type,
sF12: $int ).
tff(func_def_24,type,
sF13: 'Array[Int,Int]' ).
tff(func_def_25,type,
sF14: $int ).
tff(func_def_26,type,
sF15: 'Array[Int,Int]' ).
tff(func_def_27,type,
sF16: $int ).
tff(func_def_28,type,
sF17: $int ).
tff(func_def_29,type,
sF18: $int ).
tff(func_def_30,type,
sF19: $int ).
tff(func_def_31,type,
sF20: $int ).
tff(func_def_32,type,
sF21: $int > $int ).
tff(func_def_33,type,
sF22: $int > $int ).
tff(func_def_34,type,
sF23: $int ).
tff(func_def_35,type,
sF24: $int ).
tff(func_def_36,type,
sF25: ( $int * $int ) > $int ).
tff(f1,negated_conjecture,
~ ! [X1: 'Queue',X0: $int] :
? [X2: 'Array[Int,Int]'] :
( ( ( $greater(X0,0)
& $less(X0,size(X1))
& ~ $lesseq(key('select:(Array[Int,Int]*Int)>Int'(X2,X0)),key('select:(Array[Int,Int]*Int)>Int'(X2,$difference(X0,1))))
& $greatereq(X0,0)
& ! [X3: $int,X4: $int] :
( ( $greater(X3,0)
& ( X0 != X3 )
& $less(X4,X3)
& $greatereq(X4,0)
& $less(X3,size(X1)) )
=> $lesseq(key('select:(Array[Int,Int]*Int)>Int'(X2,X3)),key('select:(Array[Int,Int]*Int)>Int'(X2,X4))) ) )
=> ! [X4: $int,X5: 'Array[Int,Int]',X3: $int] :
? [X6: $int] :
( ( X6 = $difference(X0,1) )
& ( ( ( X5 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X6,'select:(Array[Int,Int]*Int)>Int'(X2,X0)),X0,'select:(Array[Int,Int]*Int)>Int'(X2,X6)) )
& $greatereq(X4,0)
& $greater(X3,0)
& $less(X4,X3)
& $less(X3,size(X1))
& ( X3 != X6 ) )
=> $lesseq(key('select:(Array[Int,Int]*Int)>Int'(X5,X3)),key('select:(Array[Int,Int]*Int)>Int'(X5,X4))) ) ) )
& ( X2 = elems(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1) ).
tff(f2,axiom,
! [X1: $int,X2: $int,X0: 'Array[Int,Int]'] : ( 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X0,X1,X2),X1) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2) ).
tff(f3,axiom,
! [X3: $int,X0: 'Array[Int,Int]',X1: $int,X2: $int] :
( ( X1 != X2 )
=> ( 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X0,X1,X3),X2) = 'select:(Array[Int,Int]*Int)>Int'(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_3) ).
tff(f6,plain,
~ ! [X1: 'Queue',X0: $int] :
? [X2: 'Array[Int,Int]'] :
( ( ( $less(0,X0)
& $less(X0,size(X1))
& $less(key('select:(Array[Int,Int]*Int)>Int'(X2,$sum(X0,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(X2,X0)))
& ~ $less(X0,0)
& ! [X3: $int,X4: $int] :
( ( $less(0,X3)
& ( X0 != X3 )
& $less(X4,X3)
& ~ $less(X4,0)
& $less(X3,size(X1)) )
=> ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X2,X4)),key('select:(Array[Int,Int]*Int)>Int'(X2,X3))) ) )
=> ! [X4: $int,X5: 'Array[Int,Int]',X3: $int] :
? [X6: $int] :
( ( $sum(X0,$uminus(1)) = X6 )
& ( ( ( X5 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X6,'select:(Array[Int,Int]*Int)>Int'(X2,X0)),X0,'select:(Array[Int,Int]*Int)>Int'(X2,X6)) )
& ~ $less(X4,0)
& $less(0,X3)
& $less(X4,X3)
& $less(X3,size(X1))
& ( X3 != X6 ) )
=> ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X5,X4)),key('select:(Array[Int,Int]*Int)>Int'(X5,X3))) ) ) )
& ( X2 = elems(X1) ) ),
inference(theory_normalization,[],[f1]) ).
tff(f8,plain,
! [X2: $int,X0: $int,X1: 'Array[Int,Int]',X3: $int] :
( ( X2 != X3 )
=> ( 'select:(Array[Int,Int]*Int)>Int'(X1,X3) = 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X1,X2,X0),X3) ) ),
inference(rectify,[],[f3]) ).
tff(f9,plain,
~ ! [X1: $int,X0: 'Queue'] :
? [X2: 'Array[Int,Int]'] :
( ( ( $less(X1,size(X0))
& ! [X4: $int,X3: $int] :
( ( $less(X4,X3)
& ( X1 != X3 )
& ~ $less(X4,0)
& $less(0,X3)
& $less(X3,size(X0)) )
=> ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X2,X4)),key('select:(Array[Int,Int]*Int)>Int'(X2,X3))) )
& ~ $less(X1,0)
& $less(0,X1)
& $less(key('select:(Array[Int,Int]*Int)>Int'(X2,$sum(X1,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(X2,X1))) )
=> ! [X5: $int,X7: $int,X6: 'Array[Int,Int]'] :
? [X8: $int] :
( ( $sum(X1,$uminus(1)) = X8 )
& ( ( ( 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X8,'select:(Array[Int,Int]*Int)>Int'(X2,X1)),X1,'select:(Array[Int,Int]*Int)>Int'(X2,X8)) = X6 )
& $less(X5,X7)
& $less(0,X7)
& $less(X7,size(X0))
& ( X7 != X8 )
& ~ $less(X5,0) )
=> ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X6,X5)),key('select:(Array[Int,Int]*Int)>Int'(X6,X7))) ) ) )
& ( elems(X0) = X2 ) ),
inference(rectify,[],[f6]) ).
tff(f10,plain,
! [X0: $int,X2: 'Array[Int,Int]',X1: $int] : ( 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X0,X1),X0) = X1 ),
inference(rectify,[],[f2]) ).
tff(f13,plain,
? [X1: $int,X0: 'Queue'] :
! [X2: 'Array[Int,Int]'] :
( ( ? [X5: $int,X7: $int,X6: 'Array[Int,Int]'] :
! [X8: $int] :
( ( $sum(X1,$uminus(1)) != X8 )
| ( $less(key('select:(Array[Int,Int]*Int)>Int'(X6,X5)),key('select:(Array[Int,Int]*Int)>Int'(X6,X7)))
& ( 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X8,'select:(Array[Int,Int]*Int)>Int'(X2,X1)),X1,'select:(Array[Int,Int]*Int)>Int'(X2,X8)) = X6 )
& $less(X5,X7)
& $less(0,X7)
& $less(X7,size(X0))
& ( X7 != X8 )
& ~ $less(X5,0) ) )
& $less(X1,size(X0))
& ! [X4: $int,X3: $int] :
( ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X2,X4)),key('select:(Array[Int,Int]*Int)>Int'(X2,X3)))
| ~ $less(X4,X3)
| ( X1 = X3 )
| $less(X4,0)
| ~ $less(0,X3)
| ~ $less(X3,size(X0)) )
& ~ $less(X1,0)
& $less(0,X1)
& $less(key('select:(Array[Int,Int]*Int)>Int'(X2,$sum(X1,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(X2,X1))) )
| ( elems(X0) != X2 ) ),
inference(ennf_transformation,[],[f9]) ).
tff(f14,plain,
? [X1: $int,X0: 'Queue'] :
! [X2: 'Array[Int,Int]'] :
( ( elems(X0) != X2 )
| ( ? [X7: $int,X6: 'Array[Int,Int]',X5: $int] :
! [X8: $int] :
( ( $sum(X1,$uminus(1)) != X8 )
| ( $less(X7,size(X0))
& ( 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X8,'select:(Array[Int,Int]*Int)>Int'(X2,X1)),X1,'select:(Array[Int,Int]*Int)>Int'(X2,X8)) = X6 )
& $less(0,X7)
& ~ $less(X5,0)
& $less(key('select:(Array[Int,Int]*Int)>Int'(X6,X5)),key('select:(Array[Int,Int]*Int)>Int'(X6,X7)))
& ( X7 != X8 )
& $less(X5,X7) ) )
& ~ $less(X1,0)
& ! [X3: $int,X4: $int] :
( $less(X4,0)
| ~ $less(X4,X3)
| ( X1 = X3 )
| ~ $less(X3,size(X0))
| ~ $less(0,X3)
| ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X2,X4)),key('select:(Array[Int,Int]*Int)>Int'(X2,X3))) )
& $less(key('select:(Array[Int,Int]*Int)>Int'(X2,$sum(X1,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(X2,X1)))
& $less(0,X1)
& $less(X1,size(X0)) ) ),
inference(flattening,[],[f13]) ).
tff(f15,plain,
! [X2: $int,X3: $int,X1: 'Array[Int,Int]',X0: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(X1,X3) = 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X1,X2,X0),X3) )
| ( X2 = X3 ) ),
inference(ennf_transformation,[],[f8]) ).
tff(f16,plain,
? [X0: $int,X1: 'Queue'] :
! [X2: 'Array[Int,Int]'] :
( ( elems(X1) != X2 )
| ( ? [X3: $int,X4: 'Array[Int,Int]',X5: $int] :
! [X6: $int] :
( ( $sum(X0,$uminus(1)) != X6 )
| ( $less(X3,size(X1))
& ( 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X6,'select:(Array[Int,Int]*Int)>Int'(X2,X0)),X0,'select:(Array[Int,Int]*Int)>Int'(X2,X6)) = X4 )
& $less(0,X3)
& ~ $less(X5,0)
& $less(key('select:(Array[Int,Int]*Int)>Int'(X4,X5)),key('select:(Array[Int,Int]*Int)>Int'(X4,X3)))
& ( X3 != X6 )
& $less(X5,X3) ) )
& ~ $less(X0,0)
& ! [X7: $int,X8: $int] :
( $less(X8,0)
| ~ $less(X8,X7)
| ( X0 = X7 )
| ~ $less(X7,size(X1))
| ~ $less(0,X7)
| ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X2,X8)),key('select:(Array[Int,Int]*Int)>Int'(X2,X7))) )
& $less(key('select:(Array[Int,Int]*Int)>Int'(X2,$sum(X0,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(X2,X0)))
& $less(0,X0)
& $less(X0,size(X1)) ) ),
inference(rectify,[],[f14]) ).
tff(f17,plain,
! [X2: 'Array[Int,Int]'] :
( ( elems(sK1) != X2 )
| ( ! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| ( $less(sK2(X2),size(sK1))
& ( 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X6,'select:(Array[Int,Int]*Int)>Int'(X2,sK0)),sK0,'select:(Array[Int,Int]*Int)>Int'(X2,X6)) = sK3(X2) )
& $less(0,sK2(X2))
& ~ $less(sK4(X2),0)
& $less(key('select:(Array[Int,Int]*Int)>Int'(sK3(X2),sK4(X2))),key('select:(Array[Int,Int]*Int)>Int'(sK3(X2),sK2(X2))))
& ( sK2(X2) != X6 )
& $less(sK4(X2),sK2(X2)) ) )
& ~ $less(sK0,0)
& ! [X7: $int,X8: $int] :
( $less(X8,0)
| ~ $less(X8,X7)
| ( sK0 = X7 )
| ~ $less(X7,size(sK1))
| ~ $less(0,X7)
| ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X2,X8)),key('select:(Array[Int,Int]*Int)>Int'(X2,X7))) )
& $less(key('select:(Array[Int,Int]*Int)>Int'(X2,$sum(sK0,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(X2,sK0)))
& $less(0,sK0)
& $less(sK0,size(sK1)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X3,sK2(X2)),skolemize(X4,sK3(X2)),skolemize(X5,sK4(X2))],[f16]) ).
tff(f18,plain,
! [X0: $int,X1: 'Array[Int,Int]',X2: $int] : ( 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X1,X0,X2),X0) = X2 ),
inference(rectify,[],[f10]) ).
tff(f21,plain,
! [X0: $int,X1: $int,X2: 'Array[Int,Int]',X3: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X0,X3),X1) = 'select:(Array[Int,Int]*Int)>Int'(X2,X1) )
| ( X0 = X1 ) ),
inference(rectify,[],[f15]) ).
tff(f22,plain,
! [X2: 'Array[Int,Int]'] :
( ( elems(sK1) != X2 )
| $less(sK0,size(sK1)) ),
inference(cnf_transformation,[],[f17]) ).
tff(f23,plain,
! [X2: 'Array[Int,Int]'] :
( ( elems(sK1) != X2 )
| $less(0,sK0) ),
inference(cnf_transformation,[],[f17]) ).
tff(f24,plain,
! [X2: 'Array[Int,Int]'] :
( ( elems(sK1) != X2 )
| $less(key('select:(Array[Int,Int]*Int)>Int'(X2,$sum(sK0,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(X2,sK0))) ),
inference(cnf_transformation,[],[f17]) ).
tff(f25,plain,
! [X2: 'Array[Int,Int]',X8: $int,X7: $int] :
( ( elems(sK1) != X2 )
| $less(X8,0)
| ~ $less(X8,X7)
| ( sK0 = X7 )
| ~ $less(X7,size(sK1))
| ~ $less(0,X7)
| ~ $less(key('select:(Array[Int,Int]*Int)>Int'(X2,X8)),key('select:(Array[Int,Int]*Int)>Int'(X2,X7))) ),
inference(cnf_transformation,[],[f17]) ).
tff(f27,plain,
! [X2: 'Array[Int,Int]',X6: $int] :
( ( elems(sK1) != X2 )
| ( $sum(sK0,$uminus(1)) != X6 )
| $less(sK4(X2),sK2(X2)) ),
inference(cnf_transformation,[],[f17]) ).
tff(f28,plain,
! [X2: 'Array[Int,Int]',X6: $int] :
( ( elems(sK1) != X2 )
| ( $sum(sK0,$uminus(1)) != X6 )
| ( sK2(X2) != X6 ) ),
inference(cnf_transformation,[],[f17]) ).
tff(f29,plain,
! [X2: 'Array[Int,Int]',X6: $int] :
( ( elems(sK1) != X2 )
| ( $sum(sK0,$uminus(1)) != X6 )
| $less(key('select:(Array[Int,Int]*Int)>Int'(sK3(X2),sK4(X2))),key('select:(Array[Int,Int]*Int)>Int'(sK3(X2),sK2(X2)))) ),
inference(cnf_transformation,[],[f17]) ).
tff(f30,plain,
! [X2: 'Array[Int,Int]',X6: $int] :
( ( elems(sK1) != X2 )
| ( $sum(sK0,$uminus(1)) != X6 )
| ~ $less(sK4(X2),0) ),
inference(cnf_transformation,[],[f17]) ).
tff(f31,plain,
! [X2: 'Array[Int,Int]',X6: $int] :
( ( elems(sK1) != X2 )
| ( $sum(sK0,$uminus(1)) != X6 )
| $less(0,sK2(X2)) ),
inference(cnf_transformation,[],[f17]) ).
tff(f32,plain,
! [X2: 'Array[Int,Int]',X6: $int] :
( ( elems(sK1) != X2 )
| ( $sum(sK0,$uminus(1)) != X6 )
| ( 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X6,'select:(Array[Int,Int]*Int)>Int'(X2,sK0)),sK0,'select:(Array[Int,Int]*Int)>Int'(X2,X6)) = sK3(X2) ) ),
inference(cnf_transformation,[],[f17]) ).
tff(f33,plain,
! [X2: 'Array[Int,Int]',X6: $int] :
( ( elems(sK1) != X2 )
| ( $sum(sK0,$uminus(1)) != X6 )
| $less(sK2(X2),size(sK1)) ),
inference(cnf_transformation,[],[f17]) ).
tff(f35,plain,
! [X2: $int,X0: $int,X1: 'Array[Int,Int]'] : ( 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X1,X0,X2),X0) = X2 ),
inference(cnf_transformation,[],[f18]) ).
tff(f37,plain,
! [X2: 'Array[Int,Int]',X3: $int,X0: $int,X1: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(X2,X0,X3),X1) = 'select:(Array[Int,Int]*Int)>Int'(X2,X1) )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f21]) ).
tff(f38,plain,
! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| $less(sK2(elems(sK1)),size(sK1)) ),
inference(equality_resolution,[],[f33]) ).
tff(f39,plain,
$less(sK2(elems(sK1)),size(sK1)),
inference(equality_resolution,[],[f38]) ).
tff(f40,plain,
! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| ( 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(elems(sK1),X6,'select:(Array[Int,Int]*Int)>Int'(elems(sK1),sK0)),sK0,'select:(Array[Int,Int]*Int)>Int'(elems(sK1),X6)) = sK3(elems(sK1)) ) ),
inference(equality_resolution,[],[f32]) ).
tff(f41,plain,
sK3(elems(sK1)) = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'('store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(elems(sK1),$sum(sK0,$uminus(1)),'select:(Array[Int,Int]*Int)>Int'(elems(sK1),sK0)),sK0,'select:(Array[Int,Int]*Int)>Int'(elems(sK1),$sum(sK0,$uminus(1)))),
inference(equality_resolution,[],[f40]) ).
tff(f42,plain,
! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| $less(0,sK2(elems(sK1))) ),
inference(equality_resolution,[],[f31]) ).
tff(f43,plain,
$less(0,sK2(elems(sK1))),
inference(equality_resolution,[],[f42]) ).
tff(f44,plain,
! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| ~ $less(sK4(elems(sK1)),0) ),
inference(equality_resolution,[],[f30]) ).
tff(f45,plain,
~ $less(sK4(elems(sK1)),0),
inference(equality_resolution,[],[f44]) ).
tff(f46,plain,
! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| $less(key('select:(Array[Int,Int]*Int)>Int'(sK3(elems(sK1)),sK4(elems(sK1)))),key('select:(Array[Int,Int]*Int)>Int'(sK3(elems(sK1)),sK2(elems(sK1))))) ),
inference(equality_resolution,[],[f29]) ).
tff(f47,plain,
$less(key('select:(Array[Int,Int]*Int)>Int'(sK3(elems(sK1)),sK4(elems(sK1)))),key('select:(Array[Int,Int]*Int)>Int'(sK3(elems(sK1)),sK2(elems(sK1))))),
inference(equality_resolution,[],[f46]) ).
tff(f48,plain,
! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| ( sK2(elems(sK1)) != X6 ) ),
inference(equality_resolution,[],[f28]) ).
tff(f49,plain,
sK2(elems(sK1)) != $sum(sK0,$uminus(1)),
inference(equality_resolution,[],[f48]) ).
tff(f50,plain,
! [X6: $int] :
( ( $sum(sK0,$uminus(1)) != X6 )
| $less(sK4(elems(sK1)),sK2(elems(sK1))) ),
inference(equality_resolution,[],[f27]) ).
tff(f51,plain,
$less(sK4(elems(sK1)),sK2(elems(sK1))),
inference(equality_resolution,[],[f50]) ).
tff(f53,plain,
! [X8: $int,X7: $int] :
( $less(X8,0)
| ~ $less(X8,X7)
| ( sK0 = X7 )
| ~ $less(X7,size(sK1))
| ~ $less(0,X7)
| ~ $less(key('select:(Array[Int,Int]*Int)>Int'(elems(sK1),X8)),key('select:(Array[Int,Int]*Int)>Int'(elems(sK1),X7))) ),
inference(equality_resolution,[],[f25]) ).
tff(f54,plain,
$less(key('select:(Array[Int,Int]*Int)>Int'(elems(sK1),$sum(sK0,$uminus(1)))),key('select:(Array[Int,Int]*Int)>Int'(elems(sK1),sK0))),
inference(equality_resolution,[],[f24]) ).
tff(f55,plain,
$less(0,sK0),
inference(equality_resolution,[],[f23]) ).
tff(f56,plain,
$less(sK0,size(sK1)),
inference(equality_resolution,[],[f22]) ).
tff(f57,definition,
sF6 = elems(sK1),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
tff(f58,plain,
elems(sK1) = sF6,
inference(reorient_equations,[],[f57]) ).
tff(f59,definition,
sF7 = sK2(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f60,definition,
sF8 = size(sK1),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f61,plain,
$less(sF7,sF8),
inference(definition_folding,[],[f39,f60,f59,f58]) ).
tff(f62,definition,
sF9 = sK3(sF6),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f63,plain,
sK3(sF6) = sF9,
inference(reorient_equations,[],[f62]) ).
tff(f64,definition,
sF10 = $uminus(1),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f65,plain,
$uminus(1) = sF10,
inference(reorient_equations,[],[f64]) ).
tff(f66,definition,
sF11 = $sum(sK0,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f67,plain,
$sum(sK0,sF10) = sF11,
inference(reorient_equations,[],[f66]) ).
tff(f68,definition,
sF12 = 'select:(Array[Int,Int]*Int)>Int'(sF6,sK0),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f69,plain,
'select:(Array[Int,Int]*Int)>Int'(sF6,sK0) = sF12,
inference(reorient_equations,[],[f68]) ).
tff(f70,definition,
sF13 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(sF6,sF11,sF12),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f71,definition,
sF14 = 'select:(Array[Int,Int]*Int)>Int'(sF6,sF11),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f72,plain,
'select:(Array[Int,Int]*Int)>Int'(sF6,sF11) = sF14,
inference(reorient_equations,[],[f71]) ).
tff(f73,definition,
sF15 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(sF13,sK0,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f74,plain,
sF15 = sF9,
inference(definition_folding,[],[f41,f73,f72,f67,f65,f58,f70,f69,f58,f67,f65,f58,f63,f58]) ).
tff(f75,plain,
$less(0,sF7),
inference(definition_folding,[],[f43,f59,f58]) ).
tff(f76,definition,
sF16 = sK4(sF6),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f77,plain,
~ $less(sF16,0),
inference(definition_folding,[],[f45,f76,f58]) ).
tff(f78,definition,
sF17 = 'select:(Array[Int,Int]*Int)>Int'(sF9,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f79,definition,
sF18 = key(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f80,plain,
key(sF17) = sF18,
inference(reorient_equations,[],[f79]) ).
tff(f81,definition,
sF19 = 'select:(Array[Int,Int]*Int)>Int'(sF9,sF7),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
tff(f82,definition,
sF20 = key(sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
tff(f83,plain,
$less(sF18,sF20),
inference(definition_folding,[],[f47,f82,f81,f59,f58,f63,f58,f80,f78,f76,f58,f63,f58]) ).
tff(f84,plain,
sF7 != sF11,
inference(definition_folding,[],[f49,f67,f65,f59,f58]) ).
tff(f85,plain,
$less(sF16,sF7),
inference(definition_folding,[],[f51,f59,f58,f76,f58]) ).
tff(f86,definition,
! [X8: $int] : ( sF21(X8) = 'select:(Array[Int,Int]*Int)>Int'(sF6,X8) ),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
tff(f87,definition,
! [X8: $int] : ( sF22(X8) = key(sF21(X8)) ),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
tff(f88,plain,
! [X8: $int] : ( key(sF21(X8)) = sF22(X8) ),
inference(reorient_equations,[],[f87]) ).
tff(f89,plain,
! [X8: $int,X7: $int] :
( ~ $less(sF22(X8),sF22(X7))
| $less(X8,0)
| ~ $less(0,X7)
| ~ $less(X8,X7)
| ( sK0 = X7 )
| ~ $less(X7,sF8) ),
inference(definition_folding,[],[f53,f88,f86,f58,f88,f86,f58,f60]) ).
tff(f90,definition,
sF23 = key(sF14),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
tff(f91,plain,
key(sF14) = sF23,
inference(reorient_equations,[],[f90]) ).
tff(f92,definition,
sF24 = key(sF12),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
tff(f93,plain,
$less(sF23,sF24),
inference(definition_folding,[],[f54,f92,f69,f58,f91,f72,f67,f65,f58]) ).
tff(f94,plain,
$less(sK0,sF8),
inference(definition_folding,[],[f56,f60]) ).
tff(f98,plain,
-1 = sF10,
inference(evaluation,[],[f65]) ).
tff(f100,definition,
( spl26_1
<=> ( $sum(sK0,sF10) = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl26_1])],[avatar_definition]) ).
tff(f102,plain,
( ( $sum(sK0,sF10) = sF11 )
| ~ spl26_1 ),
inference(avatar_component_clause,[],[f100]) ).
tff(f103,plain,
spl26_1,
inference(avatar_split_clause,[],[f67,f100]) ).
tff(f105,definition,
( spl26_2
<=> ( sF7 = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl26_2])],[avatar_definition]) ).
tff(f107,plain,
( ( sF7 != sF11 )
| spl26_2 ),
inference(avatar_component_clause,[],[f105]) ).
tff(f108,plain,
~ spl26_2,
inference(avatar_split_clause,[],[f84,f105]) ).
tff(f110,definition,
( spl26_3
<=> $less(0,sF7) ),
introduced(definition,[new_symbols(definition,[spl26_3])],[avatar_definition]) ).
tff(f112,plain,
( $less(0,sF7)
| ~ spl26_3 ),
inference(avatar_component_clause,[],[f110]) ).
tff(f113,plain,
spl26_3,
inference(avatar_split_clause,[],[f75,f110]) ).
tff(f115,definition,
( spl26_4
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sF6,sF11) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl26_4])],[avatar_definition]) ).
tff(f117,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sF6,sF11) = sF14 )
| ~ spl26_4 ),
inference(avatar_component_clause,[],[f115]) ).
tff(f118,plain,
spl26_4,
inference(avatar_split_clause,[],[f72,f115]) ).
tff(f125,definition,
( spl26_6
<=> $less(sF16,0) ),
introduced(definition,[new_symbols(definition,[spl26_6])],[avatar_definition]) ).
tff(f127,plain,
( ~ $less(sF16,0)
| spl26_6 ),
inference(avatar_component_clause,[],[f125]) ).
tff(f128,plain,
~ spl26_6,
inference(avatar_split_clause,[],[f77,f125]) ).
tff(f130,definition,
( spl26_7
<=> ( -1 = sF10 ) ),
introduced(definition,[new_symbols(definition,[spl26_7])],[avatar_definition]) ).
tff(f132,plain,
( ( -1 = sF10 )
| ~ spl26_7 ),
inference(avatar_component_clause,[],[f130]) ).
tff(f133,plain,
spl26_7,
inference(avatar_split_clause,[],[f98,f130]) ).
tff(f135,definition,
( spl26_8
<=> ( sF20 = key(sF19) ) ),
introduced(definition,[new_symbols(definition,[spl26_8])],[avatar_definition]) ).
tff(f137,plain,
( ( sF20 = key(sF19) )
| ~ spl26_8 ),
inference(avatar_component_clause,[],[f135]) ).
tff(f138,plain,
spl26_8,
inference(avatar_split_clause,[],[f82,f135]) ).
tff(f140,definition,
( spl26_9
<=> $less(0,sK0) ),
introduced(definition,[new_symbols(definition,[spl26_9])],[avatar_definition]) ).
tff(f143,plain,
spl26_9,
inference(avatar_split_clause,[],[f55,f140]) ).
tff(f145,definition,
( spl26_10
<=> ( sF15 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(sF13,sK0,sF14) ) ),
introduced(definition,[new_symbols(definition,[spl26_10])],[avatar_definition]) ).
tff(f147,plain,
( ( sF15 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(sF13,sK0,sF14) )
| ~ spl26_10 ),
inference(avatar_component_clause,[],[f145]) ).
tff(f148,plain,
spl26_10,
inference(avatar_split_clause,[],[f73,f145]) ).
tff(f150,definition,
( spl26_11
<=> $less(sF16,sF7) ),
introduced(definition,[new_symbols(definition,[spl26_11])],[avatar_definition]) ).
tff(f152,plain,
( $less(sF16,sF7)
| ~ spl26_11 ),
inference(avatar_component_clause,[],[f150]) ).
tff(f153,plain,
spl26_11,
inference(avatar_split_clause,[],[f85,f150]) ).
tff(f160,definition,
( spl26_13
<=> ( sF19 = 'select:(Array[Int,Int]*Int)>Int'(sF9,sF7) ) ),
introduced(definition,[new_symbols(definition,[spl26_13])],[avatar_definition]) ).
tff(f162,plain,
( ( sF19 = 'select:(Array[Int,Int]*Int)>Int'(sF9,sF7) )
| ~ spl26_13 ),
inference(avatar_component_clause,[],[f160]) ).
tff(f163,plain,
spl26_13,
inference(avatar_split_clause,[],[f81,f160]) ).
tff(f165,definition,
( spl26_14
<=> ( sF17 = 'select:(Array[Int,Int]*Int)>Int'(sF9,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl26_14])],[avatar_definition]) ).
tff(f167,plain,
( ( sF17 = 'select:(Array[Int,Int]*Int)>Int'(sF9,sF16) )
| ~ spl26_14 ),
inference(avatar_component_clause,[],[f165]) ).
tff(f168,plain,
spl26_14,
inference(avatar_split_clause,[],[f78,f165]) ).
tff(f170,definition,
( spl26_15
<=> ( sF24 = key(sF12) ) ),
introduced(definition,[new_symbols(definition,[spl26_15])],[avatar_definition]) ).
tff(f173,plain,
spl26_15,
inference(avatar_split_clause,[],[f92,f170]) ).
tff(f180,definition,
( spl26_17
<=> ( sF15 = sF9 ) ),
introduced(definition,[new_symbols(definition,[spl26_17])],[avatar_definition]) ).
tff(f182,plain,
( ( sF15 = sF9 )
| ~ spl26_17 ),
inference(avatar_component_clause,[],[f180]) ).
tff(f183,plain,
spl26_17,
inference(avatar_split_clause,[],[f74,f180]) ).
tff(f185,definition,
( spl26_18
<=> ( sF13 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(sF6,sF11,sF12) ) ),
introduced(definition,[new_symbols(definition,[spl26_18])],[avatar_definition]) ).
tff(f187,plain,
( ( sF13 = 'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]'(sF6,sF11,sF12) )
| ~ spl26_18 ),
inference(avatar_component_clause,[],[f185]) ).
tff(f188,plain,
spl26_18,
inference(avatar_split_clause,[],[f70,f185]) ).
tff(f205,definition,
( spl26_22
<=> ( key(sF17) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl26_22])],[avatar_definition]) ).
tff(f207,plain,
( ( key(sF17) = sF18 )
| ~ spl26_22 ),
inference(avatar_component_clause,[],[f205]) ).
tff(f208,plain,
spl26_22,
inference(avatar_split_clause,[],[f80,f205]) ).
tff(f215,definition,
( spl26_24
<=> $less(sF23,sF24) ),
introduced(definition,[new_symbols(definition,[spl26_24])],[avatar_definition]) ).
tff(f218,plain,
spl26_24,
inference(avatar_split_clause,[],[f93,f215]) ).
tff(f220,definition,
( spl26_25
<=> ( key(sF14) = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl26_25])],[avatar_definition]) ).
tff(f222,plain,
( ( key(sF14) = sF23 )
| ~ spl26_25 ),
inference(avatar_component_clause,[],[f220]) ).
tff(f223,plain,
spl26_25,
inference(avatar_split_clause,[],[f91,f220]) ).
tff(f225,definition,
( spl26_26
<=> $less(sF18,sF20) ),
introduced(definition,[new_symbols(definition,[spl26_26])],[avatar_definition]) ).
tff(f227,plain,
( $less(sF18,sF20)
| ~ spl26_26 ),
inference(avatar_component_clause,[],[f225]) ).
tff(f228,plain,
spl26_26,
inference(avatar_split_clause,[],[f83,f225]) ).
tff(f230,definition,
( spl26_27
<=> $less(sF7,sF8) ),
introduced(definition,[new_symbols(definition,[spl26_27])],[avatar_definition]) ).
tff(f232,plain,
( $less(sF7,sF8)
| ~ spl26_27 ),
inference(avatar_component_clause,[],[f230]) ).
tff(f233,plain,
spl26_27,
inference(avatar_split_clause,[],[f61,f230]) ).
tff(f235,definition,
( spl26_28
<=> $less(sK0,sF8) ),
introduced(definition,[new_symbols(definition,[spl26_28])],[avatar_definition]) ).
tff(f238,plain,
spl26_28,
inference(avatar_split_clause,[],[f94,f235]) ).
tff(f240,plain,
( ( $sum(sK0,-1) = sF11 )
| ~ spl26_1
| ~ spl26_7 ),
inference(superposition,[],[f102,f132]) ).
tff(f242,definition,
( spl26_29
<=> ( $sum(sK0,-1) = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl26_29])],[avatar_definition]) ).
tff(f245,plain,
( spl26_29
| ~ spl26_1
| ~ spl26_7 ),
inference(avatar_split_clause,[],[f240,f130,f100,f242]) ).
tff(f246,plain,
! [X0: $int] : ( sF22(X0) = key('select:(Array[Int,Int]*Int)>Int'(sF6,X0)) ),
inference(superposition,[],[f88,f86]) ).
tff(f247,plain,
( ( key(sF14) = sF22(sF11) )
| ~ spl26_4 ),
inference(superposition,[],[f246,f117]) ).
tff(f250,plain,
( ( sF22(sF11) = sF23 )
| ~ spl26_4
| ~ spl26_25 ),
inference(forward_demodulation,[],[f247,f222]) ).
tff(f257,definition,
( spl26_31
<=> ( sF22(sF11) = sF23 ) ),
introduced(definition,[new_symbols(definition,[spl26_31])],[avatar_definition]) ).
tff(f259,plain,
( ( sF22(sF11) = sF23 )
| ~ spl26_31 ),
inference(avatar_component_clause,[],[f257]) ).
tff(f260,plain,
( spl26_31
| ~ spl26_4
| ~ spl26_25 ),
inference(avatar_split_clause,[],[f250,f220,f115,f257]) ).
tff(f261,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sF15,sK0) = sF14 )
| ~ spl26_10 ),
inference(superposition,[],[f35,f147]) ).
tff(f262,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sF13,sF11) = sF12 )
| ~ spl26_18 ),
inference(superposition,[],[f35,f187]) ).
tff(f263,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sF9,sK0) = sF14 )
| ~ spl26_10
| ~ spl26_17 ),
inference(forward_demodulation,[],[f261,f182]) ).
tff(f265,definition,
( spl26_32
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sF13,sF11) = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl26_32])],[avatar_definition]) ).
tff(f267,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sF13,sF11) = sF12 )
| ~ spl26_32 ),
inference(avatar_component_clause,[],[f265]) ).
tff(f268,plain,
( spl26_32
| ~ spl26_18 ),
inference(avatar_split_clause,[],[f262,f185,f265]) ).
tff(f270,definition,
( spl26_33
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sF9,sK0) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl26_33])],[avatar_definition]) ).
tff(f272,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sF9,sK0) = sF14 )
| ~ spl26_33 ),
inference(avatar_component_clause,[],[f270]) ).
tff(f273,plain,
( spl26_33
| ~ spl26_10
| ~ spl26_17 ),
inference(avatar_split_clause,[],[f263,f180,f145,f270]) ).
tff(f274,plain,
( ! [X0: $int] :
( ( sK0 = X0 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sF13,X0) = 'select:(Array[Int,Int]*Int)>Int'(sF15,X0) ) )
| ~ spl26_10 ),
inference(superposition,[],[f37,f147]) ).
tff(f275,plain,
( ! [X0: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sF13,X0) = 'select:(Array[Int,Int]*Int)>Int'(sF6,X0) )
| ( sF11 = X0 ) )
| ~ spl26_18 ),
inference(superposition,[],[f37,f187]) ).
tff(f276,plain,
( ! [X0: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sF9,X0) = 'select:(Array[Int,Int]*Int)>Int'(sF13,X0) )
| ( sK0 = X0 ) )
| ~ spl26_10
| ~ spl26_17 ),
inference(forward_demodulation,[],[f274,f182]) ).
tff(f302,plain,
( ( sK0 = sF11 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sF9,sF11) = sF12 )
| ~ spl26_10
| ~ spl26_17
| ~ spl26_32 ),
inference(superposition,[],[f267,f276]) ).
tff(f305,definition,
( spl26_34
<=> ( sK0 = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl26_34])],[avatar_definition]) ).
tff(f309,definition,
( spl26_35
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sF9,sF11) = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl26_35])],[avatar_definition]) ).
tff(f313,plain,
( spl26_35
| spl26_34
| ~ spl26_10
| ~ spl26_17
| ~ spl26_32 ),
inference(avatar_split_clause,[],[f302,f265,f180,f145,f305,f309]) ).
tff(f315,plain,
( ! [X0: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(sF9,X0) = 'select:(Array[Int,Int]*Int)>Int'(sF6,X0) )
| ( sK0 = X0 )
| ( sF11 = X0 ) )
| ~ spl26_10
| ~ spl26_17
| ~ spl26_18 ),
inference(superposition,[],[f276,f275]) ).
tff(f337,plain,
( ( sF19 = 'select:(Array[Int,Int]*Int)>Int'(sF6,sF7) )
| ( sF7 = sK0 )
| ( sF7 = sF11 )
| ~ spl26_10
| ~ spl26_13
| ~ spl26_17
| ~ spl26_18 ),
inference(superposition,[],[f162,f315]) ).
tff(f338,plain,
( ( sF16 = sK0 )
| ( sF16 = sF11 )
| ( 'select:(Array[Int,Int]*Int)>Int'(sF6,sF16) = sF17 )
| ~ spl26_10
| ~ spl26_14
| ~ spl26_17
| ~ spl26_18 ),
inference(superposition,[],[f167,f315]) ).
tff(f347,definition,
( spl26_36
<=> ( sF16 = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl26_36])],[avatar_definition]) ).
tff(f351,definition,
( spl26_37
<=> ( sF16 = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl26_37])],[avatar_definition]) ).
tff(f353,plain,
( ( sF16 = sK0 )
| ~ spl26_37 ),
inference(avatar_component_clause,[],[f351]) ).
tff(f355,definition,
( spl26_38
<=> ( 'select:(Array[Int,Int]*Int)>Int'(sF6,sF16) = sF17 ) ),
introduced(definition,[new_symbols(definition,[spl26_38])],[avatar_definition]) ).
tff(f357,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(sF6,sF16) = sF17 )
| ~ spl26_38 ),
inference(avatar_component_clause,[],[f355]) ).
tff(f359,plain,
( spl26_36
| spl26_37
| spl26_38
| ~ spl26_10
| ~ spl26_14
| ~ spl26_17
| ~ spl26_18 ),
inference(avatar_split_clause,[],[f338,f185,f180,f165,f145,f355,f351,f347]) ).
tff(f360,plain,
( ( sF7 = sK0 )
| ( sF19 = 'select:(Array[Int,Int]*Int)>Int'(sF6,sF7) )
| spl26_2
| ~ spl26_10
| ~ spl26_13
| ~ spl26_17
| ~ spl26_18 ),
inference(forward_subsumption_resolution,[],[f337,f107]) ).
tff(f362,definition,
( spl26_39
<=> ( sF19 = 'select:(Array[Int,Int]*Int)>Int'(sF6,sF7) ) ),
introduced(definition,[new_symbols(definition,[spl26_39])],[avatar_definition]) ).
tff(f364,plain,
( ( sF19 = 'select:(Array[Int,Int]*Int)>Int'(sF6,sF7) )
| ~ spl26_39 ),
inference(avatar_component_clause,[],[f362]) ).
tff(f366,definition,
( spl26_40
<=> ( sF7 = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl26_40])],[avatar_definition]) ).
tff(f370,plain,
( spl26_39
| spl26_40
| spl26_2
| ~ spl26_10
| ~ spl26_13
| ~ spl26_17
| ~ spl26_18 ),
inference(avatar_split_clause,[],[f360,f185,f180,f160,f145,f105,f366,f362]) ).
tff(f387,plain,
( ( sF17 = 'select:(Array[Int,Int]*Int)>Int'(sF9,sK0) )
| ~ spl26_14
| ~ spl26_37 ),
inference(superposition,[],[f167,f353]) ).
tff(f388,plain,
( $less(sK0,sF7)
| ~ spl26_11
| ~ spl26_37 ),
inference(superposition,[],[f152,f353]) ).
tff(f390,plain,
( ( sF17 = sF14 )
| ~ spl26_14
| ~ spl26_33
| ~ spl26_37 ),
inference(forward_demodulation,[],[f387,f272]) ).
tff(f392,definition,
( spl26_41
<=> $less(sK0,sF7) ),
introduced(definition,[new_symbols(definition,[spl26_41])],[avatar_definition]) ).
tff(f395,plain,
( spl26_41
| ~ spl26_11
| ~ spl26_37 ),
inference(avatar_split_clause,[],[f388,f351,f150,f392]) ).
tff(f397,definition,
( spl26_42
<=> ( sF17 = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl26_42])],[avatar_definition]) ).
tff(f400,plain,
( spl26_42
| ~ spl26_14
| ~ spl26_33
| ~ spl26_37 ),
inference(avatar_split_clause,[],[f390,f351,f270,f165,f397]) ).
tff(f409,plain,
( ( key(sF17) = sF22(sF16) )
| ~ spl26_38 ),
inference(superposition,[],[f246,f357]) ).
tff(f410,plain,
( ( sF18 = sF22(sF16) )
| ~ spl26_22
| ~ spl26_38 ),
inference(forward_demodulation,[],[f409,f207]) ).
tff(f412,definition,
( spl26_43
<=> ( sF18 = sF22(sF16) ) ),
introduced(definition,[new_symbols(definition,[spl26_43])],[avatar_definition]) ).
tff(f414,plain,
( ( sF18 = sF22(sF16) )
| ~ spl26_43 ),
inference(avatar_component_clause,[],[f412]) ).
tff(f415,plain,
( spl26_43
| ~ spl26_22
| ~ spl26_38 ),
inference(avatar_split_clause,[],[f410,f355,f205,f412]) ).
tff(f436,plain,
( ( key(sF19) = sF22(sF7) )
| ~ spl26_39 ),
inference(superposition,[],[f246,f364]) ).
tff(f437,plain,
( ( sF20 = sF22(sF7) )
| ~ spl26_8
| ~ spl26_39 ),
inference(forward_demodulation,[],[f436,f137]) ).
tff(f439,definition,
( spl26_47
<=> ( sF20 = sF22(sF7) ) ),
introduced(definition,[new_symbols(definition,[spl26_47])],[avatar_definition]) ).
tff(f441,plain,
( ( sF20 = sF22(sF7) )
| ~ spl26_47 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f442,plain,
( spl26_47
| ~ spl26_8
| ~ spl26_39 ),
inference(avatar_split_clause,[],[f437,f362,f135,f439]) ).
tff(f524,plain,
( ! [X0: $int] :
( $less(X0,0)
| ~ $less(0,sF7)
| ( sF7 = sK0 )
| ~ $less(sF7,sF8)
| ~ $less(X0,sF7)
| ~ $less(sF22(X0),sF20) )
| ~ spl26_47 ),
inference(superposition,[],[f89,f441]) ).
tff(f526,plain,
( ! [X0: $int] :
( ~ $less(X0,sF7)
| $less(X0,0)
| ( sF7 = sK0 )
| ~ $less(sF22(X0),sF20)
| ~ $less(sF7,sF8) )
| ~ spl26_3
| ~ spl26_47 ),
inference(forward_subsumption_resolution,[],[f524,f112]) ).
tff(f535,plain,
( ! [X0: $int] :
( ~ $less(X0,sF7)
| ~ $less(sF22(X0),sF20)
| ( sF7 = sK0 )
| $less(X0,0) )
| ~ spl26_3
| ~ spl26_27
| ~ spl26_47 ),
inference(forward_subsumption_resolution,[],[f526,f232]) ).
tff(f537,definition,
( spl26_56
<=> ! [X0: $int] :
( ~ $less(X0,sF7)
| $less(X0,0)
| ~ $less(sF22(X0),sF20) ) ),
introduced(definition,[new_symbols(definition,[spl26_56])],[avatar_definition]) ).
tff(f538,plain,
( ! [X0: $int] :
( ~ $less(sF22(X0),sF20)
| ~ $less(X0,sF7)
| $less(X0,0) )
| ~ spl26_56 ),
inference(avatar_component_clause,[],[f537]) ).
tff(f539,plain,
( spl26_56
| spl26_40
| ~ spl26_3
| ~ spl26_27
| ~ spl26_47 ),
inference(avatar_split_clause,[],[f535,f439,f230,f110,f366,f537]) ).
tff(f768,plain,
( ! [X0: $int] :
( ~ $less(X0,sF11)
| ( sK0 = sF11 )
| $less(X0,0)
| ~ $less(sF11,sF8)
| ~ $less(0,sF11)
| ~ $less(sF22(X0),sF23) )
| ~ spl26_31 ),
inference(superposition,[],[f89,f259]) ).
tff(f779,definition,
( spl26_67
<=> $less(sF11,0) ),
introduced(definition,[new_symbols(definition,[spl26_67])],[avatar_definition]) ).
tff(f788,definition,
( spl26_69
<=> $less(sF11,sF8) ),
introduced(definition,[new_symbols(definition,[spl26_69])],[avatar_definition]) ).
tff(f792,definition,
( spl26_70
<=> $less(0,sF11) ),
introduced(definition,[new_symbols(definition,[spl26_70])],[avatar_definition]) ).
tff(f796,definition,
( spl26_71
<=> ! [X0: $int] :
( ~ $less(X0,sF11)
| ~ $less(sF22(X0),sF23)
| $less(X0,0) ) ),
introduced(definition,[new_symbols(definition,[spl26_71])],[avatar_definition]) ).
tff(f797,plain,
( ! [X0: $int] :
( ~ $less(sF22(X0),sF23)
| ~ $less(X0,sF11)
| $less(X0,0) )
| ~ spl26_71 ),
inference(avatar_component_clause,[],[f796]) ).
tff(f798,plain,
( ~ spl26_69
| spl26_34
| ~ spl26_70
| spl26_71
| ~ spl26_31 ),
inference(avatar_split_clause,[],[f768,f257,f796,f792,f305,f788]) ).
tff(f866,plain,
( ~ $less(sF16,sF11)
| ~ $less(sF18,sF23)
| $less(sF16,0)
| ~ spl26_43
| ~ spl26_71 ),
inference(superposition,[],[f797,f414]) ).
tff(f867,plain,
( ~ $less(sF18,sF23)
| ~ $less(sF16,sF11)
| spl26_6
| ~ spl26_43
| ~ spl26_71 ),
inference(forward_subsumption_resolution,[],[f866,f127]) ).
tff(f888,definition,
( spl26_79
<=> $less(sF18,sF23) ),
introduced(definition,[new_symbols(definition,[spl26_79])],[avatar_definition]) ).
tff(f892,definition,
( spl26_80
<=> $less(sF16,sF11) ),
introduced(definition,[new_symbols(definition,[spl26_80])],[avatar_definition]) ).
tff(f895,plain,
( ~ spl26_79
| ~ spl26_80
| spl26_6
| ~ spl26_43
| ~ spl26_71 ),
inference(avatar_split_clause,[],[f867,f796,f412,f125,f892,f888]) ).
tff(f984,plain,
( ~ $less(sF11,sF7)
| $less(sF11,0)
| ~ $less(sF23,sF20)
| ~ spl26_31
| ~ spl26_56 ),
inference(superposition,[],[f538,f259]) ).
tff(f985,plain,
( $less(sF16,0)
| ~ $less(sF18,sF20)
| ~ $less(sF16,sF7)
| ~ spl26_43
| ~ spl26_56 ),
inference(superposition,[],[f538,f414]) ).
tff(f986,plain,
( ~ $less(sF18,sF20)
| ~ $less(sF16,sF7)
| spl26_6
| ~ spl26_43
| ~ spl26_56 ),
inference(forward_subsumption_resolution,[],[f985,f127]) ).
tff(f989,definition,
( spl26_83
<=> $less(sF23,sF20) ),
introduced(definition,[new_symbols(definition,[spl26_83])],[avatar_definition]) ).
tff(f993,definition,
( spl26_84
<=> $less(sF11,sF7) ),
introduced(definition,[new_symbols(definition,[spl26_84])],[avatar_definition]) ).
tff(f996,plain,
( ~ spl26_83
| spl26_67
| ~ spl26_84
| ~ spl26_31
| ~ spl26_56 ),
inference(avatar_split_clause,[],[f984,f537,f257,f993,f779,f989]) ).
tff(f1006,plain,
( ~ $less(sF16,sF7)
| spl26_6
| ~ spl26_26
| ~ spl26_43
| ~ spl26_56 ),
inference(forward_subsumption_resolution,[],[f986,f227]) ).
tff(f1012,plain,
( $false
| spl26_6
| ~ spl26_11
| ~ spl26_26
| ~ spl26_43
| ~ spl26_56 ),
inference(forward_subsumption_resolution,[],[f1006,f152]) ).
tff(f1013,plain,
( spl26_6
| ~ spl26_11
| ~ spl26_26
| ~ spl26_43
| ~ spl26_56 ),
inference(avatar_contradiction_clause,[],[f1012]) ).
tff(f1014,plain,
$false,
inference(avatar_smt_refutation,[],[f1013,f996,f895,f798,f539,f442,f415,f400,f395,f370,f359,f313,f273,f268,f260,f245,f238,f233,f228,f223,f218,f208,f188,f183,f173,f168,f163,f153,f148,f143,f138,f133,f128,f118,f113,f108,f103]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : DAT329_1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.17 % Computer : n008.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Sep 29 00:20:09 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.20 Running first-order theorem proving
% 0.10/0.20 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.16/1.21 % (2800655)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 4.16/1.21 % (2800664)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2866538834:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 4.16/1.21 % (2800664)Instruction limit reached!
% 4.16/1.21 % (2800664)------------------------------
% 4.16/1.21 % (2800664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.21 % (2800664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.21 % (2800664)CaDiCaL version: 2.1.3
% 4.16/1.21 % (2800664)Termination reason: Instruction limit
% 4.16/1.21 % (2800664)Termination phase: Saturation
% 4.16/1.21 % (2800664)Time elapsed: 0.003 s
% 4.16/1.21 % (2800664)Peak memory usage: 89 MB
% 4.16/1.21 % (2800664)Instructions burned: 7 (million)
% 4.16/1.21 % (2800661)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4134397154:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 4.16/1.21 % (2800666)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1136134546:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 4.16/1.21 % (2800663)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1559840436:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 4.16/1.21 % (2800660)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=891929835:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 4.16/1.21 % (2800662)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2354178911:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 4.16/1.21 % (2800663)Instruction limit reached!
% 4.16/1.21 % (2800663)------------------------------
% 4.16/1.21 % (2800663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.21 % (2800663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.21 % (2800663)CaDiCaL version: 2.1.3
% 4.16/1.21 % (2800663)Termination reason: Instruction limit
% 4.16/1.21 % (2800663)Termination phase: Saturation
% 4.16/1.21 % (2800663)Time elapsed: 0.005 s
% 4.16/1.21 % (2800663)Peak memory usage: 88 MB
% 4.16/1.21 % (2800663)Instructions burned: 8 (million)
% 4.16/1.21 % (2800665)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3831219664:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 4.16/1.21 % (2800660)Instruction limit reached!
% 4.16/1.21 % (2800660)------------------------------
% 4.16/1.21 % (2800660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.21 % (2800660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.21 % (2800660)CaDiCaL version: 2.1.3
% 4.16/1.21 % (2800660)Termination reason: Instruction limit
% 4.16/1.21 % (2800660)Termination phase: Saturation
% 4.16/1.21 % (2800660)Time elapsed: 0.031 s
% 4.16/1.21 % (2800660)Peak memory usage: 116 MB
% 4.16/1.21 % (2800660)Instructions burned: 13 (million)
% 4.16/1.21 % (2800666)Instruction limit reached!
% 4.16/1.21 % (2800666)------------------------------
% 4.16/1.21 % (2800666)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.21 % (2800666)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.21 % (2800666)CaDiCaL version: 2.1.3
% 4.16/1.21 % (2800666)Termination reason: Instruction limit
% 4.16/1.21 % (2800666)Termination phase: Saturation
% 4.16/1.21 % (2800666)Time elapsed: 0.048 s
% 4.16/1.21 % (2800666)Peak memory usage: 116 MB
% 4.16/1.21 % (2800666)Instructions burned: 33 (million)
% 4.16/1.21 % (2800665)Instruction limit reached!
% 4.16/1.21 % (2800665)------------------------------
% 4.16/1.21 % (2800665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.16/1.21 % (2800665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.21 % (2800665)CaDiCaL version: 2.1.3
% 4.16/1.21 % (2800665)Termination reason: Instruction limit
% 4.16/1.21 % (2800665)Termination phase: Saturation
% 4.16/1.21 % (2800665)Time elapsed: 0.055 s
% 4.16/1.21 % (2800665)Peak memory usage: 116 MB
% 4.16/1.21 % (2800665)Instructions burned: 46 (million)
% 4.16/1.21 % (2800668)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3625319974:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.16/1.21 % (2800668)Refutation not found, incomplete strategy
% 4.16/1.21 % (2800668)------------------------------
% 4.70/1.36 % (2800668)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.36 % (2800668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.36 % (2800668)CaDiCaL version: 2.1.3
% 4.70/1.36 % (2800668)Termination reason: Refutation not found, incomplete strategy
% 4.70/1.36 % (2800668)Time elapsed: 0.0000 s
% 4.70/1.36 % (2800668)Peak memory usage: 87 MB
% 4.70/1.36 % (2800674)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=2209495078:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.70/1.36 % (2800674)Instruction limit reached!
% 4.70/1.36 % (2800674)------------------------------
% 4.70/1.36 % (2800674)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.36 % (2800674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.36 % (2800674)CaDiCaL version: 2.1.3
% 4.70/1.36 % (2800674)Termination reason: Instruction limit
% 4.70/1.36 % (2800674)Termination phase: Saturation
% 4.70/1.36 % (2800674)Time elapsed: 0.023 s
% 4.70/1.36 % (2800674)Peak memory usage: 89 MB
% 4.70/1.36 % (2800674)Instructions burned: 30 (million)
% 4.70/1.36 % (2800677)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1482140770:i=24:canc=force:rtra=on_2998 on theBenchmark for (2998ds/24Mi)
% 4.70/1.36 % (2800676)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1303503823:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.70/1.36 % (2800662)Instruction limit reached!
% 4.70/1.36 % (2800662)------------------------------
% 4.70/1.36 % (2800662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.36 % (2800662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.36 % (2800662)CaDiCaL version: 2.1.3
% 4.70/1.36 % (2800662)Termination reason: Instruction limit
% 4.70/1.36 % (2800662)Termination phase: Saturation
% 4.70/1.36 % (2800662)Time elapsed: 0.175 s
% 4.70/1.36 % (2800662)Peak memory usage: 118 MB
% 4.70/1.36 % (2800662)Instructions burned: 201 (million)
% 4.70/1.36 % (2800676)Instruction limit reached!
% 4.70/1.36 % (2800676)------------------------------
% 4.70/1.36 % (2800676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.36 % (2800676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.36 % (2800676)CaDiCaL version: 2.1.3
% 4.70/1.36 % (2800676)Termination reason: Instruction limit
% 4.70/1.36 % (2800676)Termination phase: Saturation
% 4.70/1.36 % (2800676)Time elapsed: 0.011 s
% 4.70/1.36 % (2800676)Peak memory usage: 90 MB
% 4.70/1.36 % (2800676)Instructions burned: 16 (million)
% 4.70/1.36 % (2800677)Instruction limit reached!
% 4.70/1.36 % (2800677)------------------------------
% 4.70/1.36 % (2800677)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.36 % (2800677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.36 % (2800677)CaDiCaL version: 2.1.3
% 4.70/1.36 % (2800677)Termination reason: Instruction limit
% 4.70/1.36 % (2800677)Termination phase: Saturation
% 4.70/1.36 % (2800677)Time elapsed: 0.019 s
% 4.70/1.36 % (2800677)Peak memory usage: 89 MB
% 4.70/1.36 % (2800677)Instructions burned: 25 (million)
% 4.70/1.36 % (2800679)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=1094497281:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.70/1.36 % (2800661)Instruction limit reached!
% 4.70/1.36 % (2800661)------------------------------
% 4.70/1.36 % (2800661)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.36 % (2800661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.70/1.36 % (2800661)CaDiCaL version: 2.1.3
% 4.70/1.36 % (2800661)Termination reason: Instruction limit
% 4.70/1.36 % (2800661)Termination phase: Saturation
% 4.70/1.36 % (2800661)Time elapsed: 0.200 s
% 4.70/1.36 % (2800661)Peak memory usage: 117 MB
% 4.70/1.36 % (2800661)Instructions burned: 307 (million)
% 4.70/1.36 % (2800679)Refutation not found, incomplete strategy
% 4.70/1.36 % (2800679)------------------------------
% 4.70/1.36 % (2800679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.70/1.36 % (2800679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.54/1.53 % (2800679)CaDiCaL version: 2.1.3
% 5.54/1.53 % (2800679)Termination reason: Refutation not found, incomplete strategy
% 5.54/1.53 % (2800679)Time elapsed: 0.002 s
% 5.54/1.53 % (2800679)Peak memory usage: 89 MB
% 5.54/1.53 % (2800679)Instructions burned: 2 (million)
% 5.54/1.53 % (2800668)------------------------------
% 5.54/1.53 % (2800668)------------------------------
% 5.54/1.53 % (2800681)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=4287895636:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 5.54/1.53 % (2800684)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1429374577:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.54/1.53 % (2800684)Instruction limit reached!
% 5.54/1.53 % (2800684)------------------------------
% 5.54/1.53 % (2800684)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.54/1.53 % (2800684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.54/1.53 % (2800684)CaDiCaL version: 2.1.3
% 5.54/1.53 % (2800684)Termination reason: Instruction limit
% 5.54/1.53 % (2800684)Termination phase: Saturation
% 5.54/1.53 % (2800684)Time elapsed: 0.003 s
% 5.54/1.53 % (2800684)Peak memory usage: 88 MB
% 5.54/1.53 % (2800684)Instructions burned: 3 (million)
% 5.54/1.53 % (2800687)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2709476968:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.54/1.53 % (2800685)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1608009217:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.54/1.53 % (2800685)Refutation not found, incomplete strategy
% 5.54/1.53 % (2800685)------------------------------
% 5.54/1.53 % (2800685)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.54/1.53 % (2800685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.54/1.53 % (2800685)CaDiCaL version: 2.1.3
% 5.54/1.53 % (2800685)Termination reason: Refutation not found, incomplete strategy
% 5.54/1.53 % (2800685)Time elapsed: 0.001 s
% 5.54/1.53 % (2800685)Peak memory usage: 87 MB
% 5.54/1.53 % (2800687)Refutation not found, incomplete strategy
% 5.54/1.53 % (2800687)------------------------------
% 5.54/1.53 % (2800687)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.54/1.53 % (2800687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.54/1.53 % (2800687)CaDiCaL version: 2.1.3
% 5.54/1.53 % (2800687)Termination reason: Refutation not found, incomplete strategy
% 5.54/1.53 % (2800687)Time elapsed: 0.002 s
% 5.54/1.53 % (2800687)Peak memory usage: 88 MB
% 5.54/1.53 % (2800687)Instructions burned: 2 (million)
% 5.54/1.53 % (2800689)lrs+10_1_thi=all:si=on:fd=off:random_seed=613667710:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.54/1.53 % (2800688)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=934288731:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.54/1.53 % (2800681)Instruction limit reached!
% 5.54/1.53 % (2800681)------------------------------
% 5.54/1.53 % (2800681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.54/1.53 % (2800681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.54/1.53 % (2800681)CaDiCaL version: 2.1.3
% 5.54/1.53 % (2800681)Termination reason: Instruction limit
% 5.54/1.53 % (2800681)Termination phase: Saturation
% 5.54/1.53 % (2800681)Time elapsed: 0.056 s
% 5.54/1.53 % (2800681)Peak memory usage: 89 MB
% 5.54/1.53 % (2800681)Instructions burned: 86 (million)
% 5.54/1.53 % (2800689)Instruction limit reached!
% 5.54/1.53 % (2800689)------------------------------
% 5.54/1.53 % (2800689)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.54/1.53 % (2800689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.54/1.53 % (2800689)CaDiCaL version: 2.1.3
% 5.54/1.53 % (2800689)Termination reason: Instruction limit
% 5.54/1.53 % (2800689)Termination phase: Saturation
% 5.54/1.53 % (2800689)Time elapsed: 0.036 s
% 5.54/1.53 % (2800689)Peak memory usage: 116 MB
% 5.54/1.53 % (2800689)Instructions burned: 54 (million)
% 5.54/1.53 % (2800688)Instruction limit reached!
% 5.54/1.53 % (2800688)------------------------------
% 5.54/1.53 % (2800688)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.54/1.53 % (2800688)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.82 % (2800688)CaDiCaL version: 2.1.3
% 7.57/1.82 % (2800688)Termination reason: Instruction limit
% 7.57/1.82 % (2800688)Termination phase: Saturation
% 7.57/1.82 % (2800688)Time elapsed: 0.095 s
% 7.57/1.82 % (2800688)Peak memory usage: 134 MB
% 7.57/1.82 % (2800688)Instructions burned: 67 (million)
% 7.57/1.82 % (2800679)------------------------------
% 7.57/1.82 % (2800679)------------------------------
% 7.57/1.82 % (2800693)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=2725538608:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 7.57/1.82 % (2800693)Instruction limit reached!
% 7.57/1.82 % (2800693)------------------------------
% 7.57/1.82 % (2800693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.57/1.82 % (2800693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.82 % (2800693)CaDiCaL version: 2.1.3
% 7.57/1.82 % (2800693)Termination reason: Instruction limit
% 7.57/1.82 % (2800693)Termination phase: Saturation
% 7.57/1.82 % (2800693)Time elapsed: 0.006 s
% 7.57/1.82 % (2800693)Peak memory usage: 88 MB
% 7.57/1.82 % (2800693)Instructions burned: 8 (million)
% 7.57/1.82 % (2800699)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=354101457:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.57/1.82 % (2800699)Instruction limit reached!
% 7.57/1.82 % (2800699)------------------------------
% 7.57/1.82 % (2800699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.57/1.82 % (2800699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.82 % (2800699)CaDiCaL version: 2.1.3
% 7.57/1.82 % (2800699)Termination reason: Instruction limit
% 7.57/1.82 % (2800699)Termination phase: Saturation
% 7.57/1.82 % (2800699)Time elapsed: 0.002 s
% 7.57/1.82 % (2800699)Peak memory usage: 89 MB
% 7.57/1.82 % (2800699)Instructions burned: 4 (million)
% 7.57/1.82 % (2800698)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=394846939:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 7.57/1.82 % (2800698)Refutation not found, incomplete strategy
% 7.57/1.82 % (2800698)------------------------------
% 7.57/1.82 % (2800698)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.57/1.82 % (2800698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.82 % (2800698)CaDiCaL version: 2.1.3
% 7.57/1.82 % (2800698)Termination reason: Refutation not found, incomplete strategy
% 7.57/1.82 % (2800698)Time elapsed: 0.001 s
% 7.57/1.82 % (2800698)Peak memory usage: 87 MB
% 7.57/1.82 % (2800706)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=268345598: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_2993 on theBenchmark for (2993ds/35Mi)
% 7.57/1.82 % (2800687)------------------------------
% 7.57/1.82 % (2800687)------------------------------
% 7.57/1.82 % (2800685)------------------------------
% 7.57/1.82 % (2800685)------------------------------
% 7.57/1.82 % (2800706)Instruction limit reached!
% 7.57/1.82 % (2800706)------------------------------
% 7.57/1.82 % (2800706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.57/1.82 % (2800706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.82 % (2800706)CaDiCaL version: 2.1.3
% 7.57/1.82 % (2800706)Termination reason: Instruction limit
% 7.57/1.82 % (2800706)Termination phase: Saturation
% 7.57/1.82 % (2800706)Time elapsed: 0.015 s
% 7.57/1.82 % (2800706)Peak memory usage: 89 MB
% 7.57/1.82 % (2800706)Instructions burned: 36 (million)
% 7.57/1.82 % (2800700)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4122244938:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 7.57/1.82 % (2800703)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3431569513:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.57/1.82 % (2800702)dis+10_1_si=on:random_seed=2218925609:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.57/1.82 % (2800703)Refutation not found, incomplete strategy
% 7.57/1.82 % (2800703)------------------------------
% 7.57/1.82 % (2800703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.57/1.82 % (2800703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.57/1.82 % (2800703)CaDiCaL version: 2.1.3
% 7.57/1.82 % (2800703)Termination reason: Refutation not found, incomplete strategy
% 8.60/2.01 % (2800703)Time elapsed: 0.002 s
% 8.60/2.01 % (2800703)Peak memory usage: 88 MB
% 8.60/2.01 % (2800703)Instructions burned: 2 (million)
% 8.60/2.01 % (2800702)Instruction limit reached!
% 8.60/2.01 % (2800702)------------------------------
% 8.60/2.01 % (2800702)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.01 % (2800702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.01 % (2800702)CaDiCaL version: 2.1.3
% 8.60/2.01 % (2800702)Termination reason: Instruction limit
% 8.60/2.01 % (2800702)Termination phase: Saturation
% 8.60/2.01 % (2800702)Time elapsed: 0.008 s
% 8.60/2.01 % (2800702)Peak memory usage: 88 MB
% 8.60/2.01 % (2800702)Instructions burned: 10 (million)
% 8.60/2.01 % (2800709)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=649792964:i=2:fsr=off:rtra=on:inst=on_2992 on theBenchmark for (2992ds/2Mi)
% 8.60/2.01 % (2800709)Instruction limit reached!
% 8.60/2.01 % (2800709)------------------------------
% 8.60/2.01 % (2800709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.01 % (2800709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.01 % (2800709)CaDiCaL version: 2.1.3
% 8.60/2.01 % (2800709)Termination reason: Instruction limit
% 8.60/2.01 % (2800709)Termination phase: Saturation
% 8.60/2.01 % (2800709)Time elapsed: 0.002 s
% 8.60/2.01 % (2800709)Peak memory usage: 89 MB
% 8.60/2.01 % (2800709)Instructions burned: 5 (million)
% 8.60/2.01 % (2800700)Instruction limit reached!
% 8.60/2.01 % (2800700)------------------------------
% 8.60/2.01 % (2800700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.01 % (2800700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.01 % (2800700)CaDiCaL version: 2.1.3
% 8.60/2.01 % (2800700)Termination reason: Instruction limit
% 8.60/2.01 % (2800700)Termination phase: Saturation
% 8.60/2.01 % (2800700)Time elapsed: 0.115 s
% 8.60/2.01 % (2800700)Peak memory usage: 117 MB
% 8.60/2.01 % (2800700)Instructions burned: 127 (million)
% 8.60/2.01 % (2800710)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=2476727026:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2992 on theBenchmark for (2992ds/8Mi)
% 8.60/2.01 % (2800710)Instruction limit reached!
% 8.60/2.01 % (2800710)------------------------------
% 8.60/2.01 % (2800710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.01 % (2800710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.01 % (2800710)CaDiCaL version: 2.1.3
% 8.60/2.01 % (2800710)Termination reason: Instruction limit
% 8.60/2.01 % (2800710)Termination phase: Saturation
% 8.60/2.01 % (2800710)Time elapsed: 0.008 s
% 8.60/2.01 % (2800710)Peak memory usage: 88 MB
% 8.60/2.01 % (2800710)Instructions burned: 8 (million)
% 8.60/2.01 % (2800711)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=791257836:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi)
% 8.60/2.01 % (2800698)------------------------------
% 8.60/2.01 % (2800698)------------------------------
% 8.60/2.01 % (2800714)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2822581291:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 8.60/2.01 % (2800716)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3582649501:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 8.60/2.01 % (2800714)Instruction limit reached!
% 8.60/2.01 % (2800714)------------------------------
% 8.60/2.01 % (2800714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.01 % (2800714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.01 % (2800714)CaDiCaL version: 2.1.3
% 8.60/2.01 % (2800714)Termination reason: Instruction limit
% 8.60/2.01 % (2800714)Termination phase: Saturation
% 8.60/2.01 % (2800714)Time elapsed: 0.032 s
% 8.60/2.01 % (2800714)Peak memory usage: 116 MB
% 8.60/2.01 % (2800714)Instructions burned: 13 (million)
% 8.60/2.01 % (2800716)Refutation not found, incomplete strategy
% 8.60/2.01 % (2800716)------------------------------
% 8.60/2.01 % (2800716)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.60/2.01 % (2800716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.60/2.01 % (2800716)CaDiCaL version: 2.1.3
% 8.60/2.01 % (2800716)Termination reason: Refutation not found, incomplete strategy
% 10.81/2.20 % (2800716)Time elapsed: 0.016 s
% 10.81/2.20 % (2800716)Peak memory usage: 111 MB
% 10.81/2.20 % (2800716)Instructions burned: 5 (million)
% 10.81/2.20 % (2800717)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1180921634:i=10:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 10.81/2.20 % (2800717)Instruction limit reached!
% 10.81/2.20 % (2800717)------------------------------
% 10.81/2.20 % (2800717)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.20 % (2800717)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.20 % (2800717)CaDiCaL version: 2.1.3
% 10.81/2.20 % (2800717)Termination reason: Instruction limit
% 10.81/2.20 % (2800717)Termination phase: Saturation
% 10.81/2.20 % (2800717)Time elapsed: 0.009 s
% 10.81/2.20 % (2800717)Peak memory usage: 88 MB
% 10.81/2.20 % (2800717)Instructions burned: 11 (million)
% 10.81/2.20 % (2800703)------------------------------
% 10.81/2.20 % (2800703)------------------------------
% 10.81/2.20 % (2800720)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1560865328:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi)
% 10.81/2.20 % (2800722)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=2380354518:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi)
% 10.81/2.20 % (2800711)Instruction limit reached!
% 10.81/2.20 % (2800711)------------------------------
% 10.81/2.20 % (2800711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.20 % (2800711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.20 % (2800711)CaDiCaL version: 2.1.3
% 10.81/2.20 % (2800711)Termination reason: Instruction limit
% 10.81/2.20 % (2800711)Termination phase: Saturation
% 10.81/2.20 % (2800711)Time elapsed: 0.181 s
% 10.81/2.20 % (2800711)Peak memory usage: 89 MB
% 10.81/2.20 % (2800711)Instructions burned: 371 (million)
% 10.81/2.20 % (2800724)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=2392835295:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 10.81/2.20 % (2800716)------------------------------
% 10.81/2.20 % (2800716)------------------------------
% 10.81/2.20 % (2800722)Instruction limit reached!
% 10.81/2.20 % (2800722)------------------------------
% 10.81/2.20 % (2800722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.20 % (2800722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.20 % (2800722)CaDiCaL version: 2.1.3
% 10.81/2.20 % (2800722)Termination reason: Instruction limit
% 10.81/2.20 % (2800722)Termination phase: Saturation
% 10.81/2.20 % (2800722)Time elapsed: 0.048 s
% 10.81/2.20 % (2800722)Peak memory usage: 90 MB
% 10.81/2.20 % (2800722)Instructions burned: 76 (million)
% 10.81/2.20 % (2800720)Instruction limit reached!
% 10.81/2.20 % (2800720)------------------------------
% 10.81/2.20 % (2800720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.81/2.20 % (2800720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.81/2.20 % (2800720)CaDiCaL version: 2.1.3
% 10.81/2.20 % (2800720)Termination reason: Instruction limit
% 10.81/2.20 % (2800720)Termination phase: Saturation
% 10.81/2.20 % (2800720)Time elapsed: 0.088 s
% 10.81/2.20 % (2800720)Peak memory usage: 133 MB
% 10.81/2.20 % (2800720)Instructions burned: 72 (million)
% 10.81/2.20 % (2800728)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3948566218:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 10.81/2.20 % (2800726)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1582000888:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 10.81/2.20 % (2800733)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3451155814:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 10.81/2.20 % (2800731)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1792034477:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 10.81/2.20 % (2800732)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2357697986:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi)
% 10.81/2.20 % (2800734)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=4078713675:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 12.80/2.59 % (2800726)Instruction limit reached!
% 12.80/2.59 % (2800726)------------------------------
% 12.80/2.59 % (2800726)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.59 % (2800726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.59 % (2800726)CaDiCaL version: 2.1.3
% 12.80/2.59 % (2800726)Termination reason: Instruction limit
% 12.80/2.59 % (2800726)Termination phase: Saturation
% 12.80/2.59 % (2800726)Time elapsed: 0.108 s
% 12.80/2.59 % (2800726)Peak memory usage: 117 MB
% 12.80/2.59 % (2800726)Instructions burned: 130 (million)
% 12.80/2.59 % (2800724)Instruction limit reached!
% 12.80/2.59 % (2800724)------------------------------
% 12.80/2.59 % (2800724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.59 % (2800724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.59 % (2800724)CaDiCaL version: 2.1.3
% 12.80/2.59 % (2800724)Termination reason: Instruction limit
% 12.80/2.59 % (2800724)Termination phase: Saturation
% 12.80/2.59 % (2800724)Time elapsed: 0.190 s
% 12.80/2.59 % (2800724)Peak memory usage: 90 MB
% 12.80/2.59 % (2800724)Instructions burned: 294 (million)
% 12.80/2.59 % (2800731)Instruction limit reached!
% 12.80/2.59 % (2800731)------------------------------
% 12.80/2.59 % (2800731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.59 % (2800731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.59 % (2800731)CaDiCaL version: 2.1.3
% 12.80/2.59 % (2800731)Termination reason: Instruction limit
% 12.80/2.59 % (2800731)Termination phase: Saturation
% 12.80/2.59 % (2800731)Time elapsed: 0.071 s
% 12.80/2.59 % (2800731)Peak memory usage: 133 MB
% 12.80/2.59 % (2800731)Instructions burned: 41 (million)
% 12.80/2.59 % (2800728)Instruction limit reached!
% 12.80/2.59 % (2800728)------------------------------
% 12.80/2.59 % (2800728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.59 % (2800728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.59 % (2800728)CaDiCaL version: 2.1.3
% 12.80/2.59 % (2800728)Termination reason: Instruction limit
% 12.80/2.59 % (2800728)Termination phase: Saturation
% 12.80/2.59 % (2800728)Time elapsed: 0.126 s
% 12.80/2.59 % (2800728)Peak memory usage: 134 MB
% 12.80/2.59 % (2800728)Instructions burned: 132 (million)
% 12.80/2.59 % (2800734)Instruction limit reached!
% 12.80/2.59 % (2800734)------------------------------
% 12.80/2.59 % (2800734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.59 % (2800734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.59 % (2800734)CaDiCaL version: 2.1.3
% 12.80/2.59 % (2800734)Termination reason: Instruction limit
% 12.80/2.59 % (2800734)Termination phase: Saturation
% 12.80/2.59 % (2800734)Time elapsed: 0.109 s
% 12.80/2.59 % (2800734)Peak memory usage: 117 MB
% 12.80/2.59 % (2800734)Instructions burned: 131 (million)
% 12.80/2.59 % (2800741)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=2822444218:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2987 on theBenchmark for (2987ds/259Mi)
% 12.80/2.59 % (2800732)Instruction limit reached!
% 12.80/2.59 % (2800732)------------------------------
% 12.80/2.59 % (2800732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.59 % (2800732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.59 % (2800732)CaDiCaL version: 2.1.3
% 12.80/2.59 % (2800732)Termination reason: Instruction limit
% 12.80/2.59 % (2800732)Termination phase: Saturation
% 12.80/2.59 % (2800732)Time elapsed: 0.175 s
% 12.80/2.59 % (2800732)Peak memory usage: 91 MB
% 12.80/2.59 % (2800732)Instructions burned: 307 (million)
% 12.80/2.59 % (2800744)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2459493450:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 12.80/2.59 % (2800742)dis+10_1_si=on:random_seed=881174715:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi)
% 12.80/2.59 % (2800743)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=874334652:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi)
% 12.80/2.59 % (2800741)Refutation not found, incomplete strategy
% 12.80/2.59 % (2800741)------------------------------
% 12.80/2.59 % (2800741)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.78 % (2800741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.78 % (2800741)CaDiCaL version: 2.1.3
% 13.52/2.78 % (2800741)Termination reason: Refutation not found, incomplete strategy
% 13.52/2.78 % (2800741)Time elapsed: 0.026 s
% 13.52/2.78 % (2800741)Peak memory usage: 111 MB
% 13.52/2.78 % (2800741)Instructions burned: 5 (million)
% 13.52/2.78 % (2800733)Instruction limit reached!
% 13.52/2.78 % (2800733)------------------------------
% 13.52/2.78 % (2800733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.78 % (2800733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.78 % (2800733)CaDiCaL version: 2.1.3
% 13.52/2.78 % (2800733)Termination reason: Instruction limit
% 13.52/2.78 % (2800733)Termination phase: Saturation
% 13.52/2.78 % (2800733)Time elapsed: 0.235 s
% 13.52/2.78 % (2800733)Peak memory usage: 138 MB
% 13.52/2.78 % (2800733)Instructions burned: 599 (million)
% 13.52/2.78 % (2800745)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2663458751:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 13.52/2.78 % (2800744)Instruction limit reached!
% 13.52/2.78 % (2800744)------------------------------
% 13.52/2.78 % (2800744)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.78 % (2800744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.78 % (2800744)CaDiCaL version: 2.1.3
% 13.52/2.78 % (2800744)Termination reason: Instruction limit
% 13.52/2.78 % (2800744)Termination phase: Saturation
% 13.52/2.78 % (2800744)Time elapsed: 0.090 s
% 13.52/2.78 % (2800744)Peak memory usage: 90 MB
% 13.52/2.78 % (2800744)Instructions burned: 141 (million)
% 13.52/2.78 % (2800745)Refutation not found, incomplete strategy
% 13.52/2.78 % (2800745)------------------------------
% 13.52/2.78 % (2800745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.78 % (2800745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.78 % (2800745)CaDiCaL version: 2.1.3
% 13.52/2.78 % (2800745)Termination reason: Refutation not found, incomplete strategy
% 13.52/2.78 % (2800745)Time elapsed: 0.027 s
% 13.52/2.78 % (2800745)Peak memory usage: 112 MB
% 13.52/2.78 % (2800745)Instructions burned: 6 (million)
% 13.52/2.78 % (2800750)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=1242575550:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 13.52/2.78 % (2800751)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=2987614466:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 13.52/2.78 % (2800751)Refutation not found, incomplete strategy
% 13.52/2.78 % (2800751)------------------------------
% 13.52/2.78 % (2800751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.78 % (2800751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.78 % (2800751)CaDiCaL version: 2.1.3
% 13.52/2.78 % (2800751)Termination reason: Refutation not found, incomplete strategy
% 13.52/2.78 % (2800751)Time elapsed: 0.016 s
% 13.52/2.78 % (2800751)Peak memory usage: 113 MB
% 13.52/2.78 % (2800751)Instructions burned: 7 (million)
% 13.52/2.78 % (2800750)Instruction limit reached!
% 13.52/2.78 % (2800750)------------------------------
% 13.52/2.78 % (2800750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.78 % (2800750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.78 % (2800750)CaDiCaL version: 2.1.3
% 13.52/2.78 % (2800750)Termination reason: Instruction limit
% 13.52/2.78 % (2800750)Termination phase: Saturation
% 13.52/2.78 % (2800750)Time elapsed: 0.071 s
% 13.52/2.78 % (2800750)Peak memory usage: 89 MB
% 13.52/2.78 % (2800750)Instructions burned: 122 (million)
% 13.52/2.78 % (2800743)Instruction limit reached!
% 13.52/2.78 % (2800743)------------------------------
% 13.52/2.78 % (2800743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.52/2.78 % (2800743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.52/2.78 % (2800743)CaDiCaL version: 2.1.3
% 13.52/2.78 % (2800743)Termination reason: Instruction limit
% 13.52/2.78 % (2800743)Termination phase: Saturation
% 13.52/2.78 % (2800743)Time elapsed: 0.215 s
% 13.52/2.78 % (2800743)Peak memory usage: 96 MB
% 13.52/2.78 % (2800743)Instructions burned: 383 (million)
% 13.52/2.78 % (2800753)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=2718794342:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 17.91/3.18 % (2800753)Refutation not found, incomplete strategy
% 17.91/3.18 % (2800753)------------------------------
% 17.91/3.18 % (2800753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/3.18 % (2800753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/3.18 % (2800753)CaDiCaL version: 2.1.3
% 17.91/3.18 % (2800753)Termination reason: Refutation not found, incomplete strategy
% 17.91/3.18 % (2800753)Time elapsed: 0.027 s
% 17.91/3.18 % (2800753)Peak memory usage: 112 MB
% 17.91/3.18 % (2800753)Instructions burned: 7 (million)
% 17.91/3.18 % (2800741)------------------------------
% 17.91/3.18 % (2800741)------------------------------
% 17.91/3.18 % (2800751)------------------------------
% 17.91/3.18 % (2800751)------------------------------
% 17.91/3.18 % (2800756)dis+1010_1_to=kbo:si=on:random_seed=1098439072:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi)
% 17.91/3.18 % (2800758)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2025266571:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 17.91/3.18 % (2800745)------------------------------
% 17.91/3.18 % (2800745)------------------------------
% 17.91/3.18 % (2800760)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=609424712:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi)
% 17.91/3.18 % (2800759)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=1362803678:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi)
% 17.91/3.18 % (2800756)Instruction limit reached!
% 17.91/3.18 % (2800756)------------------------------
% 17.91/3.18 % (2800756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/3.18 % (2800756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/3.18 % (2800756)CaDiCaL version: 2.1.3
% 17.91/3.18 % (2800756)Termination reason: Instruction limit
% 17.91/3.18 % (2800756)Termination phase: Saturation
% 17.91/3.18 % (2800756)Time elapsed: 0.123 s
% 17.91/3.18 % (2800756)Peak memory usage: 91 MB
% 17.91/3.19 % (2800756)Instructions burned: 175 (million)
% 17.91/3.19 % (2800753)------------------------------
% 17.91/3.19 % (2800753)------------------------------
% 17.91/3.19 % (2800760)Instruction limit reached!
% 17.91/3.19 % (2800760)------------------------------
% 17.91/3.19 % (2800760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/3.19 % (2800760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/3.19 % (2800760)CaDiCaL version: 2.1.3
% 17.91/3.19 % (2800760)Termination reason: Instruction limit
% 17.91/3.19 % (2800760)Termination phase: Saturation
% 17.91/3.19 % (2800760)Time elapsed: 0.100 s
% 17.91/3.19 % (2800760)Peak memory usage: 136 MB
% 17.91/3.19 % (2800760)Instructions burned: 216 (million)
% 17.91/3.19 % (2800763)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=3185162121:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 17.91/3.19 % (2800769)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2318486570:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi)
% 17.91/3.19 % (2800766)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=479123538:st=2:i=295:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/295Mi)
% 17.91/3.19 % (2800766)Refutation not found, incomplete strategy
% 17.91/3.19 % (2800766)------------------------------
% 17.91/3.19 % (2800766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/3.19 % (2800766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/3.19 % (2800766)CaDiCaL version: 2.1.3
% 17.91/3.19 % (2800766)Termination reason: Refutation not found, incomplete strategy
% 17.91/3.19 % (2800766)Time elapsed: 0.001 s
% 17.91/3.19 % (2800766)Peak memory usage: 88 MB
% 17.91/3.19 % (2800758)Instruction limit reached!
% 17.91/3.19 % (2800758)------------------------------
% 17.91/3.19 % (2800758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.91/3.19 % (2800758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.91/3.19 % (2800758)CaDiCaL version: 2.1.3
% 17.91/3.19 % (2800758)Termination reason: Instruction limit
% 17.91/3.19 % (2800758)Termination phase: Saturation
% 17.91/3.19 % (2800758)Time elapsed: 0.259 s
% 18.36/3.37 % (2800758)Peak memory usage: 120 MB
% 18.36/3.37 % (2800758)Instructions burned: 329 (million)
% 18.36/3.37 % (2800768)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3568992864:i=328:kws=inv_frequency:nm=20:rtra=on_2981 on theBenchmark for (2981ds/328Mi)
% 18.36/3.37 % (2800742)Instruction limit reached!
% 18.36/3.37 % (2800742)------------------------------
% 18.36/3.37 % (2800742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/3.37 % (2800742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/3.37 % (2800742)CaDiCaL version: 2.1.3
% 18.36/3.37 % (2800742)Termination reason: Instruction limit
% 18.36/3.37 % (2800742)Termination phase: Saturation
% 18.36/3.37 % (2800742)Time elapsed: 0.625 s
% 18.36/3.37 % (2800742)Peak memory usage: 95 MB
% 18.36/3.37 % (2800742)Instructions burned: 1001 (million)
% 18.36/3.37 % (2800769)Instruction limit reached!
% 18.36/3.37 % (2800769)------------------------------
% 18.36/3.37 % (2800769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/3.37 % (2800769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/3.37 % (2800769)CaDiCaL version: 2.1.3
% 18.36/3.37 % (2800769)Termination reason: Instruction limit
% 18.36/3.37 % (2800769)Termination phase: Saturation
% 18.36/3.37 % (2800769)Time elapsed: 0.113 s
% 18.36/3.37 % (2800769)Peak memory usage: 117 MB
% 18.36/3.37 % (2800769)Instructions burned: 283 (million)
% 18.36/3.37 % (2800759)Instruction limit reached!
% 18.36/3.37 % (2800759)------------------------------
% 18.36/3.37 % (2800759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/3.37 % (2800759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/3.37 % (2800759)CaDiCaL version: 2.1.3
% 18.36/3.37 % (2800759)Termination reason: Instruction limit
% 18.36/3.37 % (2800759)Termination phase: Saturation
% 18.36/3.37 % (2800759)Time elapsed: 0.328 s
% 18.36/3.37 % (2800759)Peak memory usage: 134 MB
% 18.36/3.37 % (2800759)Instructions burned: 483 (million)
% 18.36/3.37 % (2800772)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1920610197:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2980 on theBenchmark for (2980ds/484Mi)
% 18.36/3.37 % (2800772)Refutation not found, incomplete strategy
% 18.36/3.37 % (2800772)------------------------------
% 18.36/3.37 % (2800772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/3.37 % (2800772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/3.37 % (2800772)CaDiCaL version: 2.1.3
% 18.36/3.37 % (2800772)Termination reason: Refutation not found, incomplete strategy
% 18.36/3.37 % (2800772)Time elapsed: 0.001 s
% 18.36/3.37 % (2800772)Peak memory usage: 87 MB
% 18.36/3.37 % (2800763)Instruction limit reached!
% 18.36/3.37 % (2800763)------------------------------
% 18.36/3.37 % (2800763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/3.37 % (2800763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/3.37 % (2800763)CaDiCaL version: 2.1.3
% 18.36/3.37 % (2800763)Termination reason: Instruction limit
% 18.36/3.37 % (2800763)Termination phase: Saturation
% 18.36/3.37 % (2800763)Time elapsed: 0.252 s
% 18.36/3.37 % (2800763)Peak memory usage: 119 MB
% 18.36/3.37 % (2800763)Instructions burned: 349 (million)
% 18.36/3.37 % (2800774)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=4128691616:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi)
% 18.36/3.37 % (2800774)Refutation not found, incomplete strategy
% 18.36/3.37 % (2800774)------------------------------
% 18.36/3.37 % (2800774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/3.37 % (2800774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.36/3.37 % (2800774)CaDiCaL version: 2.1.3
% 18.36/3.37 % (2800774)Termination reason: Refutation not found, incomplete strategy
% 18.36/3.37 % (2800774)Time elapsed: 0.026 s
% 18.36/3.37 % (2800774)Peak memory usage: 111 MB
% 18.36/3.37 % (2800774)Instructions burned: 5 (million)
% 18.36/3.37 % (2800775)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1837712948:i=416:rtra=on:gtg=position:ss=axioms_2979 on theBenchmark for (2979ds/416Mi)
% 18.36/3.37 % (2800775)Refutation not found, incomplete strategy
% 18.36/3.37 % (2800775)------------------------------
% 18.36/3.37 % (2800775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.36/3.37 % (2800775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.68 % (2800775)CaDiCaL version: 2.1.3
% 20.32/3.68 % (2800775)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.68 % (2800775)Time elapsed: 0.016 s
% 20.32/3.68 % (2800775)Peak memory usage: 111 MB
% 20.32/3.68 % (2800775)Instructions burned: 5 (million)
% 20.32/3.68 % (2800766)------------------------------
% 20.32/3.68 % (2800766)------------------------------
% 20.32/3.68 % (2800768)Instruction limit reached!
% 20.32/3.68 % (2800768)------------------------------
% 20.32/3.68 % (2800768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.68 % (2800768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.68 % (2800768)CaDiCaL version: 2.1.3
% 20.32/3.68 % (2800768)Termination reason: Instruction limit
% 20.32/3.68 % (2800768)Termination phase: Saturation
% 20.32/3.68 % (2800768)Time elapsed: 0.224 s
% 20.32/3.68 % (2800768)Peak memory usage: 118 MB
% 20.32/3.68 % (2800768)Instructions burned: 329 (million)
% 20.32/3.68 % (2800777)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3342049909:i=471:thf=on:kws=precedence:rtra=on_2979 on theBenchmark for (2979ds/471Mi)
% 20.32/3.68 % (2800779)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=4283382043:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi)
% 20.32/3.68 % (2800775)------------------------------
% 20.32/3.68 % (2800775)------------------------------
% 20.32/3.68 % (2800781)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3273516699:i=375:kws=inv_arity_squared:rtra=on_2978 on theBenchmark for (2978ds/375Mi)
% 20.32/3.68 % (2800772)------------------------------
% 20.32/3.68 % (2800772)------------------------------
% 20.32/3.68 % (2800782)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=1335405167:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi)
% 20.32/3.68 % (2800782)Refutation not found, incomplete strategy
% 20.32/3.68 % (2800782)------------------------------
% 20.32/3.68 % (2800782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.68 % (2800782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.68 % (2800782)CaDiCaL version: 2.1.3
% 20.32/3.68 % (2800782)Termination reason: Refutation not found, incomplete strategy
% 20.32/3.68 % (2800782)Time elapsed: 0.026 s
% 20.32/3.68 % (2800782)Peak memory usage: 111 MB
% 20.32/3.68 % (2800782)Instructions burned: 5 (million)
% 20.32/3.68 % (2800774)------------------------------
% 20.32/3.68 % (2800774)------------------------------
% 20.32/3.68 % (2800785)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1798721398:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi)
% 20.32/3.68 % (2800788)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2553938558:i=334:rtra=on_2976 on theBenchmark for (2976ds/334Mi)
% 20.32/3.68 % (2800779)Instruction limit reached!
% 20.32/3.68 % (2800779)------------------------------
% 20.32/3.68 % (2800779)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.68 % (2800779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.68 % (2800779)CaDiCaL version: 2.1.3
% 20.32/3.68 % (2800779)Termination reason: Instruction limit
% 20.32/3.68 % (2800779)Termination phase: Saturation
% 20.32/3.68 % (2800779)Time elapsed: 0.228 s
% 20.32/3.68 % (2800779)Peak memory usage: 134 MB
% 20.32/3.68 % (2800779)Instructions burned: 276 (million)
% 20.32/3.68 % (2800777)Instruction limit reached!
% 20.32/3.68 % (2800777)------------------------------
% 20.32/3.68 % (2800777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.32/3.68 % (2800777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.32/3.68 % (2800777)CaDiCaL version: 2.1.3
% 20.32/3.68 % (2800777)Termination reason: Instruction limit
% 20.32/3.68 % (2800777)Termination phase: Saturation
% 20.32/3.68 % (2800777)Time elapsed: 0.268 s
% 20.32/3.68 % (2800777)Peak memory usage: 119 MB
% 20.32/3.68 % (2800777)Instructions burned: 472 (million)
% 20.32/3.68 % (2800789)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1150367283:i=359:rtra=on:gtg=exists_top:ss=axioms_2976 on theBenchmark for (2976ds/359Mi)
% 20.32/3.68 % (2800785)Instruction limit reached!
% 24.39/4.07 % (2800785)------------------------------
% 24.39/4.07 % (2800785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/4.07 % (2800785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/4.07 % (2800785)CaDiCaL version: 2.1.3
% 24.39/4.07 % (2800785)Termination reason: Instruction limit
% 24.39/4.07 % (2800785)Termination phase: Saturation
% 24.39/4.07 % (2800785)Time elapsed: 0.164 s
% 24.39/4.07 % (2800785)Peak memory usage: 92 MB
% 24.39/4.07 % (2800785)Instructions burned: 514 (million)
% 24.39/4.07 % (2800781)Instruction limit reached!
% 24.39/4.07 % (2800781)------------------------------
% 24.39/4.07 % (2800781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/4.07 % (2800781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/4.07 % (2800781)CaDiCaL version: 2.1.3
% 24.39/4.07 % (2800781)Termination reason: Instruction limit
% 24.39/4.07 % (2800781)Termination phase: Saturation
% 24.39/4.07 % (2800781)Time elapsed: 0.244 s
% 24.39/4.07 % (2800781)Peak memory usage: 119 MB
% 24.39/4.07 % (2800781)Instructions burned: 375 (million)
% 24.39/4.07 % (2800792)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=521593176:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2975 on theBenchmark for (2975ds/341Mi)
% 24.39/4.07 % (2800782)------------------------------
% 24.39/4.07 % (2800782)------------------------------
% 24.39/4.07 % (2800793)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=1840645497:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2975 on theBenchmark for (2975ds/261Mi)
% 24.39/4.07 % (2800795)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=2746491565:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2974 on theBenchmark for (2974ds/235Mi)
% 24.39/4.07 % (2800793)Refutation not found, incomplete strategy
% 24.39/4.07 % (2800793)------------------------------
% 24.39/4.07 % (2800793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/4.07 % (2800793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/4.07 % (2800793)CaDiCaL version: 2.1.3
% 24.39/4.07 % (2800793)Termination reason: Refutation not found, incomplete strategy
% 24.39/4.07 % (2800793)Time elapsed: 0.026 s
% 24.39/4.07 % (2800793)Peak memory usage: 111 MB
% 24.39/4.07 % (2800793)Instructions burned: 5 (million)
% 24.39/4.07 % (2800795)Refutation not found, incomplete strategy
% 24.39/4.07 % (2800795)------------------------------
% 24.39/4.07 % (2800795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/4.07 % (2800795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/4.07 % (2800795)CaDiCaL version: 2.1.3
% 24.39/4.07 % (2800795)Termination reason: Refutation not found, incomplete strategy
% 24.39/4.07 % (2800795)Time elapsed: 0.016 s
% 24.39/4.07 % (2800795)Peak memory usage: 111 MB
% 24.39/4.07 % (2800795)Instructions burned: 5 (million)
% 24.39/4.07 % (2800789)Instruction limit reached!
% 24.39/4.07 % (2800789)------------------------------
% 24.39/4.07 % (2800789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/4.07 % (2800789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/4.07 % (2800789)CaDiCaL version: 2.1.3
% 24.39/4.07 % (2800789)Termination reason: Instruction limit
% 24.39/4.07 % (2800789)Termination phase: Saturation
% 24.39/4.07 % (2800789)Time elapsed: 0.182 s
% 24.39/4.07 % (2800789)Peak memory usage: 90 MB
% 24.39/4.07 % (2800789)Instructions burned: 360 (million)
% 24.39/4.07 % (2800796)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=745197880:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2974 on theBenchmark for (2974ds/273Mi)
% 24.39/4.07 % (2800788)Instruction limit reached!
% 24.39/4.07 % (2800788)------------------------------
% 24.39/4.07 % (2800788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 24.39/4.07 % (2800788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.39/4.07 % (2800788)CaDiCaL version: 2.1.3
% 24.39/4.07 % (2800788)Termination reason: Instruction limit
% 24.39/4.07 % (2800788)Termination phase: Saturation
% 24.39/4.07 % (2800788)Time elapsed: 0.251 s
% 24.39/4.07 % (2800788)Peak memory usage: 135 MB
% 24.39/4.07 % (2800788)Instructions burned: 335 (million)
% 24.39/4.07 % (2800799)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2902586370:i=146:doe=on:rtra=on_2973 on theBenchmark for (2973ds/146Mi)
% 25.63/4.32 % (2800795)------------------------------
% 25.63/4.32 % (2800795)------------------------------
% 25.63/4.32 % (2800792)Instruction limit reached!
% 25.63/4.32 % (2800792)------------------------------
% 25.63/4.32 % (2800792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800792)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800792)Termination reason: Instruction limit
% 25.63/4.32 % (2800792)Termination phase: Saturation
% 25.63/4.32 % (2800792)Time elapsed: 0.230 s
% 25.63/4.32 % (2800792)Peak memory usage: 122 MB
% 25.63/4.32 % (2800792)Instructions burned: 341 (million)
% 25.63/4.32 % (2800801)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=970963684:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi)
% 25.63/4.32 % (2800799)Instruction limit reached!
% 25.63/4.32 % (2800799)------------------------------
% 25.63/4.32 % (2800799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800799)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800799)Termination reason: Instruction limit
% 25.63/4.32 % (2800799)Termination phase: Saturation
% 25.63/4.32 % (2800799)Time elapsed: 0.095 s
% 25.63/4.32 % (2800799)Peak memory usage: 90 MB
% 25.63/4.32 % (2800799)Instructions burned: 147 (million)
% 25.63/4.32 % (2800803)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=2223931811:avsq=on:i=276:avsqr=1,2:rtra=on_2972 on theBenchmark for (2972ds/276Mi)
% 25.63/4.32 % (2800793)------------------------------
% 25.63/4.32 % (2800793)------------------------------
% 25.63/4.32 % (2800796)Instruction limit reached!
% 25.63/4.32 % (2800796)------------------------------
% 25.63/4.32 % (2800796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800796)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800796)Termination reason: Instruction limit
% 25.63/4.32 % (2800796)Termination phase: Saturation
% 25.63/4.32 % (2800796)Time elapsed: 0.184 s
% 25.63/4.32 % (2800796)Peak memory usage: 91 MB
% 25.63/4.32 % (2800796)Instructions burned: 274 (million)
% 25.63/4.32 % (2800805)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=2819803937:i=1052:rtra=on_2972 on theBenchmark for (2972ds/1052Mi)
% 25.63/4.32 % (2800807)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=3544503046:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2971 on theBenchmark for (2971ds/655Mi)
% 25.63/4.32 % (2800809)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=1439701464:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2971 on theBenchmark for (2971ds/1054Mi)
% 25.63/4.32 % (2800809)Refutation not found, incomplete strategy
% 25.63/4.32 % (2800809)------------------------------
% 25.63/4.32 % (2800809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800809)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800809)Termination reason: Refutation not found, incomplete strategy
% 25.63/4.32 % (2800809)Time elapsed: 0.001 s
% 25.63/4.32 % (2800809)Peak memory usage: 87 MB
% 25.63/4.32 % (2800810)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1339967131:i=107:rtra=on_2971 on theBenchmark for (2971ds/107Mi)
% 25.63/4.32 % (2800811)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=4108381592:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi)
% 25.63/4.32 % (2800810)Refutation not found, incomplete strategy
% 25.63/4.32 % (2800810)------------------------------
% 25.63/4.32 % (2800810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800810)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800810)Termination reason: Refutation not found, incomplete strategy
% 25.63/4.32 % (2800810)Time elapsed: 0.027 s
% 25.63/4.32 % (2800810)Peak memory usage: 112 MB
% 25.63/4.32 % (2800810)Instructions burned: 7 (million)
% 25.63/4.32 % (2800803)Instruction limit reached!
% 25.63/4.32 % (2800803)------------------------------
% 25.63/4.32 % (2800803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800803)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800803)Termination reason: Instruction limit
% 25.63/4.32 % (2800803)Termination phase: Saturation
% 25.63/4.32 % (2800803)Time elapsed: 0.229 s
% 25.63/4.32 % (2800803)Peak memory usage: 134 MB
% 25.63/4.32 % (2800803)Instructions burned: 276 (million)
% 25.63/4.32 % (2800809)------------------------------
% 25.63/4.32 % (2800809)------------------------------
% 25.63/4.32 % (2800817)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off
% 25.63/4.32 % (2800817)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1654271252:i=1090:aac=none:nm=0:rtra=on:rawr=on_2969 on theBenchmark for (2969ds/1090Mi)
% 25.63/4.32 % (2800805)Instruction limit reached!
% 25.63/4.32 % (2800805)------------------------------
% 25.63/4.32 % (2800805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800805)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800805)Termination reason: Instruction limit
% 25.63/4.32 % (2800805)Termination phase: Saturation
% 25.63/4.32 % (2800805)Time elapsed: 0.330 s
% 25.63/4.32 % (2800805)Peak memory usage: 92 MB
% 25.63/4.32 % (2800805)Instructions burned: 1053 (million)
% 25.63/4.32 % (2800810)------------------------------
% 25.63/4.32 % (2800810)------------------------------
% 25.63/4.32 % (2800820)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2051944025:i=312:kws=inv_frequency:nm=20:rtra=on_2967 on theBenchmark for (2967ds/312Mi)
% 25.63/4.32 % (2800819)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=85342859:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2968 on theBenchmark for (2968ds/130Mi)
% 25.63/4.32 % (2800807)Instruction limit reached!
% 25.63/4.32 % (2800807)------------------------------
% 25.63/4.32 % (2800807)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800807)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800807)Termination reason: Instruction limit
% 25.63/4.32 % (2800807)Termination phase: Saturation
% 25.63/4.32 % (2800807)Time elapsed: 0.381 s
% 25.63/4.32 % (2800807)Peak memory usage: 94 MB
% 25.63/4.32 % (2800807)Instructions burned: 656 (million)
% 25.63/4.32 % (2800811)Instruction limit reached!
% 25.63/4.32 % (2800811)------------------------------
% 25.63/4.32 % (2800811)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800811)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800811)Termination reason: Instruction limit
% 25.63/4.32 % (2800811)Termination phase: Saturation
% 25.63/4.32 % (2800811)Time elapsed: 0.303 s
% 25.63/4.32 % (2800811)Peak memory usage: 134 MB
% 25.63/4.32 % (2800811)Instructions burned: 451 (million)
% 25.63/4.32 % (2800819)First to succeed.
% 25.63/4.32 % (2800819)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2800655"
% 25.63/4.32 % (2800821)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=4286928430:i=491:doe=on:rtra=on:gtg=position_2967 on theBenchmark for (2967ds/491Mi)
% 25.63/4.32 % (2800821)Refutation not found, incomplete strategy
% 25.63/4.32 % (2800821)------------------------------
% 25.63/4.32 % (2800821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800821)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800821)Termination reason: Refutation not found, incomplete strategy
% 25.63/4.32 % (2800821)Time elapsed: 0.002 s
% 25.63/4.32 % (2800821)Peak memory usage: 89 MB
% 25.63/4.32 % (2800821)Instructions burned: 2 (million)
% 25.63/4.32 % (2800820)Instruction limit reached!
% 25.63/4.32 % (2800820)------------------------------
% 25.63/4.32 % (2800820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800820)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800820)Termination reason: Instruction limit
% 25.63/4.32 % (2800820)Termination phase: Saturation
% 25.63/4.32 % (2800820)Time elapsed: 0.115 s
% 25.63/4.32 % (2800820)Peak memory usage: 118 MB
% 25.63/4.32 % (2800820)Instructions burned: 315 (million)
% 25.63/4.32 % (2800824)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=2164371448:s2a=on:i=835:s2at=2:rtra=on_2966 on theBenchmark for (2966ds/835Mi)
% 25.63/4.32 % (2800825)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3602266493:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2966 on theBenchmark for (2966ds/307Mi)
% 25.63/4.32 % (2800825)Refutation not found, incomplete strategy
% 25.63/4.32 % (2800825)------------------------------
% 25.63/4.32 % (2800825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.63/4.32 % (2800825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.63/4.32 % (2800825)CaDiCaL version: 2.1.3
% 25.63/4.32 % (2800825)Termination reason: Refutation not found, incomplete strategy
% 25.63/4.32 % (2800825)Time elapsed: 0.003 s
% 25.63/4.32 % (2800825)Peak memory usage: 88 MB
% 25.63/4.32 % (2800825)Instructions burned: 2 (million)
% 25.63/4.32 % (2800827)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1566619342:i=776:doe=on:rtra=on_2965 on theBenchmark for (2965ds/776Mi)
% 25.63/4.32 % (2800817)Also succeeded, but the first one will report.
% 25.63/4.32 % (2800819)Refutation found. Thanks to Tanya!
% 25.63/4.32 % SZS status Unsatisfiable for theBenchmark
% 25.63/4.32 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/4.51 % (2800819)------------------------------
% 0.18/4.51 % (2800819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/4.51 % (2800819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/4.51 % (2800819)CaDiCaL version: 2.1.3
% 0.18/4.51 % (2800819)Termination reason: Refutation
% 0.18/4.51 % (2800819)Time elapsed: 0.100 s
% 0.18/4.51 % (2800819)Peak memory usage: 118 MB
% 0.18/4.51 % (2800819)Instructions burned: 115 (million)
% 0.18/4.51 % (2800819)------------------------------
% 0.18/4.51 % (2800819)------------------------------
% 0.18/4.51 % (2800655)Success in time 3.678 s
% 0.18/4.51 % Vampire exiting
%------------------------------------------------------------------------------