%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX087_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 : n017.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:51 PM UTC 2026
% Result : Theorem 8.72s 2.04s
% Output : Refutation 10.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 18
% Syntax : Number of formulae : 150 ( 14 unt; 0 typ; 10 def)
% Number of atoms : 717 ( 345 equ)
% Maximal formula atoms : 40 ( 4 avg)
% Number of connectives : 824 ( 257 ~; 295 |; 249 &)
% ( 17 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 355 ( 38 atm; 49 fun; 163 num; 105 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 : 27 ( 23 usr; 8 prp; 0-3 aty)
% Number of functors : 47 ( 42 usr; 7 con; 0-3 aty)
% Number of variables : 415 ( 0 sgn 245 !; 170 ?; 415 :)
% 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,
h_i: $int ).
tff(func_def_10,type,
sK3: general > symbol ).
tff(func_def_11,type,
sK4: general ).
tff(func_def_12,type,
sK5: general ).
tff(func_def_13,type,
sK6: general > $int ).
tff(func_def_14,type,
sK7: ( general * general ) > general ).
tff(func_def_15,type,
sK8: ( general * general ) > general ).
tff(func_def_16,type,
sK9: ( general * general ) > general ).
tff(func_def_17,type,
sK10: ( general * general ) > general ).
tff(func_def_18,type,
sK11: ( general * general ) > general ).
tff(func_def_19,type,
sK12: ( general * general ) > general ).
tff(func_def_20,type,
sK13: ( general * general * general ) > general ).
tff(func_def_21,type,
sK14: ( general * general * general ) > general ).
tff(func_def_22,type,
sK15: ( general * general * general ) > general ).
tff(func_def_23,type,
sK16: ( general * general * general ) > general ).
tff(func_def_24,type,
sK17: ( general * general * general ) > general ).
tff(func_def_25,type,
sK18: ( general * general * general ) > general ).
tff(func_def_26,type,
sK19: ( general * general * general ) > general ).
tff(func_def_27,type,
sK20: ( general * general * general ) > $int ).
tff(func_def_28,type,
sK21: ( general * general * general ) > $int ).
tff(func_def_29,type,
sK22: ( general * general * general ) > general ).
tff(func_def_30,type,
sK23: ( general * general * general ) > general ).
tff(func_def_31,type,
sK24: ( general * general * general ) > general ).
tff(func_def_32,type,
sK25: ( general * general * general ) > general ).
tff(func_def_33,type,
sK26: ( general * general * general ) > general ).
tff(func_def_34,type,
sK27: ( general * general * general ) > general ).
tff(func_def_35,type,
sK28: ( general * general * general ) > general ).
tff(func_def_36,type,
sK29: ( general * general * general ) > general ).
tff(func_def_37,type,
sK30: ( general * general * general ) > general ).
tff(func_def_38,type,
sK31: ( general * general * general ) > $int ).
tff(func_def_39,type,
sK32: ( general * general * general ) > $int ).
tff(func_def_40,type,
sK33: ( general * general * general ) > general ).
tff(func_def_41,type,
sK34: ( general * general * general ) > general ).
tff(func_def_42,type,
sK35: ( general * general * general ) > $int ).
tff(func_def_43,type,
sK36: ( general * general * general ) > $int ).
tff(func_def_44,type,
sK37: ( general * general * general ) > $int ).
tff(func_def_45,type,
sK38: ( general * general * general ) > $int ).
tff(func_def_46,type,
sK39: ( general * general * general ) > $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,
in0: ( general * general ) > $o ).
tff(pred_def_9,type,
person: general > $o ).
tff(pred_def_10,type,
goto: ( general * general * general ) > $o ).
tff(pred_def_11,type,
go: ( general * general ) > $o ).
tff(pred_def_12,type,
in_building: ( general * general ) > $o ).
tff(pred_def_13,type,
in: ( general * general * general ) > $o ).
tff(pred_def_14,type,
in_building_p: ( general * general ) > $o ).
tff(pred_def_17,type,
sP0: ( general * general * general ) > $o ).
tff(pred_def_18,type,
sP1: ( general * general * general ) > $o ).
tff(pred_def_19,type,
sP2: ( general * general * general ) > $o ).
tff(f4,axiom,
! [X1: $int,X0: $int] :
( ( X0 = X1 )
<=> ( f__integer__(X0) = f__integer__(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f__integer__def_ax) ).
tff(f6,axiom,
! [X0: $int,X1: $int] :
( $lesseq(X0,X1)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',numeral_ordering_ax) ).
tff(f17,axiom,
! [X0: general,X1: general] :
( in0(X0,X1)
=> person(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_1_unnamed_formula) ).
tff(f18,axiom,
! [X1: general,X2: general,X0: general] :
( goto(X0,X1,X2)
=> person(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_2_unnamed_formula) ).
tff(f24,axiom,
! [X2: general,X0: general,X1: general] :
( in(X0,X1,X2)
<=> ( ? [X4: general,X3: general,X7: general] :
( ? [X5: general,X6: general] :
( ( X5 = X6 )
& ( X5 = X7 )
& ? [X8: $int,X11: $int,X9: $int] :
( $lesseq(X11,X9)
& ( X6 = f__integer__(X11) )
& $lesseq(X8,X11)
& ( X8 = 0 )
& ? [X12: $int,X8: $int] :
( ( X12 = 1 )
& ( X8 = h_i )
& ( X9 = $difference(X8,X12) ) ) ) )
& ? [X5: general,X6: general,X10: general] :
( in(X5,X6,X10)
& ( X5 = X3 )
& ( X10 = X7 )
& ( X6 = X4 ) )
& ( X0 = X3 )
& ? [X9: $int,X8: $int] :
( ( X9 = 1 )
& ( X2 = f__integer__($sum(X8,X9)) )
& ( f__integer__(X8) = X7 ) )
& in(X0,X1,X2)
& ( X1 = X4 ) )
| ? [X4: general,X3: general] :
( ( X1 = X4 )
& ( X0 = X3 )
& ( X2 = f__integer__(0) )
& ? [X5: general,X6: general] :
( ( X5 = X3 )
& ( X6 = X4 )
& in0(X5,X6) ) )
| ? [X7: general,X4: general,X3: general] :
( ? [X9: $int,X8: $int] :
( ( X2 = f__integer__($sum(X8,X9)) )
& ( f__integer__(X8) = X7 )
& ( X9 = 1 ) )
& ( X1 = X4 )
& ( X0 = X3 )
& ? [X6: general,X5: general,X10: general] :
( ( X10 = X7 )
& goto(X5,X6,X10)
& ( X6 = X4 )
& ( X5 = X3 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_8_completed_definition_of_in_3) ).
tff(f25,conjecture,
! [X1: general,X0: general] :
( in(X0,X1,f__integer__(0))
=> person(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_9_base_case) ).
tff(f26,negated_conjecture,
~ ! [X1: general,X0: general] :
( in(X0,X1,f__integer__(0))
=> person(X0) ),
inference(negated_conjecture,[status(cth)],[f25]) ).
tff(f27,plain,
! [X1: $int,X0: $int] :
( ~ $less(X1,X0)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
inference(theory_normalization,[],[f6]) ).
tff(f29,plain,
! [X2: general,X0: general,X1: general] :
( in(X0,X1,X2)
<=> ( ? [X4: general,X3: general,X7: general] :
( ? [X5: general,X6: general] :
( ( X5 = X6 )
& ( X5 = X7 )
& ? [X8: $int,X11: $int,X9: $int] :
( ~ $less(X9,X11)
& ( X6 = f__integer__(X11) )
& ~ $less(X11,X8)
& ( X8 = 0 )
& ? [X12: $int,X8: $int] :
( ( X12 = 1 )
& ( X8 = h_i )
& ( $sum(X8,$uminus(X12)) = X9 ) ) ) )
& ? [X5: general,X6: general,X10: general] :
( in(X5,X6,X10)
& ( X5 = X3 )
& ( X10 = X7 )
& ( X6 = X4 ) )
& ( X0 = X3 )
& ? [X9: $int,X8: $int] :
( ( X9 = 1 )
& ( X2 = f__integer__($sum(X8,X9)) )
& ( f__integer__(X8) = X7 ) )
& in(X0,X1,X2)
& ( X1 = X4 ) )
| ? [X4: general,X3: general] :
( ( X1 = X4 )
& ( X0 = X3 )
& ( X2 = f__integer__(0) )
& ? [X5: general,X6: general] :
( ( X5 = X3 )
& ( X6 = X4 )
& in0(X5,X6) ) )
| ? [X7: general,X4: general,X3: general] :
( ? [X9: $int,X8: $int] :
( ( X2 = f__integer__($sum(X8,X9)) )
& ( f__integer__(X8) = X7 )
& ( X9 = 1 ) )
& ( X1 = X4 )
& ( X0 = X3 )
& ? [X6: general,X5: general,X10: general] :
( ( X10 = X7 )
& goto(X5,X6,X10)
& ( X6 = X4 )
& ( X5 = X3 ) ) ) ) ),
inference(theory_normalization,[],[f24]) ).
tff(f31,plain,
! [X0: $int,X1: $int] : ( $sum(X0,X1) = $sum(X1,X0) ),
introduced(definition,[],[tha_commutativity]) ).
tff(f40,plain,
! [X0: $int,X1: $int] :
( $less(X0,X1)
| $less(X1,$sum(X0,1)) ),
introduced(definition,[],[tha_order_plus_one_dichotomy]) ).
tff(f45,plain,
~ ! [X1: general,X0: general] :
( in(X1,X0,f__integer__(0))
=> person(X1) ),
inference(rectify,[],[f26]) ).
tff(f50,plain,
! [X2: general,X0: general,X1: general] :
( ( ? [X24: general,X22: general,X23: general] :
( ? [X26: $int,X25: $int] :
( ( f__integer__($sum(X26,X25)) = X0 )
& ( 1 = X25 )
& ( f__integer__(X26) = X22 ) )
& ( X2 = X23 )
& ? [X27: general,X28: general,X29: general] :
( ( X24 = X28 )
& ( X23 = X27 )
& goto(X28,X27,X29)
& ( X22 = X29 ) )
& ( X1 = X24 ) )
| ? [X18: general,X19: general] :
( ( X1 = X19 )
& ? [X20: general,X21: general] :
( in0(X20,X21)
& ( X19 = X20 )
& ( X18 = X21 ) )
& ( X2 = X18 )
& ( f__integer__(0) = X0 ) )
| ? [X5: general,X4: general,X3: general] :
( ( X2 = X3 )
& ? [X13: general,X14: general,X15: general] :
( ( X3 = X14 )
& ( X5 = X15 )
& in(X13,X14,X15)
& ( X4 = X13 ) )
& in(X1,X2,X0)
& ( X1 = X4 )
& ? [X17: $int,X16: $int] :
( ( f__integer__(X17) = X5 )
& ( 1 = X16 )
& ( f__integer__($sum(X17,X16)) = X0 ) )
& ? [X7: general,X6: general] :
( ( X5 = X6 )
& ? [X9: $int,X8: $int,X10: $int] :
( ? [X11: $int,X12: $int] :
( ( h_i = X12 )
& ( 1 = X11 )
& ( $sum(X12,$uminus(X11)) = X10 ) )
& ( f__integer__(X9) = X7 )
& ~ $less(X10,X9)
& ( X8 = 0 )
& ~ $less(X9,X8) )
& ( X6 = X7 ) ) ) )
<=> in(X1,X2,X0) ),
inference(rectify,[],[f29]) ).
tff(f54,plain,
! [X1: general,X0: general,X2: general] :
( goto(X2,X0,X1)
=> person(X2) ),
inference(rectify,[],[f18]) ).
tff(f60,plain,
! [X1: general,X0: general] :
( ~ in0(X0,X1)
| person(X0) ),
inference(ennf_transformation,[],[f17]) ).
tff(f65,plain,
! [X0: general,X1: general,X2: general] :
( person(X2)
| ~ goto(X2,X0,X1) ),
inference(ennf_transformation,[],[f54]) ).
tff(f66,plain,
? [X1: general,X0: general] :
( in(X1,X0,f__integer__(0))
& ~ person(X1) ),
inference(ennf_transformation,[],[f45]) ).
tff(f72,definition,
! [X2: general,X0: general,X1: general] :
( sP0(X2,X0,X1)
<=> ? [X5: general,X4: general,X3: general] :
( ( X2 = X3 )
& ? [X13: general,X14: general,X15: general] :
( ( X3 = X14 )
& ( X5 = X15 )
& in(X13,X14,X15)
& ( X4 = X13 ) )
& in(X1,X2,X0)
& ( X1 = X4 )
& ? [X17: $int,X16: $int] :
( ( f__integer__(X17) = X5 )
& ( 1 = X16 )
& ( f__integer__($sum(X17,X16)) = X0 ) )
& ? [X7: general,X6: general] :
( ( X5 = X6 )
& ? [X9: $int,X8: $int,X10: $int] :
( ? [X11: $int,X12: $int] :
( ( h_i = X12 )
& ( 1 = X11 )
& ( $sum(X12,$uminus(X11)) = X10 ) )
& ( f__integer__(X9) = X7 )
& ~ $less(X10,X9)
& ( X8 = 0 )
& ~ $less(X9,X8) )
& ( X6 = X7 ) ) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
tff(f73,definition,
! [X0: general,X2: general,X1: general] :
( sP1(X0,X2,X1)
<=> ? [X24: general,X22: general,X23: general] :
( ? [X26: $int,X25: $int] :
( ( f__integer__($sum(X26,X25)) = X0 )
& ( 1 = X25 )
& ( f__integer__(X26) = X22 ) )
& ( X2 = X23 )
& ? [X27: general,X28: general,X29: general] :
( ( X24 = X28 )
& ( X23 = X27 )
& goto(X28,X27,X29)
& ( X22 = X29 ) )
& ( X1 = X24 ) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
tff(f74,definition,
! [X1: general,X2: general,X0: general] :
( sP2(X1,X2,X0)
<=> ( sP1(X0,X2,X1)
| ? [X18: general,X19: general] :
( ( X1 = X19 )
& ? [X20: general,X21: general] :
( in0(X20,X21)
& ( X19 = X20 )
& ( X18 = X21 ) )
& ( X2 = X18 )
& ( f__integer__(0) = X0 ) )
| sP0(X2,X0,X1) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
tff(f75,plain,
! [X2: general,X0: general,X1: general] :
( sP2(X1,X2,X0)
<=> in(X1,X2,X0) ),
inference(definition_folding,[],[f50,f74,f73,f72]) ).
tff(f76,plain,
! [X0: general,X1: general] :
( ~ in0(X1,X0)
| person(X1) ),
inference(rectify,[],[f60]) ).
tff(f81,plain,
? [X0: general,X1: general] :
( in(X0,X1,f__integer__(0))
& ~ person(X0) ),
inference(rectify,[],[f66]) ).
tff(f82,plain,
( in(sK4,sK5,f__integer__(0))
& ~ person(sK4) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X0,sK4),skolemize(X1,sK5)],[f81]) ).
tff(f84,plain,
! [X1: $int,X0: $int] :
( ( ( X0 = X1 )
| ( f__integer__(X1) != f__integer__(X0) ) )
& ( ( f__integer__(X0) = f__integer__(X1) )
| ( X0 != X1 ) ) ),
inference(nnf_transformation,[],[f4]) ).
tff(f85,plain,
! [X0: $int,X1: $int] :
( ( ( X0 = X1 )
| ( f__integer__(X1) != f__integer__(X0) ) )
& ( ( f__integer__(X0) = f__integer__(X1) )
| ( X0 != X1 ) ) ),
inference(rectify,[],[f84]) ).
tff(f90,plain,
! [X1: $int,X0: $int] :
( ( ~ $less(X1,X0)
| ~ p__less_equal__(f__integer__(X0),f__integer__(X1)) )
& ( p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X1,X0) ) ),
inference(nnf_transformation,[],[f27]) ).
tff(f91,plain,
! [X0: $int,X1: $int] :
( ( ~ $less(X0,X1)
| ~ p__less_equal__(f__integer__(X1),f__integer__(X0)) )
& ( p__less_equal__(f__integer__(X1),f__integer__(X0))
| $less(X0,X1) ) ),
inference(rectify,[],[f90]) ).
tff(f92,plain,
! [X1: general,X2: general,X0: general] :
( ( sP2(X1,X2,X0)
| ( ~ sP1(X0,X2,X1)
& ! [X18: general,X19: general] :
( ( X1 != X19 )
| ! [X20: general,X21: general] :
( ~ in0(X20,X21)
| ( X19 != X20 )
| ( X18 != X21 ) )
| ( X2 != X18 )
| ( f__integer__(0) != X0 ) )
& ~ sP0(X2,X0,X1) ) )
& ( sP1(X0,X2,X1)
| ? [X18: general,X19: general] :
( ( X1 = X19 )
& ? [X20: general,X21: general] :
( in0(X20,X21)
& ( X19 = X20 )
& ( X18 = X21 ) )
& ( X2 = X18 )
& ( f__integer__(0) = X0 ) )
| sP0(X2,X0,X1)
| ~ sP2(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f74]) ).
tff(f93,plain,
! [X1: general,X2: general,X0: general] :
( ( sP2(X1,X2,X0)
| ( ~ sP1(X0,X2,X1)
& ! [X18: general,X19: general] :
( ( X1 != X19 )
| ! [X20: general,X21: general] :
( ~ in0(X20,X21)
| ( X19 != X20 )
| ( X18 != X21 ) )
| ( X2 != X18 )
| ( f__integer__(0) != X0 ) )
& ~ sP0(X2,X0,X1) ) )
& ( sP1(X0,X2,X1)
| ? [X18: general,X19: general] :
( ( X1 = X19 )
& ? [X20: general,X21: general] :
( in0(X20,X21)
& ( X19 = X20 )
& ( X18 = X21 ) )
& ( X2 = X18 )
& ( f__integer__(0) = X0 ) )
| sP0(X2,X0,X1)
| ~ sP2(X1,X2,X0) ) ),
inference(flattening,[],[f92]) ).
tff(f94,plain,
! [X0: general,X1: general,X2: general] :
( ( sP2(X0,X1,X2)
| ( ~ sP1(X2,X1,X0)
& ! [X3: general,X4: general] :
( ( X0 != X4 )
| ! [X5: general,X6: general] :
( ~ in0(X5,X6)
| ( X4 != X5 )
| ( X3 != X6 ) )
| ( X1 != X3 )
| ( f__integer__(0) != X2 ) )
& ~ sP0(X1,X2,X0) ) )
& ( sP1(X2,X1,X0)
| ? [X7: general,X8: general] :
( ( X0 = X8 )
& ? [X9: general,X10: general] :
( in0(X9,X10)
& ( X8 = X9 )
& ( X7 = X10 ) )
& ( X1 = X7 )
& ( f__integer__(0) = X2 ) )
| sP0(X1,X2,X0)
| ~ sP2(X0,X1,X2) ) ),
inference(rectify,[],[f93]) ).
tff(f95,plain,
! [X0: general,X1: general,X2: general] :
( ( sP2(X0,X1,X2)
| ( ~ sP1(X2,X1,X0)
& ! [X3: general,X4: general] :
( ( X0 != X4 )
| ! [X5: general,X6: general] :
( ~ in0(X5,X6)
| ( X4 != X5 )
| ( X3 != X6 ) )
| ( X1 != X3 )
| ( f__integer__(0) != X2 ) )
& ~ sP0(X1,X2,X0) ) )
& ( sP1(X2,X1,X0)
| ( ( sK14(X0,X1,X2) = X0 )
& in0(sK15(X0,X1,X2),sK16(X0,X1,X2))
& ( sK15(X0,X1,X2) = sK14(X0,X1,X2) )
& ( sK13(X0,X1,X2) = sK16(X0,X1,X2) )
& ( sK13(X0,X1,X2) = X1 )
& ( f__integer__(0) = X2 ) )
| sP0(X1,X2,X0)
| ~ sP2(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16]),skolemize(X7,sK13(X0,X1,X2)),skolemize(X8,sK14(X0,X1,X2)),skolemize(X9,sK15(X0,X1,X2)),skolemize(X10,sK16(X0,X1,X2))],[f94]) ).
tff(f96,plain,
! [X0: general,X2: general,X1: general] :
( ( sP1(X0,X2,X1)
| ! [X24: general,X22: general,X23: general] :
( ! [X26: $int,X25: $int] :
( ( f__integer__($sum(X26,X25)) != X0 )
| ( 1 != X25 )
| ( f__integer__(X26) != X22 ) )
| ( X2 != X23 )
| ! [X27: general,X28: general,X29: general] :
( ( X24 != X28 )
| ( X23 != X27 )
| ~ goto(X28,X27,X29)
| ( X22 != X29 ) )
| ( X1 != X24 ) ) )
& ( ? [X24: general,X22: general,X23: general] :
( ? [X26: $int,X25: $int] :
( ( f__integer__($sum(X26,X25)) = X0 )
& ( 1 = X25 )
& ( f__integer__(X26) = X22 ) )
& ( X2 = X23 )
& ? [X27: general,X28: general,X29: general] :
( ( X24 = X28 )
& ( X23 = X27 )
& goto(X28,X27,X29)
& ( X22 = X29 ) )
& ( X1 = X24 ) )
| ~ sP1(X0,X2,X1) ) ),
inference(nnf_transformation,[],[f73]) ).
tff(f97,plain,
! [X0: general,X1: general,X2: general] :
( ( sP1(X0,X1,X2)
| ! [X3: general,X4: general,X5: general] :
( ! [X6: $int,X7: $int] :
( ( f__integer__($sum(X6,X7)) != X0 )
| ( 1 != X7 )
| ( f__integer__(X6) != X4 ) )
| ( X1 != X5 )
| ! [X8: general,X9: general,X10: general] :
( ( X3 != X9 )
| ( X5 != X8 )
| ~ goto(X9,X8,X10)
| ( X4 != X10 ) )
| ( X2 != X3 ) ) )
& ( ? [X11: general,X12: general,X13: general] :
( ? [X14: $int,X15: $int] :
( ( f__integer__($sum(X14,X15)) = X0 )
& ( 1 = X15 )
& ( f__integer__(X14) = X12 ) )
& ( X1 = X13 )
& ? [X16: general,X17: general,X18: general] :
( ( X11 = X17 )
& ( X13 = X16 )
& goto(X17,X16,X18)
& ( X12 = X18 ) )
& ( X2 = X11 ) )
| ~ sP1(X0,X1,X2) ) ),
inference(rectify,[],[f96]) ).
tff(f98,plain,
! [X0: general,X1: general,X2: general] :
( ( sP1(X0,X1,X2)
| ! [X3: general,X4: general,X5: general] :
( ! [X6: $int,X7: $int] :
( ( f__integer__($sum(X6,X7)) != X0 )
| ( 1 != X7 )
| ( f__integer__(X6) != X4 ) )
| ( X1 != X5 )
| ! [X8: general,X9: general,X10: general] :
( ( X3 != X9 )
| ( X5 != X8 )
| ~ goto(X9,X8,X10)
| ( X4 != X10 ) )
| ( X2 != X3 ) ) )
& ( ( ( f__integer__($sum(sK20(X0,X1,X2),sK21(X0,X1,X2))) = X0 )
& ( 1 = sK21(X0,X1,X2) )
& ( sK18(X0,X1,X2) = f__integer__(sK20(X0,X1,X2)) )
& ( sK19(X0,X1,X2) = X1 )
& ( sK23(X0,X1,X2) = sK17(X0,X1,X2) )
& ( sK22(X0,X1,X2) = sK19(X0,X1,X2) )
& goto(sK23(X0,X1,X2),sK22(X0,X1,X2),sK24(X0,X1,X2))
& ( sK24(X0,X1,X2) = sK18(X0,X1,X2) )
& ( sK17(X0,X1,X2) = X2 ) )
| ~ sP1(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24]),skolemize(X11,sK17(X0,X1,X2)),skolemize(X12,sK18(X0,X1,X2)),skolemize(X13,sK19(X0,X1,X2)),skolemize(X14,sK20(X0,X1,X2)),skolemize(X15,sK21(X0,X1,X2)),skolemize(X16,sK22(X0,X1,X2)),skolemize(X17,sK23(X0,X1,X2)),skolemize(X18,sK24(X0,X1,X2))],[f97]) ).
tff(f99,plain,
! [X2: general,X0: general,X1: general] :
( ( sP0(X2,X0,X1)
| ! [X5: general,X4: general,X3: general] :
( ( X2 != X3 )
| ! [X13: general,X14: general,X15: general] :
( ( X3 != X14 )
| ( X5 != X15 )
| ~ in(X13,X14,X15)
| ( X4 != X13 ) )
| ~ in(X1,X2,X0)
| ( X1 != X4 )
| ! [X17: $int,X16: $int] :
( ( f__integer__(X17) != X5 )
| ( 1 != X16 )
| ( f__integer__($sum(X17,X16)) != X0 ) )
| ! [X7: general,X6: general] :
( ( X5 != X6 )
| ! [X9: $int,X8: $int,X10: $int] :
( ! [X11: $int,X12: $int] :
( ( h_i != X12 )
| ( 1 != X11 )
| ( $sum(X12,$uminus(X11)) != X10 ) )
| ( f__integer__(X9) != X7 )
| $less(X10,X9)
| ( 0 != X8 )
| $less(X9,X8) )
| ( X6 != X7 ) ) ) )
& ( ? [X5: general,X4: general,X3: general] :
( ( X2 = X3 )
& ? [X13: general,X14: general,X15: general] :
( ( X3 = X14 )
& ( X5 = X15 )
& in(X13,X14,X15)
& ( X4 = X13 ) )
& in(X1,X2,X0)
& ( X1 = X4 )
& ? [X17: $int,X16: $int] :
( ( f__integer__(X17) = X5 )
& ( 1 = X16 )
& ( f__integer__($sum(X17,X16)) = X0 ) )
& ? [X7: general,X6: general] :
( ( X5 = X6 )
& ? [X9: $int,X8: $int,X10: $int] :
( ? [X11: $int,X12: $int] :
( ( h_i = X12 )
& ( 1 = X11 )
& ( $sum(X12,$uminus(X11)) = X10 ) )
& ( f__integer__(X9) = X7 )
& ~ $less(X10,X9)
& ( X8 = 0 )
& ~ $less(X9,X8) )
& ( X6 = X7 ) ) )
| ~ sP0(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f72]) ).
tff(f100,plain,
! [X0: general,X1: general,X2: general] :
( ( sP0(X0,X1,X2)
| ! [X3: general,X4: general,X5: general] :
( ( X0 != X5 )
| ! [X6: general,X7: general,X8: general] :
( ( X5 != X7 )
| ( X3 != X8 )
| ~ in(X6,X7,X8)
| ( X4 != X6 ) )
| ~ in(X2,X0,X1)
| ( X2 != X4 )
| ! [X9: $int,X10: $int] :
( ( f__integer__(X9) != X3 )
| ( 1 != X10 )
| ( f__integer__($sum(X9,X10)) != X1 ) )
| ! [X11: general,X12: general] :
( ( X3 != X12 )
| ! [X13: $int,X14: $int,X15: $int] :
( ! [X16: $int,X17: $int] :
( ( h_i != X17 )
| ( 1 != X16 )
| ( $sum(X17,$uminus(X16)) != X15 ) )
| ( f__integer__(X13) != X11 )
| $less(X15,X13)
| ( 0 != X14 )
| $less(X13,X14) )
| ( X11 != X12 ) ) ) )
& ( ? [X18: general,X19: general,X20: general] :
( ( X0 = X20 )
& ? [X21: general,X22: general,X23: general] :
( ( X20 = X22 )
& ( X18 = X23 )
& in(X21,X22,X23)
& ( X19 = X21 ) )
& in(X2,X0,X1)
& ( X2 = X19 )
& ? [X24: $int,X25: $int] :
( ( f__integer__(X24) = X18 )
& ( 1 = X25 )
& ( f__integer__($sum(X24,X25)) = X1 ) )
& ? [X26: general,X27: general] :
( ( X18 = X27 )
& ? [X28: $int,X29: $int,X30: $int] :
( ? [X31: $int,X32: $int] :
( ( h_i = X32 )
& ( 1 = X31 )
& ( $sum(X32,$uminus(X31)) = X30 ) )
& ( f__integer__(X28) = X26 )
& ~ $less(X30,X28)
& ( 0 = X29 )
& ~ $less(X28,X29) )
& ( X26 = X27 ) ) )
| ~ sP0(X0,X1,X2) ) ),
inference(rectify,[],[f99]) ).
tff(f101,plain,
! [X0: general,X1: general,X2: general] :
( ( sP0(X0,X1,X2)
| ! [X3: general,X4: general,X5: general] :
( ( X0 != X5 )
| ! [X6: general,X7: general,X8: general] :
( ( X5 != X7 )
| ( X3 != X8 )
| ~ in(X6,X7,X8)
| ( X4 != X6 ) )
| ~ in(X2,X0,X1)
| ( X2 != X4 )
| ! [X9: $int,X10: $int] :
( ( f__integer__(X9) != X3 )
| ( 1 != X10 )
| ( f__integer__($sum(X9,X10)) != X1 ) )
| ! [X11: general,X12: general] :
( ( X3 != X12 )
| ! [X13: $int,X14: $int,X15: $int] :
( ! [X16: $int,X17: $int] :
( ( h_i != X17 )
| ( 1 != X16 )
| ( $sum(X17,$uminus(X16)) != X15 ) )
| ( f__integer__(X13) != X11 )
| $less(X15,X13)
| ( 0 != X14 )
| $less(X13,X14) )
| ( X11 != X12 ) ) ) )
& ( ( ( sK27(X0,X1,X2) = X0 )
& ( sK27(X0,X1,X2) = sK29(X0,X1,X2) )
& ( sK30(X0,X1,X2) = sK25(X0,X1,X2) )
& in(sK28(X0,X1,X2),sK29(X0,X1,X2),sK30(X0,X1,X2))
& ( sK28(X0,X1,X2) = sK26(X0,X1,X2) )
& in(X2,X0,X1)
& ( sK26(X0,X1,X2) = X2 )
& ( sK25(X0,X1,X2) = f__integer__(sK31(X0,X1,X2)) )
& ( 1 = sK32(X0,X1,X2) )
& ( f__integer__($sum(sK31(X0,X1,X2),sK32(X0,X1,X2))) = X1 )
& ( sK25(X0,X1,X2) = sK34(X0,X1,X2) )
& ( h_i = sK39(X0,X1,X2) )
& ( 1 = sK38(X0,X1,X2) )
& ( $sum(sK39(X0,X1,X2),$uminus(sK38(X0,X1,X2))) = sK37(X0,X1,X2) )
& ( sK33(X0,X1,X2) = f__integer__(sK35(X0,X1,X2)) )
& ~ $less(sK37(X0,X1,X2),sK35(X0,X1,X2))
& ( 0 = sK36(X0,X1,X2) )
& ~ $less(sK35(X0,X1,X2),sK36(X0,X1,X2))
& ( sK33(X0,X1,X2) = sK34(X0,X1,X2) ) )
| ~ sP0(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39]),skolemize(X18,sK25(X0,X1,X2)),skolemize(X19,sK26(X0,X1,X2)),skolemize(X20,sK27(X0,X1,X2)),skolemize(X21,sK28(X0,X1,X2)),skolemize(X22,sK29(X0,X1,X2)),skolemize(X23,sK30(X0,X1,X2)),skolemize(X24,sK31(X0,X1,X2)),skolemize(X25,sK32(X0,X1,X2)),skolemize(X26,sK33(X0,X1,X2)),skolemize(X27,sK34(X0,X1,X2)),skolemize(X28,sK35(X0,X1,X2)),skolemize(X29,sK36(X0,X1,X2)),skolemize(X30,sK37(X0,X1,X2)),skolemize(X31,sK38(X0,X1,X2)),skolemize(X32,sK39(X0,X1,X2))],[f100]) ).
tff(f102,plain,
! [X2: general,X0: general,X1: general] :
( ( sP2(X1,X2,X0)
| ~ in(X1,X2,X0) )
& ( in(X1,X2,X0)
| ~ sP2(X1,X2,X0) ) ),
inference(nnf_transformation,[],[f75]) ).
tff(f103,plain,
! [X0: general,X1: general,X2: general] :
( ( sP2(X2,X0,X1)
| ~ in(X2,X0,X1) )
& ( in(X2,X0,X1)
| ~ sP2(X2,X0,X1) ) ),
inference(rectify,[],[f102]) ).
tff(f106,plain,
! [X0: general,X1: general] :
( ~ in0(X1,X0)
| person(X1) ),
inference(cnf_transformation,[],[f76]) ).
tff(f108,plain,
! [X2: general,X0: general,X1: general] :
( ~ goto(X2,X0,X1)
| person(X2) ),
inference(cnf_transformation,[],[f65]) ).
tff(f117,plain,
~ person(sK4),
inference(cnf_transformation,[],[f82]) ).
tff(f118,plain,
in(sK4,sK5,f__integer__(0)),
inference(cnf_transformation,[],[f82]) ).
tff(f123,plain,
! [X0: $int,X1: $int] :
( ( f__integer__(X1) != f__integer__(X0) )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f85]) ).
tff(f133,plain,
! [X0: $int,X1: $int] :
( p__less_equal__(f__integer__(X1),f__integer__(X0))
| $less(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
tff(f134,plain,
! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(X1),f__integer__(X0))
| ~ $less(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
tff(f136,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( sK13(X0,X1,X2) = X1 )
| sP1(X2,X1,X0)
| sP0(X1,X2,X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f137,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( sK13(X0,X1,X2) = sK16(X0,X1,X2) )
| sP0(X1,X2,X0)
| sP1(X2,X1,X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f138,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| sP1(X2,X1,X0)
| ( sK15(X0,X1,X2) = sK14(X0,X1,X2) )
| sP0(X1,X2,X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f139,plain,
! [X2: general,X0: general,X1: general] :
( in0(sK15(X0,X1,X2),sK16(X0,X1,X2))
| sP0(X1,X2,X0)
| sP1(X2,X1,X0)
| ~ sP2(X0,X1,X2) ),
inference(cnf_transformation,[],[f95]) ).
tff(f140,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP2(X0,X1,X2)
| ( sK14(X0,X1,X2) = X0 )
| sP1(X2,X1,X0)
| sP0(X1,X2,X0) ),
inference(cnf_transformation,[],[f95]) ).
tff(f144,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP1(X0,X1,X2)
| ( sK17(X0,X1,X2) = X2 ) ),
inference(cnf_transformation,[],[f98]) ).
tff(f146,plain,
! [X2: general,X0: general,X1: general] :
( goto(sK23(X0,X1,X2),sK22(X0,X1,X2),sK24(X0,X1,X2))
| ~ sP1(X0,X1,X2) ),
inference(cnf_transformation,[],[f98]) ).
tff(f148,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP1(X0,X1,X2)
| ( sK23(X0,X1,X2) = sK17(X0,X1,X2) ) ),
inference(cnf_transformation,[],[f98]) ).
tff(f154,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2)
| ( sK33(X0,X1,X2) = sK34(X0,X1,X2) ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f155,plain,
! [X2: general,X0: general,X1: general] :
( ~ $less(sK35(X0,X1,X2),sK36(X0,X1,X2))
| ~ sP0(X0,X1,X2) ),
inference(cnf_transformation,[],[f101]) ).
tff(f156,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2)
| ( 0 = sK36(X0,X1,X2) ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f158,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2)
| ( sK33(X0,X1,X2) = f__integer__(sK35(X0,X1,X2)) ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f162,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2)
| ( sK25(X0,X1,X2) = sK34(X0,X1,X2) ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f163,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2)
| ( f__integer__($sum(sK31(X0,X1,X2),sK32(X0,X1,X2))) = X1 ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f164,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2)
| ( 1 = sK32(X0,X1,X2) ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f165,plain,
! [X2: general,X0: general,X1: general] :
( ~ sP0(X0,X1,X2)
| ( sK25(X0,X1,X2) = f__integer__(sK31(X0,X1,X2)) ) ),
inference(cnf_transformation,[],[f101]) ).
tff(f175,plain,
! [X2: general,X0: general,X1: general] :
( ~ in(X2,X0,X1)
| sP2(X2,X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
tff(f226,plain,
! [X0: general,X1: general] : ~ goto(sK4,X0,X1),
inference(unit_resulting_resolution,[],[f108,f117]) ).
tff(f228,plain,
sP2(sK4,sK5,f__integer__(0)),
inference(unit_resulting_resolution,[],[f175,f118]) ).
tff(f234,plain,
( sP0(sK5,f__integer__(0),sK4)
| sP1(f__integer__(0),sK5,sK4)
| ( sK4 = sK14(sK4,sK5,f__integer__(0)) ) ),
inference(resolution,[],[f228,f140]) ).
tff(f235,plain,
( sP1(f__integer__(0),sK5,sK4)
| sP0(sK5,f__integer__(0),sK4)
| ( sK16(sK4,sK5,f__integer__(0)) = sK13(sK4,sK5,f__integer__(0)) ) ),
inference(resolution,[],[f228,f137]) ).
tff(f237,plain,
( ( sK14(sK4,sK5,f__integer__(0)) = sK15(sK4,sK5,f__integer__(0)) )
| sP0(sK5,f__integer__(0),sK4)
| sP1(f__integer__(0),sK5,sK4) ),
inference(resolution,[],[f228,f138]) ).
tff(f239,plain,
( sP0(sK5,f__integer__(0),sK4)
| ( sK5 = sK13(sK4,sK5,f__integer__(0)) )
| sP1(f__integer__(0),sK5,sK4) ),
inference(resolution,[],[f228,f136]) ).
tff(f241,definition,
( spl40_1
<=> ( sK5 = sK13(sK4,sK5,f__integer__(0)) ) ),
introduced(definition,[new_symbols(definition,[spl40_1])],[avatar_definition]) ).
tff(f243,plain,
( ( sK5 = sK13(sK4,sK5,f__integer__(0)) )
| ~ spl40_1 ),
inference(avatar_component_clause,[],[f241]) ).
tff(f245,definition,
( spl40_2
<=> sP0(sK5,f__integer__(0),sK4) ),
introduced(definition,[new_symbols(definition,[spl40_2])],[avatar_definition]) ).
tff(f246,plain,
( ~ sP0(sK5,f__integer__(0),sK4)
| spl40_2 ),
inference(avatar_component_clause,[],[f245]) ).
tff(f247,plain,
( sP0(sK5,f__integer__(0),sK4)
| ~ spl40_2 ),
inference(avatar_component_clause,[],[f245]) ).
tff(f249,definition,
( spl40_3
<=> sP1(f__integer__(0),sK5,sK4) ),
introduced(definition,[new_symbols(definition,[spl40_3])],[avatar_definition]) ).
tff(f250,plain,
( ~ sP1(f__integer__(0),sK5,sK4)
| spl40_3 ),
inference(avatar_component_clause,[],[f249]) ).
tff(f251,plain,
( sP1(f__integer__(0),sK5,sK4)
| ~ spl40_3 ),
inference(avatar_component_clause,[],[f249]) ).
tff(f252,plain,
( spl40_1
| spl40_2
| spl40_3 ),
inference(avatar_split_clause,[],[f239,f249,f245,f241]) ).
tff(f254,definition,
( spl40_4
<=> ( sK14(sK4,sK5,f__integer__(0)) = sK15(sK4,sK5,f__integer__(0)) ) ),
introduced(definition,[new_symbols(definition,[spl40_4])],[avatar_definition]) ).
tff(f256,plain,
( ( sK14(sK4,sK5,f__integer__(0)) = sK15(sK4,sK5,f__integer__(0)) )
| ~ spl40_4 ),
inference(avatar_component_clause,[],[f254]) ).
tff(f257,plain,
( spl40_4
| spl40_2
| spl40_3 ),
inference(avatar_split_clause,[],[f237,f249,f245,f254]) ).
tff(f259,definition,
( spl40_5
<=> ( sK16(sK4,sK5,f__integer__(0)) = sK13(sK4,sK5,f__integer__(0)) ) ),
introduced(definition,[new_symbols(definition,[spl40_5])],[avatar_definition]) ).
tff(f261,plain,
( ( sK16(sK4,sK5,f__integer__(0)) = sK13(sK4,sK5,f__integer__(0)) )
| ~ spl40_5 ),
inference(avatar_component_clause,[],[f259]) ).
tff(f262,plain,
( spl40_2
| spl40_3
| spl40_5 ),
inference(avatar_split_clause,[],[f235,f259,f249,f245]) ).
tff(f264,definition,
( spl40_6
<=> ( sK4 = sK14(sK4,sK5,f__integer__(0)) ) ),
introduced(definition,[new_symbols(definition,[spl40_6])],[avatar_definition]) ).
tff(f266,plain,
( ( sK4 = sK14(sK4,sK5,f__integer__(0)) )
| ~ spl40_6 ),
inference(avatar_component_clause,[],[f264]) ).
tff(f267,plain,
( spl40_3
| spl40_2
| spl40_6 ),
inference(avatar_split_clause,[],[f234,f264,f245,f249]) ).
tff(f415,plain,
( ( sK4 = sK17(f__integer__(0),sK5,sK4) )
| ~ spl40_3 ),
inference(unit_resulting_resolution,[],[f144,f251]) ).
tff(f419,plain,
( ( sK23(f__integer__(0),sK5,sK4) = sK17(f__integer__(0),sK5,sK4) )
| ~ spl40_3 ),
inference(unit_resulting_resolution,[],[f148,f251]) ).
tff(f449,plain,
( ( sK23(f__integer__(0),sK5,sK4) = sK4 )
| ~ spl40_3 ),
inference(superposition,[],[f415,f419]) ).
tff(f450,plain,
( goto(sK4,sK22(f__integer__(0),sK5,sK4),sK24(f__integer__(0),sK5,sK4))
| ~ sP1(f__integer__(0),sK5,sK4)
| ~ spl40_3 ),
inference(superposition,[],[f146,f449]) ).
tff(f451,plain,
( ~ sP1(f__integer__(0),sK5,sK4)
| ~ spl40_3 ),
inference(forward_subsumption_resolution,[],[f450,f226]) ).
tff(f452,plain,
( $false
| ~ spl40_3 ),
inference(forward_subsumption_resolution,[],[f451,f251]) ).
tff(f453,plain,
~ spl40_3,
inference(avatar_contradiction_clause,[],[f452]) ).
tff(f602,plain,
( ( sK5 = sK16(sK4,sK5,f__integer__(0)) )
| ~ spl40_1
| ~ spl40_5 ),
inference(forward_demodulation,[],[f261,f243]) ).
tff(f604,plain,
( in0(sK15(sK4,sK5,f__integer__(0)),sK16(sK4,sK5,f__integer__(0)))
| spl40_2
| spl40_3 ),
inference(unit_resulting_resolution,[],[f139,f228,f250,f246]) ).
tff(f609,plain,
( in0(sK15(sK4,sK5,f__integer__(0)),sK5)
| ~ spl40_1
| spl40_2
| spl40_3
| ~ spl40_5 ),
inference(forward_demodulation,[],[f604,f602]) ).
tff(f647,plain,
( ( sK4 = sK15(sK4,sK5,f__integer__(0)) )
| ~ spl40_4
| ~ spl40_6 ),
inference(superposition,[],[f256,f266]) ).
tff(f654,plain,
( person(sK15(sK4,sK5,f__integer__(0)))
| ~ spl40_1
| spl40_2
| spl40_3
| ~ spl40_5 ),
inference(resolution,[],[f609,f106]) ).
tff(f659,plain,
( person(sK4)
| ~ spl40_1
| spl40_2
| spl40_3
| ~ spl40_4
| ~ spl40_5
| ~ spl40_6 ),
inference(forward_demodulation,[],[f654,f647]) ).
tff(f662,plain,
( $false
| ~ spl40_1
| spl40_2
| spl40_3
| ~ spl40_4
| ~ spl40_5
| ~ spl40_6 ),
inference(forward_subsumption_resolution,[],[f659,f117]) ).
tff(f663,plain,
( ~ spl40_1
| spl40_2
| spl40_3
| ~ spl40_4
| ~ spl40_5
| ~ spl40_6 ),
inference(avatar_contradiction_clause,[],[f662]) ).
tff(f666,plain,
( ( sK34(sK5,f__integer__(0),sK4) = sK33(sK5,f__integer__(0),sK4) )
| ~ spl40_2 ),
inference(unit_resulting_resolution,[],[f154,f247]) ).
tff(f667,plain,
( ~ $less(sK35(sK5,f__integer__(0),sK4),sK36(sK5,f__integer__(0),sK4))
| ~ spl40_2 ),
inference(unit_resulting_resolution,[],[f155,f247]) ).
tff(f674,plain,
( ( sK25(sK5,f__integer__(0),sK4) = sK34(sK5,f__integer__(0),sK4) )
| ~ spl40_2 ),
inference(unit_resulting_resolution,[],[f162,f247]) ).
tff(f676,plain,
( ( 1 = sK32(sK5,f__integer__(0),sK4) )
| ~ spl40_2 ),
inference(unit_resulting_resolution,[],[f164,f247]) ).
tff(f687,plain,
( ( 0 = sK36(sK5,f__integer__(0),sK4) )
| ~ spl40_2 ),
inference(resolution,[],[f247,f156]) ).
tff(f688,plain,
( ( sK33(sK5,f__integer__(0),sK4) = f__integer__(sK35(sK5,f__integer__(0),sK4)) )
| ~ spl40_2 ),
inference(resolution,[],[f247,f158]) ).
tff(f693,plain,
( ( f__integer__(0) = f__integer__($sum(sK31(sK5,f__integer__(0),sK4),sK32(sK5,f__integer__(0),sK4))) )
| ~ spl40_2 ),
inference(resolution,[],[f247,f163]) ).
tff(f695,plain,
( ( sK25(sK5,f__integer__(0),sK4) = f__integer__(sK31(sK5,f__integer__(0),sK4)) )
| ~ spl40_2 ),
inference(resolution,[],[f247,f165]) ).
tff(f709,plain,
( ( sK34(sK5,f__integer__(0),sK4) = f__integer__(sK35(sK5,f__integer__(0),sK4)) )
| ~ spl40_2 ),
inference(forward_demodulation,[],[f666,f688]) ).
tff(f824,plain,
( p__less_equal__(f__integer__(sK36(sK5,f__integer__(0),sK4)),f__integer__(sK35(sK5,f__integer__(0),sK4)))
| ~ spl40_2 ),
inference(unit_resulting_resolution,[],[f133,f667]) ).
tff(f878,definition,
( spl40_24
<=> $less(sK31(sK5,f__integer__(0),sK4),0) ),
introduced(definition,[new_symbols(definition,[spl40_24])],[avatar_definition]) ).
tff(f879,plain,
( ~ $less(sK31(sK5,f__integer__(0),sK4),0)
| spl40_24 ),
inference(avatar_component_clause,[],[f878]) ).
tff(f880,plain,
( $less(sK31(sK5,f__integer__(0),sK4),0)
| ~ spl40_24 ),
inference(avatar_component_clause,[],[f878]) ).
tff(f904,plain,
( ( sK25(sK5,f__integer__(0),sK4) = f__integer__(sK35(sK5,f__integer__(0),sK4)) )
| ~ spl40_2 ),
inference(superposition,[],[f674,f709]) ).
tff(f911,plain,
( ( 0 = $sum(sK31(sK5,f__integer__(0),sK4),sK32(sK5,f__integer__(0),sK4)) )
| ~ spl40_2 ),
inference(unit_resulting_resolution,[],[f123,f693]) ).
tff(f931,plain,
( ( 0 = $sum(sK31(sK5,f__integer__(0),sK4),1) )
| ~ spl40_2 ),
inference(forward_demodulation,[],[f911,f676]) ).
tff(f942,plain,
( ( 0 = $sum(1,sK31(sK5,f__integer__(0),sK4)) )
| ~ spl40_2 ),
inference(forward_demodulation,[],[f931,f31]) ).
tff(f1249,plain,
( $less(0,$sum(sK31(sK5,f__integer__(0),sK4),1))
| spl40_24 ),
inference(unit_resulting_resolution,[],[f40,f879]) ).
tff(f1264,plain,
( $less(0,$sum(1,sK31(sK5,f__integer__(0),sK4)))
| spl40_24 ),
inference(forward_demodulation,[],[f1249,f31]) ).
tff(f1268,plain,
( $less(0,0)
| ~ spl40_2
| spl40_24 ),
inference(forward_demodulation,[],[f1264,f942]) ).
tff(f1269,plain,
( $false
| ~ spl40_2
| spl40_24 ),
inference(evaluation,[],[f1268]) ).
tff(f1270,plain,
( ~ spl40_2
| spl40_24 ),
inference(avatar_contradiction_clause,[],[f1269]) ).
tff(f1279,plain,
( ~ p__less_equal__(f__integer__(0),f__integer__(sK31(sK5,f__integer__(0),sK4)))
| ~ spl40_24 ),
inference(unit_resulting_resolution,[],[f134,f880]) ).
tff(f1294,plain,
( ~ p__less_equal__(f__integer__(0),sK25(sK5,f__integer__(0),sK4))
| ~ spl40_2
| ~ spl40_24 ),
inference(forward_demodulation,[],[f1279,f695]) ).
tff(f1302,plain,
( p__less_equal__(f__integer__(0),f__integer__(sK35(sK5,f__integer__(0),sK4)))
| ~ spl40_2 ),
inference(forward_demodulation,[],[f824,f687]) ).
tff(f1330,plain,
( ~ p__less_equal__(f__integer__(0),f__integer__(sK35(sK5,f__integer__(0),sK4)))
| ~ spl40_2
| ~ spl40_24 ),
inference(forward_demodulation,[],[f1294,f904]) ).
tff(f1341,plain,
( $false
| ~ spl40_2
| ~ spl40_24 ),
inference(forward_subsumption_resolution,[],[f1330,f1302]) ).
tff(f1342,plain,
( ~ spl40_2
| ~ spl40_24 ),
inference(avatar_contradiction_clause,[],[f1341]) ).
cnf(s1,plain,
( spl40_1
| spl40_2
| spl40_3 ),
inference(sat_conversion,[],[f252]) ).
cnf(s2,plain,
( spl40_2
| spl40_3
| spl40_4 ),
inference(sat_conversion,[],[f257]) ).
cnf(s3,plain,
( spl40_2
| spl40_3
| spl40_5 ),
inference(sat_conversion,[],[f262]) ).
cnf(s4,plain,
( spl40_2
| spl40_3
| spl40_6 ),
inference(sat_conversion,[],[f267]) ).
cnf(s11,plain,
~ spl40_3,
inference(sat_conversion,[],[f453]) ).
cnf(s25,plain,
( ~ spl40_1
| spl40_2
| spl40_3
| ~ spl40_4
| ~ spl40_5
| ~ spl40_6 ),
inference(sat_conversion,[],[f663]) ).
cnf(s62,plain,
( ~ spl40_2
| spl40_24 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s68,plain,
( ~ spl40_2
| ~ spl40_24 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s73,plain,
( spl40_2
| spl40_6 ),
inference(rat,[],[s4,s11]) ).
cnf(s74,plain,
( spl40_2
| spl40_5 ),
inference(rat,[],[s3,s11]) ).
cnf(s75,plain,
( spl40_2
| spl40_4 ),
inference(rat,[],[s2,s11]) ).
cnf(s76,plain,
( spl40_1
| spl40_2 ),
inference(rat,[],[s1,s11]) ).
cnf(s77,plain,
~ spl40_2,
inference(rat,[],[s62,s68]) ).
cnf(s78,plain,
spl40_6,
inference(rat,[],[s73,s77]) ).
cnf(s79,plain,
spl40_5,
inference(rat,[],[s74,s77]) ).
cnf(s80,plain,
spl40_4,
inference(rat,[],[s75,s77]) ).
cnf(s81,plain,
spl40_1,
inference(rat,[],[s76,s77]) ).
cnf(s82,plain,
$false,
inference(rat,[],[s25,s78,s79,s77,s11,s81,s80]) ).
tff(f1375,plain,
$false,
inference(avatar_sat_refutation,[],[s82]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX087_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n017.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 14:56:06 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 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.66/1.22 % (3613299)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.66/1.22 % (3613304)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1568495087:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.66/1.22 % (3613304)Refutation not found, incomplete strategy
% 3.66/1.22 % (3613304)------------------------------
% 3.66/1.22 % (3613304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.66/1.22 % (3613304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.66/1.22 % (3613304)CaDiCaL version: 2.1.3
% 3.66/1.22 % (3613304)Termination reason: Refutation not found, incomplete strategy
% 3.66/1.22 % (3613304)Time elapsed: 0.019 s
% 3.66/1.22 % (3613304)Peak memory usage: 116 MB
% 3.66/1.22 % (3613304)Instructions burned: 10 (million)
% 3.66/1.22 % (3613305)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3725279097:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.66/1.22 % (3613309)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3325484190:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.66/1.22 % (3613308)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2162507330:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.66/1.22 % (3613307)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1184451099:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.66/1.22 % (3613306)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=314798756:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.66/1.22 % (3613310)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4125671679:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.66/1.22 % (3613308)Instruction limit reached!
% 3.66/1.22 % (3613308)------------------------------
% 3.66/1.22 % (3613308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.66/1.22 % (3613308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.66/1.22 % (3613308)CaDiCaL version: 2.1.3
% 3.66/1.22 % (3613308)Termination reason: Instruction limit
% 3.66/1.22 % (3613308)Termination phase: Saturation
% 3.66/1.22 % (3613308)Time elapsed: 0.003 s
% 3.66/1.22 % (3613308)Peak memory usage: 87 MB
% 3.66/1.22 % (3613308)Instructions burned: 4 (million)
% 3.66/1.22 % (3613307)Instruction limit reached!
% 3.66/1.22 % (3613307)------------------------------
% 3.66/1.22 % (3613307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.66/1.22 % (3613307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.66/1.22 % (3613307)CaDiCaL version: 2.1.3
% 3.66/1.22 % (3613307)Termination reason: Instruction limit
% 3.66/1.22 % (3613307)Termination phase: Saturation
% 3.66/1.22 % (3613307)Time elapsed: 0.005 s
% 3.66/1.22 % (3613307)Peak memory usage: 88 MB
% 3.66/1.22 % (3613307)Instructions burned: 7 (million)
% 3.66/1.22 % (3613310)Instruction limit reached!
% 3.66/1.22 % (3613310)------------------------------
% 3.66/1.22 % (3613310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.66/1.22 % (3613310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.66/1.22 % (3613310)CaDiCaL version: 2.1.3
% 3.66/1.22 % (3613310)Termination reason: Instruction limit
% 3.66/1.22 % (3613310)Termination phase: Saturation
% 3.66/1.22 % (3613310)Time elapsed: 0.047 s
% 3.66/1.22 % (3613310)Peak memory usage: 116 MB
% 3.66/1.22 % (3613310)Instructions burned: 33 (million)
% 3.66/1.22 % (3613309)Instruction limit reached!
% 3.66/1.22 % (3613309)------------------------------
% 3.66/1.22 % (3613309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.66/1.22 % (3613309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.66/1.22 % (3613309)CaDiCaL version: 2.1.3
% 3.66/1.22 % (3613309)Termination reason: Instruction limit
% 3.66/1.22 % (3613309)Termination phase: Saturation
% 3.66/1.22 % (3613309)Time elapsed: 0.055 s
% 3.66/1.22 % (3613309)Peak memory usage: 116 MB
% 3.66/1.22 % (3613309)Instructions burned: 46 (million)
% 3.66/1.22 % (3613304)------------------------------
% 3.66/1.22 % (3613304)------------------------------
% 3.66/1.22 % (3613306)Instruction limit reached!
% 3.66/1.22 % (3613306)------------------------------
% 3.66/1.22 % (3613306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.66/1.22 % (3613306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.37 % (3613306)CaDiCaL version: 2.1.3
% 4.58/1.37 % (3613306)Termination reason: Instruction limit
% 4.58/1.37 % (3613306)Termination phase: Saturation
% 4.58/1.37 % (3613306)Time elapsed: 0.125 s
% 4.58/1.37 % (3613306)Peak memory usage: 116 MB
% 4.58/1.37 % (3613306)Instructions burned: 202 (million)
% 4.58/1.37 % (3613318)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3935044369:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.58/1.37 % (3613319)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=1502090649:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.58/1.37 % (3613318)Instruction limit reached!
% 4.58/1.37 % (3613318)------------------------------
% 4.58/1.37 % (3613318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.37 % (3613318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.37 % (3613318)CaDiCaL version: 2.1.3
% 4.58/1.37 % (3613318)Termination reason: Instruction limit
% 4.58/1.37 % (3613318)Termination phase: Saturation
% 4.58/1.37 % (3613318)Time elapsed: 0.011 s
% 4.58/1.37 % (3613318)Peak memory usage: 88 MB
% 4.58/1.37 % (3613318)Instructions burned: 15 (million)
% 4.58/1.37 % (3613319)Instruction limit reached!
% 4.58/1.37 % (3613319)------------------------------
% 4.58/1.37 % (3613319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.37 % (3613319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.37 % (3613319)CaDiCaL version: 2.1.3
% 4.58/1.37 % (3613319)Termination reason: Instruction limit
% 4.58/1.37 % (3613319)Termination phase: Property scanning
% 4.58/1.37 % (3613319)Time elapsed: 0.012 s
% 4.58/1.37 % (3613319)Peak memory usage: 86 MB
% 4.58/1.37 % (3613319)Instructions burned: 30 (million)
% 4.58/1.37 % (3613320)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2817720168:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 4.58/1.37 % (3613305)Instruction limit reached!
% 4.58/1.37 % (3613305)------------------------------
% 4.58/1.37 % (3613305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.37 % (3613305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.37 % (3613305)CaDiCaL version: 2.1.3
% 4.58/1.37 % (3613305)Termination reason: Instruction limit
% 4.58/1.37 % (3613305)Termination phase: Saturation
% 4.58/1.37 % (3613305)Time elapsed: 0.198 s
% 4.58/1.37 % (3613305)Peak memory usage: 117 MB
% 4.58/1.37 % (3613305)Instructions burned: 307 (million)
% 4.58/1.37 % (3613320)Instruction limit reached!
% 4.58/1.37 % (3613320)------------------------------
% 4.58/1.37 % (3613320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.37 % (3613320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.37 % (3613320)CaDiCaL version: 2.1.3
% 4.58/1.37 % (3613320)Termination reason: Instruction limit
% 4.58/1.37 % (3613320)Termination phase: Saturation
% 4.58/1.37 % (3613320)Time elapsed: 0.011 s
% 4.58/1.37 % (3613320)Peak memory usage: 90 MB
% 4.58/1.37 % (3613320)Instructions burned: 16 (million)
% 4.58/1.37 % (3613321)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=838317456:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.58/1.37 % (3613322)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=861956057:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.58/1.37 % (3613322)Refutation not found, incomplete strategy
% 4.58/1.37 % (3613322)------------------------------
% 4.58/1.37 % (3613322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.58/1.37 % (3613322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.58/1.37 % (3613322)CaDiCaL version: 2.1.3
% 4.58/1.37 % (3613322)Termination reason: Refutation not found, incomplete strategy
% 4.58/1.37 % (3613322)Time elapsed: 0.002 s
% 4.58/1.37 % (3613322)Peak memory usage: 89 MB
% 4.58/1.37 % (3613322)Instructions burned: 5 (million)
% 4.58/1.37 % (3613321)Instruction limit reached!
% 4.58/1.37 % (3613321)------------------------------
% 4.58/1.37 % (3613321)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.38/1.52 % (3613321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.52 % (3613321)CaDiCaL version: 2.1.3
% 5.38/1.52 % (3613321)Termination reason: Instruction limit
% 5.38/1.52 % (3613321)Termination phase: Saturation
% 5.38/1.52 % (3613321)Time elapsed: 0.020 s
% 5.38/1.52 % (3613321)Peak memory usage: 89 MB
% 5.38/1.52 % (3613321)Instructions burned: 25 (million)
% 5.38/1.52 % (3613323)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=158233154:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 5.38/1.52 % (3613326)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2836099754:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 5.38/1.52 % (3613327)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=782861571:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 5.38/1.52 % (3613326)Instruction limit reached!
% 5.38/1.52 % (3613326)------------------------------
% 5.38/1.52 % (3613326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.38/1.52 % (3613326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.52 % (3613326)CaDiCaL version: 2.1.3
% 5.38/1.52 % (3613326)Termination reason: Instruction limit
% 5.38/1.52 % (3613326)Termination phase: Property scanning
% 5.38/1.52 % (3613326)Time elapsed: 0.002 s
% 5.38/1.52 % (3613326)Peak memory usage: 86 MB
% 5.38/1.52 % (3613326)Instructions burned: 2 (million)
% 5.38/1.52 % (3613327)Refutation not found, incomplete strategy
% 5.38/1.52 % (3613327)------------------------------
% 5.38/1.52 % (3613327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.38/1.52 % (3613327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.52 % (3613327)CaDiCaL version: 2.1.3
% 5.38/1.52 % (3613327)Termination reason: Refutation not found, incomplete strategy
% 5.38/1.52 % (3613327)Time elapsed: 0.002 s
% 5.38/1.52 % (3613327)Peak memory usage: 89 MB
% 5.38/1.52 % (3613327)Instructions burned: 1 (million)
% 5.38/1.52 % (3613323)Instruction limit reached!
% 5.38/1.52 % (3613323)------------------------------
% 5.38/1.52 % (3613323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.38/1.52 % (3613323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.52 % (3613323)CaDiCaL version: 2.1.3
% 5.38/1.52 % (3613323)Termination reason: Instruction limit
% 5.38/1.52 % (3613323)Termination phase: Saturation
% 5.38/1.52 % (3613323)Time elapsed: 0.043 s
% 5.38/1.52 % (3613323)Peak memory usage: 89 MB
% 5.38/1.52 % (3613323)Instructions burned: 85 (million)
% 5.38/1.52 % (3613330)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2010988915:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 5.38/1.52 % (3613331)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1611031672:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 5.38/1.52 % (3613330)Instruction limit reached!
% 5.38/1.52 % (3613330)------------------------------
% 5.38/1.52 % (3613330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.38/1.52 % (3613330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.52 % (3613330)CaDiCaL version: 2.1.3
% 5.38/1.52 % (3613330)Termination reason: Instruction limit
% 5.38/1.52 % (3613330)Termination phase: Saturation
% 5.38/1.52 % (3613330)Time elapsed: 0.003 s
% 5.38/1.52 % (3613330)Peak memory usage: 87 MB
% 5.38/1.52 % (3613330)Instructions burned: 4 (million)
% 5.38/1.52 % (3613333)lrs+10_1_thi=all:si=on:fd=off:random_seed=1941574486:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 5.38/1.52 % (3613322)------------------------------
% 5.38/1.52 % (3613322)------------------------------
% 5.38/1.52 % (3613333)Instruction limit reached!
% 5.38/1.52 % (3613333)------------------------------
% 5.38/1.52 % (3613333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.38/1.52 % (3613333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.38/1.52 % (3613333)CaDiCaL version: 2.1.3
% 5.38/1.52 % (3613333)Termination reason: Instruction limit
% 5.38/1.52 % (3613333)Termination phase: Saturation
% 5.38/1.52 % (3613333)Time elapsed: 0.064 s
% 5.38/1.52 % (3613333)Peak memory usage: 116 MB
% 5.38/1.52 % (3613333)Instructions burned: 54 (million)
% 5.38/1.52 % (3613331)Instruction limit reached!
% 5.38/1.52 % (3613331)------------------------------
% 5.38/1.52 % (3613331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.72 % (3613331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.72 % (3613331)CaDiCaL version: 2.1.3
% 6.76/1.72 % (3613331)Termination reason: Instruction limit
% 6.76/1.72 % (3613331)Termination phase: Saturation
% 6.76/1.72 % (3613331)Time elapsed: 0.097 s
% 6.76/1.72 % (3613331)Peak memory usage: 134 MB
% 6.76/1.72 % (3613331)Instructions burned: 67 (million)
% 6.76/1.72 % (3613337)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=3652416965:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 6.76/1.72 % (3613337)Instruction limit reached!
% 6.76/1.72 % (3613337)------------------------------
% 6.76/1.72 % (3613337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.72 % (3613337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.72 % (3613337)CaDiCaL version: 2.1.3
% 6.76/1.72 % (3613337)Termination reason: Instruction limit
% 6.76/1.72 % (3613337)Termination phase: Saturation
% 6.76/1.72 % (3613337)Time elapsed: 0.006 s
% 6.76/1.72 % (3613337)Peak memory usage: 88 MB
% 6.76/1.72 % (3613337)Instructions burned: 8 (million)
% 6.76/1.72 % (3613340)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=2704392885:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 6.76/1.72 % (3613340)Instruction limit reached!
% 6.76/1.72 % (3613340)------------------------------
% 6.76/1.72 % (3613340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.72 % (3613340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.72 % (3613340)CaDiCaL version: 2.1.3
% 6.76/1.72 % (3613340)Termination reason: Instruction limit
% 6.76/1.72 % (3613340)Termination phase: Property scanning
% 6.76/1.72 % (3613340)Time elapsed: 0.002 s
% 6.76/1.72 % (3613340)Peak memory usage: 86 MB
% 6.76/1.72 % (3613340)Instructions burned: 2 (million)
% 6.76/1.72 % (3613341)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2977266963:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 6.76/1.72 % (3613341)Instruction limit reached!
% 6.76/1.72 % (3613341)------------------------------
% 6.76/1.72 % (3613341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.72 % (3613341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.72 % (3613341)CaDiCaL version: 2.1.3
% 6.76/1.72 % (3613341)Termination reason: Instruction limit
% 6.76/1.72 % (3613341)Termination phase: Property scanning
% 6.76/1.72 % (3613341)Time elapsed: 0.002 s
% 6.76/1.72 % (3613341)Peak memory usage: 86 MB
% 6.76/1.72 % (3613341)Instructions burned: 2 (million)
% 6.76/1.72 % (3613343)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=398603783:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi)
% 6.76/1.72 % (3613343)Instruction limit reached!
% 6.76/1.72 % (3613343)------------------------------
% 6.76/1.72 % (3613343)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.72 % (3613343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.72 % (3613343)CaDiCaL version: 2.1.3
% 6.76/1.72 % (3613343)Termination reason: Instruction limit
% 6.76/1.72 % (3613343)Termination phase: Saturation
% 6.76/1.72 % (3613343)Time elapsed: 0.050 s
% 6.76/1.72 % (3613343)Peak memory usage: 116 MB
% 6.76/1.72 % (3613343)Instructions burned: 128 (million)
% 6.76/1.72 % (3613327)------------------------------
% 6.76/1.72 % (3613327)------------------------------
% 6.76/1.72 % (3613346)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2765616359:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi)
% 6.76/1.72 % (3613344)dis+10_1_si=on:random_seed=2431084151:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 6.76/1.72 % (3613346)Refutation not found, incomplete strategy
% 6.76/1.72 % (3613346)------------------------------
% 6.76/1.72 % (3613346)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.76/1.72 % (3613346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.76/1.72 % (3613346)CaDiCaL version: 2.1.3
% 6.76/1.72 % (3613346)Termination reason: Refutation not found, incomplete strategy
% 6.76/1.72 % (3613346)Time elapsed: 0.005 s
% 6.76/1.72 % (3613346)Peak memory usage: 88 MB
% 6.76/1.72 % (3613346)Instructions burned: 6 (million)
% 6.76/1.72 % (3613344)Instruction limit reached!
% 8.09/1.96 % (3613344)------------------------------
% 8.09/1.96 % (3613344)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/1.96 % (3613344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.96 % (3613344)CaDiCaL version: 2.1.3
% 8.09/1.96 % (3613344)Termination reason: Instruction limit
% 8.09/1.96 % (3613344)Termination phase: Saturation
% 8.09/1.96 % (3613344)Time elapsed: 0.008 s
% 8.09/1.96 % (3613344)Peak memory usage: 88 MB
% 8.09/1.96 % (3613344)Instructions burned: 10 (million)
% 8.09/1.96 % (3613347)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=2973757889: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)
% 8.09/1.96 % (3613352)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3223568984:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2994 on theBenchmark for (2994ds/8Mi)
% 8.09/1.96 % (3613349)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=78166767:i=2:fsr=off:rtra=on:inst=on_2994 on theBenchmark for (2994ds/2Mi)
% 8.09/1.96 % (3613349)Instruction limit reached!
% 8.09/1.96 % (3613349)------------------------------
% 8.09/1.96 % (3613349)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/1.96 % (3613349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.96 % (3613349)CaDiCaL version: 2.1.3
% 8.09/1.96 % (3613349)Termination reason: Instruction limit
% 8.09/1.96 % (3613349)Termination phase: Property scanning
% 8.09/1.96 % (3613349)Time elapsed: 0.002 s
% 8.09/1.96 % (3613349)Peak memory usage: 86 MB
% 8.09/1.96 % (3613349)Instructions burned: 2 (million)
% 8.09/1.96 % (3613352)Instruction limit reached!
% 8.09/1.96 % (3613352)------------------------------
% 8.09/1.96 % (3613352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/1.96 % (3613352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.96 % (3613352)CaDiCaL version: 2.1.3
% 8.09/1.96 % (3613352)Termination reason: Instruction limit
% 8.09/1.96 % (3613352)Termination phase: Saturation
% 8.09/1.96 % (3613352)Time elapsed: 0.007 s
% 8.09/1.96 % (3613352)Peak memory usage: 89 MB
% 8.09/1.96 % (3613352)Instructions burned: 9 (million)
% 8.09/1.96 % (3613353)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1948197795:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi)
% 8.09/1.96 % (3613353)Refutation not found, incomplete strategy
% 8.09/1.96 % (3613353)------------------------------
% 8.09/1.96 % (3613353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/1.96 % (3613353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.96 % (3613353)CaDiCaL version: 2.1.3
% 8.09/1.96 % (3613353)Termination reason: Refutation not found, incomplete strategy
% 8.09/1.96 % (3613353)Time elapsed: 0.002 s
% 8.09/1.96 % (3613353)Peak memory usage: 88 MB
% 8.09/1.96 % (3613353)Instructions burned: 5 (million)
% 8.09/1.96 % (3613347)Instruction limit reached!
% 8.09/1.96 % (3613347)------------------------------
% 8.09/1.96 % (3613347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/1.96 % (3613347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.09/1.96 % (3613347)CaDiCaL version: 2.1.3
% 8.09/1.96 % (3613347)Termination reason: Instruction limit
% 8.09/1.96 % (3613347)Termination phase: Saturation
% 8.09/1.96 % (3613347)Time elapsed: 0.029 s
% 8.09/1.96 % (3613347)Peak memory usage: 89 MB
% 8.09/1.96 % (3613347)Instructions burned: 35 (million)
% 8.09/1.96 % (3613356)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=1838671703:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 8.09/1.96 % (3613358)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2202235204:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 8.09/1.96 % (3613361)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=4144389309:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 8.09/1.96 % (3613356)Instruction limit reached!
% 8.09/1.96 % (3613356)------------------------------
% 8.09/1.96 % (3613356)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.09/1.96 % (3613356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.03 % (3613356)CaDiCaL version: 2.1.3
% 8.72/2.03 % (3613356)Termination reason: Instruction limit
% 8.72/2.03 % (3613356)Termination phase: Saturation
% 8.72/2.03 % (3613356)Time elapsed: 0.029 s
% 8.72/2.03 % (3613356)Peak memory usage: 112 MB
% 8.72/2.03 % (3613356)Instructions burned: 13 (million)
% 8.72/2.03 % (3613361)Instruction limit reached!
% 8.72/2.03 % (3613361)------------------------------
% 8.72/2.03 % (3613361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.03 % (3613361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.03 % (3613361)CaDiCaL version: 2.1.3
% 8.72/2.03 % (3613361)Termination reason: Instruction limit
% 8.72/2.03 % (3613361)Termination phase: Saturation
% 8.72/2.03 % (3613361)Time elapsed: 0.009 s
% 8.72/2.03 % (3613361)Peak memory usage: 88 MB
% 8.72/2.03 % (3613361)Instructions burned: 11 (million)
% 8.72/2.03 % (3613358)Refutation not found, incomplete strategy
% 8.72/2.03 % (3613358)------------------------------
% 8.72/2.03 % (3613358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613358)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613358)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.04 % (3613358)Time elapsed: 0.029 s
% 8.72/2.04 % (3613358)Peak memory usage: 115 MB
% 8.72/2.04 % (3613358)Instructions burned: 7 (million)
% 8.72/2.04 % (3613362)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=1722026575:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi)
% 8.72/2.04 % (3613364)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=2815082342:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2992 on theBenchmark for (2992ds/75Mi)
% 8.72/2.04 % (3613353)------------------------------
% 8.72/2.04 % (3613353)------------------------------
% 8.72/2.04 % (3613364)Instruction limit reached!
% 8.72/2.04 % (3613364)------------------------------
% 8.72/2.04 % (3613364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613364)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613364)Termination reason: Instruction limit
% 8.72/2.04 % (3613364)Termination phase: Saturation
% 8.72/2.04 % (3613364)Time elapsed: 0.060 s
% 8.72/2.04 % (3613364)Peak memory usage: 90 MB
% 8.72/2.04 % (3613364)Instructions burned: 76 (million)
% 8.72/2.04 % (3613346)------------------------------
% 8.72/2.04 % (3613346)------------------------------
% 8.72/2.04 % (3613362)Instruction limit reached!
% 8.72/2.04 % (3613362)------------------------------
% 8.72/2.04 % (3613362)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613362)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613362)Termination reason: Instruction limit
% 8.72/2.04 % (3613362)Termination phase: Saturation
% 8.72/2.04 % (3613362)Time elapsed: 0.098 s
% 8.72/2.04 % (3613362)Peak memory usage: 133 MB
% 8.72/2.04 % (3613362)Instructions burned: 71 (million)
% 8.72/2.04 % (3613372)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=369085468:i=131:rtra=on_2991 on theBenchmark for (2991ds/131Mi)
% 8.72/2.04 % (3613370)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3949963494:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2991 on theBenchmark for (2991ds/130Mi)
% 8.72/2.04 % (3613368)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=4170257437:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi)
% 8.72/2.04 % (3613372)Instruction limit reached!
% 8.72/2.04 % (3613372)------------------------------
% 8.72/2.04 % (3613372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613372)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613372)Termination reason: Instruction limit
% 8.72/2.04 % (3613372)Termination phase: Saturation
% 8.72/2.04 % (3613372)Time elapsed: 0.076 s
% 8.72/2.04 % (3613372)Peak memory usage: 134 MB
% 8.72/2.04 % (3613372)Instructions burned: 134 (million)
% 8.72/2.04 % (3613370)Instruction limit reached!
% 8.72/2.04 % (3613370)------------------------------
% 8.72/2.04 % (3613370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613370)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613370)Termination reason: Instruction limit
% 8.72/2.04 % (3613370)Termination phase: Saturation
% 8.72/2.04 % (3613370)Time elapsed: 0.079 s
% 8.72/2.04 % (3613370)Peak memory usage: 113 MB
% 8.72/2.04 % (3613370)Instructions burned: 130 (million)
% 8.72/2.04 % (3613373)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=588299374:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi)
% 8.72/2.04 % (3613374)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4284548092:i=307:rtra=on:gtg=exists_top_2990 on theBenchmark for (2990ds/307Mi)
% 8.72/2.04 % (3613375)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1792216696:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2990 on theBenchmark for (2990ds/598Mi)
% 8.72/2.04 % (3613358)------------------------------
% 8.72/2.04 % (3613358)------------------------------
% 8.72/2.04 % (3613374)First to succeed.
% 8.72/2.04 % (3613374)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3613299"
% 8.72/2.04 % (3613373)Instruction limit reached!
% 8.72/2.04 % (3613373)------------------------------
% 8.72/2.04 % (3613373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613373)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613373)Termination reason: Instruction limit
% 8.72/2.04 % (3613373)Termination phase: Saturation
% 8.72/2.04 % (3613373)Time elapsed: 0.071 s
% 8.72/2.04 % (3613373)Peak memory usage: 134 MB
% 8.72/2.04 % (3613373)Instructions burned: 41 (million)
% 8.72/2.04 % (3613368)Instruction limit reached!
% 8.72/2.04 % (3613368)------------------------------
% 8.72/2.04 % (3613368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613368)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613368)Termination reason: Instruction limit
% 8.72/2.04 % (3613368)Termination phase: Saturation
% 8.72/2.04 % (3613368)Time elapsed: 0.187 s
% 8.72/2.04 % (3613368)Peak memory usage: 90 MB
% 8.72/2.04 % (3613368)Instructions burned: 295 (million)
% 8.72/2.04 % (3613379)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=3503811170:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 8.72/2.04 % (3613381)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=3036000758:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi)
% 8.72/2.04 % (3613381)Refutation not found, incomplete strategy
% 8.72/2.04 % (3613381)------------------------------
% 8.72/2.04 % (3613381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613381)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613381)Termination reason: Refutation not found, incomplete strategy
% 8.72/2.04 % (3613381)Time elapsed: 0.028 s
% 8.72/2.04 % (3613381)Peak memory usage: 115 MB
% 8.72/2.04 % (3613381)Instructions burned: 7 (million)
% 8.72/2.04 % (3613384)dis+10_1_si=on:random_seed=2081481190:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi)
% 8.72/2.04 % (3613385)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=2085758906:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi)
% 8.72/2.04 % (3613379)Instruction limit reached!
% 8.72/2.04 % (3613379)------------------------------
% 8.72/2.04 % (3613379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.72/2.04 % (3613379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.72/2.04 % (3613379)CaDiCaL version: 2.1.3
% 8.72/2.04 % (3613379)Termination reason: Instruction limit
% 8.72/2.04 % (3613379)Termination phase: Saturation
% 8.72/2.04 % (3613379)Time elapsed: 0.095 s
% 8.72/2.04 % (3613379)Peak memory usage: 117 MB
% 8.72/2.04 % (3613379)Instructions burned: 132 (million)
% 8.72/2.04 % (3613386)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=2931439630:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi)
% 8.72/2.04 % (3613374)Refutation found. Thanks to Tanya!
% 8.72/2.04 % SZS status Theorem for theBenchmark
% 8.72/2.04 % SZS output start Proof for theBenchmark
% See solution above
% 10.31/2.23 % (3613374)------------------------------
% 10.31/2.23 % (3613374)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.31/2.23 % (3613374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.31/2.23 % (3613374)CaDiCaL version: 2.1.3
% 10.31/2.23 % (3613374)Termination reason: Refutation
% 10.31/2.23 % (3613374)Time elapsed: 0.035 s
% 10.31/2.23 % (3613374)Peak memory usage: 91 MB
% 10.31/2.23 % (3613374)Instructions burned: 52 (million)
% 10.31/2.23 % (3613374)------------------------------
% 10.31/2.23 % (3613374)------------------------------
% 10.31/2.23 % (3613299)Success in time 1.375 s
% 10.31/2.23 % Vampire exiting
%------------------------------------------------------------------------------