%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX109_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:45:54 PM UTC 2026
% Result : Theorem 15.11s 3.01s
% Output : Refutation 15.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 25
% Syntax : Number of formulae : 130 ( 1 unt; 0 typ; 23 def)
% Number of atoms : 528 ( 255 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 604 ( 206 ~; 206 |; 158 &)
% ( 22 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 242 ( 0 atm; 93 fun; 71 num; 78 var)
% Number of types : 4 ( 2 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 35 ( 33 usr; 23 prp; 0-4 aty)
% Number of functors : 23 ( 18 usr; 12 con; 0-2 aty)
% Number of variables : 298 ( 198 !; 100 ?; 298 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
general: $tType ).
tff(type_def_6,type,
symbol: $tType ).
tff(func_def_0,type,
f__integer__: $int > general ).
tff(func_def_1,type,
f__symbolic__: symbol > general ).
tff(func_def_2,type,
c__infimum__: general ).
tff(func_def_3,type,
c__supremum__: general ).
tff(func_def_8,type,
sK1: general > symbol ).
tff(func_def_9,type,
sK2: general > $int ).
tff(func_def_10,type,
sK3: ( general * general ) > $int ).
tff(func_def_11,type,
sK4: ( general * general ) > $int ).
tff(func_def_12,type,
sK5: ( general * general ) > general ).
tff(func_def_13,type,
sK6: ( general * general ) > general ).
tff(func_def_14,type,
sK7: general ).
tff(func_def_15,type,
sK8: general ).
tff(func_def_16,type,
sK9: general ).
tff(func_def_17,type,
sK10: general ).
tff(func_def_18,type,
sK11: general ).
tff(func_def_19,type,
sK12: general ).
tff(func_def_20,type,
sK13: $int ).
tff(func_def_21,type,
sK14: $int ).
tff(pred_def_1,type,
p__is_integer__: general > $o ).
tff(pred_def_2,type,
p__is_symbolic__: general > $o ).
tff(pred_def_3,type,
p__less_equal__: ( general * general ) > $o ).
tff(pred_def_4,type,
p__less__: ( general * general ) > $o ).
tff(pred_def_5,type,
p__greater_equal__: ( general * general ) > $o ).
tff(pred_def_6,type,
p__greater__: ( general * general ) > $o ).
tff(pred_def_8,type,
hq: ( general * general ) > $o ).
tff(pred_def_9,type,
tq: ( general * general ) > $o ).
tff(pred_def_10,type,
hp: ( general * general ) > $o ).
tff(pred_def_11,type,
tp: ( general * general ) > $o ).
tff(pred_def_13,type,
sP0: ( general * general * general * general ) > $o ).
tff(f18,axiom,
! [X3: general,X1: general,X2: general,X0: general] :
( ( ( ( X0 = X2 )
& ? [X4: general,X5: general] :
( ? [X7: $int,X6: $int] :
( ( X7 = 1 )
& ( X5 = f__integer__($difference(X6,X7)) )
& ( f__integer__(X6) = X3 ) )
& tp(X4,X5)
& ( X4 = X2 ) )
& ( X1 = X3 ) )
=> tq(X0,X1) )
& ( ( ( X0 = X2 )
& ? [X5: general,X4: general] :
( hp(X4,X5)
& ? [X6: $int,X7: $int] :
( ( f__integer__(X6) = X3 )
& ( X5 = f__integer__($difference(X6,X7)) )
& ( X7 = 1 ) )
& ( X4 = X2 ) )
& ( X1 = X3 ) )
=> hq(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2_right_0) ).
tff(f19,conjecture,
! [X3: general,X0: general,X2: general,X1: general] :
( ( ( ? [X5: $int,X4: $int] :
( ( X1 = f__integer__($sum(X4,X5)) )
& ( f__integer__(X4) = X3 )
& ( X5 = 1 ) )
& ( X0 = X2 )
& ? [X6: general,X7: general] :
( hp(X6,X7)
& ( X7 = X3 )
& ( X6 = X2 ) ) )
=> hq(X0,X1) )
& ( ( ? [X4: $int,X5: $int] :
( ( X1 = f__integer__($sum(X4,X5)) )
& ( X5 = 1 )
& ( f__integer__(X4) = X3 ) )
& ? [X7: general,X6: general] :
( ( X7 = X3 )
& tp(X6,X7)
& ( X6 = X2 ) )
& ( X0 = X2 ) )
=> tq(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_3_left_0) ).
tff(f20,negated_conjecture,
~ ! [X3: general,X0: general,X2: general,X1: general] :
( ( ( ? [X5: $int,X4: $int] :
( ( X1 = f__integer__($sum(X4,X5)) )
& ( f__integer__(X4) = X3 )
& ( X5 = 1 ) )
& ( X0 = X2 )
& ? [X6: general,X7: general] :
( hp(X6,X7)
& ( X7 = X3 )
& ( X6 = X2 ) ) )
=> hq(X0,X1) )
& ( ( ? [X4: $int,X5: $int] :
( ( X1 = f__integer__($sum(X4,X5)) )
& ( X5 = 1 )
& ( f__integer__(X4) = X3 ) )
& ? [X7: general,X6: general] :
( ( X7 = X3 )
& tp(X6,X7)
& ( X6 = X2 ) )
& ( X0 = X2 ) )
=> tq(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
tff(f21,plain,
! [X3: general,X1: general,X2: general,X0: general] :
( ( ( ( X0 = X2 )
& ? [X4: general,X5: general] :
( ? [X7: $int,X6: $int] :
( ( X7 = 1 )
& ( f__integer__($sum(X6,$uminus(X7))) = X5 )
& ( f__integer__(X6) = X3 ) )
& tp(X4,X5)
& ( X4 = X2 ) )
& ( X1 = X3 ) )
=> tq(X0,X1) )
& ( ( ( X0 = X2 )
& ? [X5: general,X4: general] :
( hp(X4,X5)
& ? [X6: $int,X7: $int] :
( ( f__integer__(X6) = X3 )
& ( f__integer__($sum(X6,$uminus(X7))) = X5 )
& ( X7 = 1 ) )
& ( X4 = X2 ) )
& ( X1 = X3 ) )
=> hq(X0,X1) ) ),
inference(theory_normalization,[],[f18]) ).
tff(f23,plain,
! [X3: general,X1: general,X2: general,X0: general] :
( ( ( ( X2 = X3 )
& ( X0 = X1 )
& ? [X9: general,X8: general] :
( hp(X9,X8)
& ? [X11: $int,X10: $int] :
( ( f__integer__($sum(X10,$uminus(X11))) = X8 )
& ( f__integer__(X10) = X0 )
& ( 1 = X11 ) )
& ( X2 = X9 ) ) )
=> hq(X3,X1) )
& ( ( ( X2 = X3 )
& ? [X4: general,X5: general] :
( tp(X4,X5)
& ? [X6: $int,X7: $int] :
( ( f__integer__(X7) = X0 )
& ( f__integer__($sum(X7,$uminus(X6))) = X5 )
& ( 1 = X6 ) )
& ( X4 = X2 ) )
& ( X0 = X1 ) )
=> tq(X3,X1) ) ),
inference(rectify,[],[f21]) ).
tff(f30,plain,
~ ! [X2: general,X3: general,X1: general,X0: general] :
( ( ( ? [X7: general,X6: general] :
( ( X0 = X7 )
& hp(X6,X7)
& ( X6 = X2 ) )
& ? [X4: $int,X5: $int] :
( ( f__integer__(X5) = X0 )
& ( 1 = X4 )
& ( f__integer__($sum(X5,X4)) = X3 ) )
& ( X1 = X2 ) )
=> hq(X1,X3) )
& ( ( ? [X11: general,X10: general] :
( ( X2 = X11 )
& ( X0 = X10 )
& tp(X11,X10) )
& ( X1 = X2 )
& ? [X8: $int,X9: $int] :
( ( f__integer__($sum(X8,X9)) = X3 )
& ( f__integer__(X8) = X0 )
& ( 1 = X9 ) ) )
=> tq(X1,X3) ) ),
inference(rectify,[],[f20]) ).
tff(f35,plain,
? [X2: general,X3: general,X1: general,X0: general] :
( ( ~ hq(X1,X3)
& ? [X7: general,X6: general] :
( ( X0 = X7 )
& hp(X6,X7)
& ( X6 = X2 ) )
& ? [X4: $int,X5: $int] :
( ( f__integer__(X5) = X0 )
& ( 1 = X4 )
& ( f__integer__($sum(X5,X4)) = X3 ) )
& ( X1 = X2 ) )
| ( ~ tq(X1,X3)
& ? [X11: general,X10: general] :
( ( X2 = X11 )
& ( X0 = X10 )
& tp(X11,X10) )
& ( X1 = X2 )
& ? [X8: $int,X9: $int] :
( ( f__integer__($sum(X8,X9)) = X3 )
& ( f__integer__(X8) = X0 )
& ( 1 = X9 ) ) ) ),
inference(ennf_transformation,[],[f30]) ).
tff(f36,plain,
? [X0: general,X1: general,X3: general,X2: general] :
( ( ? [X7: general,X6: general] :
( ( X0 = X7 )
& hp(X6,X7)
& ( X6 = X2 ) )
& ( X1 = X2 )
& ? [X4: $int,X5: $int] :
( ( f__integer__(X5) = X0 )
& ( 1 = X4 )
& ( f__integer__($sum(X5,X4)) = X3 ) )
& ~ hq(X1,X3) )
| ( ? [X8: $int,X9: $int] :
( ( f__integer__($sum(X8,X9)) = X3 )
& ( f__integer__(X8) = X0 )
& ( 1 = X9 ) )
& ( X1 = X2 )
& ~ tq(X1,X3)
& ? [X11: general,X10: general] :
( ( X2 = X11 )
& ( X0 = X10 )
& tp(X11,X10) ) ) ),
inference(flattening,[],[f35]) ).
tff(f38,plain,
! [X3: general,X1: general,X2: general,X0: general] :
( ( hq(X3,X1)
| ( X2 != X3 )
| ( X0 != X1 )
| ! [X9: general,X8: general] :
( ! [X10: $int,X11: $int] :
( ( f__integer__(X10) != X0 )
| ( f__integer__($sum(X10,$uminus(X11))) != X8 )
| ( 1 != X11 ) )
| ~ hp(X9,X8)
| ( X2 != X9 ) ) )
& ( tq(X3,X1)
| ( X2 != X3 )
| ! [X5: general,X4: general] :
( ! [X6: $int,X7: $int] :
( ( 1 != X6 )
| ( f__integer__($sum(X7,$uminus(X6))) != X5 )
| ( f__integer__(X7) != X0 ) )
| ~ tp(X4,X5)
| ( X2 != X4 ) )
| ( X0 != X1 ) ) ),
inference(ennf_transformation,[],[f23]) ).
tff(f39,plain,
! [X0: general,X3: general,X1: general,X2: general] :
( ( ( X0 != X1 )
| hq(X3,X1)
| ( X2 != X3 )
| ! [X9: general,X8: general] :
( ! [X10: $int,X11: $int] :
( ( f__integer__(X10) != X0 )
| ( f__integer__($sum(X10,$uminus(X11))) != X8 )
| ( 1 != X11 ) )
| ~ hp(X9,X8)
| ( X2 != X9 ) ) )
& ( ( X0 != X1 )
| tq(X3,X1)
| ! [X5: general,X4: general] :
( ! [X6: $int,X7: $int] :
( ( 1 != X6 )
| ( f__integer__($sum(X7,$uminus(X6))) != X5 )
| ( f__integer__(X7) != X0 ) )
| ~ tp(X4,X5)
| ( X2 != X4 ) )
| ( X2 != X3 ) ) ),
inference(flattening,[],[f38]) ).
tff(f48,definition,
! [X3: general,X0: general,X2: general,X1: general] :
( ( ? [X8: $int,X9: $int] :
( ( f__integer__($sum(X8,X9)) = X3 )
& ( f__integer__(X8) = X0 )
& ( 1 = X9 ) )
& ( X1 = X2 )
& ~ tq(X1,X3)
& ? [X11: general,X10: general] :
( ( X2 = X11 )
& ( X0 = X10 )
& tp(X11,X10) ) )
| ~ sP0(X3,X0,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f49,plain,
? [X0: general,X1: general,X3: general,X2: general] :
( ( ? [X7: general,X6: general] :
( ( X0 = X7 )
& hp(X6,X7)
& ( X6 = X2 ) )
& ( X1 = X2 )
& ? [X4: $int,X5: $int] :
( ( f__integer__(X5) = X0 )
& ( 1 = X4 )
& ( f__integer__($sum(X5,X4)) = X3 ) )
& ~ hq(X1,X3) )
| sP0(X3,X0,X2,X1) ),
inference(definition_folding,[],[f36,f48]) ).
tff(f55,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ( X0 != X2 )
| hq(X1,X2)
| ( X1 != X3 )
| ! [X4: general,X5: general] :
( ! [X6: $int,X7: $int] :
( ( f__integer__(X6) != X0 )
| ( f__integer__($sum(X6,$uminus(X7))) != X5 )
| ( 1 != X7 ) )
| ~ hp(X4,X5)
| ( X3 != X4 ) ) )
& ( ( X0 != X2 )
| tq(X1,X2)
| ! [X8: general,X9: general] :
( ! [X10: $int,X11: $int] :
( ( 1 != X10 )
| ( f__integer__($sum(X11,$uminus(X10))) != X8 )
| ( f__integer__(X11) != X0 ) )
| ~ tp(X9,X8)
| ( X3 != X9 ) )
| ( X1 != X3 ) ) ),
inference(rectify,[],[f39]) ).
tff(f56,plain,
! [X3: general,X0: general,X2: general,X1: general] :
( ( ? [X8: $int,X9: $int] :
( ( f__integer__($sum(X8,X9)) = X3 )
& ( f__integer__(X8) = X0 )
& ( 1 = X9 ) )
& ( X1 = X2 )
& ~ tq(X1,X3)
& ? [X11: general,X10: general] :
( ( X2 = X11 )
& ( X0 = X10 )
& tp(X11,X10) ) )
| ~ sP0(X3,X0,X2,X1) ),
inference(nnf_transformation,[],[f48]) ).
tff(f57,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ? [X4: $int,X5: $int] :
( ( f__integer__($sum(X4,X5)) = X0 )
& ( f__integer__(X4) = X1 )
& ( 1 = X5 ) )
& ( X2 = X3 )
& ~ tq(X3,X0)
& ? [X6: general,X7: general] :
( ( X2 = X6 )
& ( X1 = X7 )
& tp(X6,X7) ) )
| ~ sP0(X0,X1,X2,X3) ),
inference(rectify,[],[f56]) ).
tff(f58,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ( f__integer__($sum(sK3(X0,X1),sK4(X0,X1))) = X0 )
& ( f__integer__(sK3(X0,X1)) = X1 )
& ( 1 = sK4(X0,X1) )
& ( X2 = X3 )
& ~ tq(X3,X0)
& ( sK5(X1,X2) = X2 )
& ( sK6(X1,X2) = X1 )
& tp(sK5(X1,X2),sK6(X1,X2)) )
| ~ sP0(X0,X1,X2,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(X4,sK3(X0,X1)),skolemize(X5,sK4(X0,X1)),skolemize(X6,sK5(X1,X2)),skolemize(X7,sK6(X1,X2))],[f57]) ).
tff(f59,plain,
? [X0: general,X1: general,X2: general,X3: general] :
( ( ? [X4: general,X5: general] :
( ( X0 = X4 )
& hp(X5,X4)
& ( X3 = X5 ) )
& ( X1 = X3 )
& ? [X6: $int,X7: $int] :
( ( f__integer__(X7) = X0 )
& ( 1 = X6 )
& ( f__integer__($sum(X7,X6)) = X2 ) )
& ~ hq(X1,X2) )
| sP0(X2,X0,X3,X1) ),
inference(rectify,[],[f49]) ).
tff(f60,plain,
( ( ( sK11 = sK7 )
& hp(sK12,sK11)
& ( sK12 = sK10 )
& ( sK10 = sK8 )
& ( f__integer__(sK14) = sK7 )
& ( 1 = sK13 )
& ( f__integer__($sum(sK14,sK13)) = sK9 )
& ~ hq(sK8,sK9) )
| sP0(sK9,sK7,sK10,sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14]),skolemize(X0,sK7),skolemize(X1,sK8),skolemize(X2,sK9),skolemize(X3,sK10),skolemize(X4,sK11),skolemize(X5,sK12),skolemize(X6,sK13),skolemize(X7,sK14)],[f59]) ).
tff(f79,plain,
! [X2: general,X3: general,X10: $int,X0: general,X11: $int,X1: general,X8: general,X9: general] :
( ( X0 != X2 )
| tq(X1,X2)
| ( 1 != X10 )
| ( f__integer__($sum(X11,$uminus(X10))) != X8 )
| ( f__integer__(X11) != X0 )
| ~ tp(X9,X8)
| ( X3 != X9 )
| ( X1 != X3 ) ),
inference(cnf_transformation,[],[f55]) ).
tff(f80,plain,
! [X2: general,X3: general,X0: general,X1: general,X6: $int,X7: $int,X4: general,X5: general] :
( ( X0 != X2 )
| hq(X1,X2)
| ( X1 != X3 )
| ( f__integer__(X6) != X0 )
| ( f__integer__($sum(X6,$uminus(X7))) != X5 )
| ( 1 != X7 )
| ~ hp(X4,X5)
| ( X3 != X4 ) ),
inference(cnf_transformation,[],[f55]) ).
tff(f82,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| tp(sK5(X1,X2),sK6(X1,X2)) ),
inference(cnf_transformation,[],[f58]) ).
tff(f83,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK6(X1,X2) = X1 )
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f58]) ).
tff(f84,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK5(X1,X2) = X2 )
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f58]) ).
tff(f85,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ tq(X3,X0)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f58]) ).
tff(f86,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( X2 = X3 ) ),
inference(cnf_transformation,[],[f58]) ).
tff(f87,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( 1 = sK4(X0,X1) ) ),
inference(cnf_transformation,[],[f58]) ).
tff(f88,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( f__integer__(sK3(X0,X1)) = X1 ) ),
inference(cnf_transformation,[],[f58]) ).
tff(f89,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( f__integer__($sum(sK3(X0,X1),sK4(X0,X1))) = X0 ) ),
inference(cnf_transformation,[],[f58]) ).
tff(f90,plain,
( sP0(sK9,sK7,sK10,sK8)
| ~ hq(sK8,sK9) ),
inference(cnf_transformation,[],[f60]) ).
tff(f91,plain,
( sP0(sK9,sK7,sK10,sK8)
| ( f__integer__($sum(sK14,sK13)) = sK9 ) ),
inference(cnf_transformation,[],[f60]) ).
tff(f92,plain,
( sP0(sK9,sK7,sK10,sK8)
| ( 1 = sK13 ) ),
inference(cnf_transformation,[],[f60]) ).
tff(f93,plain,
( ( f__integer__(sK14) = sK7 )
| sP0(sK9,sK7,sK10,sK8) ),
inference(cnf_transformation,[],[f60]) ).
tff(f94,plain,
( sP0(sK9,sK7,sK10,sK8)
| ( sK10 = sK8 ) ),
inference(cnf_transformation,[],[f60]) ).
tff(f95,plain,
( ( sK12 = sK10 )
| sP0(sK9,sK7,sK10,sK8) ),
inference(cnf_transformation,[],[f60]) ).
tff(f96,plain,
( hp(sK12,sK11)
| sP0(sK9,sK7,sK10,sK8) ),
inference(cnf_transformation,[],[f60]) ).
tff(f97,plain,
( sP0(sK9,sK7,sK10,sK8)
| ( sK11 = sK7 ) ),
inference(cnf_transformation,[],[f60]) ).
tff(f102,plain,
! [X2: general,X3: general,X1: general,X6: $int,X7: $int,X4: general,X5: general] :
( hq(X1,X2)
| ( X1 != X3 )
| ( f__integer__(X6) != X2 )
| ( f__integer__($sum(X6,$uminus(X7))) != X5 )
| ( 1 != X7 )
| ~ hp(X4,X5)
| ( X3 != X4 ) ),
inference(equality_resolution,[],[f80]) ).
tff(f103,plain,
! [X2: general,X3: general,X6: $int,X7: $int,X4: general,X5: general] :
( hq(X3,X2)
| ( f__integer__(X6) != X2 )
| ( f__integer__($sum(X6,$uminus(X7))) != X5 )
| ( 1 != X7 )
| ~ hp(X4,X5)
| ( X3 != X4 ) ),
inference(equality_resolution,[],[f102]) ).
tff(f104,plain,
! [X3: general,X6: $int,X7: $int,X4: general,X5: general] :
( hq(X3,f__integer__(X6))
| ( f__integer__($sum(X6,$uminus(X7))) != X5 )
| ( 1 != X7 )
| ~ hp(X4,X5)
| ( X3 != X4 ) ),
inference(equality_resolution,[],[f103]) ).
tff(f105,plain,
! [X3: general,X6: $int,X7: $int,X4: general] :
( hq(X3,f__integer__(X6))
| ( 1 != X7 )
| ~ hp(X4,f__integer__($sum(X6,$uminus(X7))))
| ( X3 != X4 ) ),
inference(equality_resolution,[],[f104]) ).
tff(f106,plain,
! [X3: general,X6: $int,X4: general] :
( hq(X3,f__integer__(X6))
| ~ hp(X4,f__integer__($sum(X6,$uminus(1))))
| ( X3 != X4 ) ),
inference(equality_resolution,[],[f105]) ).
tff(f107,plain,
! [X6: $int,X4: general] :
( ~ hp(X4,f__integer__($sum(X6,$uminus(1))))
| hq(X4,f__integer__(X6)) ),
inference(equality_resolution,[],[f106]) ).
tff(f108,plain,
! [X2: general,X3: general,X10: $int,X11: $int,X1: general,X8: general,X9: general] :
( tq(X1,X2)
| ( 1 != X10 )
| ( f__integer__($sum(X11,$uminus(X10))) != X8 )
| ( f__integer__(X11) != X2 )
| ~ tp(X9,X8)
| ( X3 != X9 )
| ( X1 != X3 ) ),
inference(equality_resolution,[],[f79]) ).
tff(f109,plain,
! [X2: general,X3: general,X11: $int,X1: general,X8: general,X9: general] :
( tq(X1,X2)
| ( f__integer__($sum(X11,$uminus(1))) != X8 )
| ( f__integer__(X11) != X2 )
| ~ tp(X9,X8)
| ( X3 != X9 )
| ( X1 != X3 ) ),
inference(equality_resolution,[],[f108]) ).
tff(f110,plain,
! [X2: general,X3: general,X11: $int,X1: general,X9: general] :
( tq(X1,X2)
| ( f__integer__(X11) != X2 )
| ~ tp(X9,f__integer__($sum(X11,$uminus(1))))
| ( X3 != X9 )
| ( X1 != X3 ) ),
inference(equality_resolution,[],[f109]) ).
tff(f111,plain,
! [X3: general,X11: $int,X1: general,X9: general] :
( tq(X1,f__integer__(X11))
| ~ tp(X9,f__integer__($sum(X11,$uminus(1))))
| ( X3 != X9 )
| ( X1 != X3 ) ),
inference(equality_resolution,[],[f110]) ).
tff(f112,plain,
! [X11: $int,X1: general,X9: general] :
( tq(X1,f__integer__(X11))
| ~ tp(X9,f__integer__($sum(X11,$uminus(1))))
| ( X1 != X9 ) ),
inference(equality_resolution,[],[f111]) ).
tff(f113,plain,
! [X11: $int,X9: general] :
( tq(X9,f__integer__(X11))
| ~ tp(X9,f__integer__($sum(X11,$uminus(1)))) ),
inference(equality_resolution,[],[f112]) ).
tff(f114,plain,
! [X11: $int,X9: general] :
( tq(X9,f__integer__(X11))
| ~ tp(X9,f__integer__($sum(X11,-1))) ),
inference(evaluation,[],[f113]) ).
tff(f115,plain,
! [X6: $int,X4: general] :
( hq(X4,f__integer__(X6))
| ~ hp(X4,f__integer__($sum(X6,-1))) ),
inference(evaluation,[],[f107]) ).
tff(f119,definition,
( spl15_1
<=> hp(sK12,sK11) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
tff(f121,plain,
( hp(sK12,sK11)
| ~ spl15_1 ),
inference(avatar_component_clause,[],[f119]) ).
tff(f123,definition,
( spl15_2
<=> sP0(sK9,sK7,sK10,sK8) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
tff(f125,plain,
( sP0(sK9,sK7,sK10,sK8)
| ~ spl15_2 ),
inference(avatar_component_clause,[],[f123]) ).
tff(f126,plain,
( spl15_1
| spl15_2 ),
inference(avatar_split_clause,[],[f96,f123,f119]) ).
tff(f128,definition,
( spl15_3
<=> ( sK10 = sK8 ) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
tff(f130,plain,
( ( sK10 = sK8 )
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f128]) ).
tff(f131,plain,
( spl15_2
| spl15_3 ),
inference(avatar_split_clause,[],[f94,f128,f123]) ).
tff(f133,definition,
( spl15_4
<=> ( sK12 = sK10 ) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
tff(f135,plain,
( ( sK12 = sK10 )
| ~ spl15_4 ),
inference(avatar_component_clause,[],[f133]) ).
tff(f136,plain,
( spl15_2
| spl15_4 ),
inference(avatar_split_clause,[],[f95,f133,f123]) ).
tff(f138,definition,
( spl15_5
<=> ( 1 = sK13 ) ),
introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition]) ).
tff(f140,plain,
( ( 1 = sK13 )
| ~ spl15_5 ),
inference(avatar_component_clause,[],[f138]) ).
tff(f141,plain,
( spl15_5
| spl15_2 ),
inference(avatar_split_clause,[],[f92,f123,f138]) ).
tff(f143,definition,
( spl15_6
<=> hq(sK8,sK9) ),
introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition]) ).
tff(f145,plain,
( ~ hq(sK8,sK9)
| spl15_6 ),
inference(avatar_component_clause,[],[f143]) ).
tff(f146,plain,
( spl15_2
| ~ spl15_6 ),
inference(avatar_split_clause,[],[f90,f143,f123]) ).
tff(f148,definition,
( spl15_7
<=> ( f__integer__(sK14) = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition]) ).
tff(f151,plain,
( spl15_2
| spl15_7 ),
inference(avatar_split_clause,[],[f93,f148,f123]) ).
tff(f153,definition,
( spl15_8
<=> ( sK11 = sK7 ) ),
introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition]) ).
tff(f155,plain,
( ( sK11 = sK7 )
| ~ spl15_8 ),
inference(avatar_component_clause,[],[f153]) ).
tff(f156,plain,
( spl15_8
| spl15_2 ),
inference(avatar_split_clause,[],[f97,f123,f153]) ).
tff(f158,definition,
( spl15_9
<=> ( f__integer__($sum(sK14,sK13)) = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition]) ).
tff(f160,plain,
( ( f__integer__($sum(sK14,sK13)) = sK9 )
| ~ spl15_9 ),
inference(avatar_component_clause,[],[f158]) ).
tff(f161,plain,
( spl15_2
| spl15_9 ),
inference(avatar_split_clause,[],[f91,f158,f123]) ).
tff(f164,plain,
( ( sK10 = sK8 )
| ~ spl15_2 ),
inference(resolution,[],[f86,f125]) ).
tff(f165,plain,
( spl15_3
| ~ spl15_2 ),
inference(avatar_split_clause,[],[f164,f123,f128]) ).
tff(f166,plain,
( sP0(sK9,sK7,sK8,sK8)
| ~ spl15_2
| ~ spl15_3 ),
inference(superposition,[],[f125,f130]) ).
tff(f168,definition,
( spl15_10
<=> sP0(sK9,sK7,sK8,sK8) ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
tff(f170,plain,
( sP0(sK9,sK7,sK8,sK8)
| ~ spl15_10 ),
inference(avatar_component_clause,[],[f168]) ).
tff(f171,plain,
( spl15_10
| ~ spl15_2
| ~ spl15_3 ),
inference(avatar_split_clause,[],[f166,f128,f123,f168]) ).
tff(f196,plain,
( ( 1 = sK4(sK9,sK7) )
| ~ spl15_2 ),
inference(resolution,[],[f87,f125]) ).
tff(f199,definition,
( spl15_13
<=> ( 1 = sK4(sK9,sK7) ) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
tff(f201,plain,
( ( 1 = sK4(sK9,sK7) )
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f199]) ).
tff(f203,plain,
( spl15_13
| ~ spl15_2 ),
inference(avatar_split_clause,[],[f196,f123,f199]) ).
tff(f204,plain,
! [X2: general,X3: general,X0: general,X1: $int] :
( ~ sP0(f__integer__(X1),X2,X3,X0)
| ~ tp(X0,f__integer__($sum(X1,-1))) ),
inference(resolution,[],[f114,f85]) ).
tff(f211,plain,
( ( sK7 = f__integer__(sK3(sK9,sK7)) )
| ~ spl15_2 ),
inference(resolution,[],[f88,f125]) ).
tff(f214,definition,
( spl15_14
<=> ( sK7 = f__integer__(sK3(sK9,sK7)) ) ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
tff(f217,plain,
( spl15_14
| ~ spl15_2 ),
inference(avatar_split_clause,[],[f211,f123,f214]) ).
tff(f254,plain,
( ( sK12 = sK8 )
| ~ spl15_3
| ~ spl15_4 ),
inference(forward_demodulation,[],[f135,f130]) ).
tff(f256,definition,
( spl15_20
<=> ( sK12 = sK8 ) ),
introduced(definition,[new_symbols(definition,[spl15_20])],[avatar_definition]) ).
tff(f258,plain,
( ( sK12 = sK8 )
| ~ spl15_20 ),
inference(avatar_component_clause,[],[f256]) ).
tff(f259,plain,
( spl15_20
| ~ spl15_3
| ~ spl15_4 ),
inference(avatar_split_clause,[],[f254,f133,f128,f256]) ).
tff(f292,plain,
( ( sK9 = f__integer__($sum(sK3(sK9,sK7),sK4(sK9,sK7))) )
| ~ spl15_10 ),
inference(resolution,[],[f170,f89]) ).
tff(f293,plain,
( tp(sK5(sK7,sK8),sK6(sK7,sK8))
| ~ spl15_10 ),
inference(resolution,[],[f170,f82]) ).
tff(f297,plain,
( ( sK9 = f__integer__($sum(sK3(sK9,sK7),1)) )
| ~ spl15_10
| ~ spl15_13 ),
inference(forward_demodulation,[],[f292,f201]) ).
tff(f299,definition,
( spl15_21
<=> tp(sK5(sK7,sK8),sK6(sK7,sK8)) ),
introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition]) ).
tff(f301,plain,
( tp(sK5(sK7,sK8),sK6(sK7,sK8))
| ~ spl15_21 ),
inference(avatar_component_clause,[],[f299]) ).
tff(f302,plain,
( spl15_21
| ~ spl15_10 ),
inference(avatar_split_clause,[],[f293,f168,f299]) ).
tff(f304,definition,
( spl15_22
<=> ( sK9 = f__integer__($sum(sK3(sK9,sK7),1)) ) ),
introduced(definition,[new_symbols(definition,[spl15_22])],[avatar_definition]) ).
tff(f306,plain,
( ( sK9 = f__integer__($sum(sK3(sK9,sK7),1)) )
| ~ spl15_22 ),
inference(avatar_component_clause,[],[f304]) ).
tff(f307,plain,
( spl15_22
| ~ spl15_10
| ~ spl15_13 ),
inference(avatar_split_clause,[],[f297,f199,f168,f304]) ).
tff(f383,plain,
( ! [X0: general,X1: general] :
( ~ sP0(X0,sK7,sK8,X1)
| tp(sK5(sK7,sK8),sK7) )
| ~ spl15_21 ),
inference(superposition,[],[f301,f83]) ).
tff(f385,definition,
( spl15_25
<=> ! [X0: general,X1: general] : ~ sP0(X0,sK7,sK8,X1) ),
introduced(definition,[new_symbols(definition,[spl15_25])],[avatar_definition]) ).
tff(f386,plain,
( ! [X0: general,X1: general] : ~ sP0(X0,sK7,sK8,X1)
| ~ spl15_25 ),
inference(avatar_component_clause,[],[f385]) ).
tff(f388,definition,
( spl15_26
<=> tp(sK5(sK7,sK8),sK7) ),
introduced(definition,[new_symbols(definition,[spl15_26])],[avatar_definition]) ).
tff(f390,plain,
( tp(sK5(sK7,sK8),sK7)
| ~ spl15_26 ),
inference(avatar_component_clause,[],[f388]) ).
tff(f391,plain,
( spl15_25
| spl15_26
| ~ spl15_21 ),
inference(avatar_split_clause,[],[f383,f299,f388,f385]) ).
tff(f400,plain,
( $false
| ~ spl15_10
| ~ spl15_25 ),
inference(resolution,[],[f386,f170]) ).
tff(f401,plain,
( ~ spl15_10
| ~ spl15_25 ),
inference(avatar_contradiction_clause,[],[f400]) ).
tff(f403,plain,
( ! [X0: general,X1: general] :
( ~ sP0(X0,sK7,sK8,X1)
| tp(sK8,sK7) )
| ~ spl15_26 ),
inference(superposition,[],[f390,f84]) ).
tff(f405,definition,
( spl15_28
<=> tp(sK8,sK7) ),
introduced(definition,[new_symbols(definition,[spl15_28])],[avatar_definition]) ).
tff(f408,plain,
( spl15_28
| spl15_25
| ~ spl15_26 ),
inference(avatar_split_clause,[],[f403,f388,f385,f405]) ).
tff(f445,plain,
( ! [X2: general,X0: general,X1: general] :
( ~ sP0(sK9,X0,X1,X2)
| ~ tp(X2,f__integer__($sum($sum(sK3(sK9,sK7),1),-1))) )
| ~ spl15_22 ),
inference(superposition,[],[f204,f306]) ).
tff(f852,plain,
( ~ tp(sK8,f__integer__($sum($sum(sK3(sK9,sK7),1),-1)))
| ~ spl15_10
| ~ spl15_22 ),
inference(resolution,[],[f445,f170]) ).
tff(f854,definition,
( spl15_56
<=> tp(sK8,f__integer__($sum($sum(sK3(sK9,sK7),1),-1))) ),
introduced(definition,[new_symbols(definition,[spl15_56])],[avatar_definition]) ).
tff(f857,plain,
( ~ spl15_56
| ~ spl15_10
| ~ spl15_22 ),
inference(avatar_split_clause,[],[f852,f304,f168,f854]) ).
tff(f861,plain,
( ( sK9 = f__integer__($sum(sK14,1)) )
| ~ spl15_5
| ~ spl15_9 ),
inference(forward_demodulation,[],[f160,f140]) ).
tff(f862,plain,
( hp(sK12,sK7)
| ~ spl15_1
| ~ spl15_8 ),
inference(forward_demodulation,[],[f121,f155]) ).
tff(f871,definition,
( spl15_57
<=> ( sK9 = f__integer__($sum(sK14,1)) ) ),
introduced(definition,[new_symbols(definition,[spl15_57])],[avatar_definition]) ).
tff(f873,plain,
( ( sK9 = f__integer__($sum(sK14,1)) )
| ~ spl15_57 ),
inference(avatar_component_clause,[],[f871]) ).
tff(f874,plain,
( spl15_57
| ~ spl15_5
| ~ spl15_9 ),
inference(avatar_split_clause,[],[f861,f158,f138,f871]) ).
tff(f875,plain,
( hp(sK8,sK7)
| ~ spl15_1
| ~ spl15_8
| ~ spl15_20 ),
inference(forward_demodulation,[],[f862,f258]) ).
tff(f877,definition,
( spl15_58
<=> hp(sK8,sK7) ),
introduced(definition,[new_symbols(definition,[spl15_58])],[avatar_definition]) ).
tff(f880,plain,
( spl15_58
| ~ spl15_1
| ~ spl15_8
| ~ spl15_20 ),
inference(avatar_split_clause,[],[f875,f256,f153,f119,f877]) ).
tff(f912,plain,
( ! [X0: general] :
( hq(X0,sK9)
| ~ hp(X0,f__integer__($sum($sum(sK14,1),-1))) )
| ~ spl15_57 ),
inference(superposition,[],[f115,f873]) ).
tff(f977,plain,
( ~ hp(sK8,f__integer__($sum($sum(sK14,1),-1)))
| spl15_6
| ~ spl15_57 ),
inference(resolution,[],[f912,f145]) ).
tff(f979,definition,
( spl15_60
<=> hp(sK8,f__integer__($sum($sum(sK14,1),-1))) ),
introduced(definition,[new_symbols(definition,[spl15_60])],[avatar_definition]) ).
tff(f982,plain,
( ~ spl15_60
| spl15_6
| ~ spl15_57 ),
inference(avatar_split_clause,[],[f977,f871,f143,f979]) ).
tff(f983,plain,
$false,
inference(avatar_smt_refutation,[],[f982,f880,f874,f857,f408,f401,f391,f307,f302,f259,f217,f203,f171,f165,f161,f156,f151,f146,f141,f136,f131,f126]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX109_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n020.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 15:02:19 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 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
% 3.68/1.23 % (225749)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.68/1.23 % (225758)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=986060612:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.68/1.23 % (225758)Instruction limit reached!
% 3.68/1.23 % (225758)------------------------------
% 3.68/1.23 % (225758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.23 % (225758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.23 % (225758)CaDiCaL version: 2.1.3
% 3.68/1.23 % (225758)Termination reason: Instruction limit
% 3.68/1.23 % (225758)Termination phase: Saturation
% 3.68/1.23 % (225758)Time elapsed: 0.003 s
% 3.68/1.23 % (225758)Peak memory usage: 89 MB
% 3.68/1.23 % (225758)Instructions burned: 6 (million)
% 3.68/1.23 % (225759)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=419347514:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.68/1.23 % (225760)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1004693612:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.68/1.23 % (225756)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2749417016:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.68/1.23 % (225757)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=801021796:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.68/1.23 % (225754)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=132324912:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.68/1.23 % (225755)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2121097695:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.68/1.23 % (225757)Instruction limit reached!
% 3.68/1.23 % (225757)------------------------------
% 3.68/1.23 % (225757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.23 % (225757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.23 % (225757)CaDiCaL version: 2.1.3
% 3.68/1.23 % (225757)Termination reason: Instruction limit
% 3.68/1.23 % (225757)Termination phase: Saturation
% 3.68/1.23 % (225757)Time elapsed: 0.007 s
% 3.68/1.23 % (225757)Peak memory usage: 88 MB
% 3.68/1.23 % (225757)Instructions burned: 8 (million)
% 3.68/1.23 % (225754)Instruction limit reached!
% 3.68/1.23 % (225754)------------------------------
% 3.68/1.23 % (225754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.23 % (225754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.23 % (225754)CaDiCaL version: 2.1.3
% 3.68/1.23 % (225754)Termination reason: Instruction limit
% 3.68/1.23 % (225754)Termination phase: Saturation
% 3.68/1.23 % (225754)Time elapsed: 0.031 s
% 3.68/1.23 % (225754)Peak memory usage: 115 MB
% 3.68/1.23 % (225754)Instructions burned: 12 (million)
% 3.68/1.23 % (225760)Instruction limit reached!
% 3.68/1.23 % (225760)------------------------------
% 3.68/1.23 % (225760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.23 % (225760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.23 % (225760)CaDiCaL version: 2.1.3
% 3.68/1.23 % (225760)Termination reason: Instruction limit
% 3.68/1.23 % (225760)Termination phase: Saturation
% 3.68/1.23 % (225760)Time elapsed: 0.047 s
% 3.68/1.23 % (225760)Peak memory usage: 115 MB
% 3.68/1.23 % (225760)Instructions burned: 33 (million)
% 3.68/1.23 % (225759)Instruction limit reached!
% 3.68/1.23 % (225759)------------------------------
% 3.68/1.23 % (225759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.23 % (225759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.23 % (225759)CaDiCaL version: 2.1.3
% 3.68/1.23 % (225759)Termination reason: Instruction limit
% 3.68/1.23 % (225759)Termination phase: Saturation
% 3.68/1.23 % (225759)Time elapsed: 0.057 s
% 3.68/1.23 % (225759)Peak memory usage: 115 MB
% 3.68/1.23 % (225759)Instructions burned: 47 (million)
% 3.68/1.23 % (225762)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3925686196:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.68/1.23 % (225762)Instruction limit reached!
% 3.68/1.23 % (225762)------------------------------
% 3.68/1.23 % (225762)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.57/1.39 % (225762)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/1.39 % (225762)CaDiCaL version: 2.1.3
% 4.57/1.39 % (225762)Termination reason: Instruction limit
% 4.57/1.39 % (225762)Termination phase: Saturation
% 4.57/1.39 % (225762)Time elapsed: 0.006 s
% 4.57/1.39 % (225762)Peak memory usage: 88 MB
% 4.57/1.39 % (225762)Instructions burned: 15 (million)
% 4.57/1.39 % (225756)Instruction limit reached!
% 4.57/1.39 % (225756)------------------------------
% 4.57/1.39 % (225756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.57/1.39 % (225756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/1.39 % (225756)CaDiCaL version: 2.1.3
% 4.57/1.39 % (225756)Termination reason: Instruction limit
% 4.57/1.39 % (225756)Termination phase: Saturation
% 4.57/1.39 % (225756)Time elapsed: 0.105 s
% 4.57/1.39 % (225756)Peak memory usage: 113 MB
% 4.57/1.39 % (225756)Instructions burned: 202 (million)
% 4.57/1.39 % (225769)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=3351765591:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.57/1.39 % (225770)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1445597015:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.57/1.39 % (225769)Instruction limit reached!
% 4.57/1.39 % (225769)------------------------------
% 4.57/1.39 % (225769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.57/1.39 % (225769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/1.39 % (225769)CaDiCaL version: 2.1.3
% 4.57/1.39 % (225769)Termination reason: Instruction limit
% 4.57/1.39 % (225769)Termination phase: Saturation
% 4.57/1.39 % (225769)Time elapsed: 0.022 s
% 4.57/1.39 % (225769)Peak memory usage: 89 MB
% 4.57/1.39 % (225769)Instructions burned: 30 (million)
% 4.57/1.39 % (225771)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1638794166:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.57/1.39 % (225772)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=3562367182:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.57/1.39 % (225770)Instruction limit reached!
% 4.57/1.39 % (225770)------------------------------
% 4.57/1.39 % (225770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.57/1.39 % (225770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/1.39 % (225770)CaDiCaL version: 2.1.3
% 4.57/1.39 % (225770)Termination reason: Instruction limit
% 4.57/1.39 % (225770)Termination phase: Saturation
% 4.57/1.39 % (225770)Time elapsed: 0.012 s
% 4.57/1.39 % (225770)Peak memory usage: 90 MB
% 4.57/1.39 % (225770)Instructions burned: 17 (million)
% 4.57/1.39 % (225774)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3413727085:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.57/1.39 % (225771)Instruction limit reached!
% 4.57/1.39 % (225771)------------------------------
% 4.57/1.39 % (225771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.57/1.39 % (225771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/1.39 % (225771)CaDiCaL version: 2.1.3
% 4.57/1.39 % (225771)Termination reason: Instruction limit
% 4.57/1.39 % (225771)Termination phase: Saturation
% 4.57/1.39 % (225771)Time elapsed: 0.020 s
% 4.57/1.39 % (225771)Peak memory usage: 89 MB
% 4.57/1.39 % (225771)Instructions burned: 24 (million)
% 4.57/1.39 % (225772)Instruction limit reached!
% 4.57/1.39 % (225772)------------------------------
% 4.57/1.39 % (225772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.57/1.39 % (225772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.57/1.39 % (225772)CaDiCaL version: 2.1.3
% 4.57/1.39 % (225772)Termination reason: Instruction limit
% 4.57/1.39 % (225772)Termination phase: Saturation
% 4.57/1.39 % (225772)Time elapsed: 0.021 s
% 4.57/1.39 % (225772)Peak memory usage: 89 MB
% 4.57/1.39 % (225772)Instructions burned: 28 (million)
% 4.57/1.39 % (225774)Instruction limit reached!
% 4.57/1.39 % (225774)------------------------------
% 4.57/1.39 % (225774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.57/1.39 % (225774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.54 % (225774)CaDiCaL version: 2.1.3
% 5.53/1.54 % (225774)Termination reason: Instruction limit
% 5.53/1.54 % (225774)Termination phase: Saturation
% 5.53/1.54 % (225774)Time elapsed: 0.024 s
% 5.53/1.54 % (225774)Peak memory usage: 89 MB
% 5.53/1.54 % (225774)Instructions burned: 89 (million)
% 5.53/1.54 % (225755)Instruction limit reached!
% 5.53/1.54 % (225755)------------------------------
% 5.53/1.54 % (225755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.54 % (225755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.54 % (225755)CaDiCaL version: 2.1.3
% 5.53/1.54 % (225755)Termination reason: Instruction limit
% 5.53/1.54 % (225755)Termination phase: Saturation
% 5.53/1.54 % (225755)Time elapsed: 0.232 s
% 5.53/1.54 % (225755)Peak memory usage: 117 MB
% 5.53/1.54 % (225755)Instructions burned: 308 (million)
% 5.53/1.54 % (225775)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2948470491:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 5.53/1.54 % (225775)Instruction limit reached!
% 5.53/1.54 % (225775)------------------------------
% 5.53/1.55 % (225775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.55 % (225775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.55 % (225775)CaDiCaL version: 2.1.3
% 5.53/1.55 % (225775)Termination reason: Instruction limit
% 5.53/1.55 % (225775)Termination phase: Saturation
% 5.53/1.55 % (225775)Time elapsed: 0.002 s
% 5.53/1.55 % (225775)Peak memory usage: 88 MB
% 5.53/1.55 % (225775)Instructions burned: 2 (million)
% 5.53/1.55 % (225785)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=2761492331:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 5.53/1.55 % (225785)Instruction limit reached!
% 5.53/1.55 % (225785)------------------------------
% 5.53/1.55 % (225785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.55 % (225785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.55 % (225785)CaDiCaL version: 2.1.3
% 5.53/1.55 % (225785)Termination reason: Instruction limit
% 5.53/1.55 % (225785)Termination phase: Saturation
% 5.53/1.55 % (225785)Time elapsed: 0.004 s
% 5.53/1.55 % (225785)Peak memory usage: 88 MB
% 5.53/1.55 % (225785)Instructions burned: 9 (million)
% 5.53/1.55 % (225778)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=312942374:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.53/1.55 % (225782)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2037927264:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.53/1.55 % (225782)Instruction limit reached!
% 5.53/1.55 % (225782)------------------------------
% 5.53/1.55 % (225782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.55 % (225782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.55 % (225782)CaDiCaL version: 2.1.3
% 5.53/1.55 % (225782)Termination reason: Instruction limit
% 5.53/1.55 % (225782)Termination phase: Saturation
% 5.53/1.55 % (225782)Time elapsed: 0.004 s
% 5.53/1.55 % (225782)Peak memory usage: 89 MB
% 5.53/1.55 % (225782)Instructions burned: 4 (million)
% 5.53/1.55 % (225784)lrs+10_1_thi=all:si=on:fd=off:random_seed=3522280335:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.53/1.55 % (225783)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2934445383:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.53/1.55 % (225786)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1079561481:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.53/1.55 % (225786)Instruction limit reached!
% 5.53/1.55 % (225786)------------------------------
% 5.53/1.55 % (225786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.53/1.55 % (225786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.53/1.55 % (225786)CaDiCaL version: 2.1.3
% 5.53/1.55 % (225786)Termination reason: Instruction limit
% 5.53/1.55 % (225786)Termination phase: Saturation
% 5.53/1.55 % (225786)Time elapsed: 0.003 s
% 5.53/1.55 % (225786)Peak memory usage: 89 MB
% 5.53/1.55 % (225786)Instructions burned: 3 (million)
% 5.53/1.55 % (225788)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3934291760:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.22/1.82 % (225788)Instruction limit reached!
% 7.22/1.82 % (225788)------------------------------
% 7.22/1.82 % (225788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.82 % (225788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.82 % (225788)CaDiCaL version: 2.1.3
% 7.22/1.82 % (225788)Termination reason: Instruction limit
% 7.22/1.82 % (225788)Termination phase: Saturation
% 7.22/1.82 % (225788)Time elapsed: 0.003 s
% 7.22/1.82 % (225788)Peak memory usage: 89 MB
% 7.22/1.82 % (225788)Instructions burned: 2 (million)
% 7.22/1.82 % (225784)Instruction limit reached!
% 7.22/1.82 % (225784)------------------------------
% 7.22/1.82 % (225784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.82 % (225784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.82 % (225784)CaDiCaL version: 2.1.3
% 7.22/1.82 % (225784)Termination reason: Instruction limit
% 7.22/1.82 % (225784)Termination phase: Saturation
% 7.22/1.82 % (225784)Time elapsed: 0.062 s
% 7.22/1.82 % (225784)Peak memory usage: 116 MB
% 7.22/1.82 % (225784)Instructions burned: 53 (million)
% 7.22/1.82 % (225790)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=584511043:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 7.22/1.82 % (225778)Instruction limit reached!
% 7.22/1.82 % (225778)------------------------------
% 7.22/1.82 % (225778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.82 % (225778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.82 % (225778)CaDiCaL version: 2.1.3
% 7.22/1.82 % (225778)Termination reason: Instruction limit
% 7.22/1.82 % (225778)Termination phase: Saturation
% 7.22/1.82 % (225778)Time elapsed: 0.114 s
% 7.22/1.82 % (225778)Peak memory usage: 90 MB
% 7.22/1.82 % (225778)Instructions burned: 182 (million)
% 7.22/1.82 % (225783)Instruction limit reached!
% 7.22/1.82 % (225783)------------------------------
% 7.22/1.82 % (225783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.82 % (225783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.82 % (225783)CaDiCaL version: 2.1.3
% 7.22/1.82 % (225783)Termination reason: Instruction limit
% 7.22/1.82 % (225783)Termination phase: Saturation
% 7.22/1.82 % (225783)Time elapsed: 0.099 s
% 7.22/1.82 % (225783)Peak memory usage: 133 MB
% 7.22/1.82 % (225783)Instructions burned: 67 (million)
% 7.22/1.82 % (225790)Instruction limit reached!
% 7.22/1.82 % (225790)------------------------------
% 7.22/1.82 % (225790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.82 % (225790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.82 % (225790)CaDiCaL version: 2.1.3
% 7.22/1.82 % (225790)Termination reason: Instruction limit
% 7.22/1.82 % (225790)Termination phase: Saturation
% 7.22/1.82 % (225790)Time elapsed: 0.059 s
% 7.22/1.82 % (225790)Peak memory usage: 116 MB
% 7.22/1.82 % (225790)Instructions burned: 129 (million)
% 7.22/1.82 % (225793)dis+10_1_si=on:random_seed=1566001019:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.22/1.82 % (225793)Instruction limit reached!
% 7.22/1.82 % (225793)------------------------------
% 7.22/1.82 % (225793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.82 % (225793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.82 % (225793)CaDiCaL version: 2.1.3
% 7.22/1.82 % (225793)Termination reason: Instruction limit
% 7.22/1.82 % (225793)Termination phase: Saturation
% 7.22/1.82 % (225793)Time elapsed: 0.009 s
% 7.22/1.82 % (225793)Peak memory usage: 88 MB
% 7.22/1.82 % (225793)Instructions burned: 11 (million)
% 7.22/1.82 % (225797)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3013169473:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.22/1.82 % (225797)Refutation not found, incomplete strategy
% 7.22/1.82 % (225797)------------------------------
% 7.22/1.82 % (225797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.82 % (225797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.82 % (225797)CaDiCaL version: 2.1.3
% 7.22/1.82 % (225797)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.82 % (225797)Time elapsed: 0.004 s
% 7.22/1.82 % (225797)Peak memory usage: 89 MB
% 7.22/1.82 % (225797)Instructions burned: 3 (million)
% 7.22/1.82 % (225799)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2106713137:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 10.15/2.04 % (225800)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1080915918:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 10.15/2.04 % (225800)Instruction limit reached!
% 10.15/2.04 % (225800)------------------------------
% 10.15/2.04 % (225800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.15/2.04 % (225800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.15/2.04 % (225800)CaDiCaL version: 2.1.3
% 10.15/2.04 % (225800)Termination reason: Instruction limit
% 10.15/2.04 % (225800)Termination phase: Saturation
% 10.15/2.04 % (225800)Time elapsed: 0.002 s
% 10.15/2.04 % (225800)Peak memory usage: 88 MB
% 10.15/2.04 % (225800)Instructions burned: 2 (million)
% 10.15/2.04 % (225799)Instruction limit reached!
% 10.15/2.04 % (225799)------------------------------
% 10.15/2.04 % (225799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.15/2.04 % (225799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.15/2.04 % (225799)CaDiCaL version: 2.1.3
% 10.15/2.04 % (225799)Termination reason: Instruction limit
% 10.15/2.04 % (225799)Termination phase: Saturation
% 10.15/2.04 % (225799)Time elapsed: 0.029 s
% 10.15/2.04 % (225799)Peak memory usage: 89 MB
% 10.15/2.04 % (225799)Instructions burned: 36 (million)
% 10.15/2.04 % (225802)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3930935810:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 10.15/2.04 % (225802)Instruction limit reached!
% 10.15/2.04 % (225802)------------------------------
% 10.15/2.04 % (225802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.15/2.04 % (225802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.15/2.04 % (225802)CaDiCaL version: 2.1.3
% 10.15/2.04 % (225802)Termination reason: Instruction limit
% 10.15/2.04 % (225802)Termination phase: Saturation
% 10.15/2.04 % (225802)Time elapsed: 0.008 s
% 10.15/2.04 % (225802)Peak memory usage: 88 MB
% 10.15/2.04 % (225802)Instructions burned: 8 (million)
% 10.15/2.04 % (225805)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1552604503:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 10.15/2.04 % (225803)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3961362945:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 10.15/2.04 % (225803)Refutation not found, incomplete strategy
% 10.15/2.04 % (225803)------------------------------
% 10.15/2.04 % (225803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.15/2.04 % (225803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.15/2.04 % (225803)CaDiCaL version: 2.1.3
% 10.15/2.04 % (225803)Termination reason: Refutation not found, incomplete strategy
% 10.15/2.04 % (225803)Time elapsed: 0.003 s
% 10.15/2.04 % (225803)Peak memory usage: 89 MB
% 10.15/2.04 % (225803)Instructions burned: 3 (million)
% 10.15/2.04 % (225805)Instruction limit reached!
% 10.15/2.04 % (225805)------------------------------
% 10.15/2.04 % (225805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.15/2.04 % (225805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.15/2.04 % (225805)CaDiCaL version: 2.1.3
% 10.15/2.04 % (225805)Termination reason: Instruction limit
% 10.15/2.04 % (225805)Termination phase: Saturation
% 10.15/2.04 % (225805)Time elapsed: 0.020 s
% 10.15/2.04 % (225805)Peak memory usage: 116 MB
% 10.15/2.04 % (225805)Instructions burned: 14 (million)
% 10.15/2.04 % (225806)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1274053796:i=226:rtra=on:gtg=position:ss=axioms_2993 on theBenchmark for (2993ds/226Mi)
% 10.15/2.04 % (225810)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3397242659:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.15/2.04 % (225810)Instruction limit reached!
% 10.15/2.04 % (225810)------------------------------
% 10.15/2.04 % (225810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.15/2.04 % (225810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.15/2.04 % (225810)CaDiCaL version: 2.1.3
% 11.68/2.35 % (225810)Termination reason: Instruction limit
% 11.68/2.35 % (225810)Termination phase: Saturation
% 11.68/2.35 % (225810)Time elapsed: 0.009 s
% 11.68/2.35 % (225810)Peak memory usage: 88 MB
% 11.68/2.35 % (225810)Instructions burned: 10 (million)
% 11.68/2.35 % (225806)Refutation not found, incomplete strategy
% 11.68/2.35 % (225806)------------------------------
% 11.68/2.35 % (225806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.35 % (225806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.35 % (225806)CaDiCaL version: 2.1.3
% 11.68/2.35 % (225806)Termination reason: Refutation not found, incomplete strategy
% 11.68/2.35 % (225806)Time elapsed: 0.061 s
% 11.68/2.35 % (225806)Peak memory usage: 116 MB
% 11.68/2.35 % (225806)Instructions burned: 47 (million)
% 11.68/2.35 % (225812)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=191324668:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 11.68/2.35 % (225816)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=3171708389:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 11.68/2.35 % (225813)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=485101277:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 11.68/2.35 % (225797)------------------------------
% 11.68/2.35 % (225797)------------------------------
% 11.68/2.35 % (225813)Instruction limit reached!
% 11.68/2.35 % (225813)------------------------------
% 11.68/2.35 % (225813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.35 % (225813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.35 % (225813)CaDiCaL version: 2.1.3
% 11.68/2.35 % (225813)Termination reason: Instruction limit
% 11.68/2.35 % (225813)Termination phase: Saturation
% 11.68/2.35 % (225813)Time elapsed: 0.060 s
% 11.68/2.35 % (225813)Peak memory usage: 90 MB
% 11.68/2.35 % (225813)Instructions burned: 76 (million)
% 11.68/2.35 % (225812)Instruction limit reached!
% 11.68/2.35 % (225812)------------------------------
% 11.68/2.35 % (225812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.35 % (225812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.35 % (225812)CaDiCaL version: 2.1.3
% 11.68/2.35 % (225812)Termination reason: Instruction limit
% 11.68/2.35 % (225812)Termination phase: Saturation
% 11.68/2.35 % (225812)Time elapsed: 0.096 s
% 11.68/2.35 % (225812)Peak memory usage: 133 MB
% 11.68/2.35 % (225812)Instructions burned: 72 (million)
% 11.68/2.35 % (225803)------------------------------
% 11.68/2.35 % (225803)------------------------------
% 11.68/2.35 % (225816)Instruction limit reached!
% 11.68/2.35 % (225816)------------------------------
% 11.68/2.35 % (225816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.68/2.35 % (225816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.68/2.35 % (225816)CaDiCaL version: 2.1.3
% 11.68/2.35 % (225816)Termination reason: Instruction limit
% 11.68/2.35 % (225816)Termination phase: Saturation
% 11.68/2.35 % (225816)Time elapsed: 0.099 s
% 11.68/2.35 % (225816)Peak memory usage: 90 MB
% 11.68/2.35 % (225816)Instructions burned: 296 (million)
% 11.68/2.35 % (225819)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1604541121:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 11.68/2.35 % (225823)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=358755699:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 11.68/2.35 % (225826)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=224137943:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 11.68/2.35 % (225825)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1155819721:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi)
% 11.68/2.35 % (225824)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2929134492:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 11.68/2.35 % (225806)------------------------------
% 11.68/2.35 % (225806)------------------------------
% 11.68/2.35 % (225819)Instruction limit reached!
% 11.68/2.35 % (225819)------------------------------
% 11.68/2.35 % (225819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.70 % (225819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.70 % (225819)CaDiCaL version: 2.1.3
% 12.96/2.70 % (225819)Termination reason: Instruction limit
% 12.96/2.70 % (225819)Termination phase: Saturation
% 12.96/2.70 % (225819)Time elapsed: 0.115 s
% 12.96/2.70 % (225819)Peak memory usage: 116 MB
% 12.96/2.70 % (225819)Instructions burned: 131 (million)
% 12.96/2.70 % (225827)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1209860410:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 12.96/2.70 % (225824)Instruction limit reached!
% 12.96/2.70 % (225824)------------------------------
% 12.96/2.70 % (225824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.70 % (225824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.70 % (225824)CaDiCaL version: 2.1.3
% 12.96/2.70 % (225824)Termination reason: Instruction limit
% 12.96/2.70 % (225824)Termination phase: Saturation
% 12.96/2.70 % (225824)Time elapsed: 0.071 s
% 12.96/2.70 % (225824)Peak memory usage: 133 MB
% 12.96/2.70 % (225824)Instructions burned: 40 (million)
% 12.96/2.70 % (225823)Instruction limit reached!
% 12.96/2.70 % (225823)------------------------------
% 12.96/2.70 % (225823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.70 % (225823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.70 % (225823)CaDiCaL version: 2.1.3
% 12.96/2.70 % (225823)Termination reason: Instruction limit
% 12.96/2.70 % (225823)Termination phase: Saturation
% 12.96/2.70 % (225823)Time elapsed: 0.137 s
% 12.96/2.70 % (225823)Peak memory usage: 133 MB
% 12.96/2.70 % (225823)Instructions burned: 132 (million)
% 12.96/2.70 % (225827)Instruction limit reached!
% 12.96/2.70 % (225827)------------------------------
% 12.96/2.70 % (225827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.70 % (225827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.70 % (225827)CaDiCaL version: 2.1.3
% 12.96/2.70 % (225827)Termination reason: Instruction limit
% 12.96/2.70 % (225827)Termination phase: Saturation
% 12.96/2.70 % (225827)Time elapsed: 0.103 s
% 12.96/2.70 % (225827)Peak memory usage: 117 MB
% 12.96/2.70 % (225827)Instructions burned: 132 (million)
% 12.96/2.70 % (225833)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=111767221:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi)
% 12.96/2.70 % (225834)dis+10_1_si=on:random_seed=2973765680:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 12.96/2.70 % (225833)Refutation not found, incomplete strategy
% 12.96/2.70 % (225833)------------------------------
% 12.96/2.70 % (225833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.70 % (225833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.70 % (225833)CaDiCaL version: 2.1.3
% 12.96/2.70 % (225833)Termination reason: Refutation not found, incomplete strategy
% 12.96/2.70 % (225833)Time elapsed: 0.038 s
% 12.96/2.70 % (225833)Peak memory usage: 116 MB
% 12.96/2.70 % (225833)Instructions burned: 19 (million)
% 12.96/2.70 % (225825)Instruction limit reached!
% 12.96/2.70 % (225825)------------------------------
% 12.96/2.70 % (225825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.70 % (225825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.70 % (225825)CaDiCaL version: 2.1.3
% 12.96/2.70 % (225825)Termination reason: Instruction limit
% 12.96/2.70 % (225825)Termination phase: Saturation
% 12.96/2.70 % (225825)Time elapsed: 0.207 s
% 12.96/2.70 % (225825)Peak memory usage: 91 MB
% 12.96/2.70 % (225825)Instructions burned: 307 (million)
% 12.96/2.70 % (225836)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=3784598165:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi)
% 12.96/2.70 % (225826)Instruction limit reached!
% 12.96/2.70 % (225826)------------------------------
% 12.96/2.70 % (225826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.96/2.70 % (225826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.96/2.70 % (225826)CaDiCaL version: 2.1.3
% 12.96/2.70 % (225826)Termination reason: Instruction limit
% 12.96/2.70 % (225826)Termination phase: Saturation
% 12.96/2.70 % (225826)Time elapsed: 0.244 s
% 15.11/3.01 % (225826)Peak memory usage: 136 MB
% 15.11/3.01 % (225826)Instructions burned: 599 (million)
% 15.11/3.01 % (225837)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=146366372:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 15.11/3.01 % (225839)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=4103457425:i=65:nm=16:rtra=on_2986 on theBenchmark for (2986ds/65Mi)
% 15.11/3.01 % (225837)Instruction limit reached!
% 15.11/3.01 % (225837)------------------------------
% 15.11/3.01 % (225837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225837)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225837)Termination reason: Instruction limit
% 15.11/3.01 % (225837)Termination phase: Saturation
% 15.11/3.01 % (225837)Time elapsed: 0.096 s
% 15.11/3.01 % (225837)Peak memory usage: 90 MB
% 15.11/3.01 % (225837)Instructions burned: 141 (million)
% 15.11/3.01 % (225841)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4285025318:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 15.11/3.01 % (225844)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=549208793:s2a=on:i=128:s2at=5:ins=3:rtra=on_2986 on theBenchmark for (2986ds/128Mi)
% 15.11/3.01 % (225839)Instruction limit reached!
% 15.11/3.01 % (225839)------------------------------
% 15.11/3.01 % (225839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225839)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225839)Termination reason: Instruction limit
% 15.11/3.01 % (225839)Termination phase: Saturation
% 15.11/3.01 % (225839)Time elapsed: 0.067 s
% 15.11/3.01 % (225839)Peak memory usage: 116 MB
% 15.11/3.01 % (225839)Instructions burned: 65 (million)
% 15.11/3.01 % (225844)Instruction limit reached!
% 15.11/3.01 % (225844)------------------------------
% 15.11/3.01 % (225844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225844)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225844)Termination reason: Instruction limit
% 15.11/3.01 % (225844)Termination phase: Saturation
% 15.11/3.01 % (225844)Time elapsed: 0.062 s
% 15.11/3.01 % (225844)Peak memory usage: 117 MB
% 15.11/3.01 % (225844)Instructions burned: 130 (million)
% 15.11/3.01 % (225833)------------------------------
% 15.11/3.01 % (225833)------------------------------
% 15.11/3.01 % (225841)Instruction limit reached!
% 15.11/3.01 % (225841)------------------------------
% 15.11/3.01 % (225841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225841)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225841)Termination reason: Instruction limit
% 15.11/3.01 % (225841)Termination phase: Saturation
% 15.11/3.01 % (225841)Time elapsed: 0.076 s
% 15.11/3.01 % (225841)Peak memory usage: 89 MB
% 15.11/3.01 % (225841)Instructions burned: 121 (million)
% 15.11/3.01 % (225836)Instruction limit reached!
% 15.11/3.01 % (225836)------------------------------
% 15.11/3.01 % (225836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225836)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225836)Termination reason: Instruction limit
% 15.11/3.01 % (225836)Termination phase: Saturation
% 15.11/3.01 % (225836)Time elapsed: 0.232 s
% 15.11/3.01 % (225836)Peak memory usage: 91 MB
% 15.11/3.01 % (225836)Instructions burned: 384 (million)
% 15.11/3.01 % (225846)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=1812530531:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi)
% 15.11/3.01 % (225849)dis+1010_1_to=kbo:si=on:random_seed=459879541:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2984 on theBenchmark for (2984ds/175Mi)
% 15.11/3.01 % (225846)Instruction limit reached!
% 15.11/3.01 % (225846)------------------------------
% 15.11/3.01 % (225846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225846)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225846)Termination reason: Instruction limit
% 15.11/3.01 % (225846)Termination phase: Saturation
% 15.11/3.01 % (225846)Time elapsed: 0.053 s
% 15.11/3.01 % (225846)Peak memory usage: 116 MB
% 15.11/3.01 % (225846)Instructions burned: 39 (million)
% 15.11/3.01 % (225850)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3325434278:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi)
% 15.11/3.01 % (225851)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=34246179:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi)
% 15.11/3.01 % (225852)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=2693478300:thitd=on:i=215:nm=0:rtra=on:ev=force_2984 on theBenchmark for (2984ds/215Mi)
% 15.11/3.01 % (225853)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=526109507:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi)
% 15.11/3.01 % (225850)Instruction limit reached!
% 15.11/3.01 % (225850)------------------------------
% 15.11/3.01 % (225850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225850)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225850)Termination reason: Instruction limit
% 15.11/3.01 % (225850)Termination phase: Saturation
% 15.11/3.01 % (225850)Time elapsed: 0.082 s
% 15.11/3.01 % (225850)Peak memory usage: 113 MB
% 15.11/3.01 % (225850)Instructions burned: 332 (million)
% 15.11/3.01 % (225849)Instruction limit reached!
% 15.11/3.01 % (225849)------------------------------
% 15.11/3.01 % (225849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225849)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225849)Termination reason: Instruction limit
% 15.11/3.01 % (225849)Termination phase: Saturation
% 15.11/3.01 % (225849)Time elapsed: 0.134 s
% 15.11/3.01 % (225849)Peak memory usage: 91 MB
% 15.11/3.01 % (225849)Instructions burned: 175 (million)
% 15.11/3.01 % (225856)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=1346656544:st=2:i=295:rtra=on:ss=axioms_2982 on theBenchmark for (2982ds/295Mi)
% 15.11/3.01 % (225853)First to succeed.
% 15.11/3.01 % (225853)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-225749"
% 15.11/3.01 % (225834)Instruction limit reached!
% 15.11/3.01 % (225834)------------------------------
% 15.11/3.01 % (225834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225834)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225834)Termination reason: Instruction limit
% 15.11/3.01 % (225834)Termination phase: Saturation
% 15.11/3.01 % (225834)Time elapsed: 0.550 s
% 15.11/3.01 % (225834)Peak memory usage: 94 MB
% 15.11/3.01 % (225834)Instructions burned: 1000 (million)
% 15.11/3.01 % (225861)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=3562699179:i=328:kws=inv_frequency:nm=20:rtra=on_2982 on theBenchmark for (2982ds/328Mi)
% 15.11/3.01 % (225852)Instruction limit reached!
% 15.11/3.01 % (225852)------------------------------
% 15.11/3.01 % (225852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225852)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225852)Termination reason: Instruction limit
% 15.11/3.01 % (225852)Termination phase: Saturation
% 15.11/3.01 % (225852)Time elapsed: 0.174 s
% 15.11/3.01 % (225852)Peak memory usage: 134 MB
% 15.11/3.01 % (225852)Instructions burned: 215 (million)
% 15.11/3.01 % (225862)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=2367231856:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi)
% 15.11/3.01 % (225856)Instruction limit reached!
% 15.11/3.01 % (225856)------------------------------
% 15.11/3.01 % (225856)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225856)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225856)Termination reason: Instruction limit
% 15.11/3.01 % (225856)Termination phase: Saturation
% 15.11/3.01 % (225856)Time elapsed: 0.162 s
% 15.11/3.01 % (225856)Peak memory usage: 90 MB
% 15.11/3.01 % (225856)Instructions burned: 296 (million)
% 15.11/3.01 % (225864)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=512227043:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi)
% 15.11/3.01 % (225861)Instruction limit reached!
% 15.11/3.01 % (225861)------------------------------
% 15.11/3.01 % (225861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225861)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225861)Termination reason: Instruction limit
% 15.11/3.01 % (225861)Termination phase: Saturation
% 15.11/3.01 % (225861)Time elapsed: 0.130 s
% 15.11/3.01 % (225861)Peak memory usage: 118 MB
% 15.11/3.01 % (225861)Instructions burned: 330 (million)
% 15.11/3.01 % (225866)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=607332039:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2980 on theBenchmark for (2980ds/321Mi)
% 15.11/3.01 % (225851)Instruction limit reached!
% 15.11/3.01 % (225851)------------------------------
% 15.11/3.01 % (225851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225851)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225851)Termination reason: Instruction limit
% 15.11/3.01 % (225851)Termination phase: Saturation
% 15.11/3.01 % (225851)Time elapsed: 0.367 s
% 15.11/3.01 % (225851)Peak memory usage: 135 MB
% 15.11/3.01 % (225851)Instructions burned: 484 (million)
% 15.11/3.01 % (225862)Refutation not found, SMT solver inside AVATAR returned Unknown
% 15.11/3.01 % (225862)------------------------------
% 15.11/3.01 % (225862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.11/3.01 % (225862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.11/3.01 % (225862)CaDiCaL version: 2.1.3
% 15.11/3.01 % (225862)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 15.11/3.01 % (225862)Time elapsed: 0.155 s
% 15.11/3.01 % (225862)Peak memory usage: 117 MB
% 15.11/3.01 % (225862)Instructions burned: 186 (million)
% 15.11/3.01 % (225862)------------------------------
% 15.11/3.01 % (225862)------------------------------
% 15.11/3.01 % (225853)Refutation found. Thanks to Tanya!
% 15.11/3.01 % SZS status Theorem for theBenchmark
% 15.11/3.01 % SZS output start Proof for theBenchmark
% See solution above
% 15.74/3.12 % (225853)------------------------------
% 15.74/3.12 % (225853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.74/3.12 % (225853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.74/3.12 % (225853)CaDiCaL version: 2.1.3
% 15.74/3.12 % (225853)Termination reason: Refutation
% 15.74/3.12 % (225853)Time elapsed: 0.098 s
% 15.74/3.12 % (225853)Peak memory usage: 117 MB
% 15.74/3.12 % (225853)Instructions burned: 103 (million)
% 15.74/3.12 % (225853)------------------------------
% 15.74/3.12 % (225853)------------------------------
% 15.74/3.12 % (225749)Success in time 2.363 s
% 15.74/3.12 % Vampire exiting
%------------------------------------------------------------------------------