%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT050_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n010.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 09:47:11 AM UTC 2026
% Result : Theorem 3.51s 1.20s
% Output : Refutation 4.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 48
% Syntax : Number of formulae : 179 ( 34 unt; 0 typ; 38 def)
% Number of atoms : 443 ( 127 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 453 ( 189 ~; 203 |; 19 &)
% ( 41 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number arithmetic : 188 ( 0 atm; 42 fun; 81 num; 65 var)
% Number of types : 3 ( 1 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 34 ( 32 usr; 32 prp; 0-2 aty)
% Number of functors : 19 ( 13 usr; 13 con; 0-2 aty)
% Number of variables : 111 ( 109 !; 2 ?; 111 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
collection: $tType ).
tff(func_def_0,type,
empty: collection ).
tff(func_def_1,type,
add: ( $int * collection ) > collection ).
tff(func_def_2,type,
remove: ( $int * collection ) > collection ).
tff(func_def_3,type,
count: collection > $int ).
tff(func_def_9,type,
sK0: $int ).
tff(func_def_10,type,
sK1: collection ).
tff(func_def_11,type,
sF2: collection ).
tff(func_def_12,type,
sF3: collection ).
tff(func_def_13,type,
sF4: $int ).
tff(func_def_14,type,
sF5: collection ).
tff(func_def_15,type,
sF6: collection ).
tff(func_def_16,type,
sF7: collection ).
tff(func_def_17,type,
sF8: $int ).
tff(pred_def_1,type,
in: ( $int * collection ) > $o ).
tff(f2,axiom,
! [X1: collection,X0: $int] : in(X0,add(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
tff(f3,axiom,
! [X1: collection,X0: $int] : ~ in(X0,remove(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
tff(f4,axiom,
! [X1: collection,X2: $int,X0: $int] :
( in(X0,add(X2,X1))
<=> ( ( X0 = X2 )
| in(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
tff(f5,axiom,
! [X2: $int,X1: collection,X0: $int] :
( ( in(X0,X1)
& ( X0 != X2 ) )
<=> in(X0,remove(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
tff(f8,axiom,
! [X0: $int,X1: collection] :
( ( count(add(X0,X1)) = $sum(count(X1),1) )
<=> ~ in(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
tff(f9,axiom,
! [X1: collection,X0: $int] :
( in(X0,X1)
<=> ( count(add(X0,X1)) = count(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax4) ).
tff(f10,axiom,
! [X1: collection,X0: $int] :
( in(X0,X1)
<=> ( count(remove(X0,X1)) = $difference(count(X1),1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
tff(f11,axiom,
! [X1: collection,X0: $int] :
( ( count(remove(X0,X1)) = count(X1) )
<=> ~ in(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
tff(f12,axiom,
! [X0: $int,X1: collection] :
( in(X0,X1)
=> ( X1 = add(X0,remove(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax7) ).
tff(f13,conjecture,
! [X1: $int,X0: collection] : ( count(add(0,remove(X1,add(X1,X0)))) = count(add(0,remove(X1,X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(f14,negated_conjecture,
~ ! [X1: $int,X0: collection] : ( count(add(0,remove(X1,add(X1,X0)))) = count(add(0,remove(X1,X0))) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
tff(f16,plain,
! [X1: collection,X0: $int] :
( in(X0,X1)
<=> ( count(remove(X0,X1)) = $sum(count(X1),$uminus(1)) ) ),
inference(theory_normalization,[],[f10]) ).
tff(f17,plain,
! [X0: collection,X1: $int] : ~ in(X1,remove(X1,X0)),
inference(rectify,[],[f3]) ).
tff(f18,plain,
~ ! [X0: $int,X1: collection] : ( count(add(0,remove(X0,add(X0,X1)))) = count(add(0,remove(X0,X1))) ),
inference(rectify,[],[f14]) ).
tff(f19,plain,
! [X1: $int,X0: collection,X2: $int] :
( ( in(X2,X0)
| ( X1 = X2 ) )
<=> in(X2,add(X1,X0)) ),
inference(rectify,[],[f4]) ).
tff(f20,plain,
! [X0: $int,X1: collection,X2: $int] :
( in(X2,remove(X0,X1))
<=> ( ( X0 != X2 )
& in(X2,X1) ) ),
inference(rectify,[],[f5]) ).
tff(f21,plain,
! [X1: $int,X0: collection] : in(X1,add(X1,X0)),
inference(rectify,[],[f2]) ).
tff(f22,plain,
! [X1: $int,X0: collection] :
( ( $sum(count(X0),$uminus(1)) = count(remove(X1,X0)) )
<=> in(X1,X0) ),
inference(rectify,[],[f16]) ).
tff(f23,plain,
? [X0: $int,X1: collection] : ( count(add(0,remove(X0,add(X0,X1)))) != count(add(0,remove(X0,X1))) ),
inference(ennf_transformation,[],[f18]) ).
tff(f24,plain,
! [X1: collection,X0: $int] :
( ~ in(X0,X1)
| ( X1 = add(X0,remove(X0,X1)) ) ),
inference(ennf_transformation,[],[f12]) ).
tff(f25,plain,
! [X0: $int,X1: collection,X2: $int] :
( ( in(X2,remove(X0,X1))
| ( X0 = X2 )
| ~ in(X2,X1) )
& ( ( ( X0 != X2 )
& in(X2,X1) )
| ~ in(X2,remove(X0,X1)) ) ),
inference(nnf_transformation,[],[f20]) ).
tff(f26,plain,
! [X0: $int,X1: collection,X2: $int] :
( ( in(X2,remove(X0,X1))
| ( X0 = X2 )
| ~ in(X2,X1) )
& ( ( ( X0 != X2 )
& in(X2,X1) )
| ~ in(X2,remove(X0,X1)) ) ),
inference(flattening,[],[f25]) ).
tff(f27,plain,
! [X1: collection,X0: $int] :
( ( ( count(remove(X0,X1)) = count(X1) )
| in(X0,X1) )
& ( ~ in(X0,X1)
| ( count(X1) != count(remove(X0,X1)) ) ) ),
inference(nnf_transformation,[],[f11]) ).
tff(f28,plain,
! [X0: collection,X1: $int] :
( ( ( count(X0) = count(remove(X1,X0)) )
| in(X1,X0) )
& ( ~ in(X1,X0)
| ( count(X0) != count(remove(X1,X0)) ) ) ),
inference(rectify,[],[f27]) ).
tff(f30,plain,
! [X1: collection,X0: $int] :
( ( in(X0,X1)
| ( count(add(X0,X1)) != count(X1) ) )
& ( ( count(add(X0,X1)) = count(X1) )
| ~ in(X0,X1) ) ),
inference(nnf_transformation,[],[f9]) ).
tff(f31,plain,
! [X0: collection,X1: $int] :
( ( in(X1,X0)
| ( count(X0) != count(add(X1,X0)) ) )
& ( ( count(X0) = count(add(X1,X0)) )
| ~ in(X1,X0) ) ),
inference(rectify,[],[f30]) ).
tff(f32,plain,
! [X1: $int,X0: collection,X2: $int] :
( ( in(X2,X0)
| ( X1 = X2 )
| ~ in(X2,add(X1,X0)) )
& ( in(X2,add(X1,X0))
| ( ~ in(X2,X0)
& ( X1 != X2 ) ) ) ),
inference(nnf_transformation,[],[f19]) ).
tff(f33,plain,
! [X1: $int,X0: collection,X2: $int] :
( ( in(X2,X0)
| ( X1 = X2 )
| ~ in(X2,add(X1,X0)) )
& ( in(X2,add(X1,X0))
| ( ~ in(X2,X0)
& ( X1 != X2 ) ) ) ),
inference(flattening,[],[f32]) ).
tff(f34,plain,
! [X0: $int,X1: collection,X2: $int] :
( ( in(X2,X1)
| ( X0 = X2 )
| ~ in(X2,add(X0,X1)) )
& ( in(X2,add(X0,X1))
| ( ~ in(X2,X1)
& ( X0 != X2 ) ) ) ),
inference(rectify,[],[f33]) ).
tff(f35,plain,
count(add(0,remove(sK0,sK1))) != count(add(0,remove(sK0,add(sK0,sK1)))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f23]) ).
tff(f36,plain,
! [X0: collection,X1: $int] :
( ~ in(X1,X0)
| ( add(X1,remove(X1,X0)) = X0 ) ),
inference(rectify,[],[f24]) ).
tff(f37,plain,
! [X0: $int,X1: collection] : in(X0,add(X0,X1)),
inference(rectify,[],[f21]) ).
tff(f38,plain,
! [X0: $int,X1: collection] :
( ( ( count(add(X0,X1)) = $sum(count(X1),1) )
| in(X0,X1) )
& ( ~ in(X0,X1)
| ( count(add(X0,X1)) != $sum(count(X1),1) ) ) ),
inference(nnf_transformation,[],[f8]) ).
tff(f39,plain,
! [X1: $int,X0: collection] :
( ( ( $sum(count(X0),$uminus(1)) = count(remove(X1,X0)) )
| ~ in(X1,X0) )
& ( in(X1,X0)
| ( $sum(count(X0),$uminus(1)) != count(remove(X1,X0)) ) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f40,plain,
! [X0: $int,X1: collection] :
( ( ( count(remove(X0,X1)) = $sum(count(X1),$uminus(1)) )
| ~ in(X0,X1) )
& ( in(X0,X1)
| ( count(remove(X0,X1)) != $sum(count(X1),$uminus(1)) ) ) ),
inference(rectify,[],[f39]) ).
tff(f41,plain,
! [X2: $int,X0: $int,X1: collection] :
( ~ in(X2,remove(X0,X1))
| in(X2,X1) ),
inference(cnf_transformation,[],[f26]) ).
tff(f43,plain,
! [X2: $int,X0: $int,X1: collection] :
( in(X2,remove(X0,X1))
| ( X0 = X2 )
| ~ in(X2,X1) ),
inference(cnf_transformation,[],[f26]) ).
tff(f45,plain,
! [X0: collection,X1: $int] :
( ( count(X0) = count(remove(X1,X0)) )
| in(X1,X0) ),
inference(cnf_transformation,[],[f28]) ).
tff(f49,plain,
! [X0: collection,X1: $int] :
( ( count(X0) = count(add(X1,X0)) )
| ~ in(X1,X0) ),
inference(cnf_transformation,[],[f31]) ).
tff(f52,plain,
! [X2: $int,X0: $int,X1: collection] :
( in(X2,add(X0,X1))
| ~ in(X2,X1) ),
inference(cnf_transformation,[],[f34]) ).
tff(f53,plain,
! [X2: $int,X0: $int,X1: collection] :
( ~ in(X2,add(X0,X1))
| in(X2,X1)
| ( X0 = X2 ) ),
inference(cnf_transformation,[],[f34]) ).
tff(f54,plain,
count(add(0,remove(sK0,sK1))) != count(add(0,remove(sK0,add(sK0,sK1)))),
inference(cnf_transformation,[],[f35]) ).
tff(f55,plain,
! [X0: collection,X1: $int] : ~ in(X1,remove(X1,X0)),
inference(cnf_transformation,[],[f17]) ).
tff(f56,plain,
! [X0: collection,X1: $int] :
( ( add(X1,remove(X1,X0)) = X0 )
| ~ in(X1,X0) ),
inference(cnf_transformation,[],[f36]) ).
tff(f57,plain,
! [X0: $int,X1: collection] : in(X0,add(X0,X1)),
inference(cnf_transformation,[],[f37]) ).
tff(f60,plain,
! [X0: $int,X1: collection] :
( ( count(add(X0,X1)) = $sum(count(X1),1) )
| in(X0,X1) ),
inference(cnf_transformation,[],[f38]) ).
tff(f62,plain,
! [X0: $int,X1: collection] :
( ( count(remove(X0,X1)) = $sum(count(X1),$uminus(1)) )
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f40]) ).
tff(f66,definition,
sF2 = remove(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
tff(f67,plain,
remove(sK0,sK1) = sF2,
inference(reorient_equations,[],[f66]) ).
tff(f68,definition,
sF3 = add(0,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
tff(f69,definition,
sF4 = count(sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
tff(f70,plain,
count(sF3) = sF4,
inference(reorient_equations,[],[f69]) ).
tff(f71,definition,
sF5 = add(sK0,sK1),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
tff(f72,plain,
add(sK0,sK1) = sF5,
inference(reorient_equations,[],[f71]) ).
tff(f73,definition,
sF6 = remove(sK0,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
tff(f74,definition,
sF7 = add(0,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f75,definition,
sF8 = count(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f76,plain,
count(sF7) = sF8,
inference(reorient_equations,[],[f75]) ).
tff(f77,plain,
sF8 != sF4,
inference(definition_folding,[],[f54,f76,f74,f73,f72,f70,f68,f67]) ).
tff(f79,plain,
! [X0: $int,X1: collection] :
( ( count(remove(X0,X1)) = $sum(count(X1),-1) )
| ~ in(X0,X1) ),
inference(evaluation,[],[f62]) ).
tff(f81,definition,
( spl9_1
<=> ( sF8 = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl9_1])],[avatar_definition]) ).
tff(f84,plain,
~ spl9_1,
inference(avatar_split_clause,[],[f77,f81]) ).
tff(f86,definition,
( spl9_2
<=> ( count(sF7) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl9_2])],[avatar_definition]) ).
tff(f88,plain,
( ( count(sF7) = sF8 )
| ~ spl9_2 ),
inference(avatar_component_clause,[],[f86]) ).
tff(f89,plain,
spl9_2,
inference(avatar_split_clause,[],[f76,f86]) ).
tff(f91,definition,
( spl9_3
<=> ( sF7 = add(0,sF6) ) ),
introduced(definition,[new_symbols(definition,[spl9_3])],[avatar_definition]) ).
tff(f93,plain,
( ( sF7 = add(0,sF6) )
| ~ spl9_3 ),
inference(avatar_component_clause,[],[f91]) ).
tff(f94,plain,
spl9_3,
inference(avatar_split_clause,[],[f74,f91]) ).
tff(f96,definition,
( spl9_4
<=> ( remove(sK0,sK1) = sF2 ) ),
introduced(definition,[new_symbols(definition,[spl9_4])],[avatar_definition]) ).
tff(f98,plain,
( ( remove(sK0,sK1) = sF2 )
| ~ spl9_4 ),
inference(avatar_component_clause,[],[f96]) ).
tff(f99,plain,
spl9_4,
inference(avatar_split_clause,[],[f67,f96]) ).
tff(f106,definition,
( spl9_6
<=> ( count(sF3) = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl9_6])],[avatar_definition]) ).
tff(f108,plain,
( ( count(sF3) = sF4 )
| ~ spl9_6 ),
inference(avatar_component_clause,[],[f106]) ).
tff(f109,plain,
spl9_6,
inference(avatar_split_clause,[],[f70,f106]) ).
tff(f111,definition,
( spl9_7
<=> ( sF6 = remove(sK0,sF5) ) ),
introduced(definition,[new_symbols(definition,[spl9_7])],[avatar_definition]) ).
tff(f113,plain,
( ( sF6 = remove(sK0,sF5) )
| ~ spl9_7 ),
inference(avatar_component_clause,[],[f111]) ).
tff(f114,plain,
spl9_7,
inference(avatar_split_clause,[],[f73,f111]) ).
tff(f116,definition,
( spl9_8
<=> ( sF3 = add(0,sF2) ) ),
introduced(definition,[new_symbols(definition,[spl9_8])],[avatar_definition]) ).
tff(f118,plain,
( ( sF3 = add(0,sF2) )
| ~ spl9_8 ),
inference(avatar_component_clause,[],[f116]) ).
tff(f119,plain,
spl9_8,
inference(avatar_split_clause,[],[f68,f116]) ).
tff(f121,definition,
( spl9_9
<=> ( add(sK0,sK1) = sF5 ) ),
introduced(definition,[new_symbols(definition,[spl9_9])],[avatar_definition]) ).
tff(f123,plain,
( ( add(sK0,sK1) = sF5 )
| ~ spl9_9 ),
inference(avatar_component_clause,[],[f121]) ).
tff(f124,plain,
spl9_9,
inference(avatar_split_clause,[],[f72,f121]) ).
tff(f144,plain,
( ~ in(sK0,sF2)
| ~ spl9_4 ),
inference(superposition,[],[f55,f98]) ).
tff(f146,definition,
( spl9_13
<=> in(sK0,sF2) ),
introduced(definition,[new_symbols(definition,[spl9_13])],[avatar_definition]) ).
tff(f149,plain,
( ~ spl9_13
| ~ spl9_4 ),
inference(avatar_split_clause,[],[f144,f96,f146]) ).
tff(f150,plain,
( ~ in(sK0,sF6)
| ~ spl9_7 ),
inference(superposition,[],[f55,f113]) ).
tff(f152,definition,
( spl9_14
<=> in(sK0,sF6) ),
introduced(definition,[new_symbols(definition,[spl9_14])],[avatar_definition]) ).
tff(f154,plain,
( ~ in(sK0,sF6)
| spl9_14 ),
inference(avatar_component_clause,[],[f152]) ).
tff(f155,plain,
( ~ spl9_14
| ~ spl9_7 ),
inference(avatar_split_clause,[],[f150,f111,f152]) ).
tff(f162,plain,
( in(sK0,sF5)
| ~ spl9_9 ),
inference(superposition,[],[f57,f123]) ).
tff(f164,definition,
( spl9_16
<=> in(sK0,sF5) ),
introduced(definition,[new_symbols(definition,[spl9_16])],[avatar_definition]) ).
tff(f166,plain,
( in(sK0,sF5)
| ~ spl9_16 ),
inference(avatar_component_clause,[],[f164]) ).
tff(f167,plain,
( spl9_16
| ~ spl9_9 ),
inference(avatar_split_clause,[],[f162,f121,f164]) ).
tff(f188,plain,
( ! [X0: $int] :
( in(X0,sK1)
| ~ in(X0,sF2) )
| ~ spl9_4 ),
inference(superposition,[],[f41,f98]) ).
tff(f189,plain,
( ! [X0: $int] :
( in(X0,sF5)
| ~ in(X0,sF6) )
| ~ spl9_7 ),
inference(superposition,[],[f41,f113]) ).
tff(f192,plain,
( ! [X0: $int] :
( in(X0,sF5)
| ~ in(X0,sK1) )
| ~ spl9_9 ),
inference(superposition,[],[f52,f123]) ).
tff(f196,definition,
( spl9_21
<=> in(sK0,sK1) ),
introduced(definition,[new_symbols(definition,[spl9_21])],[avatar_definition]) ).
tff(f200,definition,
( spl9_22
<=> ( count(sK1) = count(sF2) ) ),
introduced(definition,[new_symbols(definition,[spl9_22])],[avatar_definition]) ).
tff(f201,plain,
( ( count(sK1) = count(sF2) )
| ~ spl9_22 ),
inference(avatar_component_clause,[],[f200]) ).
tff(f210,plain,
( ( count(sK1) = count(sF2) )
| in(sK0,sK1)
| ~ spl9_4 ),
inference(superposition,[],[f45,f98]) ).
tff(f217,plain,
( spl9_22
| spl9_21
| ~ spl9_4 ),
inference(avatar_split_clause,[],[f210,f96,f196,f200]) ).
tff(f218,plain,
( ( count(sF7) = count(sF6) )
| ~ in(0,sF6)
| ~ spl9_3 ),
inference(superposition,[],[f49,f93]) ).
tff(f219,plain,
( ( count(sF3) = count(sF2) )
| ~ in(0,sF2)
| ~ spl9_8 ),
inference(superposition,[],[f49,f118]) ).
tff(f220,plain,
( ~ in(sK0,sK1)
| ( count(sK1) = count(sF5) )
| ~ spl9_9 ),
inference(superposition,[],[f49,f123]) ).
tff(f223,plain,
( ( count(sF2) = sF4 )
| ~ in(0,sF2)
| ~ spl9_6
| ~ spl9_8 ),
inference(forward_demodulation,[],[f219,f108]) ).
tff(f225,plain,
( ~ in(0,sF6)
| ( count(sF6) = sF8 )
| ~ spl9_2
| ~ spl9_3 ),
inference(forward_demodulation,[],[f218,f88]) ).
tff(f227,definition,
( spl9_24
<=> in(0,sF2) ),
introduced(definition,[new_symbols(definition,[spl9_24])],[avatar_definition]) ).
tff(f229,plain,
( ~ in(0,sF2)
| spl9_24 ),
inference(avatar_component_clause,[],[f227]) ).
tff(f231,definition,
( spl9_25
<=> ( count(sF2) = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl9_25])],[avatar_definition]) ).
tff(f234,plain,
( ~ spl9_24
| spl9_25
| ~ spl9_6
| ~ spl9_8 ),
inference(avatar_split_clause,[],[f223,f116,f106,f231,f227]) ).
tff(f236,definition,
( spl9_26
<=> ( count(sK1) = count(sF5) ) ),
introduced(definition,[new_symbols(definition,[spl9_26])],[avatar_definition]) ).
tff(f241,definition,
( spl9_27
<=> in(0,sF6) ),
introduced(definition,[new_symbols(definition,[spl9_27])],[avatar_definition]) ).
tff(f243,plain,
( ~ in(0,sF6)
| spl9_27 ),
inference(avatar_component_clause,[],[f241]) ).
tff(f245,definition,
( spl9_28
<=> ( count(sF6) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl9_28])],[avatar_definition]) ).
tff(f247,plain,
( ( count(sF6) = sF8 )
| ~ spl9_28 ),
inference(avatar_component_clause,[],[f245]) ).
tff(f248,plain,
( ~ spl9_27
| spl9_28
| ~ spl9_2
| ~ spl9_3 ),
inference(avatar_split_clause,[],[f225,f91,f86,f245,f241]) ).
tff(f258,plain,
( ~ in(sK0,sK1)
| ( add(sK0,sF2) = sK1 )
| ~ spl9_4 ),
inference(superposition,[],[f56,f98]) ).
tff(f259,plain,
( ( add(sK0,sF6) = sF5 )
| ~ in(sK0,sF5)
| ~ spl9_7 ),
inference(superposition,[],[f56,f113]) ).
tff(f264,plain,
( ( add(sK0,sF6) = sF5 )
| ~ spl9_7
| ~ spl9_16 ),
inference(forward_subsumption_resolution,[],[f259,f166]) ).
tff(f267,definition,
( spl9_29
<=> ( add(sK0,sF6) = sF5 ) ),
introduced(definition,[new_symbols(definition,[spl9_29])],[avatar_definition]) ).
tff(f269,plain,
( ( add(sK0,sF6) = sF5 )
| ~ spl9_29 ),
inference(avatar_component_clause,[],[f267]) ).
tff(f270,plain,
( spl9_29
| ~ spl9_7
| ~ spl9_16 ),
inference(avatar_split_clause,[],[f264,f164,f111,f267]) ).
tff(f272,definition,
( spl9_30
<=> ( add(sK0,sF2) = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl9_30])],[avatar_definition]) ).
tff(f276,plain,
( ~ spl9_21
| spl9_26
| ~ spl9_9 ),
inference(avatar_split_clause,[],[f220,f121,f236,f196]) ).
tff(f277,plain,
( ~ spl9_21
| spl9_30
| ~ spl9_4 ),
inference(avatar_split_clause,[],[f258,f96,f272,f196]) ).
tff(f281,plain,
( ! [X0: $int] :
( in(X0,sF2)
| ( sK0 = X0 )
| ~ in(X0,sK1) )
| ~ spl9_4 ),
inference(superposition,[],[f43,f98]) ).
tff(f282,plain,
( ! [X0: $int] :
( in(X0,sF6)
| ~ in(X0,sF5)
| ( sK0 = X0 ) )
| ~ spl9_7 ),
inference(superposition,[],[f43,f113]) ).
tff(f287,plain,
( ! [X0: $int] :
( in(X0,sK1)
| ( sK0 = X0 )
| ~ in(X0,sF5) )
| ~ spl9_9 ),
inference(superposition,[],[f53,f123]) ).
tff(f312,plain,
( ( count(sF7) = $sum(count(sF6),1) )
| in(0,sF6)
| ~ spl9_3 ),
inference(superposition,[],[f60,f93]) ).
tff(f313,plain,
( ( count(sF3) = $sum(count(sF2),1) )
| in(0,sF2)
| ~ spl9_8 ),
inference(superposition,[],[f60,f118]) ).
tff(f314,plain,
( ( count(sF5) = $sum(count(sK1),1) )
| in(sK0,sK1)
| ~ spl9_9 ),
inference(superposition,[],[f60,f123]) ).
tff(f329,definition,
( spl9_34
<=> ( count(sF5) = $sum(count(sK1),1) ) ),
introduced(definition,[new_symbols(definition,[spl9_34])],[avatar_definition]) ).
tff(f331,plain,
( ( count(sF5) = $sum(count(sK1),1) )
| ~ spl9_34 ),
inference(avatar_component_clause,[],[f329]) ).
tff(f335,definition,
( spl9_35
<=> ( $sum(count(sF6),1) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl9_35])],[avatar_definition]) ).
tff(f341,definition,
( spl9_36
<=> ( $sum(count(sK1),1) = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl9_36])],[avatar_definition]) ).
tff(f343,plain,
( ( $sum(count(sK1),1) = sF4 )
| ~ spl9_36 ),
inference(avatar_component_clause,[],[f341]) ).
tff(f345,plain,
( ( count(sF3) = $sum(count(sK1),1) )
| in(0,sF2)
| ~ spl9_8
| ~ spl9_22 ),
inference(forward_demodulation,[],[f313,f201]) ).
tff(f347,plain,
( ( $sum(count(sF6),1) = sF8 )
| in(0,sF6)
| ~ spl9_2
| ~ spl9_3 ),
inference(forward_demodulation,[],[f312,f88]) ).
tff(f350,plain,
( in(0,sF2)
| ( $sum(count(sK1),1) = sF4 )
| ~ spl9_6
| ~ spl9_8
| ~ spl9_22 ),
inference(forward_demodulation,[],[f345,f108]) ).
tff(f352,plain,
( spl9_35
| spl9_27
| ~ spl9_2
| ~ spl9_3 ),
inference(avatar_split_clause,[],[f347,f91,f86,f241,f335]) ).
tff(f355,plain,
( spl9_36
| spl9_24
| ~ spl9_6
| ~ spl9_8
| ~ spl9_22 ),
inference(avatar_split_clause,[],[f350,f200,f116,f106,f227,f341]) ).
tff(f369,plain,
( ( $sum(count(sK1),-1) = count(sF2) )
| ~ in(sK0,sK1)
| ~ spl9_4 ),
inference(superposition,[],[f79,f98]) ).
tff(f370,plain,
( ~ in(sK0,sF5)
| ( $sum(count(sF5),-1) = count(sF6) )
| ~ spl9_7 ),
inference(superposition,[],[f79,f113]) ).
tff(f378,plain,
( ( $sum(count(sF5),-1) = count(sF6) )
| ~ spl9_7
| ~ spl9_16 ),
inference(forward_subsumption_resolution,[],[f370,f166]) ).
tff(f380,definition,
( spl9_38
<=> ( $sum(count(sF5),-1) = count(sF6) ) ),
introduced(definition,[new_symbols(definition,[spl9_38])],[avatar_definition]) ).
tff(f383,plain,
( spl9_38
| ~ spl9_7
| ~ spl9_16 ),
inference(avatar_split_clause,[],[f378,f164,f111,f380]) ).
tff(f403,plain,
( in(sK0,sF6)
| ( $sum(count(sF6),1) = count(sF5) )
| ~ spl9_29 ),
inference(superposition,[],[f60,f269]) ).
tff(f404,plain,
( ( $sum(count(sF6),1) = count(sF5) )
| spl9_14
| ~ spl9_29 ),
inference(forward_subsumption_resolution,[],[f403,f154]) ).
tff(f406,plain,
( ( $sum(sF8,1) = count(sF5) )
| spl9_14
| ~ spl9_28
| ~ spl9_29 ),
inference(forward_demodulation,[],[f404,f247]) ).
tff(f409,definition,
( spl9_40
<=> ( $sum(sF8,1) = count(sF5) ) ),
introduced(definition,[new_symbols(definition,[spl9_40])],[avatar_definition]) ).
tff(f412,plain,
( spl9_40
| spl9_14
| ~ spl9_28
| ~ spl9_29 ),
inference(avatar_split_clause,[],[f406,f267,f245,f152,f409]) ).
tff(f420,plain,
( ( count(sF5) = sF4 )
| ~ spl9_34
| ~ spl9_36 ),
inference(forward_demodulation,[],[f331,f343]) ).
tff(f422,definition,
( spl9_42
<=> ( count(sF5) = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl9_42])],[avatar_definition]) ).
tff(f425,plain,
( spl9_42
| ~ spl9_34
| ~ spl9_36 ),
inference(avatar_split_clause,[],[f420,f341,f329,f422]) ).
tff(f442,plain,
( ( 0 = sK0 )
| ~ in(0,sK1)
| ~ spl9_4
| spl9_24 ),
inference(resolution,[],[f281,f229]) ).
tff(f444,definition,
( spl9_45
<=> in(0,sK1) ),
introduced(definition,[new_symbols(definition,[spl9_45])],[avatar_definition]) ).
tff(f446,plain,
( ~ in(0,sK1)
| spl9_45 ),
inference(avatar_component_clause,[],[f444]) ).
tff(f448,definition,
( spl9_46
<=> ( 0 = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl9_46])],[avatar_definition]) ).
tff(f451,plain,
( ~ spl9_45
| spl9_46
| ~ spl9_4
| spl9_24 ),
inference(avatar_split_clause,[],[f442,f227,f96,f448,f444]) ).
tff(f452,plain,
( ~ in(0,sF2)
| ~ spl9_4
| spl9_45 ),
inference(resolution,[],[f446,f188]) ).
tff(f471,plain,
( ( 0 = sK0 )
| ~ in(0,sF5)
| ~ spl9_9
| spl9_45 ),
inference(resolution,[],[f287,f446]) ).
tff(f473,definition,
( spl9_49
<=> in(0,sF5) ),
introduced(definition,[new_symbols(definition,[spl9_49])],[avatar_definition]) ).
tff(f475,plain,
( ~ in(0,sF5)
| spl9_49 ),
inference(avatar_component_clause,[],[f473]) ).
tff(f476,plain,
( spl9_46
| ~ spl9_49
| ~ spl9_9
| spl9_45 ),
inference(avatar_split_clause,[],[f471,f444,f121,f473,f448]) ).
tff(f477,plain,
( ~ in(0,sK1)
| ~ spl9_9
| spl9_49 ),
inference(resolution,[],[f475,f192]) ).
tff(f478,plain,
( ~ in(0,sF6)
| ~ spl9_7
| spl9_49 ),
inference(resolution,[],[f475,f189]) ).
tff(f487,plain,
( ~ spl9_24
| ~ spl9_4
| spl9_45 ),
inference(avatar_split_clause,[],[f452,f444,f96,f227]) ).
tff(f488,plain,
( ~ spl9_27
| ~ spl9_7
| spl9_49 ),
inference(avatar_split_clause,[],[f478,f473,f111,f241]) ).
tff(f492,definition,
( spl9_51
<=> ( $sum(count(sK1),-1) = count(sF2) ) ),
introduced(definition,[new_symbols(definition,[spl9_51])],[avatar_definition]) ).
tff(f495,plain,
( ~ spl9_21
| spl9_51
| ~ spl9_4 ),
inference(avatar_split_clause,[],[f369,f96,f492,f196]) ).
tff(f498,plain,
( spl9_34
| spl9_21
| ~ spl9_9 ),
inference(avatar_split_clause,[],[f314,f121,f196,f329]) ).
tff(f499,plain,
( in(0,sF2)
| ( $sum(count(sF2),1) = sF4 )
| ~ spl9_6
| ~ spl9_8 ),
inference(forward_demodulation,[],[f313,f108]) ).
tff(f502,definition,
( spl9_52
<=> ( $sum(count(sF2),1) = sF4 ) ),
introduced(definition,[new_symbols(definition,[spl9_52])],[avatar_definition]) ).
tff(f506,plain,
( spl9_52
| spl9_24
| ~ spl9_6
| ~ spl9_8 ),
inference(avatar_split_clause,[],[f499,f116,f106,f227,f502]) ).
tff(f508,plain,
( ~ spl9_45
| ~ spl9_9
| spl9_49 ),
inference(avatar_split_clause,[],[f477,f473,f121,f444]) ).
tff(f510,plain,
( ( 0 = sK0 )
| ~ in(0,sF5)
| ~ spl9_7
| spl9_27 ),
inference(resolution,[],[f243,f282]) ).
tff(f511,plain,
( ~ spl9_49
| spl9_46
| ~ spl9_7
| spl9_27 ),
inference(avatar_split_clause,[],[f510,f241,f111,f448,f473]) ).
tff(f512,plain,
$false,
inference(avatar_smt_refutation,[],[f511,f508,f506,f498,f495,f488,f487,f476,f451,f425,f412,f383,f355,f352,f277,f276,f270,f248,f234,f217,f167,f155,f149,f124,f119,f114,f109,f99,f94,f89,f84]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT050_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.17 % Computer : n010.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 00:07:34 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.51/1.20 % (2480815)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.51/1.20 % (2480966)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2757980605:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.51/1.20 % (2480966)Instruction limit reached!
% 3.51/1.20 % (2480966)------------------------------
% 3.51/1.20 % (2480966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480966)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480966)Termination reason: Instruction limit
% 3.51/1.20 % (2480966)Termination phase: Saturation
% 3.51/1.20 % (2480966)Time elapsed: 0.003 s
% 3.51/1.20 % (2480966)Peak memory usage: 89 MB
% 3.51/1.20 % (2480966)Instructions burned: 7 (million)
% 3.51/1.20 % (2480965)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2827728618:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.51/1.20 % (2480964)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3684137500:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.51/1.20 % (2480968)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2095528857:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.51/1.20 % (2480962)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1231709509:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.51/1.20 % (2480963)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1530070937:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.51/1.20 % (2480965)Instruction limit reached!
% 3.51/1.20 % (2480965)------------------------------
% 3.51/1.20 % (2480965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480965)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480965)Termination reason: Instruction limit
% 3.51/1.20 % (2480965)Termination phase: Saturation
% 3.51/1.20 % (2480965)Time elapsed: 0.005 s
% 3.51/1.20 % (2480965)Peak memory usage: 88 MB
% 3.51/1.20 % (2480965)Instructions burned: 7 (million)
% 3.51/1.20 % (2480969)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2602515283:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.51/1.20 % (2480962)Refutation not found, incomplete strategy
% 3.51/1.20 % (2480962)------------------------------
% 3.51/1.20 % (2480962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480962)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480962)Termination reason: Refutation not found, incomplete strategy
% 3.51/1.20 % (2480962)Time elapsed: 0.033 s
% 3.51/1.20 % (2480962)Peak memory usage: 115 MB
% 3.51/1.20 % (2480962)Instructions burned: 11 (million)
% 3.51/1.20 % (2480968)Instruction limit reached!
% 3.51/1.20 % (2480968)------------------------------
% 3.51/1.20 % (2480968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480968)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480968)Termination reason: Instruction limit
% 3.51/1.20 % (2480968)Termination phase: Saturation
% 3.51/1.20 % (2480968)Time elapsed: 0.055 s
% 3.51/1.20 % (2480968)Peak memory usage: 115 MB
% 3.51/1.20 % (2480968)Instructions burned: 46 (million)
% 3.51/1.20 % (2480969)Instruction limit reached!
% 3.51/1.20 % (2480969)------------------------------
% 3.51/1.20 % (2480969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480969)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480969)Termination reason: Instruction limit
% 3.51/1.20 % (2480969)Termination phase: Saturation
% 3.51/1.20 % (2480969)Time elapsed: 0.052 s
% 3.51/1.20 % (2480969)Peak memory usage: 116 MB
% 3.51/1.20 % (2480969)Instructions burned: 34 (million)
% 3.51/1.20 % (2480963)First to succeed.
% 3.51/1.20 % (2480963)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2480815"
% 3.51/1.20 % (2480980)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2001073008:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.51/1.20 % (2480980)Instruction limit reached!
% 3.51/1.20 % (2480980)------------------------------
% 3.51/1.20 % (2480980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480980)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480980)Termination reason: Instruction limit
% 3.51/1.20 % (2480980)Termination phase: Saturation
% 3.51/1.20 % (2480980)Time elapsed: 0.006 s
% 3.51/1.20 % (2480980)Peak memory usage: 88 MB
% 3.51/1.20 % (2480980)Instructions burned: 15 (million)
% 3.51/1.20 % (2480964)Instruction limit reached!
% 3.51/1.20 % (2480964)------------------------------
% 3.51/1.20 % (2480964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480964)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480964)Termination reason: Instruction limit
% 3.51/1.20 % (2480964)Termination phase: Saturation
% 3.51/1.20 % (2480964)Time elapsed: 0.151 s
% 3.51/1.20 % (2480964)Peak memory usage: 117 MB
% 3.51/1.20 % (2480964)Instructions burned: 201 (million)
% 3.51/1.20 % (2480986)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=3984485773:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 3.51/1.20 % (2480986)Instruction limit reached!
% 3.51/1.20 % (2480986)------------------------------
% 3.51/1.20 % (2480986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480986)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480986)Termination reason: Instruction limit
% 3.51/1.20 % (2480986)Termination phase: Saturation
% 3.51/1.20 % (2480986)Time elapsed: 0.022 s
% 3.51/1.20 % (2480986)Peak memory usage: 89 MB
% 3.51/1.20 % (2480986)Instructions burned: 29 (million)
% 3.51/1.20 % (2480988)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=4024657639:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 3.51/1.20 % (2481007)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=4131975788:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 3.51/1.20 % (2480996)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1767207435:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.51/1.20 % (2480988)Instruction limit reached!
% 3.51/1.20 % (2480988)------------------------------
% 3.51/1.20 % (2480988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480988)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480988)Termination reason: Instruction limit
% 3.51/1.20 % (2480988)Termination phase: Saturation
% 3.51/1.20 % (2480988)Time elapsed: 0.012 s
% 3.51/1.20 % (2480988)Peak memory usage: 90 MB
% 3.51/1.20 % (2480988)Instructions burned: 17 (million)
% 3.51/1.20 % (2481007)Also succeeded, but the first one will report.
% 3.51/1.20 % (2480996)Instruction limit reached!
% 3.51/1.20 % (2480996)------------------------------
% 3.51/1.20 % (2480996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.51/1.20 % (2480996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.51/1.20 % (2480996)CaDiCaL version: 2.1.3
% 3.51/1.20 % (2480996)Termination reason: Instruction limit
% 3.51/1.20 % (2480996)Termination phase: Saturation
% 3.51/1.20 % (2480996)Time elapsed: 0.018 s
% 3.51/1.20 % (2480996)Peak memory usage: 89 MB
% 3.51/1.20 % (2480996)Instructions burned: 24 (million)
% 3.51/1.20 % (2480962)------------------------------
% 3.51/1.20 % (2480962)------------------------------
% 3.51/1.20 % (2481030)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=755587709:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 3.51/1.20 % (2481037)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=553690377:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 3.51/1.20 % (2480963)Refutation found. Thanks to Tanya!
% 3.51/1.20 % SZS status Theorem for theBenchmark
% 3.51/1.20 % SZS output start Proof for theBenchmark
% See solution above
% 4.47/1.39 % (2480963)------------------------------
% 4.47/1.39 % (2480963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.47/1.39 % (2480963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.47/1.39 % (2480963)CaDiCaL version: 2.1.3
% 4.47/1.39 % (2480963)Termination reason: Refutation
% 4.47/1.39 % (2480963)Time elapsed: 0.088 s
% 4.47/1.39 % (2480963)Peak memory usage: 117 MB
% 4.47/1.39 % (2480963)Instructions burned: 90 (million)
% 4.47/1.39 % (2480963)------------------------------
% 4.47/1.39 % (2480963)------------------------------
% 4.47/1.39 % (2480815)Success in time 0.543 s
% 4.47/1.39 % Vampire exiting
%------------------------------------------------------------------------------