%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX108_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 : n006.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 12.51s 2.97s
% Output : Refutation 13.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 26
% Syntax : Number of formulae : 123 ( 5 unt; 0 typ; 24 def)
% Number of atoms : 500 ( 256 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 561 ( 184 ~; 184 |; 158 &)
% ( 23 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 229 ( 0 atm; 88 fun; 66 num; 75 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 : 36 ( 34 usr; 24 prp; 0-4 aty)
% Number of functors : 21 ( 16 usr; 12 con; 0-2 aty)
% Number of variables : 278 ( 178 !; 100 ?; 278 :)
% 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 * general ) > general ).
tff(func_def_9,type,
sK2: ( general * general ) > general ).
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 ).
tff(func_def_13,type,
sK6: 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: $int ).
tff(func_def_19,type,
sK12: $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,
! [X0: general,X2: general,X3: general,X1: general] :
( ( ( ? [X6: general,X7: general] :
( ( X7 = X3 )
& ( X6 = X2 )
& tp(X6,X7) )
& ? [X5: $int,X4: $int] :
( ( X1 = f__integer__($sum(X4,X5)) )
& ( f__integer__(X4) = X3 )
& ( X5 = 1 ) )
& ( X0 = X2 ) )
=> tq(X0,X1) )
& ( ( ( X0 = X2 )
& ? [X4: $int,X5: $int] :
( ( f__integer__(X4) = X3 )
& ( X1 = f__integer__($sum(X4,X5)) )
& ( X5 = 1 ) )
& ? [X6: general,X7: general] :
( hp(X6,X7)
& ( X6 = X2 )
& ( X7 = X3 ) ) )
=> hq(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_left_0) ).
tff(f19,conjecture,
! [X3: general,X1: general,X0: general,X2: general] :
( ( ( ( X1 = X3 )
& ? [X5: general,X4: general] :
( hp(X4,X5)
& ? [X6: $int,X7: $int] :
( ( X5 = f__integer__($difference(X6,X7)) )
& ( X7 = 1 )
& ( f__integer__(X6) = X3 ) )
& ( X4 = X2 ) )
& ( X0 = X2 ) )
=> hq(X0,X1) )
& ( ( ( X0 = X2 )
& ? [X4: general,X5: general] :
( ? [X6: $int,X7: $int] :
( ( X5 = f__integer__($difference(X6,X7)) )
& ( X7 = 1 )
& ( f__integer__(X6) = X3 ) )
& tp(X4,X5)
& ( X4 = X2 ) )
& ( X1 = X3 ) )
=> tq(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_3_right_0) ).
tff(f20,negated_conjecture,
~ ! [X3: general,X1: general,X0: general,X2: general] :
( ( ( ( X1 = X3 )
& ? [X5: general,X4: general] :
( hp(X4,X5)
& ? [X6: $int,X7: $int] :
( ( X5 = f__integer__($difference(X6,X7)) )
& ( X7 = 1 )
& ( f__integer__(X6) = X3 ) )
& ( X4 = X2 ) )
& ( X0 = X2 ) )
=> hq(X0,X1) )
& ( ( ( X0 = X2 )
& ? [X4: general,X5: general] :
( ? [X6: $int,X7: $int] :
( ( X5 = f__integer__($difference(X6,X7)) )
& ( X7 = 1 )
& ( f__integer__(X6) = X3 ) )
& tp(X4,X5)
& ( X4 = X2 ) )
& ( X1 = X3 ) )
=> tq(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f19]) ).
tff(f21,plain,
~ ! [X3: general,X1: general,X0: general,X2: general] :
( ( ( ( X1 = X3 )
& ? [X5: general,X4: general] :
( hp(X4,X5)
& ? [X6: $int,X7: $int] :
( ( f__integer__($sum(X6,$uminus(X7))) = X5 )
& ( X7 = 1 )
& ( f__integer__(X6) = X3 ) )
& ( X4 = X2 ) )
& ( X0 = X2 ) )
=> hq(X0,X1) )
& ( ( ( X0 = X2 )
& ? [X4: general,X5: general] :
( ? [X6: $int,X7: $int] :
( ( f__integer__($sum(X6,$uminus(X7))) = X5 )
& ( X7 = 1 )
& ( f__integer__(X6) = X3 ) )
& tp(X4,X5)
& ( X4 = X2 ) )
& ( X1 = X3 ) )
=> tq(X0,X1) ) ),
inference(theory_normalization,[],[f20]) ).
tff(f23,plain,
~ ! [X2: general,X0: general,X3: general,X1: general] :
( ( ( ? [X5: general,X4: general] :
( ? [X7: $int,X6: $int] :
( ( f__integer__($sum(X6,$uminus(X7))) = X4 )
& ( f__integer__(X6) = X0 )
& ( X7 = 1 ) )
& ( X3 = X5 )
& hp(X5,X4) )
& ( X2 = X3 )
& ( X0 = X1 ) )
=> hq(X2,X1) )
& ( ( ? [X9: general,X8: general] :
( ( X3 = X8 )
& tp(X8,X9)
& ? [X11: $int,X10: $int] :
( ( f__integer__(X10) = X0 )
& ( f__integer__($sum(X10,$uminus(X11))) = X9 )
& ( 1 = X11 ) ) )
& ( X2 = X3 )
& ( X0 = X1 ) )
=> tq(X2,X1) ) ),
inference(rectify,[],[f21]) ).
tff(f24,plain,
! [X1: general,X3: general,X2: general,X0: general] :
( ( ( ( X0 = X1 )
& ? [X5: general,X4: general] :
( ( X1 = X4 )
& ( X2 = X5 )
& tp(X4,X5) )
& ? [X6: $int,X7: $int] :
( ( 1 = X6 )
& ( f__integer__($sum(X7,X6)) = X3 )
& ( f__integer__(X7) = X2 ) ) )
=> tq(X0,X3) )
& ( ( ? [X10: general,X11: general] :
( hp(X10,X11)
& ( X2 = X11 )
& ( X1 = X10 ) )
& ( X0 = X1 )
& ? [X8: $int,X9: $int] :
( ( 1 = X9 )
& ( f__integer__($sum(X8,X9)) = X3 )
& ( f__integer__(X8) = X2 ) ) )
=> hq(X0,X3) ) ),
inference(rectify,[],[f18]) ).
tff(f27,plain,
! [X1: general,X3: general,X2: general,X0: general] :
( ( tq(X0,X3)
| ( X0 != X1 )
| ! [X4: general,X5: general] :
( ( X2 != X5 )
| ( X1 != X4 )
| ~ tp(X4,X5) )
| ! [X6: $int,X7: $int] :
( ( 1 != X6 )
| ( f__integer__(X7) != X2 )
| ( f__integer__($sum(X7,X6)) != X3 ) ) )
& ( hq(X0,X3)
| ! [X11: general,X10: general] :
( ( X1 != X10 )
| ( X2 != X11 )
| ~ hp(X10,X11) )
| ( X0 != X1 )
| ! [X8: $int,X9: $int] :
( ( f__integer__(X8) != X2 )
| ( f__integer__($sum(X8,X9)) != X3 )
| ( 1 != X9 ) ) ) ),
inference(ennf_transformation,[],[f24]) ).
tff(f28,plain,
! [X0: general,X3: general,X1: general,X2: general] :
( ( ( X0 != X1 )
| ! [X11: general,X10: general] :
( ( X1 != X10 )
| ( X2 != X11 )
| ~ hp(X10,X11) )
| hq(X0,X3)
| ! [X8: $int,X9: $int] :
( ( f__integer__(X8) != X2 )
| ( f__integer__($sum(X8,X9)) != X3 )
| ( 1 != X9 ) ) )
& ( ! [X6: $int,X7: $int] :
( ( 1 != X6 )
| ( f__integer__(X7) != X2 )
| ( f__integer__($sum(X7,X6)) != X3 ) )
| tq(X0,X3)
| ( X0 != X1 )
| ! [X4: general,X5: general] :
( ( X2 != X5 )
| ( X1 != X4 )
| ~ tp(X4,X5) ) ) ),
inference(flattening,[],[f27]) ).
tff(f29,plain,
? [X2: general,X0: general,X3: general,X1: general] :
( ( ~ hq(X2,X1)
& ? [X5: general,X4: general] :
( ? [X7: $int,X6: $int] :
( ( f__integer__($sum(X6,$uminus(X7))) = X4 )
& ( f__integer__(X6) = X0 )
& ( X7 = 1 ) )
& ( X3 = X5 )
& hp(X5,X4) )
& ( X2 = X3 )
& ( X0 = X1 ) )
| ( ~ tq(X2,X1)
& ? [X9: general,X8: general] :
( ( X3 = X8 )
& tp(X8,X9)
& ? [X11: $int,X10: $int] :
( ( f__integer__(X10) = X0 )
& ( f__integer__($sum(X10,$uminus(X11))) = X9 )
& ( 1 = X11 ) ) )
& ( X2 = X3 )
& ( X0 = X1 ) ) ),
inference(ennf_transformation,[],[f23]) ).
tff(f30,plain,
? [X1: general,X0: general,X3: general,X2: general] :
( ( ( X0 = X1 )
& ( X2 = X3 )
& ? [X5: general,X4: general] :
( ? [X7: $int,X6: $int] :
( ( f__integer__($sum(X6,$uminus(X7))) = X4 )
& ( f__integer__(X6) = X0 )
& ( X7 = 1 ) )
& ( X3 = X5 )
& hp(X5,X4) )
& ~ hq(X2,X1) )
| ( ~ tq(X2,X1)
& ( X2 = X3 )
& ( X0 = X1 )
& ? [X9: general,X8: general] :
( ( X3 = X8 )
& tp(X8,X9)
& ? [X11: $int,X10: $int] :
( ( f__integer__(X10) = X0 )
& ( f__integer__($sum(X10,$uminus(X11))) = X9 )
& ( 1 = X11 ) ) ) ) ),
inference(flattening,[],[f29]) ).
tff(f31,definition,
! [X1: general,X2: general,X3: general,X0: general] :
( ( ~ tq(X2,X1)
& ( X2 = X3 )
& ( X0 = X1 )
& ? [X9: general,X8: general] :
( ( X3 = X8 )
& tp(X8,X9)
& ? [X11: $int,X10: $int] :
( ( f__integer__(X10) = X0 )
& ( f__integer__($sum(X10,$uminus(X11))) = X9 )
& ( 1 = X11 ) ) ) )
| ~ sP0(X1,X2,X3,X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f32,plain,
? [X1: general,X0: general,X3: general,X2: general] :
( ( ( X0 = X1 )
& ( X2 = X3 )
& ? [X5: general,X4: general] :
( ? [X7: $int,X6: $int] :
( ( f__integer__($sum(X6,$uminus(X7))) = X4 )
& ( f__integer__(X6) = X0 )
& ( X7 = 1 ) )
& ( X3 = X5 )
& hp(X5,X4) )
& ~ hq(X2,X1) )
| sP0(X1,X2,X3,X0) ),
inference(definition_folding,[],[f30,f31]) ).
tff(f34,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ( X0 != X2 )
| ! [X4: general,X5: general] :
( ( X2 != X5 )
| ( X3 != X4 )
| ~ hp(X5,X4) )
| hq(X0,X1)
| ! [X6: $int,X7: $int] :
( ( f__integer__(X6) != X3 )
| ( f__integer__($sum(X6,X7)) != X1 )
| ( 1 != X7 ) ) )
& ( ! [X8: $int,X9: $int] :
( ( 1 != X8 )
| ( f__integer__(X9) != X3 )
| ( f__integer__($sum(X9,X8)) != X1 ) )
| tq(X0,X1)
| ( X0 != X2 )
| ! [X10: general,X11: general] :
( ( X3 != X11 )
| ( X2 != X10 )
| ~ tp(X10,X11) ) ) ),
inference(rectify,[],[f28]) ).
tff(f35,plain,
! [X1: general,X2: general,X3: general,X0: general] :
( ( ~ tq(X2,X1)
& ( X2 = X3 )
& ( X0 = X1 )
& ? [X9: general,X8: general] :
( ( X3 = X8 )
& tp(X8,X9)
& ? [X11: $int,X10: $int] :
( ( f__integer__(X10) = X0 )
& ( f__integer__($sum(X10,$uminus(X11))) = X9 )
& ( 1 = X11 ) ) ) )
| ~ sP0(X1,X2,X3,X0) ),
inference(nnf_transformation,[],[f31]) ).
tff(f36,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ~ tq(X1,X0)
& ( X1 = X2 )
& ( X0 = X3 )
& ? [X4: general,X5: general] :
( ( X2 = X5 )
& tp(X5,X4)
& ? [X6: $int,X7: $int] :
( ( f__integer__(X7) = X3 )
& ( f__integer__($sum(X7,$uminus(X6))) = X4 )
& ( 1 = X6 ) ) ) )
| ~ sP0(X0,X1,X2,X3) ),
inference(rectify,[],[f35]) ).
tff(f37,plain,
! [X0: general,X1: general,X2: general,X3: general] :
( ( ~ tq(X1,X0)
& ( X1 = X2 )
& ( X0 = X3 )
& ( sK2(X2,X3) = X2 )
& tp(sK2(X2,X3),sK1(X2,X3))
& ( f__integer__(sK4(X2,X3)) = X3 )
& ( sK1(X2,X3) = f__integer__($sum(sK4(X2,X3),$uminus(sK3(X2,X3)))) )
& ( 1 = sK3(X2,X3) ) )
| ~ sP0(X0,X1,X2,X3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4]),skolemize(X4,sK1(X2,X3)),skolemize(X5,sK2(X2,X3)),skolemize(X6,sK3(X2,X3)),skolemize(X7,sK4(X2,X3))],[f36]) ).
tff(f38,plain,
? [X0: general,X1: general,X2: general,X3: general] :
( ( ( X0 = X1 )
& ( X2 = X3 )
& ? [X4: general,X5: general] :
( ? [X6: $int,X7: $int] :
( ( f__integer__($sum(X7,$uminus(X6))) = X5 )
& ( f__integer__(X7) = X1 )
& ( 1 = X6 ) )
& ( X2 = X4 )
& hp(X4,X5) )
& ~ hq(X3,X0) )
| sP0(X0,X3,X2,X1) ),
inference(rectify,[],[f32]) ).
tff(f39,plain,
( ( ( sK6 = sK5 )
& ( sK7 = sK8 )
& ( f__integer__($sum(sK12,$uminus(sK11))) = sK10 )
& ( sK6 = f__integer__(sK12) )
& ( 1 = sK11 )
& ( sK7 = sK9 )
& hp(sK9,sK10)
& ~ hq(sK8,sK5) )
| sP0(sK5,sK8,sK7,sK6) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12]),skolemize(X0,sK5),skolemize(X1,sK6),skolemize(X2,sK7),skolemize(X3,sK8),skolemize(X4,sK9),skolemize(X5,sK10),skolemize(X6,sK11),skolemize(X7,sK12)],[f38]) ).
tff(f44,plain,
! [X2: general,X3: general,X10: general,X0: general,X11: general,X1: general,X8: $int,X9: $int] :
( ( 1 != X8 )
| ( f__integer__(X9) != X3 )
| ( f__integer__($sum(X9,X8)) != X1 )
| tq(X0,X1)
| ( X0 != X2 )
| ( X3 != X11 )
| ( X2 != X10 )
| ~ tp(X10,X11) ),
inference(cnf_transformation,[],[f34]) ).
tff(f45,plain,
! [X2: general,X3: general,X0: general,X1: general,X6: $int,X7: $int,X4: general,X5: general] :
( ( X0 != X2 )
| ( X2 != X5 )
| ( X3 != X4 )
| ~ hp(X5,X4)
| hq(X0,X1)
| ( f__integer__(X6) != X3 )
| ( f__integer__($sum(X6,X7)) != X1 )
| ( 1 != X7 ) ),
inference(cnf_transformation,[],[f34]) ).
tff(f46,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( 1 = sK3(X2,X3) ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f47,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( sK1(X2,X3) = f__integer__($sum(sK4(X2,X3),$uminus(sK3(X2,X3)))) )
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f37]) ).
tff(f48,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ( f__integer__(sK4(X2,X3)) = X3 )
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f37]) ).
tff(f49,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( tp(sK2(X2,X3),sK1(X2,X3))
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f37]) ).
tff(f50,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( sK2(X2,X3) = X2 ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f51,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( X0 = X3 ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f52,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ( X1 = X2 ) ),
inference(cnf_transformation,[],[f37]) ).
tff(f53,plain,
! [X2: general,X3: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2,X3)
| ~ tq(X1,X0) ),
inference(cnf_transformation,[],[f37]) ).
tff(f54,plain,
( ~ hq(sK8,sK5)
| sP0(sK5,sK8,sK7,sK6) ),
inference(cnf_transformation,[],[f39]) ).
tff(f55,plain,
( sP0(sK5,sK8,sK7,sK6)
| hp(sK9,sK10) ),
inference(cnf_transformation,[],[f39]) ).
tff(f56,plain,
( sP0(sK5,sK8,sK7,sK6)
| ( sK7 = sK9 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f57,plain,
( ( 1 = sK11 )
| sP0(sK5,sK8,sK7,sK6) ),
inference(cnf_transformation,[],[f39]) ).
tff(f58,plain,
( sP0(sK5,sK8,sK7,sK6)
| ( sK6 = f__integer__(sK12) ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f59,plain,
( ( f__integer__($sum(sK12,$uminus(sK11))) = sK10 )
| sP0(sK5,sK8,sK7,sK6) ),
inference(cnf_transformation,[],[f39]) ).
tff(f60,plain,
( sP0(sK5,sK8,sK7,sK6)
| ( sK7 = sK8 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f61,plain,
( sP0(sK5,sK8,sK7,sK6)
| ( sK6 = sK5 ) ),
inference(cnf_transformation,[],[f39]) ).
tff(f64,plain,
! [X2: general,X3: general,X1: general,X6: $int,X7: $int,X4: general,X5: general] :
( ( X2 != X5 )
| ( X3 != X4 )
| ~ hp(X5,X4)
| hq(X2,X1)
| ( f__integer__(X6) != X3 )
| ( f__integer__($sum(X6,X7)) != X1 )
| ( 1 != X7 ) ),
inference(equality_resolution,[],[f45]) ).
tff(f65,plain,
! [X3: general,X1: general,X6: $int,X7: $int,X4: general,X5: general] :
( ( X3 != X4 )
| ~ hp(X5,X4)
| hq(X5,X1)
| ( f__integer__(X6) != X3 )
| ( f__integer__($sum(X6,X7)) != X1 )
| ( 1 != X7 ) ),
inference(equality_resolution,[],[f64]) ).
tff(f66,plain,
! [X1: general,X6: $int,X7: $int,X4: general,X5: general] :
( ~ hp(X5,X4)
| hq(X5,X1)
| ( f__integer__(X6) != X4 )
| ( f__integer__($sum(X6,X7)) != X1 )
| ( 1 != X7 ) ),
inference(equality_resolution,[],[f65]) ).
tff(f67,plain,
! [X1: general,X6: $int,X7: $int,X5: general] :
( ~ hp(X5,f__integer__(X6))
| hq(X5,X1)
| ( f__integer__($sum(X6,X7)) != X1 )
| ( 1 != X7 ) ),
inference(equality_resolution,[],[f66]) ).
tff(f68,plain,
! [X6: $int,X7: $int,X5: general] :
( ~ hp(X5,f__integer__(X6))
| hq(X5,f__integer__($sum(X6,X7)))
| ( 1 != X7 ) ),
inference(equality_resolution,[],[f67]) ).
tff(f69,plain,
! [X6: $int,X5: general] :
( hq(X5,f__integer__($sum(X6,1)))
| ~ hp(X5,f__integer__(X6)) ),
inference(equality_resolution,[],[f68]) ).
tff(f70,plain,
! [X2: general,X3: general,X10: general,X0: general,X11: general,X1: general,X9: $int] :
( ( f__integer__(X9) != X3 )
| ( f__integer__($sum(X9,1)) != X1 )
| tq(X0,X1)
| ( X0 != X2 )
| ( X3 != X11 )
| ( X2 != X10 )
| ~ tp(X10,X11) ),
inference(equality_resolution,[],[f44]) ).
tff(f71,plain,
! [X2: general,X10: general,X0: general,X11: general,X1: general,X9: $int] :
( ( f__integer__($sum(X9,1)) != X1 )
| tq(X0,X1)
| ( X0 != X2 )
| ( f__integer__(X9) != X11 )
| ( X2 != X10 )
| ~ tp(X10,X11) ),
inference(equality_resolution,[],[f70]) ).
tff(f72,plain,
! [X2: general,X10: general,X0: general,X11: general,X9: $int] :
( tq(X0,f__integer__($sum(X9,1)))
| ( X0 != X2 )
| ( f__integer__(X9) != X11 )
| ( X2 != X10 )
| ~ tp(X10,X11) ),
inference(equality_resolution,[],[f71]) ).
tff(f73,plain,
! [X2: general,X10: general,X11: general,X9: $int] :
( tq(X2,f__integer__($sum(X9,1)))
| ( f__integer__(X9) != X11 )
| ( X2 != X10 )
| ~ tp(X10,X11) ),
inference(equality_resolution,[],[f72]) ).
tff(f74,plain,
! [X2: general,X10: general,X9: $int] :
( tq(X2,f__integer__($sum(X9,1)))
| ( X2 != X10 )
| ~ tp(X10,f__integer__(X9)) ),
inference(equality_resolution,[],[f73]) ).
tff(f75,plain,
! [X10: general,X9: $int] :
( tq(X10,f__integer__($sum(X9,1)))
| ~ tp(X10,f__integer__(X9)) ),
inference(equality_resolution,[],[f74]) ).
tff(f78,definition,
( spl13_1
<=> sP0(sK5,sK8,sK7,sK6) ),
introduced(definition,[new_symbols(definition,[spl13_1])],[avatar_definition]) ).
tff(f80,plain,
( sP0(sK5,sK8,sK7,sK6)
| ~ spl13_1 ),
inference(avatar_component_clause,[],[f78]) ).
tff(f82,definition,
( spl13_2
<=> ( 1 = sK11 ) ),
introduced(definition,[new_symbols(definition,[spl13_2])],[avatar_definition]) ).
tff(f84,plain,
( ( 1 = sK11 )
| ~ spl13_2 ),
inference(avatar_component_clause,[],[f82]) ).
tff(f85,plain,
( spl13_1
| spl13_2 ),
inference(avatar_split_clause,[],[f57,f82,f78]) ).
tff(f87,definition,
( spl13_3
<=> hq(sK8,sK5) ),
introduced(definition,[new_symbols(definition,[spl13_3])],[avatar_definition]) ).
tff(f90,plain,
( ~ spl13_3
| spl13_1 ),
inference(avatar_split_clause,[],[f54,f78,f87]) ).
tff(f92,definition,
( spl13_4
<=> hp(sK9,sK10) ),
introduced(definition,[new_symbols(definition,[spl13_4])],[avatar_definition]) ).
tff(f94,plain,
( hp(sK9,sK10)
| ~ spl13_4 ),
inference(avatar_component_clause,[],[f92]) ).
tff(f95,plain,
( spl13_4
| spl13_1 ),
inference(avatar_split_clause,[],[f55,f78,f92]) ).
tff(f96,plain,
sK7 = sK8,
inference(forward_subsumption_resolution,[],[f60,f52]) ).
tff(f98,definition,
( spl13_5
<=> ( sK7 = sK9 ) ),
introduced(definition,[new_symbols(definition,[spl13_5])],[avatar_definition]) ).
tff(f100,plain,
( ( sK7 = sK9 )
| ~ spl13_5 ),
inference(avatar_component_clause,[],[f98]) ).
tff(f101,plain,
( spl13_1
| spl13_5 ),
inference(avatar_split_clause,[],[f56,f98,f78]) ).
tff(f103,definition,
( spl13_6
<=> ( sK6 = f__integer__(sK12) ) ),
introduced(definition,[new_symbols(definition,[spl13_6])],[avatar_definition]) ).
tff(f106,plain,
( spl13_6
| spl13_1 ),
inference(avatar_split_clause,[],[f58,f78,f103]) ).
tff(f108,definition,
( spl13_7
<=> ( f__integer__($sum(sK12,$uminus(sK11))) = sK10 ) ),
introduced(definition,[new_symbols(definition,[spl13_7])],[avatar_definition]) ).
tff(f110,plain,
( ( f__integer__($sum(sK12,$uminus(sK11))) = sK10 )
| ~ spl13_7 ),
inference(avatar_component_clause,[],[f108]) ).
tff(f111,plain,
( spl13_7
| spl13_1 ),
inference(avatar_split_clause,[],[f59,f78,f108]) ).
tff(f112,plain,
sK6 = sK5,
inference(forward_subsumption_resolution,[],[f61,f51]) ).
tff(f114,definition,
( spl13_8
<=> ( sK7 = sK8 ) ),
introduced(definition,[new_symbols(definition,[spl13_8])],[avatar_definition]) ).
tff(f116,plain,
( ( sK7 = sK8 )
| ~ spl13_8 ),
inference(avatar_component_clause,[],[f114]) ).
tff(f117,plain,
spl13_8,
inference(avatar_split_clause,[],[f96,f114]) ).
tff(f119,definition,
( spl13_9
<=> ( sK6 = sK5 ) ),
introduced(definition,[new_symbols(definition,[spl13_9])],[avatar_definition]) ).
tff(f121,plain,
( ( sK6 = sK5 )
| ~ spl13_9 ),
inference(avatar_component_clause,[],[f119]) ).
tff(f122,plain,
spl13_9,
inference(avatar_split_clause,[],[f112,f119]) ).
tff(f123,plain,
( sP0(sK6,sK8,sK7,sK6)
| ~ spl13_1
| ~ spl13_9 ),
inference(forward_demodulation,[],[f80,f121]) ).
tff(f124,plain,
( sP0(sK6,sK8,sK8,sK6)
| ~ spl13_1
| ~ spl13_8
| ~ spl13_9 ),
inference(forward_demodulation,[],[f123,f116]) ).
tff(f126,definition,
( spl13_10
<=> sP0(sK6,sK8,sK8,sK6) ),
introduced(definition,[new_symbols(definition,[spl13_10])],[avatar_definition]) ).
tff(f128,plain,
( sP0(sK6,sK8,sK8,sK6)
| ~ spl13_10 ),
inference(avatar_component_clause,[],[f126]) ).
tff(f129,plain,
( spl13_10
| ~ spl13_1
| ~ spl13_8
| ~ spl13_9 ),
inference(avatar_split_clause,[],[f124,f119,f114,f78,f126]) ).
tff(f131,plain,
( ( f__integer__($sum(sK4(sK8,sK6),$uminus(sK3(sK8,sK6)))) = sK1(sK8,sK6) )
| ~ spl13_10 ),
inference(unit_resulting_resolution,[],[f47,f128]) ).
tff(f132,plain,
( ( sK6 = f__integer__(sK4(sK8,sK6)) )
| ~ spl13_10 ),
inference(unit_resulting_resolution,[],[f48,f128]) ).
tff(f133,plain,
( tp(sK2(sK8,sK6),sK1(sK8,sK6))
| ~ spl13_10 ),
inference(unit_resulting_resolution,[],[f49,f128]) ).
tff(f140,plain,
( ( 1 = sK3(sK8,sK6) )
| ~ spl13_10 ),
inference(resolution,[],[f128,f46]) ).
tff(f141,plain,
( ( sK2(sK8,sK6) = sK8 )
| ~ spl13_10 ),
inference(resolution,[],[f128,f50]) ).
tff(f142,plain,
( ~ tq(sK8,sK6)
| ~ spl13_10 ),
inference(resolution,[],[f128,f53]) ).
tff(f144,definition,
( spl13_11
<=> ( 1 = sK3(sK8,sK6) ) ),
introduced(definition,[new_symbols(definition,[spl13_11])],[avatar_definition]) ).
tff(f147,plain,
( spl13_11
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f140,f126,f144]) ).
tff(f149,definition,
( spl13_12
<=> tq(sK8,sK6) ),
introduced(definition,[new_symbols(definition,[spl13_12])],[avatar_definition]) ).
tff(f152,plain,
( ~ spl13_12
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f142,f126,f149]) ).
tff(f154,definition,
( spl13_13
<=> ( sK2(sK8,sK6) = sK8 ) ),
introduced(definition,[new_symbols(definition,[spl13_13])],[avatar_definition]) ).
tff(f157,plain,
( spl13_13
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f141,f126,f154]) ).
tff(f159,definition,
( spl13_14
<=> ( sK6 = f__integer__(sK4(sK8,sK6)) ) ),
introduced(definition,[new_symbols(definition,[spl13_14])],[avatar_definition]) ).
tff(f162,plain,
( spl13_14
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f132,f126,f159]) ).
tff(f164,definition,
( spl13_15
<=> tp(sK2(sK8,sK6),sK1(sK8,sK6)) ),
introduced(definition,[new_symbols(definition,[spl13_15])],[avatar_definition]) ).
tff(f167,plain,
( spl13_15
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f133,f126,f164]) ).
tff(f169,definition,
( spl13_16
<=> ( f__integer__($sum(sK4(sK8,sK6),$uminus(sK3(sK8,sK6)))) = sK1(sK8,sK6) ) ),
introduced(definition,[new_symbols(definition,[spl13_16])],[avatar_definition]) ).
tff(f172,plain,
( spl13_16
| ~ spl13_10 ),
inference(avatar_split_clause,[],[f131,f126,f169]) ).
tff(f193,definition,
( spl13_20
<=> tp(sK8,f__integer__($sum(sK4(sK8,sK6),-1))) ),
introduced(definition,[new_symbols(definition,[spl13_20])],[avatar_definition]) ).
tff(f195,plain,
( tp(sK8,f__integer__($sum(sK4(sK8,sK6),-1)))
| ~ spl13_20 ),
inference(avatar_component_clause,[],[f193]) ).
tff(f211,plain,
( tq(sK8,f__integer__($sum($sum(sK4(sK8,sK6),-1),1)))
| ~ spl13_20 ),
inference(unit_resulting_resolution,[],[f75,f195]) ).
tff(f213,definition,
( spl13_21
<=> tq(sK8,f__integer__($sum($sum(sK4(sK8,sK6),-1),1))) ),
introduced(definition,[new_symbols(definition,[spl13_21])],[avatar_definition]) ).
tff(f216,plain,
( spl13_21
| ~ spl13_20 ),
inference(avatar_split_clause,[],[f211,f193,f213]) ).
tff(f218,plain,
( ( sK9 = sK8 )
| ~ spl13_5
| ~ spl13_8 ),
inference(forward_demodulation,[],[f100,f116]) ).
tff(f221,definition,
( spl13_22
<=> ( sK9 = sK8 ) ),
introduced(definition,[new_symbols(definition,[spl13_22])],[avatar_definition]) ).
tff(f223,plain,
( ( sK9 = sK8 )
| ~ spl13_22 ),
inference(avatar_component_clause,[],[f221]) ).
tff(f224,plain,
( spl13_22
| ~ spl13_5
| ~ spl13_8 ),
inference(avatar_split_clause,[],[f218,f114,f98,f221]) ).
tff(f233,plain,
( hp(sK8,sK10)
| ~ spl13_4
| ~ spl13_22 ),
inference(superposition,[],[f94,f223]) ).
tff(f235,definition,
( spl13_24
<=> hp(sK8,sK10) ),
introduced(definition,[new_symbols(definition,[spl13_24])],[avatar_definition]) ).
tff(f237,plain,
( hp(sK8,sK10)
| ~ spl13_24 ),
inference(avatar_component_clause,[],[f235]) ).
tff(f238,plain,
( spl13_24
| ~ spl13_4
| ~ spl13_22 ),
inference(avatar_split_clause,[],[f233,f221,f92,f235]) ).
tff(f248,plain,
( ( f__integer__($sum(sK12,$uminus(1))) = sK10 )
| ~ spl13_2
| ~ spl13_7 ),
inference(superposition,[],[f110,f84]) ).
tff(f251,plain,
( ( f__integer__($sum(sK12,-1)) = sK10 )
| ~ spl13_2
| ~ spl13_7 ),
inference(evaluation,[],[f248]) ).
tff(f255,definition,
( spl13_25
<=> ( f__integer__($sum(sK12,-1)) = sK10 ) ),
introduced(definition,[new_symbols(definition,[spl13_25])],[avatar_definition]) ).
tff(f257,plain,
( ( f__integer__($sum(sK12,-1)) = sK10 )
| ~ spl13_25 ),
inference(avatar_component_clause,[],[f255]) ).
tff(f258,plain,
( spl13_25
| ~ spl13_2
| ~ spl13_7 ),
inference(avatar_split_clause,[],[f251,f108,f82,f255]) ).
tff(f261,plain,
( hp(sK8,f__integer__($sum(sK12,-1)))
| ~ spl13_24
| ~ spl13_25 ),
inference(superposition,[],[f237,f257]) ).
tff(f266,definition,
( spl13_26
<=> hp(sK8,f__integer__($sum(sK12,-1))) ),
introduced(definition,[new_symbols(definition,[spl13_26])],[avatar_definition]) ).
tff(f268,plain,
( hp(sK8,f__integer__($sum(sK12,-1)))
| ~ spl13_26 ),
inference(avatar_component_clause,[],[f266]) ).
tff(f269,plain,
( spl13_26
| ~ spl13_24
| ~ spl13_25 ),
inference(avatar_split_clause,[],[f261,f255,f235,f266]) ).
tff(f276,plain,
( hq(sK8,f__integer__($sum($sum(sK12,-1),1)))
| ~ spl13_26 ),
inference(unit_resulting_resolution,[],[f69,f268]) ).
tff(f279,definition,
( spl13_28
<=> hq(sK8,f__integer__($sum($sum(sK12,-1),1))) ),
introduced(definition,[new_symbols(definition,[spl13_28])],[avatar_definition]) ).
tff(f282,plain,
( spl13_28
| ~ spl13_26 ),
inference(avatar_split_clause,[],[f276,f266,f279]) ).
tff(f283,plain,
$false,
inference(avatar_smt_refutation,[],[f282,f269,f258,f238,f224,f216,f172,f167,f162,f157,f152,f147,f129,f122,f117,f111,f106,f101,f95,f90,f85]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX108_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.08/0.22 % Computer : n006.cluster.edu
% 0.08/0.22 % Model : x86_64 x86_64
% 0.08/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.22 % Memory : 8046.5625MB
% 0.08/0.22 % OS : Linux 6.8.0-71-generic
% 0.08/0.22 % CPULimit : 300
% 0.08/0.22 % WCLimit : 300
% 0.08/0.22 % DateTime : Mon Sep 28 15:01:10 UTC 2026
% 0.08/0.23 % CPUTime :
% 0.08/0.23 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.24/0.28 Running first-order theorem proving
% 0.24/0.28 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
% 5.33/1.71 % (4031110)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.33/1.71 % (4031116)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1721823310:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.33/1.71 % (4031121)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2768491116:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.33/1.71 % (4031119)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=29944553:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.33/1.71 % (4031118)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2254259208:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.33/1.71 % (4031117)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=724350617:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.33/1.71 % (4031120)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1470277061:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.33/1.71 % (4031115)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3437229878:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.33/1.71 % (4031119)Instruction limit reached!
% 5.33/1.71 % (4031119)------------------------------
% 5.33/1.71 % (4031119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.71 % (4031119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.71 % (4031119)CaDiCaL version: 2.1.3
% 5.33/1.71 % (4031119)Termination reason: Instruction limit
% 5.33/1.71 % (4031119)Termination phase: Saturation
% 5.33/1.71 % (4031119)Time elapsed: 0.006 s
% 5.33/1.71 % (4031119)Peak memory usage: 89 MB
% 5.33/1.71 % (4031119)Instructions burned: 4 (million)
% 5.33/1.71 % (4031118)Instruction limit reached!
% 5.33/1.71 % (4031118)------------------------------
% 5.33/1.71 % (4031118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.71 % (4031118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.71 % (4031118)CaDiCaL version: 2.1.3
% 5.33/1.71 % (4031118)Termination reason: Instruction limit
% 5.33/1.71 % (4031118)Termination phase: Saturation
% 5.33/1.71 % (4031118)Time elapsed: 0.010 s
% 5.33/1.71 % (4031118)Peak memory usage: 88 MB
% 5.33/1.71 % (4031118)Instructions burned: 8 (million)
% 5.33/1.71 % (4031121)Instruction limit reached!
% 5.33/1.71 % (4031121)------------------------------
% 5.33/1.71 % (4031121)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.71 % (4031121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.71 % (4031121)CaDiCaL version: 2.1.3
% 5.33/1.71 % (4031121)Termination reason: Instruction limit
% 5.33/1.71 % (4031121)Termination phase: Saturation
% 5.33/1.71 % (4031121)Time elapsed: 0.069 s
% 5.33/1.71 % (4031121)Peak memory usage: 116 MB
% 5.33/1.71 % (4031121)Instructions burned: 33 (million)
% 5.33/1.71 % (4031115)Instruction limit reached!
% 5.33/1.71 % (4031115)------------------------------
% 5.33/1.71 % (4031115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.71 % (4031115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.71 % (4031115)CaDiCaL version: 2.1.3
% 5.33/1.72 % (4031115)Termination reason: Instruction limit
% 5.33/1.72 % (4031115)Termination phase: Saturation
% 5.33/1.72 % (4031115)Time elapsed: 0.043 s
% 5.33/1.72 % (4031115)Peak memory usage: 115 MB
% 5.33/1.72 % (4031115)Instructions burned: 12 (million)
% 5.33/1.72 % (4031116)Instruction limit reached!
% 5.33/1.72 % (4031116)------------------------------
% 5.33/1.72 % (4031116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.72 % (4031116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.33/1.72 % (4031116)CaDiCaL version: 2.1.3
% 5.33/1.72 % (4031116)Termination reason: Instruction limit
% 5.33/1.72 % (4031116)Termination phase: Saturation
% 5.33/1.72 % (4031116)Time elapsed: 0.153 s
% 5.33/1.72 % (4031116)Peak memory usage: 117 MB
% 5.33/1.72 % (4031116)Instructions burned: 309 (million)
% 5.33/1.72 % (4031120)Instruction limit reached!
% 5.33/1.72 % (4031120)------------------------------
% 5.33/1.72 % (4031120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.33/1.72 % (4031120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.96 % (4031120)CaDiCaL version: 2.1.3
% 6.88/1.96 % (4031120)Termination reason: Instruction limit
% 6.88/1.96 % (4031120)Termination phase: Saturation
% 6.88/1.96 % (4031120)Time elapsed: 0.085 s
% 6.88/1.96 % (4031120)Peak memory usage: 116 MB
% 6.88/1.96 % (4031120)Instructions burned: 46 (million)
% 6.88/1.96 % (4031117)Instruction limit reached!
% 6.88/1.96 % (4031117)------------------------------
% 6.88/1.96 % (4031117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.96 % (4031117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.96 % (4031117)CaDiCaL version: 2.1.3
% 6.88/1.96 % (4031117)Termination reason: Instruction limit
% 6.88/1.96 % (4031117)Termination phase: Saturation
% 6.88/1.96 % (4031117)Time elapsed: 0.170 s
% 6.88/1.96 % (4031117)Peak memory usage: 113 MB
% 6.88/1.96 % (4031117)Instructions burned: 202 (million)
% 6.88/1.96 % (4031129)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3800636844:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2997 on theBenchmark for (2997ds/14Mi)
% 6.88/1.96 % (4031133)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=262978520:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.88/1.96 % (4031132)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1059269429:i=24:canc=force:rtra=on_2996 on theBenchmark for (2996ds/24Mi)
% 6.88/1.96 % (4031129)Instruction limit reached!
% 6.88/1.96 % (4031129)------------------------------
% 6.88/1.96 % (4031129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.96 % (4031129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.96 % (4031129)CaDiCaL version: 2.1.3
% 6.88/1.96 % (4031129)Termination reason: Instruction limit
% 6.88/1.96 % (4031129)Termination phase: Saturation
% 6.88/1.96 % (4031129)Time elapsed: 0.018 s
% 6.88/1.96 % (4031129)Peak memory usage: 88 MB
% 6.88/1.96 % (4031129)Instructions burned: 14 (million)
% 6.88/1.96 % (4031131)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=123680460:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/16Mi)
% 6.88/1.96 % (4031130)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=3674133389:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 6.88/1.96 % (4031133)Instruction limit reached!
% 6.88/1.96 % (4031133)------------------------------
% 6.88/1.96 % (4031133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.96 % (4031133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.96 % (4031133)CaDiCaL version: 2.1.3
% 6.88/1.96 % (4031133)Termination reason: Instruction limit
% 6.88/1.96 % (4031133)Termination phase: Saturation
% 6.88/1.96 % (4031133)Time elapsed: 0.017 s
% 6.88/1.96 % (4031133)Peak memory usage: 89 MB
% 6.88/1.96 % (4031133)Instructions burned: 27 (million)
% 6.88/1.96 % (4031131)Instruction limit reached!
% 6.88/1.96 % (4031131)------------------------------
% 6.88/1.96 % (4031131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.96 % (4031131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.96 % (4031131)CaDiCaL version: 2.1.3
% 6.88/1.96 % (4031131)Termination reason: Instruction limit
% 6.88/1.96 % (4031131)Termination phase: Saturation
% 6.88/1.96 % (4031131)Time elapsed: 0.020 s
% 6.88/1.96 % (4031131)Peak memory usage: 90 MB
% 6.88/1.96 % (4031131)Instructions burned: 18 (million)
% 6.88/1.96 % (4031132)Instruction limit reached!
% 6.88/1.96 % (4031132)------------------------------
% 6.88/1.96 % (4031132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.96 % (4031132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.88/1.96 % (4031132)CaDiCaL version: 2.1.3
% 6.88/1.96 % (4031132)Termination reason: Instruction limit
% 6.88/1.96 % (4031132)Termination phase: Saturation
% 6.88/1.96 % (4031132)Time elapsed: 0.026 s
% 6.88/1.96 % (4031132)Peak memory usage: 89 MB
% 6.88/1.96 % (4031132)Instructions burned: 24 (million)
% 6.88/1.96 % (4031130)Instruction limit reached!
% 6.88/1.96 % (4031130)------------------------------
% 6.88/1.96 % (4031130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.88/1.96 % (4031130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.55/2.25 % (4031130)CaDiCaL version: 2.1.3
% 9.55/2.25 % (4031130)Termination reason: Instruction limit
% 9.55/2.25 % (4031130)Termination phase: Saturation
% 9.55/2.25 % (4031130)Time elapsed: 0.033 s
% 9.55/2.25 % (4031130)Peak memory usage: 89 MB
% 9.55/2.25 % (4031130)Instructions burned: 29 (million)
% 9.55/2.25 % (4031134)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3969494789:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 9.55/2.25 % (4031136)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=285227222:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2995 on theBenchmark for (2995ds/2Mi)
% 9.55/2.25 % (4031136)Instruction limit reached!
% 9.55/2.25 % (4031136)------------------------------
% 9.55/2.25 % (4031136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.55/2.25 % (4031136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.55/2.25 % (4031136)CaDiCaL version: 2.1.3
% 9.55/2.25 % (4031136)Termination reason: Instruction limit
% 9.55/2.25 % (4031136)Termination phase: Saturation
% 9.55/2.25 % (4031136)Time elapsed: 0.003 s
% 9.55/2.25 % (4031136)Peak memory usage: 87 MB
% 9.55/2.25 % (4031136)Instructions burned: 2 (million)
% 9.55/2.25 % (4031134)Instruction limit reached!
% 9.55/2.25 % (4031134)------------------------------
% 9.55/2.25 % (4031134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.55/2.25 % (4031134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.55/2.25 % (4031134)CaDiCaL version: 2.1.3
% 9.55/2.25 % (4031134)Termination reason: Instruction limit
% 9.55/2.25 % (4031134)Termination phase: Saturation
% 9.55/2.25 % (4031134)Time elapsed: 0.069 s
% 9.55/2.25 % (4031134)Peak memory usage: 88 MB
% 9.55/2.25 % (4031134)Instructions burned: 86 (million)
% 9.55/2.25 % (4031142)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=175354381:i=181:rtra=on:ss=axioms:ev=cautious_2994 on theBenchmark for (2994ds/181Mi)
% 9.55/2.25 % (4031146)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=2346207005:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2994 on theBenchmark for (2994ds/8Mi)
% 9.55/2.25 % (4031146)Instruction limit reached!
% 9.55/2.25 % (4031146)------------------------------
% 9.55/2.25 % (4031146)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.55/2.25 % (4031146)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.55/2.25 % (4031146)CaDiCaL version: 2.1.3
% 9.55/2.25 % (4031146)Termination reason: Instruction limit
% 9.55/2.25 % (4031146)Termination phase: Saturation
% 9.55/2.25 % (4031146)Time elapsed: 0.006 s
% 9.55/2.25 % (4031146)Peak memory usage: 88 MB
% 9.55/2.25 % (4031146)Instructions burned: 9 (million)
% 9.55/2.25 % (4031144)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2123450938:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2994 on theBenchmark for (2994ds/66Mi)
% 9.55/2.25 % (4031143)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2276745072:i=4:ep=RST:ins=2:rtra=on_2994 on theBenchmark for (2994ds/4Mi)
% 9.55/2.25 % (4031145)lrs+10_1_thi=all:si=on:fd=off:random_seed=622064787:i=53:rtra=on:gtg=all_2994 on theBenchmark for (2994ds/53Mi)
% 9.55/2.25 % (4031143)Instruction limit reached!
% 9.55/2.25 % (4031143)------------------------------
% 9.55/2.25 % (4031143)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.55/2.25 % (4031143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.55/2.25 % (4031143)CaDiCaL version: 2.1.3
% 9.55/2.25 % (4031143)Termination reason: Instruction limit
% 9.55/2.25 % (4031143)Termination phase: Saturation
% 9.55/2.25 % (4031143)Time elapsed: 0.006 s
% 9.55/2.25 % (4031143)Peak memory usage: 89 MB
% 9.55/2.25 % (4031143)Instructions burned: 5 (million)
% 9.55/2.25 % (4031150)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1341564765:st=3:i=2:rtra=on:ss=axioms_2993 on theBenchmark for (2993ds/2Mi)
% 9.55/2.25 % (4031150)Instruction limit reached!
% 9.55/2.25 % (4031150)------------------------------
% 9.55/2.25 % (4031150)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.55/2.25 % (4031150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.55/2.25 % (4031150)CaDiCaL version: 2.1.3
% 9.55/2.25 % (4031150)Termination reason: Instruction limit
% 9.55/2.25 % (4031150)Termination phase: Saturation
% 11.76/2.66 % (4031150)Time elapsed: 0.003 s
% 11.76/2.66 % (4031150)Peak memory usage: 89 MB
% 11.76/2.66 % (4031150)Instructions burned: 3 (million)
% 11.76/2.66 % (4031145)Instruction limit reached!
% 11.76/2.66 % (4031145)------------------------------
% 11.76/2.66 % (4031145)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.66 % (4031145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.66 % (4031145)CaDiCaL version: 2.1.3
% 11.76/2.66 % (4031145)Termination reason: Instruction limit
% 11.76/2.66 % (4031145)Termination phase: Saturation
% 11.76/2.66 % (4031145)Time elapsed: 0.090 s
% 11.76/2.66 % (4031145)Peak memory usage: 115 MB
% 11.76/2.66 % (4031145)Instructions burned: 53 (million)
% 11.76/2.66 % (4031142)Instruction limit reached!
% 11.76/2.66 % (4031142)------------------------------
% 11.76/2.66 % (4031142)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.66 % (4031142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.66 % (4031142)CaDiCaL version: 2.1.3
% 11.76/2.66 % (4031142)Termination reason: Instruction limit
% 11.76/2.66 % (4031142)Termination phase: Saturation
% 11.76/2.66 % (4031142)Time elapsed: 0.163 s
% 11.76/2.66 % (4031142)Peak memory usage: 90 MB
% 11.76/2.66 % (4031142)Instructions burned: 182 (million)
% 11.76/2.66 % (4031144)Instruction limit reached!
% 11.76/2.66 % (4031144)------------------------------
% 11.76/2.66 % (4031144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.66 % (4031144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.66 % (4031144)CaDiCaL version: 2.1.3
% 11.76/2.66 % (4031144)Termination reason: Instruction limit
% 11.76/2.66 % (4031144)Termination phase: Saturation
% 11.76/2.66 % (4031144)Time elapsed: 0.134 s
% 11.76/2.66 % (4031144)Peak memory usage: 133 MB
% 11.76/2.66 % (4031144)Instructions burned: 66 (million)
% 11.76/2.66 % (4031151)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3797839381:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 11.76/2.66 % (4031151)Instruction limit reached!
% 11.76/2.66 % (4031151)------------------------------
% 11.76/2.66 % (4031151)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.66 % (4031151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.66 % (4031151)CaDiCaL version: 2.1.3
% 11.76/2.66 % (4031151)Termination reason: Instruction limit
% 11.76/2.66 % (4031151)Termination phase: Saturation
% 11.76/2.66 % (4031151)Time elapsed: 0.004 s
% 11.76/2.66 % (4031151)Peak memory usage: 88 MB
% 11.76/2.66 % (4031151)Instructions burned: 2 (million)
% 11.76/2.66 % (4031154)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=501339537:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 11.76/2.66 % (4031154)Instruction limit reached!
% 11.76/2.66 % (4031154)------------------------------
% 11.76/2.66 % (4031154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.66 % (4031154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.66 % (4031154)CaDiCaL version: 2.1.3
% 11.76/2.66 % (4031154)Termination reason: Instruction limit
% 11.76/2.66 % (4031154)Termination phase: Saturation
% 11.76/2.66 % (4031154)Time elapsed: 0.096 s
% 11.76/2.66 % (4031154)Peak memory usage: 116 MB
% 11.76/2.66 % (4031154)Instructions burned: 129 (million)
% 11.76/2.66 % (4031158)dis+10_1_si=on:random_seed=2655952795:i=10:ep=R:rtra=on_2991 on theBenchmark for (2991ds/10Mi)
% 11.76/2.66 % (4031158)Instruction limit reached!
% 11.76/2.66 % (4031158)------------------------------
% 11.76/2.66 % (4031158)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.76/2.66 % (4031158)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.76/2.66 % (4031158)CaDiCaL version: 2.1.3
% 11.76/2.66 % (4031158)Termination reason: Instruction limit
% 11.76/2.66 % (4031158)Termination phase: Saturation
% 11.76/2.66 % (4031158)Time elapsed: 0.013 s
% 11.76/2.66 % (4031158)Peak memory usage: 88 MB
% 11.76/2.66 % (4031158)Instructions burned: 10 (million)
% 11.76/2.66 % (4031161)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=4225248743: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_2991 on theBenchmark for (2991ds/35Mi)
% 11.76/2.66 % (4031160)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=3639356550:i=26:canc=cautious:av=off:rtra=on_2991 on theBenchmark for (2991ds/26Mi)
% 11.76/2.66 % (4031160)Refutation not found, incomplete strategy
% 12.51/2.97 % (4031160)------------------------------
% 12.51/2.97 % (4031160)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031160)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031160)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031160)Termination reason: Refutation not found, incomplete strategy
% 12.51/2.97 % (4031160)Time elapsed: 0.006 s
% 12.51/2.97 % (4031160)Peak memory usage: 89 MB
% 12.51/2.97 % (4031160)Instructions burned: 3 (million)
% 12.51/2.97 % (4031161)Instruction limit reached!
% 12.51/2.97 % (4031161)------------------------------
% 12.51/2.97 % (4031161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031161)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031161)Termination reason: Instruction limit
% 12.51/2.97 % (4031161)Termination phase: Saturation
% 12.51/2.97 % (4031161)Time elapsed: 0.046 s
% 12.51/2.97 % (4031161)Peak memory usage: 89 MB
% 12.51/2.97 % (4031161)Instructions burned: 35 (million)
% 12.51/2.97 % (4031162)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4266946978:i=2:fsr=off:rtra=on:inst=on_2991 on theBenchmark for (2991ds/2Mi)
% 12.51/2.97 % (4031162)Instruction limit reached!
% 12.51/2.97 % (4031162)------------------------------
% 12.51/2.97 % (4031162)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031162)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031162)Termination reason: Instruction limit
% 12.51/2.97 % (4031162)Termination phase: Saturation
% 12.51/2.97 % (4031162)Time elapsed: 0.004 s
% 12.51/2.97 % (4031162)Peak memory usage: 88 MB
% 12.51/2.97 % (4031162)Instructions burned: 2 (million)
% 12.51/2.97 % (4031165)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=4277429063:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2990 on theBenchmark for (2990ds/8Mi)
% 12.51/2.97 % (4031166)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3209106966:i=370:ep=RS:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/370Mi)
% 12.51/2.97 % (4031166)Refutation not found, incomplete strategy
% 12.51/2.97 % (4031166)------------------------------
% 12.51/2.97 % (4031166)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031166)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031166)Termination reason: Refutation not found, incomplete strategy
% 12.51/2.97 % (4031166)Time elapsed: 0.005 s
% 12.51/2.97 % (4031166)Peak memory usage: 88 MB
% 12.51/2.97 % (4031166)Instructions burned: 2 (million)
% 12.51/2.97 % (4031165)Instruction limit reached!
% 12.51/2.97 % (4031165)------------------------------
% 12.51/2.97 % (4031165)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031165)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031165)Termination reason: Instruction limit
% 12.51/2.97 % (4031165)Termination phase: Saturation
% 12.51/2.97 % (4031165)Time elapsed: 0.011 s
% 12.51/2.97 % (4031165)Peak memory usage: 88 MB
% 12.51/2.97 % (4031165)Instructions burned: 8 (million)
% 12.51/2.97 % (4031170)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3234465638:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/13Mi)
% 12.51/2.97 % (4031170)Instruction limit reached!
% 12.51/2.97 % (4031170)------------------------------
% 12.51/2.97 % (4031170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031170)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031170)Termination reason: Instruction limit
% 12.51/2.97 % (4031170)Termination phase: Saturation
% 12.51/2.97 % (4031170)Time elapsed: 0.023 s
% 12.51/2.97 % (4031170)Peak memory usage: 115 MB
% 12.51/2.97 % (4031170)Instructions burned: 13 (million)
% 12.51/2.97 % (4031171)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=464181425:i=226:rtra=on:gtg=position:ss=axioms_2989 on theBenchmark for (2989ds/226Mi)
% 12.51/2.97 % (4031171)First to succeed.
% 12.51/2.97 % (4031174)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1992494930:i=10:rtra=on_2988 on theBenchmark for (2988ds/10Mi)
% 12.51/2.97 % (4031171)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4031110"
% 12.51/2.97 % (4031180)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=587425667:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 12.51/2.97 % (4031174)Instruction limit reached!
% 12.51/2.97 % (4031174)------------------------------
% 12.51/2.97 % (4031174)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031174)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031174)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031174)Termination reason: Instruction limit
% 12.51/2.97 % (4031174)Termination phase: Saturation
% 12.51/2.97 % (4031174)Time elapsed: 0.014 s
% 12.51/2.97 % (4031174)Peak memory usage: 89 MB
% 12.51/2.97 % (4031174)Instructions burned: 10 (million)
% 12.51/2.97 % (4031176)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=2368147929:i=71:rtra=on:gtg=exists_top_2988 on theBenchmark for (2988ds/71Mi)
% 12.51/2.97 % (4031160)------------------------------
% 12.51/2.97 % (4031160)------------------------------
% 12.51/2.97 % (4031180)Instruction limit reached!
% 12.51/2.97 % (4031180)------------------------------
% 12.51/2.97 % (4031180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031180)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031180)Termination reason: Instruction limit
% 12.51/2.97 % (4031180)Termination phase: Saturation
% 12.51/2.97 % (4031180)Time elapsed: 0.092 s
% 12.51/2.97 % (4031180)Peak memory usage: 90 MB
% 12.51/2.97 % (4031180)Instructions burned: 75 (million)
% 12.51/2.97 % (4031182)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=1810173481:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2987 on theBenchmark for (2987ds/294Mi)
% 12.51/2.97 % (4031176)Instruction limit reached!
% 12.51/2.97 % (4031176)------------------------------
% 12.51/2.97 % (4031176)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031176)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031176)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031176)Termination reason: Instruction limit
% 12.51/2.97 % (4031176)Termination phase: Saturation
% 12.51/2.97 % (4031176)Time elapsed: 0.136 s
% 12.51/2.97 % (4031176)Peak memory usage: 133 MB
% 12.51/2.97 % (4031176)Instructions burned: 71 (million)
% 12.51/2.97 % (4031166)------------------------------
% 12.51/2.97 % (4031166)------------------------------
% 12.51/2.97 % (4031182)Instruction limit reached!
% 12.51/2.97 % (4031182)------------------------------
% 12.51/2.97 % (4031182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031182)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031182)Termination reason: Instruction limit
% 12.51/2.97 % (4031182)Termination phase: Saturation
% 12.51/2.97 % (4031182)Time elapsed: 0.156 s
% 12.51/2.97 % (4031182)Peak memory usage: 90 MB
% 12.51/2.97 % (4031182)Instructions burned: 294 (million)
% 12.51/2.97 % (4031187)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2872464800:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi)
% 12.51/2.97 % (4031190)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=1629240562:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 12.51/2.97 % (4031192)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=1651798507:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 12.51/2.97 % (4031191)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1194984712:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2985 on theBenchmark for (2985ds/40Mi)
% 12.51/2.97 % (4031187)Refutation not found, SMT solver inside AVATAR returned Unknown
% 12.51/2.97 % (4031187)------------------------------
% 12.51/2.97 % (4031187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.51/2.97 % (4031187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.51/2.97 % (4031187)CaDiCaL version: 2.1.3
% 12.51/2.97 % (4031187)Termination reason: Refutation not found, SMT solver inside AVATAR returned Unknown
% 12.51/2.97 % (4031187)Time elapsed: 0.153 s
% 12.51/2.97 % (4031187)Peak memory usage: 117 MB
% 12.51/2.97 % (4031187)Instructions burned: 105 (million)
% 12.51/2.97 % (4031187)------------------------------
% 12.51/2.97 % (4031187)------------------------------
% 12.51/2.97 % (4031171)Refutation found. Thanks to Tanya!
% 12.51/2.97 % SZS status Theorem for theBenchmark
% 12.51/2.97 % SZS output start Proof for theBenchmark
% See solution above
% 13.91/3.28 % (4031171)------------------------------
% 13.91/3.28 % (4031171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.91/3.28 % (4031171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.91/3.28 % (4031171)CaDiCaL version: 2.1.3
% 13.91/3.28 % (4031171)Termination reason: Refutation
% 13.91/3.28 % (4031171)Time elapsed: 0.080 s
% 13.91/3.28 % (4031171)Peak memory usage: 117 MB
% 13.91/3.28 % (4031171)Instructions burned: 38 (million)
% 13.91/3.28 % (4031171)------------------------------
% 13.91/3.28 % (4031171)------------------------------
% 13.91/3.28 % (4031110)Success in time 2.108 s
% 13.91/3.28 % Vampire exiting
%------------------------------------------------------------------------------