%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX103_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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:53 PM UTC 2026
% Result : Theorem 10.70s 2.20s
% Output : Refutation 11.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 17
% Syntax : Number of formulae : 72 ( 9 unt; 0 typ; 13 def)
% Number of atoms : 399 ( 170 equ)
% Maximal formula atoms : 46 ( 5 avg)
% Number of connectives : 487 ( 160 ~; 125 |; 175 &)
% ( 21 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 411 ( 106 atm; 90 fun; 85 num; 130 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 : 29 ( 24 usr; 14 prp; 0-2 aty)
% Number of functors : 36 ( 32 usr; 11 con; 0-2 aty)
% Number of variables : 196 ( 97 !; 99 ?; 196 :)
% 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_4,type,
a_i: $int ).
tff(func_def_5,type,
b_i: $int ).
tff(func_def_11,type,
sK0: general > symbol ).
tff(func_def_12,type,
sK1: $int > $int ).
tff(func_def_13,type,
sK2: $int ).
tff(func_def_14,type,
sK3: $int ).
tff(func_def_15,type,
sK4: $int ).
tff(func_def_16,type,
sK5: general > general ).
tff(func_def_17,type,
sK6: general > general ).
tff(func_def_18,type,
sK7: general > general ).
tff(func_def_19,type,
sK8: general > $int ).
tff(func_def_20,type,
sK9: general > $int ).
tff(func_def_21,type,
sK10: general > $int ).
tff(func_def_22,type,
sK11: general > general ).
tff(func_def_23,type,
sK12: general > general ).
tff(func_def_24,type,
sK13: general > $int ).
tff(func_def_25,type,
sK14: general > $int ).
tff(func_def_26,type,
sK15: general > general ).
tff(func_def_27,type,
sK16: general > general ).
tff(func_def_28,type,
sK17: general > $int ).
tff(func_def_29,type,
sK18: general > $int ).
tff(func_def_30,type,
sK19: general > $int ).
tff(func_def_31,type,
sK20: general > $int ).
tff(func_def_32,type,
sK21: general > $int ).
tff(func_def_33,type,
sK22: general > $int ).
tff(func_def_34,type,
sK23: general > $int ).
tff(func_def_36,type,
'$inst25': $int ).
tff(func_def_38,type,
'$inst26': $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,
composite: general > $o ).
tff(pred_def_9,type,
sqrtb: general > $o ).
tff(pred_def_10,type,
composite_p: general > $o ).
tff(pred_def_11,type,
prime: general > $o ).
tff(pred_def_12,type,
sqrt: ( general * general ) > $o ).
tff(f18,axiom,
! [X0: general] :
( ? [X1: general] :
( ? [X2: general,X3: general] :
( ( X3 = f__integer__(b_i) )
& ? [X5: $int,X4: $int] :
( ( X2 = f__integer__($product(X4,X5)) )
& ? [X4: $int,X8: $int] :
( ( X8 = 1 )
& ( X5 = $sum(X4,X8) )
& ( f__integer__(X4) = X1 ) )
& ? [X7: $int,X5: $int] :
( ( f__integer__(X7) = X1 )
& ( X4 = $sum(X7,X5) )
& ( X5 = 1 ) ) )
& p__greater__(X2,X3) )
& ( X0 = X1 )
& ? [X2: general,X3: general] :
( ? [X4: $int,X6: $int,X5: $int] :
( ( X5 = b_i )
& ( X3 = f__integer__(X6) )
& $lesseq(X6,X5)
& $lesseq(X4,X6)
& ( X4 = 1 ) )
& ( X2 = X3 )
& ( X2 = X1 ) )
& ? [X2: general,X3: general] :
( p__less_equal__(X2,X3)
& ( X3 = f__integer__(b_i) )
& ? [X5: $int,X4: $int] :
( ( f__integer__(X4) = X1 )
& ( f__integer__(X5) = X1 )
& ( X2 = f__integer__($product(X4,X5)) ) ) ) )
<=> sqrtb(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_completed_definition_of_sqrtb_1) ).
tff(f21,axiom,
! [X0: $int,X1: $int] :
( sqrt(f__integer__(X0),f__integer__(X1))
<=> ( $lesseq($product(X0,X0),X1)
& $less(X1,$product($sum(X0,1),$sum(X0,1)))
& $greatereq(X0,0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_5_unnamed_formula) ).
tff(f24,axiom,
! [X0: $int] :
( $greatereq(b_i,1)
=> ( sqrt(f__integer__(X0),f__integer__(b_i))
<=> sqrtb(f__integer__(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_8_unnamed_formula) ).
tff(f25,conjecture,
! [X0: $int,X2: $int,X1: $int] :
( ( $lesseq($product(X0,X1),b_i)
& $greatereq(X1,0)
& sqrtb(f__integer__(X2))
& $greatereq(X0,0) )
=> ( $lesseq(X0,X2)
| $lesseq(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_9_unnamed_formula) ).
tff(f26,negated_conjecture,
~ ! [X0: $int,X2: $int,X1: $int] :
( ( $lesseq($product(X0,X1),b_i)
& $greatereq(X1,0)
& sqrtb(f__integer__(X2))
& $greatereq(X0,0) )
=> ( $lesseq(X0,X2)
| $lesseq(X1,X2) ) ),
inference(negated_conjecture,[status(cth)],[f25]) ).
tff(f27,plain,
! [X0: $int] :
( ~ $less(b_i,1)
=> ( sqrt(f__integer__(X0),f__integer__(b_i))
<=> sqrtb(f__integer__(X0)) ) ),
inference(theory_normalization,[],[f24]) ).
tff(f31,plain,
! [X0: general] :
( ? [X1: general] :
( ? [X2: general,X3: general] :
( ( X3 = f__integer__(b_i) )
& ? [X5: $int,X4: $int] :
( ( X2 = f__integer__($product(X4,X5)) )
& ? [X4: $int,X8: $int] :
( ( X8 = 1 )
& ( X5 = $sum(X4,X8) )
& ( f__integer__(X4) = X1 ) )
& ? [X7: $int,X5: $int] :
( ( f__integer__(X7) = X1 )
& ( X4 = $sum(X7,X5) )
& ( X5 = 1 ) ) )
& p__greater__(X2,X3) )
& ( X0 = X1 )
& ? [X2: general,X3: general] :
( ? [X4: $int,X6: $int,X5: $int] :
( ( X5 = b_i )
& ( X3 = f__integer__(X6) )
& ~ $less(X5,X6)
& ~ $less(X6,X4)
& ( X4 = 1 ) )
& ( X2 = X3 )
& ( X2 = X1 ) )
& ? [X2: general,X3: general] :
( p__less_equal__(X2,X3)
& ( X3 = f__integer__(b_i) )
& ? [X5: $int,X4: $int] :
( ( f__integer__(X4) = X1 )
& ( f__integer__(X5) = X1 )
& ( X2 = f__integer__($product(X4,X5)) ) ) ) )
<=> sqrtb(X0) ),
inference(theory_normalization,[],[f18]) ).
tff(f32,plain,
~ ! [X0: $int,X2: $int,X1: $int] :
( ( ~ $less(b_i,$product(X0,X1))
& ~ $less(X1,0)
& sqrtb(f__integer__(X2))
& ~ $less(X0,0) )
=> ( ~ $less(X2,X0)
| ~ $less(X2,X1) ) ),
inference(theory_normalization,[],[f26]) ).
tff(f33,plain,
! [X1: $int,X0: $int] :
( sqrt(f__integer__(X0),f__integer__(X1))
<=> ( $less(X1,$product($sum(X0,1),$sum(X0,1)))
& ~ $less(X1,$product(X0,X0))
& ~ $less(X0,0) ) ),
inference(theory_normalization,[],[f21]) ).
tff(f43,plain,
! [X0: general] :
( ? [X1: general] :
( ? [X11: general,X10: general] :
( ? [X14: $int,X12: $int,X13: $int] :
( ( f__integer__(X13) = X11 )
& ~ $less(X13,X12)
& ~ $less(X14,X13)
& ( b_i = X14 )
& ( 1 = X12 ) )
& ( X10 = X11 )
& ( X1 = X10 ) )
& ( X0 = X1 )
& ? [X16: general,X15: general] :
( p__less_equal__(X15,X16)
& ? [X18: $int,X17: $int] :
( ( f__integer__(X17) = X1 )
& ( f__integer__($product(X18,X17)) = X15 )
& ( f__integer__(X18) = X1 ) )
& ( f__integer__(b_i) = X16 ) )
& ? [X2: general,X3: general] :
( ? [X4: $int,X5: $int] :
( ( f__integer__($product(X5,X4)) = X2 )
& ? [X9: $int,X8: $int] :
( ( 1 = X9 )
& ( $sum(X8,X9) = X5 )
& ( f__integer__(X8) = X1 ) )
& ? [X7: $int,X6: $int] :
( ( f__integer__(X6) = X1 )
& ( $sum(X6,X7) = X4 )
& ( 1 = X7 ) ) )
& ( X3 = f__integer__(b_i) )
& p__greater__(X2,X3) ) )
<=> sqrtb(X0) ),
inference(rectify,[],[f31]) ).
tff(f45,plain,
~ ! [X1: $int,X0: $int,X2: $int] :
( ( ~ $less(X2,0)
& sqrtb(f__integer__(X1))
& ~ $less(X0,0)
& ~ $less(b_i,$product(X0,X2)) )
=> ( ~ $less(X1,X2)
| ~ $less(X1,X0) ) ),
inference(rectify,[],[f32]) ).
tff(f54,plain,
! [X0: $int] :
( ( sqrt(f__integer__(X0),f__integer__(b_i))
<=> sqrtb(f__integer__(X0)) )
| $less(b_i,1) ),
inference(ennf_transformation,[],[f27]) ).
tff(f65,plain,
? [X1: $int,X0: $int,X2: $int] :
( $less(X1,X2)
& $less(X1,X0)
& ~ $less(X2,0)
& sqrtb(f__integer__(X1))
& ~ $less(X0,0)
& ~ $less(b_i,$product(X0,X2)) ),
inference(ennf_transformation,[],[f45]) ).
tff(f66,plain,
? [X0: $int,X2: $int,X1: $int] :
( $less(X1,X2)
& $less(X1,X0)
& ~ $less(b_i,$product(X0,X2))
& ~ $less(X2,0)
& ~ $less(X0,0)
& sqrtb(f__integer__(X1)) ),
inference(flattening,[],[f65]) ).
tff(f71,plain,
! [X1: $int,X0: $int] :
( ( sqrt(f__integer__(X0),f__integer__(X1))
| ~ $less(X1,$product($sum(X0,1),$sum(X0,1)))
| $less(X1,$product(X0,X0))
| $less(X0,0) )
& ( ( $less(X1,$product($sum(X0,1),$sum(X0,1)))
& ~ $less(X1,$product(X0,X0))
& ~ $less(X0,0) )
| ~ sqrt(f__integer__(X0),f__integer__(X1)) ) ),
inference(nnf_transformation,[],[f33]) ).
tff(f72,plain,
! [X1: $int,X0: $int] :
( ( sqrt(f__integer__(X0),f__integer__(X1))
| ~ $less(X1,$product($sum(X0,1),$sum(X0,1)))
| $less(X1,$product(X0,X0))
| $less(X0,0) )
& ( ( $less(X1,$product($sum(X0,1),$sum(X0,1)))
& ~ $less(X1,$product(X0,X0))
& ~ $less(X0,0) )
| ~ sqrt(f__integer__(X0),f__integer__(X1)) ) ),
inference(flattening,[],[f71]) ).
tff(f73,plain,
! [X0: $int,X1: $int] :
( ( sqrt(f__integer__(X1),f__integer__(X0))
| ~ $less(X0,$product($sum(X1,1),$sum(X1,1)))
| $less(X0,$product(X1,X1))
| $less(X1,0) )
& ( ( $less(X0,$product($sum(X1,1),$sum(X1,1)))
& ~ $less(X0,$product(X1,X1))
& ~ $less(X1,0) )
| ~ sqrt(f__integer__(X1),f__integer__(X0)) ) ),
inference(rectify,[],[f72]) ).
tff(f77,plain,
? [X0: $int,X1: $int,X2: $int] :
( $less(X2,X1)
& $less(X2,X0)
& ~ $less(b_i,$product(X0,X1))
& ~ $less(X1,0)
& ~ $less(X0,0)
& sqrtb(f__integer__(X2)) ),
inference(rectify,[],[f66]) ).
tff(f78,plain,
( $less(sK4,sK3)
& $less(sK4,sK2)
& ~ $less(b_i,$product(sK2,sK3))
& ~ $less(sK3,0)
& ~ $less(sK2,0)
& sqrtb(f__integer__(sK4)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f77]) ).
tff(f81,plain,
! [X0: $int] :
( ( ( sqrt(f__integer__(X0),f__integer__(b_i))
| ~ sqrtb(f__integer__(X0)) )
& ( sqrtb(f__integer__(X0))
| ~ sqrt(f__integer__(X0),f__integer__(b_i)) ) )
| $less(b_i,1) ),
inference(nnf_transformation,[],[f54]) ).
tff(f87,plain,
! [X0: general] :
( ( ? [X1: general] :
( ? [X11: general,X10: general] :
( ? [X14: $int,X12: $int,X13: $int] :
( ( f__integer__(X13) = X11 )
& ~ $less(X13,X12)
& ~ $less(X14,X13)
& ( b_i = X14 )
& ( 1 = X12 ) )
& ( X10 = X11 )
& ( X1 = X10 ) )
& ( X0 = X1 )
& ? [X16: general,X15: general] :
( p__less_equal__(X15,X16)
& ? [X18: $int,X17: $int] :
( ( f__integer__(X17) = X1 )
& ( f__integer__($product(X18,X17)) = X15 )
& ( f__integer__(X18) = X1 ) )
& ( f__integer__(b_i) = X16 ) )
& ? [X2: general,X3: general] :
( ? [X4: $int,X5: $int] :
( ( f__integer__($product(X5,X4)) = X2 )
& ? [X9: $int,X8: $int] :
( ( 1 = X9 )
& ( $sum(X8,X9) = X5 )
& ( f__integer__(X8) = X1 ) )
& ? [X7: $int,X6: $int] :
( ( f__integer__(X6) = X1 )
& ( $sum(X6,X7) = X4 )
& ( 1 = X7 ) ) )
& ( X3 = f__integer__(b_i) )
& p__greater__(X2,X3) ) )
| ~ sqrtb(X0) )
& ( sqrtb(X0)
| ! [X1: general] :
( ! [X11: general,X10: general] :
( ! [X14: $int,X12: $int,X13: $int] :
( ( f__integer__(X13) != X11 )
| $less(X13,X12)
| $less(X14,X13)
| ( b_i != X14 )
| ( 1 != X12 ) )
| ( X10 != X11 )
| ( X1 != X10 ) )
| ( X0 != X1 )
| ! [X16: general,X15: general] :
( ~ p__less_equal__(X15,X16)
| ! [X18: $int,X17: $int] :
( ( f__integer__(X17) != X1 )
| ( f__integer__($product(X18,X17)) != X15 )
| ( f__integer__(X18) != X1 ) )
| ( f__integer__(b_i) != X16 ) )
| ! [X2: general,X3: general] :
( ! [X4: $int,X5: $int] :
( ( f__integer__($product(X5,X4)) != X2 )
| ! [X9: $int,X8: $int] :
( ( 1 != X9 )
| ( $sum(X8,X9) != X5 )
| ( f__integer__(X8) != X1 ) )
| ! [X7: $int,X6: $int] :
( ( f__integer__(X6) != X1 )
| ( $sum(X6,X7) != X4 )
| ( 1 != X7 ) ) )
| ( f__integer__(b_i) != X3 )
| ~ p__greater__(X2,X3) ) ) ) ),
inference(nnf_transformation,[],[f43]) ).
tff(f88,plain,
! [X0: general] :
( ( ? [X1: general] :
( ? [X2: general,X3: general] :
( ? [X4: $int,X5: $int,X6: $int] :
( ( f__integer__(X6) = X2 )
& ~ $less(X6,X5)
& ~ $less(X4,X6)
& ( b_i = X4 )
& ( 1 = X5 ) )
& ( X2 = X3 )
& ( X1 = X3 ) )
& ( X0 = X1 )
& ? [X7: general,X8: general] :
( p__less_equal__(X8,X7)
& ? [X9: $int,X10: $int] :
( ( f__integer__(X10) = X1 )
& ( f__integer__($product(X9,X10)) = X8 )
& ( f__integer__(X9) = X1 ) )
& ( f__integer__(b_i) = X7 ) )
& ? [X11: general,X12: general] :
( ? [X13: $int,X14: $int] :
( ( f__integer__($product(X14,X13)) = X11 )
& ? [X15: $int,X16: $int] :
( ( 1 = X15 )
& ( $sum(X16,X15) = X14 )
& ( f__integer__(X16) = X1 ) )
& ? [X17: $int,X18: $int] :
( ( f__integer__(X18) = X1 )
& ( $sum(X18,X17) = X13 )
& ( 1 = X17 ) ) )
& ( f__integer__(b_i) = X12 )
& p__greater__(X11,X12) ) )
| ~ sqrtb(X0) )
& ( sqrtb(X0)
| ! [X19: general] :
( ! [X20: general,X21: general] :
( ! [X22: $int,X23: $int,X24: $int] :
( ( f__integer__(X24) != X20 )
| $less(X24,X23)
| $less(X22,X24)
| ( b_i != X22 )
| ( 1 != X23 ) )
| ( X20 != X21 )
| ( X19 != X21 ) )
| ( X0 != X19 )
| ! [X25: general,X26: general] :
( ~ p__less_equal__(X26,X25)
| ! [X27: $int,X28: $int] :
( ( f__integer__(X28) != X19 )
| ( f__integer__($product(X27,X28)) != X26 )
| ( f__integer__(X27) != X19 ) )
| ( f__integer__(b_i) != X25 ) )
| ! [X29: general,X30: general] :
( ! [X31: $int,X32: $int] :
( ( f__integer__($product(X32,X31)) != X29 )
| ! [X33: $int,X34: $int] :
( ( 1 != X33 )
| ( $sum(X34,X33) != X32 )
| ( f__integer__(X34) != X19 ) )
| ! [X35: $int,X36: $int] :
( ( f__integer__(X36) != X19 )
| ( $sum(X36,X35) != X31 )
| ( 1 != X35 ) ) )
| ( f__integer__(b_i) != X30 )
| ~ p__greater__(X29,X30) ) ) ) ),
inference(rectify,[],[f87]) ).
tff(f89,plain,
! [X0: general] :
( ( ( ( sK6(X0) = f__integer__(sK10(X0)) )
& ~ $less(sK10(X0),sK9(X0))
& ~ $less(sK8(X0),sK10(X0))
& ( b_i = sK8(X0) )
& ( 1 = sK9(X0) )
& ( sK6(X0) = sK7(X0) )
& ( sK5(X0) = sK7(X0) )
& ( sK5(X0) = X0 )
& p__less_equal__(sK12(X0),sK11(X0))
& ( f__integer__(sK14(X0)) = sK5(X0) )
& ( f__integer__($product(sK13(X0),sK14(X0))) = sK12(X0) )
& ( sK5(X0) = f__integer__(sK13(X0)) )
& ( f__integer__(b_i) = sK11(X0) )
& ( f__integer__($product(sK18(X0),sK17(X0))) = sK15(X0) )
& ( 1 = sK19(X0) )
& ( sK18(X0) = $sum(sK20(X0),sK19(X0)) )
& ( f__integer__(sK20(X0)) = sK5(X0) )
& ( f__integer__(sK22(X0)) = sK5(X0) )
& ( $sum(sK22(X0),sK21(X0)) = sK17(X0) )
& ( 1 = sK21(X0) )
& ( f__integer__(b_i) = sK16(X0) )
& p__greater__(sK15(X0),sK16(X0)) )
| ~ sqrtb(X0) )
& ( sqrtb(X0)
| ! [X19: general] :
( ! [X20: general,X21: general] :
( ! [X22: $int,X23: $int,X24: $int] :
( ( f__integer__(X24) != X20 )
| $less(X24,X23)
| $less(X22,X24)
| ( b_i != X22 )
| ( 1 != X23 ) )
| ( X20 != X21 )
| ( X19 != X21 ) )
| ( X0 != X19 )
| ! [X25: general,X26: general] :
( ~ p__less_equal__(X26,X25)
| ! [X27: $int,X28: $int] :
( ( f__integer__(X28) != X19 )
| ( f__integer__($product(X27,X28)) != X26 )
| ( f__integer__(X27) != X19 ) )
| ( f__integer__(b_i) != X25 ) )
| ! [X29: general,X30: general] :
( ! [X31: $int,X32: $int] :
( ( f__integer__($product(X32,X31)) != X29 )
| ! [X33: $int,X34: $int] :
( ( 1 != X33 )
| ( $sum(X34,X33) != X32 )
| ( f__integer__(X34) != X19 ) )
| ! [X35: $int,X36: $int] :
( ( f__integer__(X36) != X19 )
| ( $sum(X36,X35) != X31 )
| ( 1 != X35 ) ) )
| ( f__integer__(b_i) != X30 )
| ~ p__greater__(X29,X30) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22]),skolemize(X1,sK5(X0)),skolemize(X2,sK6(X0)),skolemize(X3,sK7(X0)),skolemize(X4,sK8(X0)),skolemize(X5,sK9(X0)),skolemize(X6,sK10(X0)),skolemize(X7,sK11(X0)),skolemize(X8,sK12(X0)),skolemize(X9,sK13(X0)),skolemize(X10,sK14(X0)),skolemize(X11,sK15(X0)),skolemize(X12,sK16(X0)),skolemize(X13,sK17(X0)),skolemize(X14,sK18(X0)),skolemize(X15,sK19(X0)),skolemize(X16,sK20(X0)),skolemize(X17,sK21(X0)),skolemize(X18,sK22(X0))],[f88]) ).
tff(f100,plain,
! [X0: $int,X1: $int] :
( ~ $less(X0,$product(X1,X1))
| ~ sqrt(f__integer__(X1),f__integer__(X0)) ),
inference(cnf_transformation,[],[f73]) ).
tff(f101,plain,
! [X0: $int,X1: $int] :
( $less(X0,$product($sum(X1,1),$sum(X1,1)))
| ~ sqrt(f__integer__(X1),f__integer__(X0)) ),
inference(cnf_transformation,[],[f73]) ).
tff(f108,plain,
sqrtb(f__integer__(sK4)),
inference(cnf_transformation,[],[f78]) ).
tff(f111,plain,
~ $less(b_i,$product(sK2,sK3)),
inference(cnf_transformation,[],[f78]) ).
tff(f112,plain,
$less(sK4,sK2),
inference(cnf_transformation,[],[f78]) ).
tff(f113,plain,
$less(sK4,sK3),
inference(cnf_transformation,[],[f78]) ).
tff(f119,plain,
! [X0: $int] :
( $less(b_i,1)
| sqrt(f__integer__(X0),f__integer__(b_i))
| ~ sqrtb(f__integer__(X0)) ),
inference(cnf_transformation,[],[f81]) ).
tff(f144,plain,
! [X0: general] :
( ( 1 = sK9(X0) )
| ~ sqrtb(X0) ),
inference(cnf_transformation,[],[f89]) ).
tff(f145,plain,
! [X0: general] :
( ( b_i = sK8(X0) )
| ~ sqrtb(X0) ),
inference(cnf_transformation,[],[f89]) ).
tff(f146,plain,
! [X0: general] :
( ~ $less(sK8(X0),sK10(X0))
| ~ sqrtb(X0) ),
inference(cnf_transformation,[],[f89]) ).
tff(f147,plain,
! [X0: general] :
( ~ $less(sK10(X0),sK9(X0))
| ~ sqrtb(X0) ),
inference(cnf_transformation,[],[f89]) ).
tff(f175,definition,
( spl24_2
<=> $less(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl24_2])],[avatar_definition]) ).
tff(f178,plain,
spl24_2,
inference(avatar_split_clause,[],[f113,f175]) ).
tff(f193,definition,
( spl24_6
<=> $less(b_i,1) ),
introduced(definition,[new_symbols(definition,[spl24_6])],[avatar_definition]) ).
tff(f198,definition,
( spl24_7
<=> $less(b_i,$product(sK2,sK3)) ),
introduced(definition,[new_symbols(definition,[spl24_7])],[avatar_definition]) ).
tff(f201,plain,
~ spl24_7,
inference(avatar_split_clause,[],[f111,f198]) ).
tff(f203,definition,
( spl24_8
<=> ! [X0: $int] :
( sqrt(f__integer__(X0),f__integer__(b_i))
| ~ sqrtb(f__integer__(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl24_8])],[avatar_definition]) ).
tff(f204,plain,
( ! [X0: $int] :
( sqrt(f__integer__(X0),f__integer__(b_i))
| ~ sqrtb(f__integer__(X0)) )
| ~ spl24_8 ),
inference(avatar_component_clause,[],[f203]) ).
tff(f205,plain,
( spl24_6
| spl24_8 ),
inference(avatar_split_clause,[],[f119,f203,f193]) ).
tff(f207,definition,
( spl24_9
<=> sqrtb(f__integer__(sK4)) ),
introduced(definition,[new_symbols(definition,[spl24_9])],[avatar_definition]) ).
tff(f209,plain,
( sqrtb(f__integer__(sK4))
| ~ spl24_9 ),
inference(avatar_component_clause,[],[f207]) ).
tff(f210,plain,
spl24_9,
inference(avatar_split_clause,[],[f108,f207]) ).
tff(f212,definition,
( spl24_10
<=> $less(sK4,sK2) ),
introduced(definition,[new_symbols(definition,[spl24_10])],[avatar_definition]) ).
tff(f215,plain,
spl24_10,
inference(avatar_split_clause,[],[f112,f212]) ).
tff(f234,plain,
( ( 1 = sK9(f__integer__(sK4)) )
| ~ spl24_9 ),
inference(unit_resulting_resolution,[],[f144,f209]) ).
tff(f236,definition,
( spl24_14
<=> ( 1 = sK9(f__integer__(sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl24_14])],[avatar_definition]) ).
tff(f238,plain,
( ( 1 = sK9(f__integer__(sK4)) )
| ~ spl24_14 ),
inference(avatar_component_clause,[],[f236]) ).
tff(f239,plain,
( spl24_14
| ~ spl24_9 ),
inference(avatar_split_clause,[],[f234,f207,f236]) ).
tff(f240,plain,
( ( b_i = sK8(f__integer__(sK4)) )
| ~ spl24_9 ),
inference(unit_resulting_resolution,[],[f145,f209]) ).
tff(f242,definition,
( spl24_15
<=> ( b_i = sK8(f__integer__(sK4)) ) ),
introduced(definition,[new_symbols(definition,[spl24_15])],[avatar_definition]) ).
tff(f244,plain,
( ( b_i = sK8(f__integer__(sK4)) )
| ~ spl24_15 ),
inference(avatar_component_clause,[],[f242]) ).
tff(f245,plain,
( spl24_15
| ~ spl24_9 ),
inference(avatar_split_clause,[],[f240,f207,f242]) ).
tff(f294,plain,
( ~ $less(b_i,sK10(f__integer__(sK4)))
| ~ sqrtb(f__integer__(sK4))
| ~ spl24_15 ),
inference(superposition,[],[f146,f244]) ).
tff(f302,definition,
( spl24_23
<=> $less(b_i,sK10(f__integer__(sK4))) ),
introduced(definition,[new_symbols(definition,[spl24_23])],[avatar_definition]) ).
tff(f305,plain,
( ~ spl24_9
| ~ spl24_23
| ~ spl24_15 ),
inference(avatar_split_clause,[],[f294,f242,f302,f207]) ).
tff(f308,plain,
( ~ sqrtb(f__integer__(sK4))
| ~ $less(sK10(f__integer__(sK4)),1)
| ~ spl24_14 ),
inference(superposition,[],[f147,f238]) ).
tff(f311,definition,
( spl24_24
<=> $less(sK10(f__integer__(sK4)),1) ),
introduced(definition,[new_symbols(definition,[spl24_24])],[avatar_definition]) ).
tff(f314,plain,
( ~ spl24_24
| ~ spl24_9
| ~ spl24_14 ),
inference(avatar_split_clause,[],[f308,f236,f207,f311]) ).
tff(f487,plain,
( sqrt(f__integer__(sK4),f__integer__(b_i))
| ~ spl24_8
| ~ spl24_9 ),
inference(unit_resulting_resolution,[],[f204,f209]) ).
tff(f497,definition,
( spl24_40
<=> sqrt(f__integer__(sK4),f__integer__(b_i)) ),
introduced(definition,[new_symbols(definition,[spl24_40])],[avatar_definition]) ).
tff(f499,plain,
( sqrt(f__integer__(sK4),f__integer__(b_i))
| ~ spl24_40 ),
inference(avatar_component_clause,[],[f497]) ).
tff(f500,plain,
( spl24_40
| ~ spl24_8
| ~ spl24_9 ),
inference(avatar_split_clause,[],[f487,f207,f203,f497]) ).
tff(f569,plain,
( ~ $less(b_i,$product(sK4,sK4))
| ~ spl24_40 ),
inference(unit_resulting_resolution,[],[f100,f499]) ).
tff(f574,definition,
( spl24_49
<=> $less(b_i,$product(sK4,sK4)) ),
introduced(definition,[new_symbols(definition,[spl24_49])],[avatar_definition]) ).
tff(f577,plain,
( ~ spl24_49
| ~ spl24_40 ),
inference(avatar_split_clause,[],[f569,f497,f574]) ).
tff(f623,plain,
( $less(b_i,$product($sum(sK4,1),$sum(sK4,1)))
| ~ spl24_40 ),
inference(unit_resulting_resolution,[],[f101,f499]) ).
tff(f626,definition,
( spl24_53
<=> $less(b_i,$product($sum(sK4,1),$sum(sK4,1))) ),
introduced(definition,[new_symbols(definition,[spl24_53])],[avatar_definition]) ).
tff(f629,plain,
( spl24_53
| ~ spl24_40 ),
inference(avatar_split_clause,[],[f623,f497,f626]) ).
tff(f630,plain,
$false,
inference(avatar_smt_refutation,[],[f629,f577,f500,f314,f305,f245,f239,f215,f210,f205,f201,f178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX103_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n009.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:01:30 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.68/1.22 % (3125812)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.68/1.22 % (3125819)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1463594364:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.68/1.22 % (3125817)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3975107513:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.68/1.22 % (3125818)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2518486972:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.68/1.22 % (3125820)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2120970908:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.68/1.22 % (3125820)Instruction limit reached!
% 3.68/1.22 % (3125820)------------------------------
% 3.68/1.22 % (3125820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.22 % (3125820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.22 % (3125820)CaDiCaL version: 2.1.3
% 3.68/1.22 % (3125820)Termination reason: Instruction limit
% 3.68/1.22 % (3125820)Termination phase: Saturation
% 3.68/1.22 % (3125820)Time elapsed: 0.005 s
% 3.68/1.22 % (3125820)Peak memory usage: 88 MB
% 3.68/1.22 % (3125820)Instructions burned: 7 (million)
% 3.68/1.22 % (3125821)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1656301934:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.68/1.22 % (3125823)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=327228374:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.68/1.22 % (3125822)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3507568168:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.68/1.22 % (3125821)Instruction limit reached!
% 3.68/1.22 % (3125821)------------------------------
% 3.68/1.22 % (3125821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.22 % (3125821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.22 % (3125821)CaDiCaL version: 2.1.3
% 3.68/1.22 % (3125821)Termination reason: Instruction limit
% 3.68/1.22 % (3125821)Termination phase: Saturation
% 3.68/1.22 % (3125821)Time elapsed: 0.003 s
% 3.68/1.22 % (3125821)Peak memory usage: 88 MB
% 3.68/1.22 % (3125821)Instructions burned: 4 (million)
% 3.68/1.22 % (3125819)Instruction limit reached!
% 3.68/1.22 % (3125819)------------------------------
% 3.68/1.22 % (3125819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.22 % (3125819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.22 % (3125819)CaDiCaL version: 2.1.3
% 3.68/1.22 % (3125819)Termination reason: Instruction limit
% 3.68/1.22 % (3125819)Termination phase: Saturation
% 3.68/1.22 % (3125819)Time elapsed: 0.069 s
% 3.68/1.22 % (3125819)Peak memory usage: 113 MB
% 3.68/1.22 % (3125819)Instructions burned: 203 (million)
% 3.68/1.22 % (3125817)Instruction limit reached!
% 3.68/1.22 % (3125817)------------------------------
% 3.68/1.22 % (3125817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.22 % (3125817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.22 % (3125817)CaDiCaL version: 2.1.3
% 3.68/1.22 % (3125817)Termination reason: Instruction limit
% 3.68/1.22 % (3125817)Termination phase: Saturation
% 3.68/1.22 % (3125817)Time elapsed: 0.032 s
% 3.68/1.22 % (3125817)Peak memory usage: 117 MB
% 3.68/1.22 % (3125817)Instructions burned: 13 (million)
% 3.68/1.22 % (3125823)Instruction limit reached!
% 3.68/1.22 % (3125823)------------------------------
% 3.68/1.22 % (3125823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.22 % (3125823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.68/1.22 % (3125823)CaDiCaL version: 2.1.3
% 3.68/1.22 % (3125823)Termination reason: Instruction limit
% 3.68/1.22 % (3125823)Termination phase: Saturation
% 3.68/1.22 % (3125823)Time elapsed: 0.046 s
% 3.68/1.22 % (3125823)Peak memory usage: 117 MB
% 3.68/1.22 % (3125823)Instructions burned: 33 (million)
% 3.68/1.22 % (3125822)Instruction limit reached!
% 3.68/1.22 % (3125822)------------------------------
% 3.68/1.22 % (3125822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.68/1.22 % (3125822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.60/1.37 % (3125822)CaDiCaL version: 2.1.3
% 4.60/1.37 % (3125822)Termination reason: Instruction limit
% 4.60/1.37 % (3125822)Termination phase: Saturation
% 4.60/1.37 % (3125822)Time elapsed: 0.057 s
% 4.60/1.37 % (3125822)Peak memory usage: 117 MB
% 4.60/1.37 % (3125822)Instructions burned: 47 (million)
% 4.60/1.37 % (3125833)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1406385108:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 4.60/1.37 % (3125833)Instruction limit reached!
% 4.60/1.37 % (3125833)------------------------------
% 4.60/1.37 % (3125833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.60/1.37 % (3125833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.60/1.37 % (3125833)CaDiCaL version: 2.1.3
% 4.60/1.37 % (3125833)Termination reason: Instruction limit
% 4.60/1.37 % (3125833)Termination phase: Saturation
% 4.60/1.37 % (3125833)Time elapsed: 0.006 s
% 4.60/1.37 % (3125833)Peak memory usage: 90 MB
% 4.60/1.37 % (3125833)Instructions burned: 17 (million)
% 4.60/1.37 % (3125831)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2453618243:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.60/1.37 % (3125831)Instruction limit reached!
% 4.60/1.37 % (3125831)------------------------------
% 4.60/1.37 % (3125831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.60/1.37 % (3125831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.60/1.37 % (3125831)CaDiCaL version: 2.1.3
% 4.60/1.37 % (3125831)Termination reason: Instruction limit
% 4.60/1.37 % (3125831)Termination phase: Saturation
% 4.60/1.37 % (3125831)Time elapsed: 0.012 s
% 4.60/1.37 % (3125831)Peak memory usage: 88 MB
% 4.60/1.37 % (3125831)Instructions burned: 15 (million)
% 4.60/1.37 % (3125832)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=19217974:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.60/1.37 % (3125832)Instruction limit reached!
% 4.60/1.37 % (3125832)------------------------------
% 4.60/1.37 % (3125832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.60/1.37 % (3125832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.60/1.37 % (3125832)CaDiCaL version: 2.1.3
% 4.60/1.37 % (3125832)Termination reason: Instruction limit
% 4.60/1.37 % (3125832)Termination phase: Saturation
% 4.60/1.37 % (3125832)Time elapsed: 0.022 s
% 4.60/1.37 % (3125832)Peak memory usage: 89 MB
% 4.60/1.37 % (3125832)Instructions burned: 30 (million)
% 4.60/1.37 % (3125834)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3065971416:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.60/1.37 % (3125835)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=1403446729:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.60/1.37 % (3125834)Instruction limit reached!
% 4.60/1.37 % (3125834)------------------------------
% 4.60/1.37 % (3125834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.60/1.37 % (3125834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.60/1.37 % (3125834)CaDiCaL version: 2.1.3
% 4.60/1.37 % (3125834)Termination reason: Instruction limit
% 4.60/1.37 % (3125834)Termination phase: Saturation
% 4.60/1.37 % (3125834)Time elapsed: 0.020 s
% 4.60/1.37 % (3125834)Peak memory usage: 89 MB
% 4.60/1.37 % (3125834)Instructions burned: 24 (million)
% 4.60/1.37 % (3125835)Instruction limit reached!
% 4.60/1.37 % (3125835)------------------------------
% 4.60/1.37 % (3125835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.60/1.37 % (3125835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.60/1.37 % (3125835)CaDiCaL version: 2.1.3
% 4.60/1.37 % (3125835)Termination reason: Instruction limit
% 4.60/1.37 % (3125835)Termination phase: Saturation
% 4.60/1.37 % (3125835)Time elapsed: 0.016 s
% 4.60/1.37 % (3125835)Peak memory usage: 89 MB
% 4.60/1.37 % (3125835)Instructions burned: 29 (million)
% 4.60/1.37 % (3125836)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3116984332:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 4.60/1.37 % (3125818)Instruction limit reached!
% 4.60/1.37 % (3125818)------------------------------
% 4.60/1.37 % (3125818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.54 % (3125818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.54 % (3125818)CaDiCaL version: 2.1.3
% 5.47/1.54 % (3125818)Termination reason: Instruction limit
% 5.47/1.54 % (3125818)Termination phase: Saturation
% 5.47/1.54 % (3125818)Time elapsed: 0.237 s
% 5.47/1.54 % (3125818)Peak memory usage: 118 MB
% 5.47/1.54 % (3125818)Instructions burned: 308 (million)
% 5.47/1.54 % (3125839)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3948441206:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.47/1.54 % (3125839)Instruction limit reached!
% 5.47/1.54 % (3125839)------------------------------
% 5.47/1.54 % (3125839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.54 % (3125839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.54 % (3125839)CaDiCaL version: 2.1.3
% 5.47/1.54 % (3125839)Termination reason: Instruction limit
% 5.47/1.54 % (3125839)Termination phase: Saturation
% 5.47/1.54 % (3125839)Time elapsed: 0.002 s
% 5.47/1.54 % (3125839)Peak memory usage: 88 MB
% 5.47/1.54 % (3125839)Instructions burned: 4 (million)
% 5.47/1.54 % (3125836)Instruction limit reached!
% 5.47/1.54 % (3125836)------------------------------
% 5.47/1.54 % (3125836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.54 % (3125836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.54 % (3125836)CaDiCaL version: 2.1.3
% 5.47/1.54 % (3125836)Termination reason: Instruction limit
% 5.47/1.54 % (3125836)Termination phase: Saturation
% 5.47/1.54 % (3125836)Time elapsed: 0.055 s
% 5.47/1.54 % (3125836)Peak memory usage: 89 MB
% 5.47/1.54 % (3125836)Instructions burned: 86 (million)
% 5.47/1.54 % (3125840)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1648363447:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.47/1.54 % (3125843)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=639756020:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.47/1.54 % (3125843)Instruction limit reached!
% 5.47/1.54 % (3125843)------------------------------
% 5.47/1.54 % (3125843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.54 % (3125843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.54 % (3125843)CaDiCaL version: 2.1.3
% 5.47/1.54 % (3125843)Termination reason: Instruction limit
% 5.47/1.54 % (3125843)Termination phase: Saturation
% 5.47/1.54 % (3125843)Time elapsed: 0.003 s
% 5.47/1.54 % (3125843)Peak memory usage: 88 MB
% 5.47/1.54 % (3125843)Instructions burned: 4 (million)
% 5.47/1.54 % (3125845)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=545584649:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.47/1.54 % (3125847)lrs+10_1_thi=all:si=on:fd=off:random_seed=3209599182:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.47/1.54 % (3125850)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=4073717544:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 5.47/1.54 % (3125850)Instruction limit reached!
% 5.47/1.54 % (3125850)------------------------------
% 5.47/1.54 % (3125850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.54 % (3125850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.54 % (3125850)CaDiCaL version: 2.1.3
% 5.47/1.54 % (3125850)Termination reason: Instruction limit
% 5.47/1.54 % (3125850)Termination phase: Equality resolution with deletion
% 5.47/1.54 % (3125850)Time elapsed: 0.001 s
% 5.47/1.54 % (3125850)Peak memory usage: 86 MB
% 5.47/1.54 % (3125850)Instructions burned: 2 (million)
% 5.47/1.54 % (3125849)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=4273830465:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 5.47/1.54 % (3125849)Instruction limit reached!
% 5.47/1.54 % (3125849)------------------------------
% 5.47/1.54 % (3125849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.47/1.54 % (3125849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.47/1.54 % (3125849)CaDiCaL version: 2.1.3
% 5.47/1.54 % (3125849)Termination reason: Instruction limit
% 5.47/1.54 % (3125849)Termination phase: Saturation
% 7.05/1.77 % (3125849)Time elapsed: 0.006 s
% 7.05/1.77 % (3125849)Peak memory usage: 89 MB
% 7.05/1.77 % (3125849)Instructions burned: 9 (million)
% 7.05/1.77 % (3125840)Instruction limit reached!
% 7.05/1.77 % (3125840)------------------------------
% 7.05/1.77 % (3125840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.05/1.77 % (3125840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.05/1.77 % (3125840)CaDiCaL version: 2.1.3
% 7.05/1.77 % (3125840)Termination reason: Instruction limit
% 7.05/1.77 % (3125840)Termination phase: Saturation
% 7.05/1.77 % (3125840)Time elapsed: 0.116 s
% 7.05/1.77 % (3125840)Peak memory usage: 90 MB
% 7.05/1.77 % (3125840)Instructions burned: 182 (million)
% 7.05/1.77 % (3125847)Instruction limit reached!
% 7.05/1.77 % (3125847)------------------------------
% 7.05/1.77 % (3125847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.05/1.77 % (3125847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.05/1.77 % (3125847)CaDiCaL version: 2.1.3
% 7.05/1.77 % (3125847)Termination reason: Instruction limit
% 7.05/1.77 % (3125847)Termination phase: Saturation
% 7.05/1.77 % (3125847)Time elapsed: 0.065 s
% 7.05/1.77 % (3125847)Peak memory usage: 117 MB
% 7.05/1.77 % (3125847)Instructions burned: 53 (million)
% 7.05/1.77 % (3125851)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3840177300:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 7.05/1.77 % (3125851)Instruction limit reached!
% 7.05/1.77 % (3125851)------------------------------
% 7.05/1.77 % (3125851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.05/1.77 % (3125851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.05/1.77 % (3125851)CaDiCaL version: 2.1.3
% 7.05/1.77 % (3125851)Termination reason: Instruction limit
% 7.05/1.77 % (3125851)Termination phase: Equality resolution with deletion
% 7.05/1.77 % (3125851)Time elapsed: 0.002 s
% 7.05/1.77 % (3125851)Peak memory usage: 86 MB
% 7.05/1.77 % (3125851)Instructions burned: 2 (million)
% 7.05/1.77 % (3125845)Instruction limit reached!
% 7.05/1.77 % (3125845)------------------------------
% 7.05/1.77 % (3125845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.05/1.77 % (3125845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.05/1.77 % (3125845)CaDiCaL version: 2.1.3
% 7.05/1.77 % (3125845)Termination reason: Instruction limit
% 7.05/1.77 % (3125845)Termination phase: Saturation
% 7.05/1.77 % (3125845)Time elapsed: 0.096 s
% 7.05/1.77 % (3125845)Peak memory usage: 136 MB
% 7.05/1.77 % (3125845)Instructions burned: 66 (million)
% 7.05/1.77 % (3125858)dis+10_1_si=on:random_seed=3828514604:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 7.05/1.77 % (3125854)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1884820663:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 7.05/1.77 % (3125858)Instruction limit reached!
% 7.05/1.77 % (3125858)------------------------------
% 7.05/1.77 % (3125858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.05/1.77 % (3125858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.05/1.77 % (3125858)CaDiCaL version: 2.1.3
% 7.05/1.77 % (3125858)Termination reason: Instruction limit
% 7.05/1.77 % (3125858)Termination phase: Saturation
% 7.05/1.77 % (3125858)Time elapsed: 0.005 s
% 7.05/1.77 % (3125858)Peak memory usage: 88 MB
% 7.05/1.77 % (3125858)Instructions burned: 13 (million)
% 7.05/1.77 % (3125860)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=677327004:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 7.05/1.77 % (3125861)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=3950613669:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2994 on theBenchmark for (2994ds/35Mi)
% 7.05/1.77 % (3125860)Refutation not found, incomplete strategy
% 7.05/1.77 % (3125860)------------------------------
% 7.05/1.77 % (3125860)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.05/1.77 % (3125860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.05/1.77 % (3125860)CaDiCaL version: 2.1.3
% 7.05/1.77 % (3125860)Termination reason: Refutation not found, incomplete strategy
% 7.05/1.77 % (3125860)Time elapsed: 0.004 s
% 7.05/1.77 % (3125860)Peak memory usage: 89 MB
% 7.05/1.77 % (3125860)Instructions burned: 5 (million)
% 10.10/2.05 % (3125864)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3173049549:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 10.10/2.05 % (3125862)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2265610144:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 10.10/2.05 % (3125862)Instruction limit reached!
% 10.10/2.05 % (3125862)------------------------------
% 10.10/2.05 % (3125862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.10/2.05 % (3125862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/2.05 % (3125862)CaDiCaL version: 2.1.3
% 10.10/2.05 % (3125862)Termination reason: Instruction limit
% 10.10/2.05 % (3125862)Termination phase: Saturation
% 10.10/2.05 % (3125862)Time elapsed: 0.002 s
% 10.10/2.05 % (3125862)Peak memory usage: 86 MB
% 10.10/2.05 % (3125862)Instructions burned: 2 (million)
% 10.10/2.05 % (3125864)Instruction limit reached!
% 10.10/2.05 % (3125864)------------------------------
% 10.10/2.05 % (3125864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.10/2.05 % (3125864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/2.05 % (3125864)CaDiCaL version: 2.1.3
% 10.10/2.05 % (3125864)Termination reason: Instruction limit
% 10.10/2.05 % (3125864)Termination phase: Saturation
% 10.10/2.05 % (3125864)Time elapsed: 0.006 s
% 10.10/2.05 % (3125864)Peak memory usage: 88 MB
% 10.10/2.05 % (3125864)Instructions burned: 8 (million)
% 10.10/2.05 % (3125861)Instruction limit reached!
% 10.10/2.05 % (3125861)------------------------------
% 10.10/2.05 % (3125861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.10/2.05 % (3125861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/2.05 % (3125861)CaDiCaL version: 2.1.3
% 10.10/2.05 % (3125861)Termination reason: Instruction limit
% 10.10/2.05 % (3125861)Termination phase: Saturation
% 10.10/2.05 % (3125861)Time elapsed: 0.029 s
% 10.10/2.05 % (3125861)Peak memory usage: 89 MB
% 10.10/2.05 % (3125861)Instructions burned: 36 (million)
% 10.10/2.05 % (3125868)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1503252917:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2993 on theBenchmark for (2993ds/13Mi)
% 10.10/2.05 % (3125865)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=2370643365:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 10.10/2.05 % (3125854)Instruction limit reached!
% 10.10/2.05 % (3125854)------------------------------
% 10.10/2.05 % (3125854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.10/2.05 % (3125854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/2.05 % (3125854)CaDiCaL version: 2.1.3
% 10.10/2.05 % (3125854)Termination reason: Instruction limit
% 10.10/2.05 % (3125854)Termination phase: Saturation
% 10.10/2.05 % (3125854)Time elapsed: 0.119 s
% 10.10/2.05 % (3125854)Peak memory usage: 118 MB
% 10.10/2.05 % (3125854)Instructions burned: 127 (million)
% 10.10/2.05 % (3125868)Instruction limit reached!
% 10.10/2.05 % (3125868)------------------------------
% 10.10/2.05 % (3125868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.10/2.05 % (3125868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.10/2.05 % (3125868)CaDiCaL version: 2.1.3
% 10.10/2.05 % (3125868)Termination reason: Instruction limit
% 10.10/2.05 % (3125868)Termination phase: Saturation
% 10.10/2.05 % (3125868)Time elapsed: 0.019 s
% 10.10/2.05 % (3125868)Peak memory usage: 113 MB
% 10.10/2.05 % (3125868)Instructions burned: 15 (million)
% 10.10/2.05 % (3125879)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=3889546991:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2992 on theBenchmark for (2992ds/294Mi)
% 10.10/2.05 % (3125876)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1910042281:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 10.10/2.05 % (3125874)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1774787862:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 10.10/2.05 % (3125873)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=111385875:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 10.10/2.05 % (3125878)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=232030319:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 10.70/2.20 % (3125874)Instruction limit reached!
% 10.70/2.20 % (3125874)------------------------------
% 10.70/2.20 % (3125874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125874)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125874)Termination reason: Instruction limit
% 10.70/2.20 % (3125874)Termination phase: Saturation
% 10.70/2.20 % (3125874)Time elapsed: 0.007 s
% 10.70/2.20 % (3125874)Peak memory usage: 88 MB
% 10.70/2.20 % (3125874)Instructions burned: 10 (million)
% 10.70/2.20 % (3125878)Instruction limit reached!
% 10.70/2.20 % (3125878)------------------------------
% 10.70/2.20 % (3125878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125878)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125878)Termination reason: Instruction limit
% 10.70/2.20 % (3125878)Termination phase: Saturation
% 10.70/2.20 % (3125878)Time elapsed: 0.058 s
% 10.70/2.20 % (3125878)Peak memory usage: 90 MB
% 10.70/2.20 % (3125878)Instructions burned: 75 (million)
% 10.70/2.20 % (3125860)------------------------------
% 10.70/2.20 % (3125860)------------------------------
% 10.70/2.20 % (3125865)Instruction limit reached!
% 10.70/2.20 % (3125865)------------------------------
% 10.70/2.20 % (3125865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125865)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125865)Termination reason: Instruction limit
% 10.70/2.20 % (3125865)Termination phase: Saturation
% 10.70/2.20 % (3125865)Time elapsed: 0.223 s
% 10.70/2.20 % (3125865)Peak memory usage: 95 MB
% 10.70/2.20 % (3125865)Instructions burned: 371 (million)
% 10.70/2.20 % (3125876)Instruction limit reached!
% 10.70/2.20 % (3125876)------------------------------
% 10.70/2.20 % (3125876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125876)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125876)Termination reason: Instruction limit
% 10.70/2.20 % (3125876)Termination phase: Saturation
% 10.70/2.20 % (3125876)Time elapsed: 0.096 s
% 10.70/2.20 % (3125876)Peak memory usage: 135 MB
% 10.70/2.20 % (3125876)Instructions burned: 72 (million)
% 10.70/2.20 % (3125879)Instruction limit reached!
% 10.70/2.20 % (3125879)------------------------------
% 10.70/2.20 % (3125879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125879)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125879)Termination reason: Instruction limit
% 10.70/2.20 % (3125879)Termination phase: Saturation
% 10.70/2.20 % (3125879)Time elapsed: 0.107 s
% 10.70/2.20 % (3125879)Peak memory usage: 91 MB
% 10.70/2.20 % (3125879)Instructions burned: 296 (million)
% 10.70/2.20 % (3125885)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=4251159385:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 10.70/2.20 % (3125873)Instruction limit reached!
% 10.70/2.20 % (3125873)------------------------------
% 10.70/2.20 % (3125873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125873)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125873)Termination reason: Instruction limit
% 10.70/2.20 % (3125873)Termination phase: Saturation
% 10.70/2.20 % (3125873)Time elapsed: 0.179 s
% 10.70/2.20 % (3125873)Peak memory usage: 118 MB
% 10.70/2.20 % (3125873)Instructions burned: 227 (million)
% 10.70/2.20 % (3125886)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1324509421:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 10.70/2.20 % (3125890)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3530805421:i=131:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 10.70/2.20 % (3125887)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=3404182979:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 10.70/2.20 % (3125888)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=913527707:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 10.70/2.20 % (3125889)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=283445084:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 10.70/2.20 % (3125885)Instruction limit reached!
% 10.70/2.20 % (3125885)------------------------------
% 10.70/2.20 % (3125885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125885)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125885)Termination reason: Instruction limit
% 10.70/2.20 % (3125885)Termination phase: Saturation
% 10.70/2.20 % (3125885)Time elapsed: 0.101 s
% 10.70/2.20 % (3125885)Peak memory usage: 118 MB
% 10.70/2.20 % (3125885)Instructions burned: 132 (million)
% 10.70/2.20 % (3125890)Instruction limit reached!
% 10.70/2.20 % (3125890)------------------------------
% 10.70/2.20 % (3125890)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125890)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125890)Termination reason: Instruction limit
% 10.70/2.20 % (3125890)Termination phase: Saturation
% 10.70/2.20 % (3125890)Time elapsed: 0.061 s
% 10.70/2.20 % (3125890)Peak memory usage: 118 MB
% 10.70/2.20 % (3125890)Instructions burned: 133 (million)
% 10.70/2.20 % (3125887)Instruction limit reached!
% 10.70/2.20 % (3125887)------------------------------
% 10.70/2.20 % (3125887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125887)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125887)Termination reason: Instruction limit
% 10.70/2.20 % (3125887)Termination phase: Saturation
% 10.70/2.20 % (3125887)Time elapsed: 0.069 s
% 10.70/2.20 % (3125887)Peak memory usage: 135 MB
% 10.70/2.20 % (3125887)Instructions burned: 40 (million)
% 10.70/2.20 % (3125886)Instruction limit reached!
% 10.70/2.20 % (3125886)------------------------------
% 10.70/2.20 % (3125886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125886)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125886)Termination reason: Instruction limit
% 10.70/2.20 % (3125886)Termination phase: Saturation
% 10.70/2.20 % (3125886)Time elapsed: 0.132 s
% 10.70/2.20 % (3125886)Peak memory usage: 135 MB
% 10.70/2.20 % (3125886)Instructions burned: 131 (million)
% 10.70/2.20 % (3125892)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=1037417752:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 10.70/2.20 % (3125898)dis+10_1_si=on:random_seed=339940928:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 10.70/2.20 % (3125889)First to succeed.
% 10.70/2.20 % (3125889)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3125812"
% 10.70/2.20 % (3125899)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1939174539:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 10.70/2.20 % (3125900)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2762011910:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 10.70/2.20 % (3125888)Instruction limit reached!
% 10.70/2.20 % (3125888)------------------------------
% 10.70/2.20 % (3125888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125888)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125888)Termination reason: Instruction limit
% 10.70/2.20 % (3125888)Termination phase: Saturation
% 10.70/2.20 % (3125888)Time elapsed: 0.203 s
% 10.70/2.20 % (3125888)Peak memory usage: 92 MB
% 10.70/2.20 % (3125888)Instructions burned: 308 (million)
% 10.70/2.20 % (3125902)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=3692368731:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi)
% 10.70/2.20 % (3125892)Instruction limit reached!
% 10.70/2.20 % (3125892)------------------------------
% 10.70/2.20 % (3125892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125892)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125892)Termination reason: Instruction limit
% 10.70/2.20 % (3125892)Termination phase: Saturation
% 10.70/2.20 % (3125892)Time elapsed: 0.175 s
% 10.70/2.20 % (3125892)Peak memory usage: 118 MB
% 10.70/2.20 % (3125892)Instructions burned: 261 (million)
% 10.70/2.20 % (3125900)Instruction limit reached!
% 10.70/2.20 % (3125900)------------------------------
% 10.70/2.20 % (3125900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125900)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125900)Termination reason: Instruction limit
% 10.70/2.20 % (3125900)Termination phase: Saturation
% 10.70/2.20 % (3125900)Time elapsed: 0.092 s
% 10.70/2.20 % (3125900)Peak memory usage: 90 MB
% 10.70/2.20 % (3125900)Instructions burned: 141 (million)
% 10.70/2.20 % (3125902)Instruction limit reached!
% 10.70/2.20 % (3125902)------------------------------
% 10.70/2.20 % (3125902)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.70/2.20 % (3125902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.70/2.20 % (3125902)CaDiCaL version: 2.1.3
% 10.70/2.20 % (3125902)Termination reason: Instruction limit
% 10.70/2.20 % (3125902)Termination phase: Saturation
% 10.70/2.20 % (3125902)Time elapsed: 0.066 s
% 10.70/2.20 % (3125902)Peak memory usage: 118 MB
% 10.70/2.20 % (3125902)Instructions burned: 66 (million)
% 10.70/2.20 % (3125906)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=158170703:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 10.70/2.20 % (3125889)Refutation found. Thanks to Tanya!
% 10.70/2.20 % SZS status Theorem for theBenchmark
% 10.70/2.20 % SZS output start Proof for theBenchmark
% See solution above
% 11.36/2.29 % (3125889)------------------------------
% 11.36/2.29 % (3125889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.36/2.29 % (3125889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.36/2.29 % (3125889)CaDiCaL version: 2.1.3
% 11.36/2.29 % (3125889)Termination reason: Refutation
% 11.36/2.29 % (3125889)Time elapsed: 0.139 s
% 11.36/2.29 % (3125889)Peak memory usage: 137 MB
% 11.36/2.29 % (3125889)Instructions burned: 128 (million)
% 11.36/2.29 % (3125889)------------------------------
% 11.36/2.29 % (3125889)------------------------------
% 11.36/2.29 % (3125812)Success in time 1.54 s
% 11.36/2.29 % Vampire exiting
%------------------------------------------------------------------------------