%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX088_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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 3.50s 1.16s
% Output : Refutation 4.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 17
% Syntax : Number of formulae : 127 ( 24 unt; 0 typ; 13 def)
% Number of atoms : 572 ( 264 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 656 ( 211 ~; 242 |; 177 &)
% ( 17 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 175 ( 74 atm; 0 fun; 35 num; 66 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 : 33 ( 29 usr; 14 prp; 0-3 aty)
% Number of functors : 51 ( 50 usr; 14 con; 0-3 aty)
% Number of variables : 317 ( 177 !; 140 ?; 317 :)
% 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 * general * general ) > general ).
tff(func_def_11,type,
sK4: ( general * general * general ) > general ).
tff(func_def_12,type,
sK5: ( general * general * general ) > general ).
tff(func_def_13,type,
sK6: ( general * general * general ) > general ).
tff(func_def_14,type,
sK7: ( general * general * general ) > general ).
tff(func_def_15,type,
sK8: ( general * general * general ) > general ).
tff(func_def_16,type,
sK9: ( general * general * general ) > general ).
tff(func_def_17,type,
sK10: ( general * general * general ) > general ).
tff(func_def_18,type,
sK11: ( general * general * general ) > general ).
tff(func_def_19,type,
sK12: ( general * 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 ) > $int ).
tff(func_def_23,type,
sK16: ( general * general * general ) > $int ).
tff(func_def_24,type,
sK17: ( general * general * general ) > $int ).
tff(func_def_25,type,
sK18: ( general * general * general ) > $int ).
tff(func_def_26,type,
sK19: ( general * general * general ) > $int ).
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 ) > $int ).
tff(func_def_36,type,
sK29: ( general * general * general ) > $int ).
tff(func_def_37,type,
sK30: ( general * general ) > general ).
tff(func_def_38,type,
sK31: ( general * general ) > general ).
tff(func_def_39,type,
sK32: ( general * general ) > general ).
tff(func_def_40,type,
sK33: ( general * general ) > general ).
tff(func_def_41,type,
sK34: ( general * general ) > general ).
tff(func_def_42,type,
sK35: ( general * general ) > general ).
tff(func_def_43,type,
sK36: general > symbol ).
tff(func_def_44,type,
sK37: general > $int ).
tff(func_def_45,type,
sK38: general ).
tff(func_def_46,type,
sK39: general ).
tff(func_def_47,type,
sK40: general ).
tff(func_def_48,type,
sK41: general ).
tff(func_def_49,type,
sK42: $int ).
tff(func_def_50,type,
sK43: $int ).
tff(func_def_51,type,
sK44: $int ).
tff(func_def_52,type,
sK45: general ).
tff(func_def_53,type,
sK46: general ).
tff(func_def_54,type,
sK47: general ).
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(f20,axiom,
! [X0: general,X1: general] :
( in_building(X0,X1)
<=> ? [X2: general,X3: general,X4: general] :
( ? [X7: general,X5: general,X6: general] :
( ( X7 = X3 )
& ( X6 = X4 )
& ( X5 = X2 )
& in(X5,X6,X7) )
& ( X0 = X2 )
& ( X1 = X3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_4_completed_definition_of_in_building_2) ).
tff(f21,axiom,
! [X1: general,X0: general] :
( in_building_p(X0,X1)
<=> ? [X3: general,X4: general,X2: general] :
( ? [X6: general,X7: general,X5: general] :
( ( X5 = X2 )
& in(X5,X6,X7)
& ( X6 = X4 )
& ( X7 = X3 ) )
& ( X1 = X3 )
& ( X0 = X2 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_5_completed_definition_of_in_building_2) ).
tff(f23,axiom,
! [X0: general,X1: general] :
( ( ? [X3: general,X2: general] :
( ( X2 = X1 )
& ( X2 = X3 )
& ? [X6: $int,X4: $int,X5: $int] :
( ( X3 = f__integer__(X6) )
& $lesseq(X6,X5)
& ( X5 = h_i )
& ( X4 = 0 )
& $lesseq(X4,X6) ) )
& ? [X3: general,X2: general] :
( ( X3 = X1 )
& ~ in_building_p(X2,X3)
& ( X2 = X0 ) )
& ? [X2: general] :
( ( X2 = X0 )
& person(X2) ) )
=> $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_7_constraint_1) ).
tff(f27,conjecture,
! [X1: general,X0: general] :
( ( ? [X2: general,X3: general] :
( ( X2 = X1 )
& ( X2 = X3 )
& ? [X6: $int,X5: $int,X4: $int] :
( ( X4 = 0 )
& $lesseq(X6,X5)
& ( X5 = h_i )
& ( X3 = f__integer__(X6) )
& $lesseq(X4,X6) ) )
& ? [X2: general,X3: general] :
( ~ in_building(X2,X3)
& ( X2 = X0 )
& ( X3 = X1 ) )
& ? [X2: general] :
( ( X2 = X0 )
& person(X2) ) )
=> $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_11_constraint_1) ).
tff(f28,negated_conjecture,
~ ! [X1: general,X0: general] :
( ( ? [X2: general,X3: general] :
( ( X2 = X1 )
& ( X2 = X3 )
& ? [X6: $int,X5: $int,X4: $int] :
( ( X4 = 0 )
& $lesseq(X6,X5)
& ( X5 = h_i )
& ( X3 = f__integer__(X6) )
& $lesseq(X4,X6) ) )
& ? [X2: general,X3: general] :
( ~ in_building(X2,X3)
& ( X2 = X0 )
& ( X3 = X1 ) )
& ? [X2: general] :
( ( X2 = X0 )
& person(X2) ) )
=> $false ),
inference(negated_conjecture,[status(cth)],[f27]) ).
tff(f29,plain,
! [X0: general,X1: general] :
( ( ? [X3: general,X2: general] :
( ( X2 = X1 )
& ( X2 = X3 )
& ? [X6: $int,X4: $int,X5: $int] :
( ( X3 = f__integer__(X6) )
& ~ $less(X5,X6)
& ( X5 = h_i )
& ( X4 = 0 )
& ~ $less(X6,X4) ) )
& ? [X3: general,X2: general] :
( ( X3 = X1 )
& ~ in_building_p(X2,X3)
& ( X2 = X0 ) )
& ? [X2: general] :
( ( X2 = X0 )
& person(X2) ) )
=> $false ),
inference(theory_normalization,[],[f23]) ).
tff(f32,plain,
~ ! [X1: general,X0: general] :
( ( ? [X2: general,X3: general] :
( ( X2 = X1 )
& ( X2 = X3 )
& ? [X6: $int,X5: $int,X4: $int] :
( ( X4 = 0 )
& ~ $less(X5,X6)
& ( X5 = h_i )
& ( X3 = f__integer__(X6) )
& ~ $less(X6,X4) ) )
& ? [X2: general,X3: general] :
( ~ in_building(X2,X3)
& ( X2 = X0 )
& ( X3 = X1 ) )
& ? [X2: general] :
( ( X2 = X0 )
& person(X2) ) )
=> $false ),
inference(theory_normalization,[],[f28]) ).
tff(f35,plain,
! [X0: general,X1: general] :
( ? [X4: general,X3: general,X2: general] :
( ( X0 = X2 )
& ? [X6: general,X7: general,X5: general] :
( ( X4 = X7 )
& in(X6,X7,X5)
& ( X3 = X5 )
& ( X2 = X6 ) )
& ( X1 = X3 ) )
<=> in_building(X0,X1) ),
inference(rectify,[],[f20]) ).
tff(f36,plain,
! [X0: general,X1: general] :
( ( ? [X9: general] :
( person(X9)
& ( X0 = X9 ) )
& ? [X3: general,X2: general] :
( ( X1 = X3 )
& ( X2 = X3 )
& ? [X5: $int,X4: $int,X6: $int] :
( ( 0 = X5 )
& ~ $less(X4,X5)
& ~ $less(X6,X4)
& ( h_i = X6 )
& ( f__integer__(X4) = X2 ) ) )
& ? [X7: general,X8: general] :
( ~ in_building_p(X8,X7)
& ( X0 = X8 )
& ( X1 = X7 ) ) )
=> $false ),
inference(rectify,[],[f29]) ).
tff(f37,plain,
! [X1: general,X0: general] :
~ ( ? [X9: general] :
( person(X9)
& ( X0 = X9 ) )
& ? [X3: general,X2: general] :
( ( X1 = X3 )
& ( X2 = X3 )
& ? [X5: $int,X4: $int,X6: $int] :
( ( 0 = X5 )
& ~ $less(X4,X5)
& ~ $less(X6,X4)
& ( h_i = X6 )
& ( f__integer__(X4) = X2 ) ) )
& ? [X7: general,X8: general] :
( ~ in_building_p(X8,X7)
& ( X0 = X8 )
& ( X1 = X7 ) ) ),
inference(true_and_false_elimination,[],[f36]) ).
tff(f38,plain,
! [X1: general,X0: general] :
( in_building_p(X1,X0)
<=> ? [X2: general,X4: general,X3: general] :
( ? [X6: general,X5: general,X7: general] :
( ( X4 = X7 )
& ( X3 = X5 )
& ( X2 = X6 )
& in(X7,X5,X6) )
& ( X0 = X2 )
& ( X1 = X4 ) ) ),
inference(rectify,[],[f21]) ).
tff(f41,plain,
~ ! [X0: general,X1: general] :
( ( ? [X3: general,X2: general] :
( ? [X5: $int,X4: $int,X6: $int] :
( ( X5 = h_i )
& ( f__integer__(X4) = X3 )
& ~ $less(X5,X4)
& ~ $less(X4,X6)
& ( 0 = X6 ) )
& ( X0 = X2 )
& ( X2 = X3 ) )
& ? [X9: general] :
( ( X1 = X9 )
& person(X9) )
& ? [X8: general,X7: general] :
( ~ in_building(X7,X8)
& ( X1 = X7 )
& ( X0 = X8 ) ) )
=> $false ),
inference(rectify,[],[f32]) ).
tff(f42,plain,
~ ! [X0: general,X1: general] :
~ ( ? [X3: general,X2: general] :
( ? [X5: $int,X4: $int,X6: $int] :
( ( X5 = h_i )
& ( f__integer__(X4) = X3 )
& ~ $less(X5,X4)
& ~ $less(X4,X6)
& ( 0 = X6 ) )
& ( X0 = X2 )
& ( X2 = X3 ) )
& ? [X9: general] :
( ( X1 = X9 )
& person(X9) )
& ? [X8: general,X7: general] :
( ~ in_building(X7,X8)
& ( X1 = X7 )
& ( X0 = X8 ) ) ),
inference(true_and_false_elimination,[],[f41]) ).
tff(f52,plain,
! [X1: general,X0: general] :
( in_building_p(X1,X0)
=> ? [X2: general,X4: general,X3: general] :
( ? [X6: general,X5: general,X7: general] :
( ( X4 = X7 )
& ( X3 = X5 )
& ( X2 = X6 )
& in(X7,X5,X6) )
& ( X0 = X2 )
& ( X1 = X4 ) ) ),
inference(unused_predicate_definition_removal,[],[f38]) ).
tff(f53,plain,
! [X0: general,X1: general] :
( ? [X4: general,X3: general,X2: general] :
( ( X0 = X2 )
& ? [X6: general,X7: general,X5: general] :
( ( X4 = X7 )
& in(X6,X7,X5)
& ( X3 = X5 )
& ( X2 = X6 ) )
& ( X1 = X3 ) )
=> in_building(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f35]) ).
tff(f60,plain,
! [X0: general,X1: general] :
( ! [X8: general,X7: general] :
( in_building_p(X8,X7)
| ( X1 != X7 )
| ( X0 != X8 ) )
| ! [X2: general,X3: general] :
( ! [X4: $int,X6: $int,X5: $int] :
( ( f__integer__(X4) != X2 )
| $less(X4,X5)
| $less(X6,X4)
| ( 0 != X5 )
| ( h_i != X6 ) )
| ( X2 != X3 )
| ( X1 != X3 ) )
| ! [X9: general] :
( ~ person(X9)
| ( X0 != X9 ) ) ),
inference(ennf_transformation,[],[f37]) ).
tff(f68,plain,
? [X1: general,X0: general] :
( ? [X3: general,X2: general] :
( ? [X5: $int,X4: $int,X6: $int] :
( ( X5 = h_i )
& ( f__integer__(X4) = X3 )
& ~ $less(X5,X4)
& ~ $less(X4,X6)
& ( 0 = X6 ) )
& ( X0 = X2 )
& ( X2 = X3 ) )
& ? [X9: general] :
( ( X1 = X9 )
& person(X9) )
& ? [X8: general,X7: general] :
( ~ in_building(X7,X8)
& ( X1 = X7 )
& ( X0 = X8 ) ) ),
inference(ennf_transformation,[],[f42]) ).
tff(f69,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| ? [X2: general,X4: general,X3: general] :
( ? [X6: general,X5: general,X7: general] :
( ( X4 = X7 )
& ( X3 = X5 )
& ( X2 = X6 )
& in(X7,X5,X6) )
& ( X0 = X2 )
& ( X1 = X4 ) ) ),
inference(ennf_transformation,[],[f52]) ).
tff(f72,plain,
! [X0: general,X1: general] :
( ! [X2: general,X3: general,X4: general] :
( ( X1 != X3 )
| ( X0 != X2 )
| ! [X5: general,X6: general,X7: general] :
( ( X3 != X5 )
| ~ in(X6,X7,X5)
| ( X2 != X6 )
| ( X4 != X7 ) ) )
| in_building(X0,X1) ),
inference(ennf_transformation,[],[f53]) ).
tff(f94,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| ? [X2: general,X3: general,X4: general] :
( ? [X5: general,X6: general,X7: general] :
( ( X3 = X7 )
& ( X4 = X6 )
& ( X2 = X5 )
& in(X7,X6,X5) )
& ( X0 = X2 )
& ( X1 = X3 ) ) ),
inference(rectify,[],[f69]) ).
tff(f95,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| ( ( sK31(X0,X1) = sK35(X0,X1) )
& ( sK32(X0,X1) = sK34(X0,X1) )
& ( sK33(X0,X1) = sK30(X0,X1) )
& in(sK35(X0,X1),sK34(X0,X1),sK33(X0,X1))
& ( sK30(X0,X1) = X0 )
& ( sK31(X0,X1) = X1 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32,sK33,sK34,sK35]),skolemize(X2,sK30(X0,X1)),skolemize(X3,sK31(X0,X1)),skolemize(X4,sK32(X0,X1)),skolemize(X5,sK33(X0,X1)),skolemize(X6,sK34(X0,X1)),skolemize(X7,sK35(X0,X1))],[f94]) ).
tff(f96,plain,
! [X0: general,X1: general] :
( ! [X2: general,X3: general] :
( in_building_p(X2,X3)
| ( X1 != X3 )
| ( X0 != X2 ) )
| ! [X4: general,X5: general] :
( ! [X6: $int,X7: $int,X8: $int] :
( ( f__integer__(X6) != X4 )
| $less(X6,X8)
| $less(X7,X6)
| ( 0 != X8 )
| ( h_i != X7 ) )
| ( X4 != X5 )
| ( X1 != X5 ) )
| ! [X9: general] :
( ~ person(X9)
| ( X0 != X9 ) ) ),
inference(rectify,[],[f60]) ).
tff(f103,plain,
? [X0: general,X1: general] :
( ? [X2: general,X3: general] :
( ? [X4: $int,X5: $int,X6: $int] :
( ( h_i = X4 )
& ( f__integer__(X5) = X2 )
& ~ $less(X4,X5)
& ~ $less(X5,X6)
& ( 0 = X6 ) )
& ( X1 = X3 )
& ( X2 = X3 ) )
& ? [X7: general] :
( ( X0 = X7 )
& person(X7) )
& ? [X8: general,X9: general] :
( ~ in_building(X9,X8)
& ( X0 = X9 )
& ( X1 = X8 ) ) ),
inference(rectify,[],[f68]) ).
tff(f104,plain,
( ( h_i = sK42 )
& ( sK40 = f__integer__(sK43) )
& ~ $less(sK42,sK43)
& ~ $less(sK43,sK44)
& ( 0 = sK44 )
& ( sK41 = sK39 )
& ( sK41 = sK40 )
& ( sK45 = sK38 )
& person(sK45)
& ~ in_building(sK47,sK46)
& ( sK38 = sK47 )
& ( sK46 = sK39 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47]),skolemize(X0,sK38),skolemize(X1,sK39),skolemize(X2,sK40),skolemize(X3,sK41),skolemize(X4,sK42),skolemize(X5,sK43),skolemize(X6,sK44),skolemize(X7,sK45),skolemize(X8,sK46),skolemize(X9,sK47)],[f103]) ).
tff(f156,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| ( sK31(X0,X1) = X1 ) ),
inference(cnf_transformation,[],[f95]) ).
tff(f157,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| ( sK30(X0,X1) = X0 ) ),
inference(cnf_transformation,[],[f95]) ).
tff(f158,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| in(sK35(X0,X1),sK34(X0,X1),sK33(X0,X1)) ),
inference(cnf_transformation,[],[f95]) ).
tff(f159,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| ( sK33(X0,X1) = sK30(X0,X1) ) ),
inference(cnf_transformation,[],[f95]) ).
tff(f161,plain,
! [X0: general,X1: general] :
( ~ in_building_p(X1,X0)
| ( sK31(X0,X1) = sK35(X0,X1) ) ),
inference(cnf_transformation,[],[f95]) ).
tff(f162,plain,
! [X2: general,X3: general,X0: general,X1: general,X8: $int,X6: $int,X9: general,X7: $int,X4: general,X5: general] :
( in_building_p(X2,X3)
| ( X1 != X3 )
| ( X0 != X2 )
| ( f__integer__(X6) != X4 )
| $less(X6,X8)
| $less(X7,X6)
| ( 0 != X8 )
| ( h_i != X7 )
| ( X4 != X5 )
| ( X1 != X5 )
| ~ person(X9)
| ( X0 != X9 ) ),
inference(cnf_transformation,[],[f96]) ).
tff(f169,plain,
! [X2: general,X3: general,X0: general,X1: general,X6: general,X7: general,X4: general,X5: general] :
( ( X1 != X3 )
| ( X0 != X2 )
| ( X3 != X5 )
| ~ in(X6,X7,X5)
| ( X2 != X6 )
| ( X4 != X7 )
| in_building(X0,X1) ),
inference(cnf_transformation,[],[f72]) ).
tff(f177,plain,
sK46 = sK39,
inference(cnf_transformation,[],[f104]) ).
tff(f178,plain,
sK38 = sK47,
inference(cnf_transformation,[],[f104]) ).
tff(f179,plain,
~ in_building(sK47,sK46),
inference(cnf_transformation,[],[f104]) ).
tff(f180,plain,
person(sK45),
inference(cnf_transformation,[],[f104]) ).
tff(f181,plain,
sK45 = sK38,
inference(cnf_transformation,[],[f104]) ).
tff(f182,plain,
sK41 = sK40,
inference(cnf_transformation,[],[f104]) ).
tff(f183,plain,
sK41 = sK39,
inference(cnf_transformation,[],[f104]) ).
tff(f184,plain,
0 = sK44,
inference(cnf_transformation,[],[f104]) ).
tff(f185,plain,
~ $less(sK43,sK44),
inference(cnf_transformation,[],[f104]) ).
tff(f186,plain,
~ $less(sK42,sK43),
inference(cnf_transformation,[],[f104]) ).
tff(f187,plain,
sK40 = f__integer__(sK43),
inference(cnf_transformation,[],[f104]) ).
tff(f188,plain,
h_i = sK42,
inference(cnf_transformation,[],[f104]) ).
tff(f189,plain,
sK45 = sK47,
inference(definition_unfolding,[],[f181,f178]) ).
tff(f192,plain,
! [X2: general,X3: general,X0: general,X1: general,X8: $int,X6: $int,X9: general,X7: $int,X4: general,X5: general] :
( in_building_p(X2,X3)
| ( X1 != X3 )
| ( X0 != X2 )
| ( f__integer__(X6) != X4 )
| $less(X6,X8)
| $less(X7,X6)
| ( 0 != X8 )
| ( sK42 != X7 )
| ( X4 != X5 )
| ( X1 != X5 )
| ~ person(X9)
| ( X0 != X9 ) ),
inference(definition_unfolding,[],[f162,f188]) ).
tff(f194,plain,
~ $less(sK43,0),
inference(definition_unfolding,[],[f185,f184]) ).
tff(f195,plain,
sK40 = sK39,
inference(definition_unfolding,[],[f182,f183]) ).
tff(f196,plain,
person(sK47),
inference(definition_unfolding,[],[f180,f189]) ).
tff(f197,plain,
~ in_building(sK47,sK39),
inference(definition_unfolding,[],[f179,f177]) ).
tff(f227,plain,
! [X2: general,X3: general,X0: general,X8: $int,X6: $int,X9: general,X7: $int,X4: general,X5: general] :
( in_building_p(X2,X3)
| ( X0 != X2 )
| ( f__integer__(X6) != X4 )
| $less(X6,X8)
| $less(X7,X6)
| ( 0 != X8 )
| ( sK42 != X7 )
| ( X4 != X5 )
| ( X3 != X5 )
| ~ person(X9)
| ( X0 != X9 ) ),
inference(equality_resolution,[],[f192]) ).
tff(f228,plain,
! [X2: general,X3: general,X8: $int,X6: $int,X9: general,X7: $int,X4: general,X5: general] :
( in_building_p(X2,X3)
| ( f__integer__(X6) != X4 )
| $less(X6,X8)
| $less(X7,X6)
| ( 0 != X8 )
| ( sK42 != X7 )
| ( X4 != X5 )
| ( X3 != X5 )
| ~ person(X9)
| ( X2 != X9 ) ),
inference(equality_resolution,[],[f227]) ).
tff(f229,plain,
! [X2: general,X3: general,X8: $int,X6: $int,X9: general,X7: $int,X5: general] :
( in_building_p(X2,X3)
| $less(X6,X8)
| $less(X7,X6)
| ( 0 != X8 )
| ( sK42 != X7 )
| ( f__integer__(X6) != X5 )
| ( X3 != X5 )
| ~ person(X9)
| ( X2 != X9 ) ),
inference(equality_resolution,[],[f228]) ).
tff(f230,plain,
! [X2: general,X3: general,X6: $int,X9: general,X7: $int,X5: general] :
( in_building_p(X2,X3)
| $less(X6,0)
| $less(X7,X6)
| ( sK42 != X7 )
| ( f__integer__(X6) != X5 )
| ( X3 != X5 )
| ~ person(X9)
| ( X2 != X9 ) ),
inference(equality_resolution,[],[f229]) ).
tff(f231,plain,
! [X2: general,X3: general,X6: $int,X9: general,X5: general] :
( in_building_p(X2,X3)
| $less(X6,0)
| $less(sK42,X6)
| ( f__integer__(X6) != X5 )
| ( X3 != X5 )
| ~ person(X9)
| ( X2 != X9 ) ),
inference(equality_resolution,[],[f230]) ).
tff(f232,plain,
! [X2: general,X3: general,X6: $int,X9: general] :
( in_building_p(X2,X3)
| $less(X6,0)
| $less(sK42,X6)
| ( f__integer__(X6) != X3 )
| ~ person(X9)
| ( X2 != X9 ) ),
inference(equality_resolution,[],[f231]) ).
tff(f233,plain,
! [X2: general,X6: $int,X9: general] :
( in_building_p(X2,f__integer__(X6))
| $less(X6,0)
| $less(sK42,X6)
| ~ person(X9)
| ( X2 != X9 ) ),
inference(equality_resolution,[],[f232]) ).
tff(f234,plain,
! [X6: $int,X9: general] :
( ~ person(X9)
| in_building_p(X9,f__integer__(X6))
| $less(sK42,X6)
| $less(X6,0) ),
inference(equality_resolution,[],[f233]) ).
tff(f243,plain,
! [X2: general,X3: general,X0: general,X6: general,X7: general,X4: general,X5: general] :
( ( X0 != X2 )
| ( X3 != X5 )
| ~ in(X6,X7,X5)
| ( X2 != X6 )
| ( X4 != X7 )
| in_building(X0,X3) ),
inference(equality_resolution,[],[f169]) ).
tff(f244,plain,
! [X2: general,X3: general,X6: general,X7: general,X4: general,X5: general] :
( ( X3 != X5 )
| ~ in(X6,X7,X5)
| ( X2 != X6 )
| ( X4 != X7 )
| in_building(X2,X3) ),
inference(equality_resolution,[],[f243]) ).
tff(f245,plain,
! [X2: general,X6: general,X7: general,X4: general,X5: general] :
( ~ in(X6,X7,X5)
| ( X2 != X6 )
| ( X4 != X7 )
| in_building(X2,X5) ),
inference(equality_resolution,[],[f244]) ).
tff(f246,plain,
! [X6: general,X7: general,X4: general,X5: general] :
( ~ in(X6,X7,X5)
| ( X4 != X7 )
| in_building(X6,X5) ),
inference(equality_resolution,[],[f245]) ).
tff(f247,plain,
! [X6: general,X7: general,X5: general] :
( ~ in(X6,X7,X5)
| in_building(X6,X5) ),
inference(equality_resolution,[],[f246]) ).
tff(f259,definition,
( spl48_1
<=> ( sK40 = sK39 ) ),
introduced(definition,[new_symbols(definition,[spl48_1])],[avatar_definition]) ).
tff(f261,plain,
( ( sK40 = sK39 )
| ~ spl48_1 ),
inference(avatar_component_clause,[],[f259]) ).
tff(f262,plain,
spl48_1,
inference(avatar_split_clause,[],[f195,f259]) ).
tff(f269,definition,
( spl48_3
<=> in_building(sK47,sK39) ),
introduced(definition,[new_symbols(definition,[spl48_3])],[avatar_definition]) ).
tff(f271,plain,
( ~ in_building(sK47,sK39)
| spl48_3 ),
inference(avatar_component_clause,[],[f269]) ).
tff(f272,plain,
~ spl48_3,
inference(avatar_split_clause,[],[f197,f269]) ).
tff(f274,definition,
( spl48_4
<=> ( sK40 = f__integer__(sK43) ) ),
introduced(definition,[new_symbols(definition,[spl48_4])],[avatar_definition]) ).
tff(f276,plain,
( ( sK40 = f__integer__(sK43) )
| ~ spl48_4 ),
inference(avatar_component_clause,[],[f274]) ).
tff(f277,plain,
spl48_4,
inference(avatar_split_clause,[],[f187,f274]) ).
tff(f279,definition,
( spl48_5
<=> $less(sK43,0) ),
introduced(definition,[new_symbols(definition,[spl48_5])],[avatar_definition]) ).
tff(f281,plain,
( ~ $less(sK43,0)
| spl48_5 ),
inference(avatar_component_clause,[],[f279]) ).
tff(f282,plain,
~ spl48_5,
inference(avatar_split_clause,[],[f194,f279]) ).
tff(f284,definition,
( spl48_6
<=> $less(sK42,sK43) ),
introduced(definition,[new_symbols(definition,[spl48_6])],[avatar_definition]) ).
tff(f286,plain,
( ~ $less(sK42,sK43)
| spl48_6 ),
inference(avatar_component_clause,[],[f284]) ).
tff(f287,plain,
~ spl48_6,
inference(avatar_split_clause,[],[f186,f284]) ).
tff(f289,definition,
( spl48_7
<=> person(sK47) ),
introduced(definition,[new_symbols(definition,[spl48_7])],[avatar_definition]) ).
tff(f291,plain,
( person(sK47)
| ~ spl48_7 ),
inference(avatar_component_clause,[],[f289]) ).
tff(f292,plain,
spl48_7,
inference(avatar_split_clause,[],[f196,f289]) ).
tff(f293,plain,
( ( sK39 = f__integer__(sK43) )
| ~ spl48_1
| ~ spl48_4 ),
inference(forward_demodulation,[],[f261,f276]) ).
tff(f295,definition,
( spl48_8
<=> ( sK39 = f__integer__(sK43) ) ),
introduced(definition,[new_symbols(definition,[spl48_8])],[avatar_definition]) ).
tff(f297,plain,
( ( sK39 = f__integer__(sK43) )
| ~ spl48_8 ),
inference(avatar_component_clause,[],[f295]) ).
tff(f298,plain,
( spl48_8
| ~ spl48_1
| ~ spl48_4 ),
inference(avatar_split_clause,[],[f293,f274,f259,f295]) ).
tff(f299,plain,
( ~ in_building(sK47,f__integer__(sK43))
| spl48_3
| ~ spl48_8 ),
inference(superposition,[],[f271,f297]) ).
tff(f301,definition,
( spl48_9
<=> in_building(sK47,f__integer__(sK43)) ),
introduced(definition,[new_symbols(definition,[spl48_9])],[avatar_definition]) ).
tff(f303,plain,
( ~ in_building(sK47,f__integer__(sK43))
| spl48_9 ),
inference(avatar_component_clause,[],[f301]) ).
tff(f304,plain,
( ~ spl48_9
| spl48_3
| ~ spl48_8 ),
inference(avatar_split_clause,[],[f299,f295,f269,f301]) ).
tff(f305,plain,
( ! [X0: $int] :
( in_building_p(sK47,f__integer__(X0))
| $less(sK42,X0)
| $less(X0,0) )
| ~ spl48_7 ),
inference(resolution,[],[f234,f291]) ).
tff(f316,plain,
( ! [X0: $int] :
( $less(sK42,X0)
| $less(X0,0)
| ( sK31(f__integer__(X0),sK47) = sK47 ) )
| ~ spl48_7 ),
inference(resolution,[],[f156,f305]) ).
tff(f319,plain,
( $less(sK42,sK43)
| ( sK31(f__integer__(sK43),sK47) = sK47 )
| spl48_5
| ~ spl48_7 ),
inference(resolution,[],[f316,f281]) ).
tff(f327,plain,
( ( sK31(f__integer__(sK43),sK47) = sK47 )
| spl48_5
| spl48_6
| ~ spl48_7 ),
inference(forward_subsumption_resolution,[],[f319,f286]) ).
tff(f334,definition,
( spl48_12
<=> ( sK31(f__integer__(sK43),sK47) = sK47 ) ),
introduced(definition,[new_symbols(definition,[spl48_12])],[avatar_definition]) ).
tff(f336,plain,
( ( sK31(f__integer__(sK43),sK47) = sK47 )
| ~ spl48_12 ),
inference(avatar_component_clause,[],[f334]) ).
tff(f337,plain,
( spl48_12
| spl48_5
| spl48_6
| ~ spl48_7 ),
inference(avatar_split_clause,[],[f327,f289,f284,f279,f334]) ).
tff(f338,plain,
( ! [X0: $int] :
( $less(sK42,X0)
| $less(X0,0)
| ( f__integer__(X0) = sK30(f__integer__(X0),sK47) ) )
| ~ spl48_7 ),
inference(resolution,[],[f157,f305]) ).
tff(f349,plain,
( ( f__integer__(sK43) = sK30(f__integer__(sK43),sK47) )
| $less(sK42,sK43)
| spl48_5
| ~ spl48_7 ),
inference(resolution,[],[f338,f281]) ).
tff(f351,plain,
( ( f__integer__(sK43) = sK30(f__integer__(sK43),sK47) )
| spl48_5
| spl48_6
| ~ spl48_7 ),
inference(forward_subsumption_resolution,[],[f349,f286]) ).
tff(f359,definition,
( spl48_14
<=> ( f__integer__(sK43) = sK30(f__integer__(sK43),sK47) ) ),
introduced(definition,[new_symbols(definition,[spl48_14])],[avatar_definition]) ).
tff(f361,plain,
( ( f__integer__(sK43) = sK30(f__integer__(sK43),sK47) )
| ~ spl48_14 ),
inference(avatar_component_clause,[],[f359]) ).
tff(f362,plain,
( spl48_14
| spl48_5
| spl48_6
| ~ spl48_7 ),
inference(avatar_split_clause,[],[f351,f289,f284,f279,f359]) ).
tff(f456,plain,
( ! [X0: $int] :
( $less(sK42,X0)
| $less(X0,0)
| ( sK33(f__integer__(X0),sK47) = sK30(f__integer__(X0),sK47) ) )
| ~ spl48_7 ),
inference(resolution,[],[f159,f305]) ).
tff(f469,plain,
( $less(sK42,sK43)
| ( sK33(f__integer__(sK43),sK47) = sK30(f__integer__(sK43),sK47) )
| spl48_5
| ~ spl48_7 ),
inference(resolution,[],[f456,f281]) ).
tff(f471,plain,
( ( sK33(f__integer__(sK43),sK47) = sK30(f__integer__(sK43),sK47) )
| spl48_5
| spl48_6
| ~ spl48_7 ),
inference(forward_subsumption_resolution,[],[f469,f286]) ).
tff(f474,plain,
( ( f__integer__(sK43) = sK33(f__integer__(sK43),sK47) )
| spl48_5
| spl48_6
| ~ spl48_7
| ~ spl48_14 ),
inference(forward_demodulation,[],[f471,f361]) ).
tff(f482,definition,
( spl48_21
<=> ( f__integer__(sK43) = sK33(f__integer__(sK43),sK47) ) ),
introduced(definition,[new_symbols(definition,[spl48_21])],[avatar_definition]) ).
tff(f484,plain,
( ( f__integer__(sK43) = sK33(f__integer__(sK43),sK47) )
| ~ spl48_21 ),
inference(avatar_component_clause,[],[f482]) ).
tff(f485,plain,
( spl48_21
| spl48_5
| spl48_6
| ~ spl48_7
| ~ spl48_14 ),
inference(avatar_split_clause,[],[f474,f359,f289,f284,f279,f482]) ).
tff(f491,plain,
( ! [X0: $int] :
( $less(sK42,X0)
| $less(X0,0)
| ( sK31(f__integer__(X0),sK47) = sK35(f__integer__(X0),sK47) ) )
| ~ spl48_7 ),
inference(resolution,[],[f161,f305]) ).
tff(f516,plain,
( ( sK31(f__integer__(sK43),sK47) = sK35(f__integer__(sK43),sK47) )
| $less(sK42,sK43)
| spl48_5
| ~ spl48_7 ),
inference(resolution,[],[f491,f281]) ).
tff(f519,plain,
( ( sK31(f__integer__(sK43),sK47) = sK35(f__integer__(sK43),sK47) )
| spl48_5
| spl48_6
| ~ spl48_7 ),
inference(forward_subsumption_resolution,[],[f516,f286]) ).
tff(f526,plain,
( ( sK47 = sK35(f__integer__(sK43),sK47) )
| spl48_5
| spl48_6
| ~ spl48_7
| ~ spl48_12 ),
inference(forward_demodulation,[],[f519,f336]) ).
tff(f529,definition,
( spl48_27
<=> ( sK47 = sK35(f__integer__(sK43),sK47) ) ),
introduced(definition,[new_symbols(definition,[spl48_27])],[avatar_definition]) ).
tff(f531,plain,
( ( sK47 = sK35(f__integer__(sK43),sK47) )
| ~ spl48_27 ),
inference(avatar_component_clause,[],[f529]) ).
tff(f532,plain,
( spl48_27
| spl48_5
| spl48_6
| ~ spl48_7
| ~ spl48_12 ),
inference(avatar_split_clause,[],[f526,f334,f289,f284,f279,f529]) ).
tff(f559,plain,
( ! [X0: $int] :
( in(sK35(f__integer__(X0),sK47),sK34(f__integer__(X0),sK47),sK33(f__integer__(X0),sK47))
| $less(X0,0)
| $less(sK42,X0) )
| ~ spl48_7 ),
inference(resolution,[],[f158,f305]) ).
tff(f564,plain,
( in(sK47,sK34(f__integer__(sK43),sK47),sK33(f__integer__(sK43),sK47))
| $less(sK43,0)
| $less(sK42,sK43)
| ~ spl48_7
| ~ spl48_27 ),
inference(superposition,[],[f559,f531]) ).
tff(f574,plain,
( in(sK47,sK34(f__integer__(sK43),sK47),sK33(f__integer__(sK43),sK47))
| $less(sK42,sK43)
| spl48_5
| ~ spl48_7
| ~ spl48_27 ),
inference(forward_subsumption_resolution,[],[f564,f281]) ).
tff(f580,plain,
( in(sK47,sK34(f__integer__(sK43),sK47),sK33(f__integer__(sK43),sK47))
| spl48_5
| spl48_6
| ~ spl48_7
| ~ spl48_27 ),
inference(forward_subsumption_resolution,[],[f574,f286]) ).
tff(f590,plain,
( in(sK47,sK34(f__integer__(sK43),sK47),f__integer__(sK43))
| spl48_5
| spl48_6
| ~ spl48_7
| ~ spl48_21
| ~ spl48_27 ),
inference(forward_demodulation,[],[f580,f484]) ).
tff(f598,definition,
( spl48_33
<=> in(sK47,sK34(f__integer__(sK43),sK47),f__integer__(sK43)) ),
introduced(definition,[new_symbols(definition,[spl48_33])],[avatar_definition]) ).
tff(f600,plain,
( in(sK47,sK34(f__integer__(sK43),sK47),f__integer__(sK43))
| ~ spl48_33 ),
inference(avatar_component_clause,[],[f598]) ).
tff(f601,plain,
( spl48_33
| spl48_5
| spl48_6
| ~ spl48_7
| ~ spl48_21
| ~ spl48_27 ),
inference(avatar_split_clause,[],[f590,f529,f482,f289,f284,f279,f598]) ).
tff(f634,plain,
( in_building(sK47,f__integer__(sK43))
| ~ spl48_33 ),
inference(resolution,[],[f600,f247]) ).
tff(f635,plain,
( $false
| spl48_9
| ~ spl48_33 ),
inference(forward_subsumption_resolution,[],[f634,f303]) ).
tff(f636,plain,
( spl48_9
| ~ spl48_33 ),
inference(avatar_contradiction_clause,[],[f635]) ).
tff(f642,plain,
$false,
inference(avatar_smt_refutation,[],[f636,f601,f532,f485,f362,f337,f304,f298,f292,f287,f282,f277,f272,f262]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX088_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n014.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:00:30 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.50/1.16 % (1832270)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.50/1.16 % (1832280)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1915810598:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.50/1.16 % (1832280)Instruction limit reached!
% 3.50/1.16 % (1832280)------------------------------
% 3.50/1.16 % (1832280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832280)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832280)Termination reason: Instruction limit
% 3.50/1.16 % (1832280)Termination phase: Saturation
% 3.50/1.16 % (1832280)Time elapsed: 0.002 s
% 3.50/1.16 % (1832280)Peak memory usage: 88 MB
% 3.50/1.16 % (1832280)Instructions burned: 4 (million)
% 3.50/1.16 % (1832279)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3310231731:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.50/1.16 % (1832278)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=461713479:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.50/1.16 % (1832282)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=945997747:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.50/1.16 % (1832276)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3696767382:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.50/1.16 % (1832281)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2813008947:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.50/1.16 % (1832277)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4128311136:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.50/1.16 % (1832279)Instruction limit reached!
% 3.50/1.16 % (1832279)------------------------------
% 3.50/1.16 % (1832279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832279)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832279)Termination reason: Instruction limit
% 3.50/1.16 % (1832279)Termination phase: Saturation
% 3.50/1.16 % (1832279)Time elapsed: 0.005 s
% 3.50/1.16 % (1832279)Peak memory usage: 88 MB
% 3.50/1.16 % (1832279)Instructions burned: 7 (million)
% 3.50/1.16 % (1832276)Instruction limit reached!
% 3.50/1.16 % (1832276)------------------------------
% 3.50/1.16 % (1832276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832276)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832276)Termination reason: Instruction limit
% 3.50/1.16 % (1832276)Termination phase: Saturation
% 3.50/1.16 % (1832276)Time elapsed: 0.032 s
% 3.50/1.16 % (1832276)Peak memory usage: 116 MB
% 3.50/1.16 % (1832276)Instructions burned: 12 (million)
% 3.50/1.16 % (1832282)Instruction limit reached!
% 3.50/1.16 % (1832282)------------------------------
% 3.50/1.16 % (1832282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832282)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832282)Termination reason: Instruction limit
% 3.50/1.16 % (1832282)Termination phase: Saturation
% 3.50/1.16 % (1832282)Time elapsed: 0.047 s
% 3.50/1.16 % (1832282)Peak memory usage: 116 MB
% 3.50/1.16 % (1832282)Instructions burned: 34 (million)
% 3.50/1.16 % (1832281)First to succeed.
% 3.50/1.16 % (1832281)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1832270"
% 3.50/1.16 % (1832284)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3315284288:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.50/1.16 % (1832284)Instruction limit reached!
% 3.50/1.16 % (1832284)------------------------------
% 3.50/1.16 % (1832284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832284)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832284)Termination reason: Instruction limit
% 3.50/1.16 % (1832284)Termination phase: Saturation
% 3.50/1.16 % (1832284)Time elapsed: 0.006 s
% 3.50/1.16 % (1832284)Peak memory usage: 89 MB
% 3.50/1.16 % (1832284)Instructions burned: 15 (million)
% 3.50/1.16 % (1832278)Instruction limit reached!
% 3.50/1.16 % (1832278)------------------------------
% 3.50/1.16 % (1832278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832278)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832278)Termination reason: Instruction limit
% 3.50/1.16 % (1832278)Termination phase: Saturation
% 3.50/1.16 % (1832278)Time elapsed: 0.126 s
% 3.50/1.16 % (1832278)Peak memory usage: 116 MB
% 3.50/1.16 % (1832278)Instructions burned: 201 (million)
% 3.50/1.16 % (1832291)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=4253923639:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.50/1.16 % (1832291)Instruction limit reached!
% 3.50/1.16 % (1832291)------------------------------
% 3.50/1.16 % (1832291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832291)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832291)Termination reason: Instruction limit
% 3.50/1.16 % (1832291)Termination phase: Property scanning
% 3.50/1.16 % (1832291)Time elapsed: 0.012 s
% 3.50/1.16 % (1832291)Peak memory usage: 86 MB
% 3.50/1.16 % (1832291)Instructions burned: 29 (million)
% 3.50/1.16 % (1832277)Instruction limit reached!
% 3.50/1.16 % (1832277)------------------------------
% 3.50/1.16 % (1832277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832277)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832277)Termination reason: Instruction limit
% 3.50/1.16 % (1832277)Termination phase: Saturation
% 3.50/1.16 % (1832277)Time elapsed: 0.181 s
% 3.50/1.16 % (1832277)Peak memory usage: 116 MB
% 3.50/1.16 % (1832277)Instructions burned: 308 (million)
% 3.50/1.16 % (1832292)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3115903887:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 3.50/1.16 % (1832293)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3291996371:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.50/1.16 % (1832292)Instruction limit reached!
% 3.50/1.16 % (1832292)------------------------------
% 3.50/1.16 % (1832292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832292)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832292)Termination reason: Instruction limit
% 3.50/1.16 % (1832292)Termination phase: Saturation
% 3.50/1.16 % (1832292)Time elapsed: 0.010 s
% 3.50/1.16 % (1832292)Peak memory usage: 90 MB
% 3.50/1.16 % (1832292)Instructions burned: 16 (million)
% 3.50/1.16 % (1832293)Instruction limit reached!
% 3.50/1.16 % (1832293)------------------------------
% 3.50/1.16 % (1832293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832293)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832293)Termination reason: Instruction limit
% 3.50/1.16 % (1832293)Termination phase: Saturation
% 3.50/1.16 % (1832293)Time elapsed: 0.021 s
% 3.50/1.16 % (1832293)Peak memory usage: 89 MB
% 3.50/1.16 % (1832293)Instructions burned: 25 (million)
% 3.50/1.16 % (1832295)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=1942403898:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.50/1.16 % (1832295)Instruction limit reached!
% 3.50/1.16 % (1832295)------------------------------
% 3.50/1.16 % (1832295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832295)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832295)Termination reason: Instruction limit
% 3.50/1.16 % (1832295)Termination phase: Saturation
% 3.50/1.16 % (1832295)Time elapsed: 0.011 s
% 3.50/1.16 % (1832295)Peak memory usage: 90 MB
% 3.50/1.16 % (1832295)Instructions burned: 29 (million)
% 3.50/1.16 % (1832296)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3009874126:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.50/1.16 % (1832298)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2665401945:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 3.50/1.16 % (1832298)Instruction limit reached!
% 3.50/1.16 % (1832298)------------------------------
% 3.50/1.16 % (1832298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832298)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832298)Termination reason: Instruction limit
% 3.50/1.16 % (1832298)Termination phase: Preprocessing 3
% 3.50/1.16 % (1832298)Time elapsed: 0.002 s
% 3.50/1.16 % (1832298)Peak memory usage: 86 MB
% 3.50/1.16 % (1832298)Instructions burned: 2 (million)
% 3.50/1.16 % (1832296)Instruction limit reached!
% 3.50/1.16 % (1832296)------------------------------
% 3.50/1.16 % (1832296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.50/1.16 % (1832296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.50/1.16 % (1832296)CaDiCaL version: 2.1.3
% 3.50/1.16 % (1832296)Termination reason: Instruction limit
% 3.50/1.16 % (1832296)Termination phase: Saturation
% 3.50/1.16 % (1832296)Time elapsed: 0.044 s
% 3.50/1.16 % (1832296)Peak memory usage: 89 MB
% 3.50/1.16 % (1832296)Instructions burned: 85 (million)
% 3.50/1.16 % (1832299)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=1327722083:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 3.50/1.16 % (1832281)Refutation found. Thanks to Tanya!
% 3.50/1.16 % SZS status Theorem for theBenchmark
% 3.50/1.16 % SZS output start Proof for theBenchmark
% See solution above
% 4.24/1.36 % (1832281)------------------------------
% 4.24/1.36 % (1832281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.24/1.36 % (1832281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.24/1.36 % (1832281)CaDiCaL version: 2.1.3
% 4.24/1.36 % (1832281)Termination reason: Refutation
% 4.24/1.36 % (1832281)Time elapsed: 0.060 s
% 4.24/1.36 % (1832281)Peak memory usage: 117 MB
% 4.24/1.36 % (1832281)Instructions burned: 51 (million)
% 4.24/1.36 % (1832281)------------------------------
% 4.24/1.36 % (1832281)------------------------------
% 4.24/1.36 % (1832270)Success in time 0.512 s
% 4.24/1.36 % Vampire exiting
%------------------------------------------------------------------------------