%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEV425_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 : n020.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 12:57:40 PM UTC 2026
% Result : Theorem 11.31s 2.76s
% Output : Refutation 14.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 41
% Syntax : Number of formulae : 284 ( 75 unt; 0 typ; 32 def)
% Number of atoms : 631 ( 173 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 607 ( 260 ~; 245 |; 60 &)
% ( 35 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 157 ( 0 atm; 100 fun; 57 num; 0 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 : 25 ( 23 usr; 22 prp; 0-2 aty)
% Number of functors : 32 ( 26 usr; 23 con; 0-2 aty)
% Number of variables : 176 ( 0 sgn 153 !; 23 ?; 176 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
set: $tType ).
tff(type_def_6,type,
element: $tType ).
tff(func_def_0,type,
empty_set: set ).
tff(func_def_1,type,
singleton: element > set ).
tff(func_def_2,type,
intersection: ( set * set ) > set ).
tff(func_def_3,type,
union: ( set * set ) > set ).
tff(func_def_4,type,
difference: ( set * set ) > set ).
tff(func_def_5,type,
complement: set > set ).
tff(func_def_6,type,
cardinality: set > $int ).
tff(func_def_11,type,
sK0: set ).
tff(func_def_12,type,
sK1: set ).
tff(func_def_13,type,
sK2: set ).
tff(func_def_14,type,
sK3: set ).
tff(func_def_15,type,
sK4: element ).
tff(func_def_16,type,
sK5: element ).
tff(func_def_17,type,
sK6: element ).
tff(func_def_18,type,
sK7: set > element ).
tff(func_def_19,type,
sF8: set ).
tff(func_def_20,type,
sF9: set ).
tff(func_def_21,type,
sF10: set ).
tff(func_def_22,type,
sF11: set ).
tff(func_def_23,type,
sF12: $int ).
tff(func_def_24,type,
sF13: $int ).
tff(func_def_25,type,
sF14: set ).
tff(func_def_26,type,
sF15: set ).
tff(func_def_27,type,
sF16: set ).
tff(func_def_28,type,
sF17: set ).
tff(func_def_29,type,
sF18: $int ).
tff(func_def_31,type,
2: $int > $int ).
tff(pred_def_1,type,
member: ( element * set ) > $o ).
tff(pred_def_2,type,
subset: ( set * set ) > $o ).
tff(f1,axiom,
! [X0: set] :
( ! [X1: element] : ~ member(X1,X0)
<=> ( X0 = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',empty_set) ).
tff(f2,axiom,
! [X1: element,X0: element] :
( ( X0 = X1 )
<=> member(X0,singleton(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',singleton) ).
tff(f3,axiom,
! [X1: set,X0: set] :
( ! [X2: element] :
( member(X2,X0)
=> member(X2,X1) )
<=> subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subset) ).
tff(f4,axiom,
! [X1: set,X2: set,X0: element] :
( member(X0,intersection(X1,X2))
<=> ( member(X0,X1)
& member(X0,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',intersection) ).
tff(f5,axiom,
! [X0: element,X2: set,X1: set] :
( ( member(X0,X1)
| member(X0,X2) )
<=> member(X0,union(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',union) ).
tff(f8,axiom,
! [X0: set] :
( ( cardinality(X0) = 0 )
<=> ( X0 = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cardinality_empty_set) ).
tff(f10,axiom,
! [X1: set,X0: element] :
( ( cardinality(union(singleton(X0),X1)) = $sum(cardinality(X1),1) )
<=> ( intersection(singleton(X0),X1) = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cardinality_intersection_2) ).
tff(f12,axiom,
! [X1: set,X0: set] :
( ( intersection(X0,X1) = empty_set )
<=> ( cardinality(union(X0,X1)) = $sum(cardinality(X0),cardinality(X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cardinality_union) ).
tff(f13,conjecture,
! [X4: element,X5: element,X0: set,X2: set,X1: set,X6: element,X3: set] :
( ( ~ member(X6,X3)
& subset(X0,X1)
& subset(union(X2,singleton(X5)),X3)
& ~ member(X4,X1)
& subset(union(X1,singleton(X4)),X2)
& ~ member(X5,X2) )
=> ( cardinality(union(union(union(X0,singleton(X4)),singleton(X5)),singleton(X6))) = $sum(cardinality(X0),3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',vc5) ).
tff(f14,negated_conjecture,
~ ! [X4: element,X5: element,X0: set,X2: set,X1: set,X6: element,X3: set] :
( ( ~ member(X6,X3)
& subset(X0,X1)
& subset(union(X2,singleton(X5)),X3)
& ~ member(X4,X1)
& subset(union(X1,singleton(X4)),X2)
& ~ member(X5,X2) )
=> ( cardinality(union(union(union(X0,singleton(X4)),singleton(X5)),singleton(X6))) = $sum(cardinality(X0),3) ) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
tff(f15,plain,
~ ! [X1: element,X2: set,X5: element,X4: set,X3: set,X6: set,X0: element] :
( ( subset(union(X4,singleton(X0)),X3)
& ~ member(X1,X3)
& subset(union(X3,singleton(X1)),X6)
& ~ member(X5,X6)
& subset(X2,X4)
& ~ member(X0,X4) )
=> ( $sum(cardinality(X2),3) = cardinality(union(union(union(X2,singleton(X0)),singleton(X1)),singleton(X5))) ) ),
inference(rectify,[],[f14]) ).
tff(f16,plain,
! [X1: set,X0: set,X2: element] :
( member(X2,intersection(X0,X1))
<=> ( member(X2,X0)
& member(X2,X1) ) ),
inference(rectify,[],[f4]) ).
tff(f17,plain,
! [X1: set,X0: set] :
( ! [X2: element] :
( member(X2,X1)
=> member(X2,X0) )
<=> subset(X1,X0) ),
inference(rectify,[],[f3]) ).
tff(f19,plain,
! [X0: element,X1: element] :
( ( X0 = X1 )
<=> member(X1,singleton(X0)) ),
inference(rectify,[],[f2]) ).
tff(f22,plain,
! [X0: set,X1: element] :
( ( cardinality(union(singleton(X1),X0)) = $sum(cardinality(X0),1) )
<=> ( empty_set = intersection(singleton(X1),X0) ) ),
inference(rectify,[],[f10]) ).
tff(f23,plain,
! [X1: set,X2: set,X0: element] :
( ( member(X0,X1)
| member(X0,X2) )
<=> member(X0,union(X2,X1)) ),
inference(rectify,[],[f5]) ).
tff(f24,plain,
! [X0: set,X1: set] :
( ( empty_set = intersection(X1,X0) )
<=> ( cardinality(union(X1,X0)) = $sum(cardinality(X1),cardinality(X0)) ) ),
inference(rectify,[],[f12]) ).
tff(f26,plain,
! [X1: set,X0: set] :
( subset(X1,X0)
=> ! [X2: element] :
( member(X2,X1)
=> member(X2,X0) ) ),
inference(unused_predicate_definition_removal,[],[f17]) ).
tff(f27,plain,
! [X0: set,X1: set] :
( ~ subset(X1,X0)
| ! [X2: element] :
( ~ member(X2,X1)
| member(X2,X0) ) ),
inference(ennf_transformation,[],[f26]) ).
tff(f28,plain,
? [X1: element,X2: set,X5: element,X4: set,X3: set,X6: set,X0: element] :
( ( $sum(cardinality(X2),3) != cardinality(union(union(union(X2,singleton(X0)),singleton(X1)),singleton(X5))) )
& subset(union(X4,singleton(X0)),X3)
& ~ member(X1,X3)
& subset(union(X3,singleton(X1)),X6)
& ~ member(X5,X6)
& subset(X2,X4)
& ~ member(X0,X4) ),
inference(ennf_transformation,[],[f15]) ).
tff(f29,plain,
? [X4: set,X3: set,X2: set,X6: set,X5: element,X1: element,X0: element] :
( subset(X2,X4)
& subset(union(X3,singleton(X1)),X6)
& subset(union(X4,singleton(X0)),X3)
& ( $sum(cardinality(X2),3) != cardinality(union(union(union(X2,singleton(X0)),singleton(X1)),singleton(X5))) )
& ~ member(X1,X3)
& ~ member(X0,X4)
& ~ member(X5,X6) ),
inference(flattening,[],[f28]) ).
tff(f32,plain,
! [X0: element,X1: element] :
( ( ( X0 = X1 )
| ~ member(X1,singleton(X0)) )
& ( member(X1,singleton(X0))
| ( X0 != X1 ) ) ),
inference(nnf_transformation,[],[f19]) ).
tff(f34,plain,
? [X0: set,X1: set,X2: set,X3: set,X4: element,X5: element,X6: element] :
( subset(X2,X0)
& subset(union(X1,singleton(X5)),X3)
& subset(union(X0,singleton(X6)),X1)
& ( cardinality(union(union(union(X2,singleton(X6)),singleton(X5)),singleton(X4))) != $sum(cardinality(X2),3) )
& ~ member(X5,X1)
& ~ member(X6,X0)
& ~ member(X4,X3) ),
inference(rectify,[],[f29]) ).
tff(f35,plain,
( subset(sK2,sK0)
& subset(union(sK1,singleton(sK5)),sK3)
& subset(union(sK0,singleton(sK6)),sK1)
& ( $sum(cardinality(sK2),3) != cardinality(union(union(union(sK2,singleton(sK6)),singleton(sK5)),singleton(sK4))) )
& ~ member(sK5,sK1)
& ~ member(sK6,sK0)
& ~ member(sK4,sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X4,sK4),skolemize(X5,sK5),skolemize(X6,sK6)],[f34]) ).
tff(f38,plain,
! [X1: set,X2: set,X0: element] :
( ( member(X0,X1)
| member(X0,X2)
| ~ member(X0,union(X2,X1)) )
& ( member(X0,union(X2,X1))
| ( ~ member(X0,X1)
& ~ member(X0,X2) ) ) ),
inference(nnf_transformation,[],[f23]) ).
tff(f39,plain,
! [X1: set,X2: set,X0: element] :
( ( member(X0,X1)
| member(X0,X2)
| ~ member(X0,union(X2,X1)) )
& ( member(X0,union(X2,X1))
| ( ~ member(X0,X1)
& ~ member(X0,X2) ) ) ),
inference(flattening,[],[f38]) ).
tff(f40,plain,
! [X0: set,X1: set,X2: element] :
( ( member(X2,X0)
| member(X2,X1)
| ~ member(X2,union(X1,X0)) )
& ( member(X2,union(X1,X0))
| ( ~ member(X2,X0)
& ~ member(X2,X1) ) ) ),
inference(rectify,[],[f39]) ).
tff(f44,plain,
! [X0: set] :
( ( ( cardinality(X0) = 0 )
| ( empty_set != X0 ) )
& ( ( X0 = empty_set )
| ( cardinality(X0) != 0 ) ) ),
inference(nnf_transformation,[],[f8]) ).
tff(f45,plain,
! [X0: set] :
( ( ! [X1: element] : ~ member(X1,X0)
| ( empty_set != X0 ) )
& ( ( X0 = empty_set )
| ? [X1: element] : member(X1,X0) ) ),
inference(nnf_transformation,[],[f1]) ).
tff(f46,plain,
! [X0: set] :
( ( ! [X1: element] : ~ member(X1,X0)
| ( empty_set != X0 ) )
& ( ( X0 = empty_set )
| ? [X2: element] : member(X2,X0) ) ),
inference(rectify,[],[f45]) ).
tff(f47,plain,
! [X0: set] :
( ( ! [X1: element] : ~ member(X1,X0)
| ( empty_set != X0 ) )
& ( ( X0 = empty_set )
| member(sK7(X0),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0))],[f46]) ).
tff(f48,plain,
! [X1: set,X0: set,X2: element] :
( ( member(X2,intersection(X0,X1))
| ~ member(X2,X0)
| ~ member(X2,X1) )
& ( ( member(X2,X0)
& member(X2,X1) )
| ~ member(X2,intersection(X0,X1)) ) ),
inference(nnf_transformation,[],[f16]) ).
tff(f49,plain,
! [X1: set,X0: set,X2: element] :
( ( member(X2,intersection(X0,X1))
| ~ member(X2,X0)
| ~ member(X2,X1) )
& ( ( member(X2,X0)
& member(X2,X1) )
| ~ member(X2,intersection(X0,X1)) ) ),
inference(flattening,[],[f48]) ).
tff(f50,plain,
! [X0: set,X1: set,X2: element] :
( ( member(X2,intersection(X1,X0))
| ~ member(X2,X1)
| ~ member(X2,X0) )
& ( ( member(X2,X1)
& member(X2,X0) )
| ~ member(X2,intersection(X1,X0)) ) ),
inference(rectify,[],[f49]) ).
tff(f51,plain,
! [X0: set,X1: set] :
( ( ( empty_set = intersection(X1,X0) )
| ( cardinality(union(X1,X0)) != $sum(cardinality(X1),cardinality(X0)) ) )
& ( ( cardinality(union(X1,X0)) = $sum(cardinality(X1),cardinality(X0)) )
| ( empty_set != intersection(X1,X0) ) ) ),
inference(nnf_transformation,[],[f24]) ).
tff(f52,plain,
! [X0: set,X1: element] :
( ( ( cardinality(union(singleton(X1),X0)) = $sum(cardinality(X0),1) )
| ( empty_set != intersection(singleton(X1),X0) ) )
& ( ( empty_set = intersection(singleton(X1),X0) )
| ( cardinality(union(singleton(X1),X0)) != $sum(cardinality(X0),1) ) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f56,plain,
! [X0: element,X1: element] :
( ~ member(X1,singleton(X0))
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f59,plain,
~ member(sK4,sK3),
inference(cnf_transformation,[],[f35]) ).
tff(f60,plain,
~ member(sK6,sK0),
inference(cnf_transformation,[],[f35]) ).
tff(f61,plain,
~ member(sK5,sK1),
inference(cnf_transformation,[],[f35]) ).
tff(f62,plain,
$sum(cardinality(sK2),3) != cardinality(union(union(union(sK2,singleton(sK6)),singleton(sK5)),singleton(sK4))),
inference(cnf_transformation,[],[f35]) ).
tff(f63,plain,
subset(union(sK0,singleton(sK6)),sK1),
inference(cnf_transformation,[],[f35]) ).
tff(f64,plain,
subset(union(sK1,singleton(sK5)),sK3),
inference(cnf_transformation,[],[f35]) ).
tff(f65,plain,
subset(sK2,sK0),
inference(cnf_transformation,[],[f35]) ).
tff(f68,plain,
! [X2: element,X0: set,X1: set] :
( ~ subset(X1,X0)
| member(X2,X0)
| ~ member(X2,X1) ),
inference(cnf_transformation,[],[f27]) ).
tff(f69,plain,
! [X2: element,X0: set,X1: set] :
( member(X2,union(X1,X0))
| ~ member(X2,X1) ),
inference(cnf_transformation,[],[f40]) ).
tff(f70,plain,
! [X2: element,X0: set,X1: set] :
( member(X2,union(X1,X0))
| ~ member(X2,X0) ),
inference(cnf_transformation,[],[f40]) ).
tff(f71,plain,
! [X2: element,X0: set,X1: set] :
( ~ member(X2,union(X1,X0))
| member(X2,X0)
| member(X2,X1) ),
inference(cnf_transformation,[],[f40]) ).
tff(f76,plain,
! [X0: set] :
( ( cardinality(X0) = 0 )
| ( empty_set != X0 ) ),
inference(cnf_transformation,[],[f44]) ).
tff(f77,plain,
! [X0: set] :
( member(sK7(X0),X0)
| ( empty_set = X0 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f78,plain,
! [X0: set,X1: element] :
( ~ member(X1,X0)
| ( empty_set != X0 ) ),
inference(cnf_transformation,[],[f47]) ).
tff(f79,plain,
! [X2: element,X0: set,X1: set] :
( ~ member(X2,intersection(X1,X0))
| member(X2,X0) ),
inference(cnf_transformation,[],[f50]) ).
tff(f80,plain,
! [X2: element,X0: set,X1: set] :
( ~ member(X2,intersection(X1,X0))
| member(X2,X1) ),
inference(cnf_transformation,[],[f50]) ).
tff(f82,plain,
! [X0: set,X1: set] :
( ( empty_set != intersection(X1,X0) )
| ( cardinality(union(X1,X0)) = $sum(cardinality(X1),cardinality(X0)) ) ),
inference(cnf_transformation,[],[f51]) ).
tff(f85,plain,
! [X0: set,X1: element] :
( ( empty_set != intersection(singleton(X1),X0) )
| ( cardinality(union(singleton(X1),X0)) = $sum(cardinality(X0),1) ) ),
inference(cnf_transformation,[],[f52]) ).
tff(f87,plain,
0 = cardinality(empty_set),
inference(equality_resolution,[],[f76]) ).
tff(f88,plain,
! [X1: element] : ~ member(X1,empty_set),
inference(equality_resolution,[],[f78]) ).
tff(f89,definition,
sF8 = singleton(sK5),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f90,definition,
sF9 = union(sK1,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f91,plain,
subset(sF9,sK3),
inference(definition_folding,[],[f64,f90,f89]) ).
tff(f92,definition,
sF10 = singleton(sK6),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f93,definition,
sF11 = union(sK0,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f94,plain,
subset(sF11,sK1),
inference(definition_folding,[],[f63,f93,f92]) ).
tff(f95,definition,
sF12 = cardinality(sK2),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f96,definition,
sF13 = $sum(sF12,3),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f97,plain,
$sum(sF12,3) = sF13,
inference(reorient_equations,[],[f96]) ).
tff(f98,definition,
sF14 = union(sK2,sF10),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f99,plain,
union(sK2,sF10) = sF14,
inference(reorient_equations,[],[f98]) ).
tff(f100,definition,
sF15 = union(sF14,sF8),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f101,plain,
union(sF14,sF8) = sF15,
inference(reorient_equations,[],[f100]) ).
tff(f102,definition,
sF16 = singleton(sK4),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
tff(f103,definition,
sF17 = union(sF15,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
tff(f104,definition,
sF18 = cardinality(sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
tff(f105,plain,
cardinality(sF17) = sF18,
inference(reorient_equations,[],[f104]) ).
tff(f106,plain,
sF13 != sF18,
inference(definition_folding,[],[f62,f105,f103,f102,f101,f89,f99,f92,f97,f95]) ).
tff(f108,plain,
$sum(3,sF12) = sF13,
inference(evaluation,[],[f97]) ).
tff(f109,plain,
! [X0: set,X1: set] :
( ( empty_set != intersection(X1,X0) )
| ( $sum(cardinality(X0),cardinality(X1)) = cardinality(union(X1,X0)) ) ),
inference(evaluation,[],[f82]) ).
tff(f113,plain,
$sum(3,sF12) != sF18,
inference(superposition,[],[f106,f108]) ).
tff(f115,plain,
! [X0: element] :
( ~ member(X0,sF8)
| ( sK5 = X0 ) ),
inference(superposition,[],[f56,f89]) ).
tff(f116,plain,
! [X0: element] :
( ~ member(X0,sF10)
| ( sK6 = X0 ) ),
inference(superposition,[],[f56,f92]) ).
tff(f117,plain,
! [X0: element] :
( ~ member(X0,sF16)
| ( sK4 = X0 ) ),
inference(superposition,[],[f56,f102]) ).
tff(f175,plain,
! [X0: element] :
( ~ member(X0,sK0)
| member(X0,sF11) ),
inference(superposition,[],[f69,f93]) ).
tff(f176,plain,
! [X0: element] :
( ~ member(X0,sK1)
| member(X0,sF9) ),
inference(superposition,[],[f69,f90]) ).
tff(f184,plain,
! [X0: element] :
( ~ member(X0,sF10)
| member(X0,sF11) ),
inference(superposition,[],[f70,f93]) ).
tff(f185,plain,
! [X0: element] :
( ~ member(X0,sF8)
| member(X0,sF9) ),
inference(superposition,[],[f70,f90]) ).
tff(f196,plain,
! [X0: set,X1: set] :
( member(sK7(intersection(X0,X1)),X1)
| ( empty_set = intersection(X0,X1) ) ),
inference(resolution,[],[f79,f77]) ).
tff(f198,plain,
! [X0: set,X1: set] :
( member(sK7(intersection(X0,X1)),X0)
| ( empty_set = intersection(X0,X1) ) ),
inference(resolution,[],[f80,f77]) ).
tff(f200,plain,
! [X0: element] :
( ~ member(X0,sK2)
| member(X0,sK0) ),
inference(resolution,[],[f68,f65]) ).
tff(f201,plain,
! [X0: element] :
( ~ member(X0,sF9)
| member(X0,sK3) ),
inference(resolution,[],[f68,f91]) ).
tff(f202,plain,
! [X0: element] :
( ~ member(X0,sF11)
| member(X0,sK1) ),
inference(resolution,[],[f68,f94]) ).
tff(f220,plain,
! [X0: element] :
( ~ member(X0,sF14)
| member(X0,sF10)
| member(X0,sK2) ),
inference(superposition,[],[f71,f99]) ).
tff(f221,plain,
! [X0: element] :
( ~ member(X0,sF15)
| member(X0,sF8)
| member(X0,sF14) ),
inference(superposition,[],[f71,f101]) ).
tff(f272,definition,
( spl19_18
<=> ( empty_set = intersection(sF14,sF8) ) ),
introduced(definition,[new_symbols(definition,[spl19_18])],[avatar_definition]) ).
tff(f274,plain,
( ( empty_set = intersection(sF14,sF8) )
| ~ spl19_18 ),
inference(avatar_component_clause,[],[f272]) ).
tff(f276,definition,
( spl19_19
<=> ( $sum(cardinality(sF8),cardinality(sF14)) = cardinality(sF15) ) ),
introduced(definition,[new_symbols(definition,[spl19_19])],[avatar_definition]) ).
tff(f277,plain,
( ( $sum(cardinality(sF8),cardinality(sF14)) = cardinality(sF15) )
| ~ spl19_19 ),
inference(avatar_component_clause,[],[f276]) ).
tff(f278,plain,
( ( $sum(cardinality(sF8),cardinality(sF14)) != cardinality(sF15) )
| spl19_19 ),
inference(avatar_component_clause,[],[f276]) ).
tff(f284,definition,
( spl19_20
<=> ( empty_set = intersection(sK2,sF10) ) ),
introduced(definition,[new_symbols(definition,[spl19_20])],[avatar_definition]) ).
tff(f286,plain,
( ( empty_set = intersection(sK2,sF10) )
| ~ spl19_20 ),
inference(avatar_component_clause,[],[f284]) ).
tff(f288,definition,
( spl19_21
<=> ( cardinality(sF14) = $sum(sF12,cardinality(sF10)) ) ),
introduced(definition,[new_symbols(definition,[spl19_21])],[avatar_definition]) ).
tff(f289,plain,
( ( cardinality(sF14) = $sum(sF12,cardinality(sF10)) )
| ~ spl19_21 ),
inference(avatar_component_clause,[],[f288]) ).
tff(f293,definition,
( spl19_22
<=> ( empty_set = intersection(sF15,sF16) ) ),
introduced(definition,[new_symbols(definition,[spl19_22])],[avatar_definition]) ).
tff(f295,plain,
( ( empty_set = intersection(sF15,sF16) )
| ~ spl19_22 ),
inference(avatar_component_clause,[],[f293]) ).
tff(f297,definition,
( spl19_23
<=> ( $sum(cardinality(sF15),cardinality(sF16)) = sF18 ) ),
introduced(definition,[new_symbols(definition,[spl19_23])],[avatar_definition]) ).
tff(f298,plain,
( ( $sum(cardinality(sF15),cardinality(sF16)) = sF18 )
| ~ spl19_23 ),
inference(avatar_component_clause,[],[f297]) ).
tff(f332,plain,
! [X0: set] :
( ( empty_set != intersection(sF8,X0) )
| ( $sum(cardinality(X0),1) = cardinality(union(sF8,X0)) ) ),
inference(superposition,[],[f85,f89]) ).
tff(f333,plain,
! [X0: set] :
( ( empty_set != intersection(sF10,X0) )
| ( cardinality(union(sF10,X0)) = $sum(cardinality(X0),1) ) ),
inference(superposition,[],[f85,f92]) ).
tff(f334,plain,
! [X0: set] :
( ( empty_set != intersection(sF16,X0) )
| ( cardinality(union(sF16,X0)) = $sum(cardinality(X0),1) ) ),
inference(superposition,[],[f85,f102]) ).
tff(f701,plain,
! [X0: set] : ( empty_set = intersection(X0,empty_set) ),
inference(resolution,[],[f196,f88]) ).
tff(f715,plain,
! [X0: set] :
( ( sK7(intersection(X0,sF8)) = sK5 )
| ( empty_set = intersection(X0,sF8) ) ),
inference(resolution,[],[f196,f115]) ).
tff(f720,plain,
! [X0: set] :
( ( sK6 = sK7(intersection(X0,sF10)) )
| ( empty_set = intersection(X0,sF10) ) ),
inference(resolution,[],[f196,f116]) ).
tff(f728,plain,
! [X0: set] :
( ( sK7(intersection(X0,sF16)) = sK4 )
| ( empty_set = intersection(X0,sF16) ) ),
inference(resolution,[],[f196,f117]) ).
tff(f768,plain,
! [X0: set] :
( member(sK7(intersection(sK2,X0)),sK0)
| ( empty_set = intersection(sK2,X0) ) ),
inference(resolution,[],[f198,f200]) ).
tff(f779,plain,
! [X0: set] :
( member(sK7(intersection(sF14,X0)),sF10)
| ( empty_set = intersection(sF14,X0) )
| member(sK7(intersection(sF14,X0)),sK2) ),
inference(resolution,[],[f198,f220]) ).
tff(f781,plain,
! [X0: set] :
( member(sK7(intersection(sF15,X0)),sF14)
| ( empty_set = intersection(sF15,X0) )
| member(sK7(intersection(sF15,X0)),sF8) ),
inference(resolution,[],[f198,f221]) ).
tff(f1017,plain,
! [X0: set] :
( ( empty_set != empty_set )
| ( $sum(cardinality(empty_set),cardinality(X0)) = cardinality(union(X0,empty_set)) ) ),
inference(superposition,[],[f109,f701]) ).
tff(f1020,plain,
( ( cardinality(union(sF8,empty_set)) = $sum(cardinality(empty_set),1) )
| ( empty_set != empty_set ) ),
inference(superposition,[],[f332,f701]) ).
tff(f1022,plain,
( ( cardinality(union(sF10,empty_set)) = $sum(cardinality(empty_set),1) )
| ( empty_set != empty_set ) ),
inference(superposition,[],[f333,f701]) ).
tff(f1024,plain,
( ( empty_set != empty_set )
| ( cardinality(union(sF16,empty_set)) = $sum(cardinality(empty_set),1) ) ),
inference(superposition,[],[f334,f701]) ).
tff(f1026,plain,
cardinality(union(sF16,empty_set)) = $sum(cardinality(empty_set),1),
inference(trivial_inequality_removal,[],[f1024]) ).
tff(f1027,plain,
$sum(1,cardinality(empty_set)) = cardinality(union(sF16,empty_set)),
inference(evaluation,[],[f1026]) ).
tff(f1028,plain,
! [X0: set] : ( $sum(cardinality(empty_set),cardinality(X0)) = cardinality(union(X0,empty_set)) ),
inference(trivial_inequality_removal,[],[f1017]) ).
tff(f1029,plain,
! [X0: set] : ( $sum(cardinality(X0),cardinality(empty_set)) = cardinality(union(X0,empty_set)) ),
inference(evaluation,[],[f1028]) ).
tff(f1030,plain,
cardinality(union(sF10,empty_set)) = $sum(cardinality(empty_set),1),
inference(trivial_inequality_removal,[],[f1022]) ).
tff(f1031,plain,
cardinality(union(sF10,empty_set)) = $sum(1,cardinality(empty_set)),
inference(evaluation,[],[f1030]) ).
tff(f1033,plain,
cardinality(union(sF8,empty_set)) = $sum(cardinality(empty_set),1),
inference(trivial_inequality_removal,[],[f1020]) ).
tff(f1034,plain,
$sum(1,cardinality(empty_set)) = cardinality(union(sF8,empty_set)),
inference(evaluation,[],[f1033]) ).
tff(f1038,plain,
$sum(1,0) = cardinality(union(sF16,empty_set)),
inference(forward_demodulation,[],[f1027,f87]) ).
tff(f1039,plain,
1 = cardinality(union(sF16,empty_set)),
inference(evaluation,[],[f1038]) ).
tff(f1040,plain,
! [X0: set] : ( $sum(cardinality(X0),0) = cardinality(union(X0,empty_set)) ),
inference(forward_demodulation,[],[f1029,f87]) ).
tff(f1041,plain,
! [X0: set] : ( cardinality(X0) = cardinality(union(X0,empty_set)) ),
inference(evaluation,[],[f1040]) ).
tff(f1042,plain,
cardinality(union(sF10,empty_set)) = $sum(1,0),
inference(forward_demodulation,[],[f1031,f87]) ).
tff(f1043,plain,
1 = cardinality(union(sF10,empty_set)),
inference(evaluation,[],[f1042]) ).
tff(f1045,plain,
$sum(1,0) = cardinality(union(sF8,empty_set)),
inference(forward_demodulation,[],[f1034,f87]) ).
tff(f1046,plain,
1 = cardinality(union(sF8,empty_set)),
inference(evaluation,[],[f1045]) ).
tff(f1469,definition,
( spl19_106
<=> member(sK5,sK1) ),
introduced(definition,[new_symbols(definition,[spl19_106])],[avatar_definition]) ).
tff(f1471,plain,
( member(sK5,sK1)
| ~ spl19_106 ),
inference(avatar_component_clause,[],[f1469]) ).
tff(f1473,plain,
( $false
| ~ spl19_106 ),
inference(resolution,[],[f1471,f61]) ).
tff(f1475,plain,
~ spl19_106,
inference(avatar_contradiction_clause,[],[f1473]) ).
tff(f1537,plain,
( ( empty_set = intersection(sK2,sF10) )
| member(sK6,sK0)
| ( empty_set = intersection(sK2,sF10) ) ),
inference(superposition,[],[f768,f720]) ).
tff(f1539,plain,
( ( empty_set = intersection(sK2,sF10) )
| member(sK6,sK0) ),
inference(duplicate_literal_removal,[],[f1537]) ).
tff(f1545,definition,
( spl19_114
<=> member(sK5,sK0) ),
introduced(definition,[new_symbols(definition,[spl19_114])],[avatar_definition]) ).
tff(f1547,plain,
( member(sK5,sK0)
| ~ spl19_114 ),
inference(avatar_component_clause,[],[f1545]) ).
tff(f1550,definition,
( spl19_115
<=> member(sK6,sK0) ),
introduced(definition,[new_symbols(definition,[spl19_115])],[avatar_definition]) ).
tff(f1552,plain,
( member(sK6,sK0)
| ~ spl19_115 ),
inference(avatar_component_clause,[],[f1550]) ).
tff(f1553,plain,
( spl19_115
| spl19_20 ),
inference(avatar_split_clause,[],[f1539,f284,f1550]) ).
tff(f1554,plain,
( $false
| ~ spl19_115 ),
inference(resolution,[],[f1552,f60]) ).
tff(f1556,plain,
~ spl19_115,
inference(avatar_contradiction_clause,[],[f1554]) ).
tff(f1561,plain,
( ( cardinality(union(sK2,sF10)) = $sum(cardinality(sF10),cardinality(sK2)) )
| ( empty_set != empty_set )
| ~ spl19_20 ),
inference(superposition,[],[f109,f286]) ).
tff(f1563,plain,
( ( cardinality(union(sK2,sF10)) = $sum(cardinality(sF10),cardinality(sK2)) )
| ~ spl19_20 ),
inference(trivial_inequality_removal,[],[f1561]) ).
tff(f1564,plain,
( ( $sum(cardinality(sK2),cardinality(sF10)) = cardinality(union(sK2,sF10)) )
| ~ spl19_20 ),
inference(evaluation,[],[f1563]) ).
tff(f1565,plain,
( ( $sum(cardinality(sK2),cardinality(sF10)) = cardinality(sF14) )
| ~ spl19_20 ),
inference(forward_demodulation,[],[f1564,f99]) ).
tff(f1566,plain,
( ( cardinality(sF14) = $sum(sF12,cardinality(sF10)) )
| ~ spl19_20 ),
inference(forward_demodulation,[],[f1565,f95]) ).
tff(f1567,plain,
( spl19_21
| ~ spl19_20 ),
inference(avatar_split_clause,[],[f1566,f284,f288]) ).
tff(f1570,plain,
( ( $sum(cardinality(sF8),$sum(sF12,cardinality(sF10))) != cardinality(sF15) )
| spl19_19
| ~ spl19_21 ),
inference(superposition,[],[f278,f289]) ).
tff(f1572,plain,
( ( $sum(sF12,$sum(cardinality(sF8),cardinality(sF10))) != cardinality(sF15) )
| spl19_19
| ~ spl19_21 ),
inference(evaluation,[],[f1570]) ).
tff(f1673,definition,
( spl19_120
<=> member(sK4,sK1) ),
introduced(definition,[new_symbols(definition,[spl19_120])],[avatar_definition]) ).
tff(f1675,plain,
( member(sK4,sK1)
| ~ spl19_120 ),
inference(avatar_component_clause,[],[f1673]) ).
tff(f1682,definition,
( spl19_122
<=> member(sK4,sK3) ),
introduced(definition,[new_symbols(definition,[spl19_122])],[avatar_definition]) ).
tff(f1684,plain,
( member(sK4,sK3)
| ~ spl19_122 ),
inference(avatar_component_clause,[],[f1682]) ).
tff(f1690,plain,
( member(sK4,sF9)
| ~ spl19_120 ),
inference(resolution,[],[f1675,f176]) ).
tff(f1700,definition,
( spl19_124
<=> member(sK5,sF11) ),
introduced(definition,[new_symbols(definition,[spl19_124])],[avatar_definition]) ).
tff(f1702,plain,
( member(sK5,sF11)
| ~ spl19_124 ),
inference(avatar_component_clause,[],[f1700]) ).
tff(f1713,definition,
( spl19_127
<=> member(sK4,sF11) ),
introduced(definition,[new_symbols(definition,[spl19_127])],[avatar_definition]) ).
tff(f1715,plain,
( member(sK4,sF11)
| ~ spl19_127 ),
inference(avatar_component_clause,[],[f1713]) ).
tff(f1717,plain,
( $false
| ~ spl19_122 ),
inference(resolution,[],[f1684,f59]) ).
tff(f1718,plain,
~ spl19_122,
inference(avatar_contradiction_clause,[],[f1717]) ).
tff(f1728,definition,
( spl19_128
<=> member(sK4,sF9) ),
introduced(definition,[new_symbols(definition,[spl19_128])],[avatar_definition]) ).
tff(f1730,plain,
( member(sK4,sF9)
| ~ spl19_128 ),
inference(avatar_component_clause,[],[f1728]) ).
tff(f1737,plain,
( member(sK5,sK1)
| ~ spl19_124 ),
inference(resolution,[],[f1702,f202]) ).
tff(f1738,plain,
( spl19_106
| ~ spl19_124 ),
inference(avatar_split_clause,[],[f1737,f1700,f1469]) ).
tff(f1740,definition,
( spl19_130
<=> member(sK5,sF10) ),
introduced(definition,[new_symbols(definition,[spl19_130])],[avatar_definition]) ).
tff(f1742,plain,
( member(sK5,sF10)
| ~ spl19_130 ),
inference(avatar_component_clause,[],[f1740]) ).
tff(f1763,plain,
( spl19_128
| ~ spl19_120 ),
inference(avatar_split_clause,[],[f1690,f1673,f1728]) ).
tff(f1774,plain,
( member(sK4,sK3)
| ~ spl19_128 ),
inference(resolution,[],[f1730,f201]) ).
tff(f1775,plain,
( spl19_122
| ~ spl19_128 ),
inference(avatar_split_clause,[],[f1774,f1728,f1682]) ).
tff(f1865,definition,
( spl19_140
<=> member(sK4,sF14) ),
introduced(definition,[new_symbols(definition,[spl19_140])],[avatar_definition]) ).
tff(f1867,plain,
( member(sK4,sF14)
| ~ spl19_140 ),
inference(avatar_component_clause,[],[f1865]) ).
tff(f1954,definition,
( spl19_144
<=> member(sK4,sF8) ),
introduced(definition,[new_symbols(definition,[spl19_144])],[avatar_definition]) ).
tff(f1956,plain,
( member(sK4,sF8)
| ~ spl19_144 ),
inference(avatar_component_clause,[],[f1954]) ).
tff(f1969,definition,
( spl19_145
<=> member(sK4,sF10) ),
introduced(definition,[new_symbols(definition,[spl19_145])],[avatar_definition]) ).
tff(f1971,plain,
( member(sK4,sF10)
| ~ spl19_145 ),
inference(avatar_component_clause,[],[f1969]) ).
tff(f1986,plain,
( member(sK4,sF11)
| ~ spl19_145 ),
inference(resolution,[],[f1971,f184]) ).
tff(f1988,plain,
( spl19_127
| ~ spl19_145 ),
inference(avatar_split_clause,[],[f1986,f1969,f1713]) ).
tff(f3327,definition,
( spl19_239
<=> member(sK4,sK0) ),
introduced(definition,[new_symbols(definition,[spl19_239])],[avatar_definition]) ).
tff(f3329,plain,
( member(sK4,sK0)
| ~ spl19_239 ),
inference(avatar_component_clause,[],[f3327]) ).
tff(f3411,plain,
( member(sK5,sF11)
| ~ spl19_114 ),
inference(resolution,[],[f1547,f175]) ).
tff(f3412,plain,
( spl19_124
| ~ spl19_114 ),
inference(avatar_split_clause,[],[f3411,f1545,f1700]) ).
tff(f3436,plain,
( member(sK4,sF11)
| ~ spl19_239 ),
inference(resolution,[],[f3329,f175]) ).
tff(f3437,plain,
( spl19_127
| ~ spl19_239 ),
inference(avatar_split_clause,[],[f3436,f3327,f1713]) ).
tff(f3455,plain,
( member(sK4,sK1)
| ~ spl19_127 ),
inference(resolution,[],[f1715,f202]) ).
tff(f3456,plain,
( spl19_120
| ~ spl19_127 ),
inference(avatar_split_clause,[],[f3455,f1713,f1673]) ).
tff(f3614,plain,
( member(sK4,sF10)
| member(sK4,sK2)
| ~ spl19_140 ),
inference(resolution,[],[f1867,f220]) ).
tff(f3617,definition,
( spl19_259
<=> member(sK4,sK2) ),
introduced(definition,[new_symbols(definition,[spl19_259])],[avatar_definition]) ).
tff(f3619,plain,
( member(sK4,sK2)
| ~ spl19_259 ),
inference(avatar_component_clause,[],[f3617]) ).
tff(f3620,plain,
( spl19_145
| spl19_259
| ~ spl19_140 ),
inference(avatar_split_clause,[],[f3614,f1865,f3617,f1969]) ).
tff(f3632,plain,
( member(sK4,sK0)
| ~ spl19_259 ),
inference(resolution,[],[f3619,f200]) ).
tff(f3633,plain,
( spl19_239
| ~ spl19_259 ),
inference(avatar_split_clause,[],[f3632,f3617,f3327]) ).
tff(f3770,definition,
( spl19_276
<=> member(sK5,sK2) ),
introduced(definition,[new_symbols(definition,[spl19_276])],[avatar_definition]) ).
tff(f3772,plain,
( member(sK5,sK2)
| ~ spl19_276 ),
inference(avatar_component_clause,[],[f3770]) ).
tff(f3865,plain,
( member(sK5,sF10)
| ( empty_set = intersection(sF14,sF8) )
| ( empty_set = intersection(sF14,sF8) )
| member(sK5,sK2) ),
inference(superposition,[],[f779,f715]) ).
tff(f3868,plain,
( member(sK5,sK2)
| ( empty_set = intersection(sF14,sF8) )
| member(sK5,sF10) ),
inference(duplicate_literal_removal,[],[f3865]) ).
tff(f3874,plain,
( spl19_276
| spl19_130
| spl19_18 ),
inference(avatar_split_clause,[],[f3868,f272,f1740,f3770]) ).
tff(f3889,plain,
( ( $sum(cardinality(sF8),cardinality(sF14)) = cardinality(union(sF14,sF8)) )
| ( empty_set != empty_set )
| ~ spl19_18 ),
inference(superposition,[],[f109,f274]) ).
tff(f3896,plain,
( ( $sum(cardinality(sF8),cardinality(sF14)) = cardinality(union(sF14,sF8)) )
| ~ spl19_18 ),
inference(trivial_inequality_removal,[],[f3889]) ).
tff(f3898,plain,
( ( $sum(cardinality(sF8),cardinality(sF14)) = cardinality(sF15) )
| ~ spl19_18 ),
inference(forward_demodulation,[],[f3896,f101]) ).
tff(f3899,plain,
( ( $sum(cardinality(sF8),$sum(sF12,cardinality(sF10))) = cardinality(sF15) )
| ~ spl19_18
| ~ spl19_21 ),
inference(forward_demodulation,[],[f3898,f289]) ).
tff(f3900,plain,
( ( $sum(sF12,$sum(cardinality(sF8),cardinality(sF10))) = cardinality(sF15) )
| ~ spl19_18
| ~ spl19_21 ),
inference(evaluation,[],[f3899]) ).
tff(f3964,plain,
( ( $sum(sF12,$sum(cardinality(sF8),cardinality(sF10))) != $sum(sF12,$sum(cardinality(sF8),cardinality(sF10))) )
| ~ spl19_18
| spl19_19
| ~ spl19_21 ),
inference(superposition,[],[f1572,f3900]) ).
tff(f3967,plain,
( $false
| ~ spl19_18
| spl19_19
| ~ spl19_21 ),
inference(trivial_inequality_removal,[],[f3964]) ).
tff(f3968,plain,
( ~ spl19_18
| spl19_19
| ~ spl19_21 ),
inference(avatar_contradiction_clause,[],[f3967]) ).
tff(f3994,plain,
( ( empty_set = intersection(sF15,sF16) )
| ( empty_set = intersection(sF15,sF16) )
| member(sK4,sF8)
| member(sK4,sF14) ),
inference(superposition,[],[f781,f728]) ).
tff(f4000,plain,
( ( empty_set = intersection(sF15,sF16) )
| member(sK4,sF8)
| member(sK4,sF14) ),
inference(duplicate_literal_removal,[],[f3994]) ).
tff(f4010,plain,
( spl19_22
| spl19_144
| spl19_140 ),
inference(avatar_split_clause,[],[f4000,f1865,f1954,f293]) ).
tff(f4015,plain,
( ( cardinality(union(sF15,sF16)) = $sum(cardinality(sF16),cardinality(sF15)) )
| ( empty_set != empty_set )
| ~ spl19_22 ),
inference(superposition,[],[f109,f295]) ).
tff(f4023,plain,
( ( cardinality(union(sF15,sF16)) = $sum(cardinality(sF16),cardinality(sF15)) )
| ~ spl19_22 ),
inference(trivial_inequality_removal,[],[f4015]) ).
tff(f4024,plain,
( ( $sum(cardinality(sF15),cardinality(sF16)) = cardinality(union(sF15,sF16)) )
| ~ spl19_22 ),
inference(evaluation,[],[f4023]) ).
tff(f4025,plain,
( ( cardinality(sF17) = $sum(cardinality(sF15),cardinality(sF16)) )
| ~ spl19_22 ),
inference(forward_demodulation,[],[f4024,f103]) ).
tff(f7697,plain,
( ( $sum(cardinality(sF15),cardinality(sF16)) = sF18 )
| ~ spl19_22 ),
inference(forward_demodulation,[],[f4025,f105]) ).
tff(f7711,plain,
( spl19_23
| ~ spl19_22 ),
inference(avatar_split_clause,[],[f7697,f293,f297]) ).
tff(f7718,plain,
( member(sK5,sK0)
| ~ spl19_276 ),
inference(resolution,[],[f3772,f200]) ).
tff(f7720,plain,
( spl19_114
| ~ spl19_276 ),
inference(avatar_split_clause,[],[f7718,f3770,f1545]) ).
tff(f7723,plain,
( member(sK5,sF11)
| ~ spl19_130 ),
inference(resolution,[],[f1742,f184]) ).
tff(f7726,plain,
( spl19_124
| ~ spl19_130 ),
inference(avatar_split_clause,[],[f7723,f1740,f1700]) ).
tff(f7729,plain,
( ( $sum(cardinality(sF8),$sum(sF12,cardinality(sF10))) = cardinality(sF15) )
| ~ spl19_19
| ~ spl19_21 ),
inference(forward_demodulation,[],[f277,f289]) ).
tff(f7730,plain,
( ( $sum(sF12,$sum(cardinality(sF8),cardinality(sF10))) = cardinality(sF15) )
| ~ spl19_19
| ~ spl19_21 ),
inference(evaluation,[],[f7729]) ).
tff(f7758,plain,
( member(sK4,sF9)
| ~ spl19_144 ),
inference(resolution,[],[f1956,f185]) ).
tff(f7762,plain,
( spl19_128
| ~ spl19_144 ),
inference(avatar_split_clause,[],[f7758,f1954,f1728]) ).
tff(f7763,plain,
( ( $sum($sum(sF12,$sum(cardinality(sF8),cardinality(sF10))),cardinality(sF16)) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(forward_demodulation,[],[f298,f7730]) ).
tff(f7764,plain,
( ( $sum(sF12,$sum(cardinality(sF8),$sum(cardinality(sF10),cardinality(sF16)))) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(evaluation,[],[f7763]) ).
tff(f9486,plain,
1 = cardinality(sF8),
inference(superposition,[],[f1041,f1046]) ).
tff(f9487,plain,
1 = cardinality(sF10),
inference(superposition,[],[f1041,f1043]) ).
tff(f9488,plain,
1 = cardinality(sF16),
inference(superposition,[],[f1041,f1039]) ).
tff(f9538,plain,
( ( $sum(sF12,$sum(cardinality(sF8),$sum(cardinality(sF10),1))) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(superposition,[],[f7764,f9488]) ).
tff(f9542,plain,
( ( $sum(1,$sum(sF12,$sum(cardinality(sF8),cardinality(sF10)))) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(evaluation,[],[f9538]) ).
tff(f9543,plain,
( ( $sum(1,$sum(sF12,$sum(cardinality(sF8),1))) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(forward_demodulation,[],[f9542,f9487]) ).
tff(f9544,plain,
( ( $sum(2,$sum(sF12,cardinality(sF8))) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(evaluation,[],[f9543]) ).
tff(f9545,plain,
( ( $sum(2,$sum(sF12,1)) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(forward_demodulation,[],[f9544,f9486]) ).
tff(f9546,plain,
( ( $sum(3,sF12) = sF18 )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(evaluation,[],[f9545]) ).
tff(f9667,plain,
( ( $sum(3,sF12) != $sum(3,sF12) )
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(superposition,[],[f113,f9546]) ).
tff(f9668,plain,
( $false
| ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(trivial_inequality_removal,[],[f9667]) ).
tff(f9669,plain,
( ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(avatar_contradiction_clause,[],[f9668]) ).
cnf(s103,plain,
~ spl19_106,
inference(sat_conversion,[],[f1475]) ).
cnf(s110,plain,
( spl19_20
| spl19_115 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s111,plain,
~ spl19_115,
inference(sat_conversion,[],[f1556]) ).
cnf(s112,plain,
( ~ spl19_20
| spl19_21 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s128,plain,
~ spl19_122,
inference(sat_conversion,[],[f1718]) ).
cnf(s130,plain,
( spl19_106
| ~ spl19_124 ),
inference(sat_conversion,[],[f1738]) ).
cnf(s133,plain,
( ~ spl19_120
| spl19_128 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s135,plain,
( spl19_122
| ~ spl19_128 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s156,plain,
( spl19_127
| ~ spl19_145 ),
inference(sat_conversion,[],[f1988]) ).
cnf(s240,plain,
( ~ spl19_114
| spl19_124 ),
inference(sat_conversion,[],[f3412]) ).
cnf(s244,plain,
( spl19_127
| ~ spl19_239 ),
inference(sat_conversion,[],[f3437]) ).
cnf(s247,plain,
( spl19_120
| ~ spl19_127 ),
inference(sat_conversion,[],[f3456]) ).
cnf(s250,plain,
( ~ spl19_140
| spl19_145
| spl19_259 ),
inference(sat_conversion,[],[f3620]) ).
cnf(s252,plain,
( spl19_239
| ~ spl19_259 ),
inference(sat_conversion,[],[f3633]) ).
cnf(s268,plain,
( spl19_18
| spl19_130
| spl19_276 ),
inference(sat_conversion,[],[f3874]) ).
cnf(s275,plain,
( ~ spl19_18
| spl19_19
| ~ spl19_21 ),
inference(sat_conversion,[],[f3968]) ).
cnf(s278,plain,
( spl19_22
| spl19_140
| spl19_144 ),
inference(sat_conversion,[],[f4010]) ).
cnf(s530,plain,
( ~ spl19_22
| spl19_23 ),
inference(sat_conversion,[],[f7711]) ).
cnf(s533,plain,
( spl19_114
| ~ spl19_276 ),
inference(sat_conversion,[],[f7720]) ).
cnf(s535,plain,
( spl19_124
| ~ spl19_130 ),
inference(sat_conversion,[],[f7726]) ).
cnf(s541,plain,
( spl19_128
| ~ spl19_144 ),
inference(sat_conversion,[],[f7762]) ).
cnf(s651,plain,
( ~ spl19_19
| ~ spl19_21
| ~ spl19_23 ),
inference(sat_conversion,[],[f9669]) ).
cnf(s661,plain,
~ spl19_128,
inference(rat,[],[s135,s128]) ).
cnf(s662,plain,
~ spl19_144,
inference(rat,[],[s541,s661]) ).
cnf(s666,plain,
~ spl19_120,
inference(rat,[],[s133,s661]) ).
cnf(s669,plain,
~ spl19_127,
inference(rat,[],[s247,s666]) ).
cnf(s671,plain,
~ spl19_239,
inference(rat,[],[s244,s669]) ).
cnf(s674,plain,
~ spl19_145,
inference(rat,[],[s156,s669]) ).
cnf(s676,plain,
~ spl19_259,
inference(rat,[],[s252,s671]) ).
cnf(s682,plain,
~ spl19_140,
inference(rat,[],[s250,s676,s674]) ).
cnf(s683,plain,
spl19_22,
inference(rat,[],[s278,s662,s682]) ).
cnf(s686,plain,
spl19_23,
inference(rat,[],[s530,s683]) ).
cnf(s691,plain,
spl19_20,
inference(rat,[],[s110,s111]) ).
cnf(s692,plain,
spl19_21,
inference(rat,[],[s112,s691]) ).
cnf(s693,plain,
~ spl19_19,
inference(rat,[],[s651,s686,s692]) ).
cnf(s694,plain,
~ spl19_18,
inference(rat,[],[s275,s692,s693]) ).
cnf(s697,plain,
~ spl19_124,
inference(rat,[],[s130,s103]) ).
cnf(s698,plain,
~ spl19_130,
inference(rat,[],[s535,s697]) ).
cnf(s699,plain,
~ spl19_114,
inference(rat,[],[s240,s697]) ).
cnf(s704,plain,
spl19_276,
inference(rat,[],[s268,s694,s698]) ).
cnf(s705,plain,
$false,
inference(rat,[],[s533,s704,s699]) ).
tff(f9670,plain,
$false,
inference(avatar_sat_refutation,[],[s705]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEV425_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.09/0.36 % Computer : n020.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 28 06:27:49 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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.09/1.44 % (4180215)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.09/1.44 % (4180226)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1785845588:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.09/1.44 % (4180226)Instruction limit reached!
% 3.09/1.44 % (4180226)------------------------------
% 3.09/1.44 % (4180226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.44 % (4180226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.44 % (4180226)CaDiCaL version: 2.1.3
% 3.09/1.44 % (4180226)Termination reason: Instruction limit
% 3.09/1.44 % (4180226)Termination phase: Saturation
% 3.09/1.44 % (4180226)Time elapsed: 0.028 s
% 3.09/1.44 % (4180226)Peak memory usage: 116 MB
% 3.09/1.44 % (4180226)Instructions burned: 34 (million)
% 3.09/1.44 % (4180225)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1331014357:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.09/1.44 % (4180222)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4189136010:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.09/1.44 % (4180220)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4007425343:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.09/1.44 % (4180221)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4251125496:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.09/1.44 % (4180223)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3904640731:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.09/1.44 % (4180224)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2072230850:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.09/1.44 % (4180224)Instruction limit reached!
% 3.09/1.44 % (4180224)------------------------------
% 3.09/1.44 % (4180224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.44 % (4180224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.44 % (4180224)CaDiCaL version: 2.1.3
% 3.09/1.44 % (4180224)Termination reason: Instruction limit
% 3.09/1.44 % (4180224)Termination phase: Saturation
% 3.09/1.44 % (4180224)Time elapsed: 0.004 s
% 3.09/1.44 % (4180224)Peak memory usage: 88 MB
% 3.09/1.44 % (4180224)Instructions burned: 5 (million)
% 3.09/1.44 % (4180223)Instruction limit reached!
% 3.09/1.44 % (4180223)------------------------------
% 3.09/1.44 % (4180223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.44 % (4180223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.44 % (4180223)CaDiCaL version: 2.1.3
% 3.09/1.44 % (4180223)Termination reason: Instruction limit
% 3.09/1.44 % (4180223)Termination phase: Saturation
% 3.09/1.44 % (4180223)Time elapsed: 0.005 s
% 3.09/1.44 % (4180223)Peak memory usage: 88 MB
% 3.09/1.44 % (4180223)Instructions burned: 7 (million)
% 3.09/1.44 % (4180220)Instruction limit reached!
% 3.09/1.44 % (4180220)------------------------------
% 3.09/1.44 % (4180220)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.44 % (4180220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.44 % (4180220)CaDiCaL version: 2.1.3
% 3.09/1.44 % (4180220)Termination reason: Instruction limit
% 3.09/1.44 % (4180220)Termination phase: Saturation
% 3.09/1.44 % (4180220)Time elapsed: 0.031 s
% 3.09/1.44 % (4180220)Peak memory usage: 115 MB
% 3.09/1.44 % (4180220)Instructions burned: 12 (million)
% 3.09/1.44 % (4180225)Instruction limit reached!
% 3.09/1.44 % (4180225)------------------------------
% 3.09/1.44 % (4180225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.09/1.44 % (4180225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.09/1.44 % (4180225)CaDiCaL version: 2.1.3
% 3.09/1.44 % (4180225)Termination reason: Instruction limit
% 3.09/1.44 % (4180225)Termination phase: Saturation
% 3.09/1.44 % (4180225)Time elapsed: 0.056 s
% 3.09/1.44 % (4180225)Peak memory usage: 115 MB
% 3.09/1.44 % (4180225)Instructions burned: 47 (million)
% 3.09/1.44 % (4180236)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2731554182:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.09/1.44 % (4180228)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=528360606:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 4.64/1.63 % (4180236)Instruction limit reached!
% 4.64/1.63 % (4180236)------------------------------
% 4.64/1.63 % (4180236)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/1.63 % (4180236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/1.63 % (4180236)CaDiCaL version: 2.1.3
% 4.64/1.63 % (4180236)Termination reason: Instruction limit
% 4.64/1.63 % (4180236)Termination phase: Saturation
% 4.64/1.63 % (4180236)Time elapsed: 0.006 s
% 4.64/1.63 % (4180236)Peak memory usage: 90 MB
% 4.64/1.63 % (4180236)Instructions burned: 16 (million)
% 4.64/1.63 % (4180228)Instruction limit reached!
% 4.64/1.63 % (4180228)------------------------------
% 4.64/1.63 % (4180228)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/1.63 % (4180228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/1.63 % (4180228)CaDiCaL version: 2.1.3
% 4.64/1.63 % (4180228)Termination reason: Instruction limit
% 4.64/1.63 % (4180228)Termination phase: Saturation
% 4.64/1.63 % (4180228)Time elapsed: 0.010 s
% 4.64/1.63 % (4180228)Peak memory usage: 89 MB
% 4.64/1.63 % (4180228)Instructions burned: 14 (million)
% 4.64/1.63 % (4180222)Instruction limit reached!
% 4.64/1.63 % (4180222)------------------------------
% 4.64/1.63 % (4180222)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/1.63 % (4180222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/1.63 % (4180222)CaDiCaL version: 2.1.3
% 4.64/1.63 % (4180222)Termination reason: Instruction limit
% 4.64/1.63 % (4180222)Termination phase: Saturation
% 4.64/1.63 % (4180222)Time elapsed: 0.156 s
% 4.64/1.63 % (4180222)Peak memory usage: 114 MB
% 4.64/1.63 % (4180222)Instructions burned: 202 (million)
% 4.64/1.63 % (4180235)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=2937462617:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 4.64/1.63 % (4180235)Instruction limit reached!
% 4.64/1.63 % (4180235)------------------------------
% 4.64/1.63 % (4180235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/1.63 % (4180235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/1.63 % (4180235)CaDiCaL version: 2.1.3
% 4.64/1.63 % (4180235)Termination reason: Instruction limit
% 4.64/1.63 % (4180235)Termination phase: Saturation
% 4.64/1.63 % (4180235)Time elapsed: 0.023 s
% 4.64/1.63 % (4180235)Peak memory usage: 89 MB
% 4.64/1.63 % (4180235)Instructions burned: 30 (million)
% 4.64/1.63 % (4180237)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=2043181240:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 4.64/1.63 % (4180238)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=259146784:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 4.64/1.63 % (4180221)Instruction limit reached!
% 4.64/1.63 % (4180221)------------------------------
% 4.64/1.63 % (4180221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/1.63 % (4180221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/1.63 % (4180221)CaDiCaL version: 2.1.3
% 4.64/1.63 % (4180221)Termination reason: Instruction limit
% 4.64/1.63 % (4180221)Termination phase: Saturation
% 4.64/1.63 % (4180221)Time elapsed: 0.210 s
% 4.64/1.63 % (4180221)Peak memory usage: 116 MB
% 4.64/1.63 % (4180221)Instructions burned: 308 (million)
% 4.64/1.63 % (4180237)Instruction limit reached!
% 4.64/1.63 % (4180237)------------------------------
% 4.64/1.63 % (4180237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/1.63 % (4180237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.64/1.63 % (4180237)CaDiCaL version: 2.1.3
% 4.64/1.63 % (4180237)Termination reason: Instruction limit
% 4.64/1.63 % (4180237)Termination phase: Saturation
% 4.64/1.63 % (4180237)Time elapsed: 0.019 s
% 4.64/1.63 % (4180237)Peak memory usage: 89 MB
% 4.64/1.63 % (4180237)Instructions burned: 24 (million)
% 4.64/1.63 % (4180238)Refutation not found, incomplete strategy
% 4.64/1.63 % (4180238)------------------------------
% 4.64/1.63 % (4180238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.64/1.63 % (4180238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.80 % (4180238)CaDiCaL version: 2.1.3
% 6.10/1.80 % (4180238)Termination reason: Refutation not found, incomplete strategy
% 6.10/1.80 % (4180238)Time elapsed: 0.010 s
% 6.10/1.80 % (4180238)Peak memory usage: 90 MB
% 6.10/1.80 % (4180238)Instructions burned: 11 (million)
% 6.10/1.80 % (4180241)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3836975883:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 6.10/1.80 % (4180241)Instruction limit reached!
% 6.10/1.80 % (4180241)------------------------------
% 6.10/1.80 % (4180241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.80 % (4180241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.80 % (4180241)CaDiCaL version: 2.1.3
% 6.10/1.80 % (4180241)Termination reason: Instruction limit
% 6.10/1.80 % (4180241)Termination phase: Saturation
% 6.10/1.80 % (4180241)Time elapsed: 0.026 s
% 6.10/1.80 % (4180241)Peak memory usage: 88 MB
% 6.10/1.80 % (4180241)Instructions burned: 88 (million)
% 6.10/1.80 % (4180242)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=730399020:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 6.10/1.80 % (4180242)Instruction limit reached!
% 6.10/1.80 % (4180242)------------------------------
% 6.10/1.80 % (4180242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.80 % (4180242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.80 % (4180242)CaDiCaL version: 2.1.3
% 6.10/1.80 % (4180242)Termination reason: Instruction limit
% 6.10/1.80 % (4180242)Termination phase: Saturation
% 6.10/1.80 % (4180242)Time elapsed: 0.003 s
% 6.10/1.80 % (4180242)Peak memory usage: 88 MB
% 6.10/1.80 % (4180242)Instructions burned: 3 (million)
% 6.10/1.80 % (4180243)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=561342379:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 6.10/1.80 % (4180246)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1935346556:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 6.10/1.80 % (4180246)Refutation not found, incomplete strategy
% 6.10/1.80 % (4180246)------------------------------
% 6.10/1.80 % (4180246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.80 % (4180246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.80 % (4180246)CaDiCaL version: 2.1.3
% 6.10/1.80 % (4180246)Termination reason: Refutation not found, incomplete strategy
% 6.10/1.80 % (4180246)Time elapsed: 0.003 s
% 6.10/1.80 % (4180246)Peak memory usage: 88 MB
% 6.10/1.80 % (4180246)Instructions burned: 3 (million)
% 6.10/1.80 % (4180248)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=2952999789:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 6.10/1.80 % (4180249)lrs+10_1_thi=all:si=on:fd=off:random_seed=2863190013:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 6.10/1.80 % (4180251)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=2846314243:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 6.10/1.80 % (4180251)Instruction limit reached!
% 6.10/1.80 % (4180251)------------------------------
% 6.10/1.80 % (4180251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.80 % (4180251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.80 % (4180251)CaDiCaL version: 2.1.3
% 6.10/1.80 % (4180251)Termination reason: Instruction limit
% 6.10/1.80 % (4180251)Termination phase: Saturation
% 6.10/1.80 % (4180251)Time elapsed: 0.004 s
% 6.10/1.80 % (4180251)Peak memory usage: 88 MB
% 6.10/1.80 % (4180251)Instructions burned: 11 (million)
% 6.10/1.80 % (4180249)Instruction limit reached!
% 6.10/1.80 % (4180249)------------------------------
% 6.10/1.80 % (4180249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.80 % (4180249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.80 % (4180249)CaDiCaL version: 2.1.3
% 6.10/1.80 % (4180249)Termination reason: Instruction limit
% 6.10/1.80 % (4180249)Termination phase: Saturation
% 6.10/1.80 % (4180249)Time elapsed: 0.059 s
% 6.10/1.80 % (4180249)Peak memory usage: 113 MB
% 6.10/1.80 % (4180249)Instructions burned: 53 (million)
% 6.10/1.80 % (4180243)Instruction limit reached!
% 8.71/2.05 % (4180243)------------------------------
% 8.71/2.05 % (4180243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.05 % (4180243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.05 % (4180243)CaDiCaL version: 2.1.3
% 8.71/2.05 % (4180243)Termination reason: Instruction limit
% 8.71/2.05 % (4180243)Termination phase: Saturation
% 8.71/2.05 % (4180243)Time elapsed: 0.126 s
% 8.71/2.05 % (4180243)Peak memory usage: 91 MB
% 8.71/2.05 % (4180243)Instructions burned: 182 (million)
% 8.71/2.05 % (4180248)Instruction limit reached!
% 8.71/2.05 % (4180248)------------------------------
% 8.71/2.05 % (4180248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.05 % (4180248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.05 % (4180248)CaDiCaL version: 2.1.3
% 8.71/2.05 % (4180248)Termination reason: Instruction limit
% 8.71/2.05 % (4180248)Termination phase: Saturation
% 8.71/2.05 % (4180248)Time elapsed: 0.090 s
% 8.71/2.05 % (4180248)Peak memory usage: 133 MB
% 8.71/2.05 % (4180248)Instructions burned: 66 (million)
% 8.71/2.05 % (4180238)------------------------------
% 8.71/2.05 % (4180238)------------------------------
% 8.71/2.05 % (4180253)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1486752327:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 8.71/2.05 % (4180253)Instruction limit reached!
% 8.71/2.05 % (4180253)------------------------------
% 8.71/2.05 % (4180253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.05 % (4180253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.05 % (4180253)CaDiCaL version: 2.1.3
% 8.71/2.05 % (4180253)Termination reason: Instruction limit
% 8.71/2.05 % (4180253)Termination phase: Saturation
% 8.71/2.05 % (4180253)Time elapsed: 0.003 s
% 8.71/2.05 % (4180253)Peak memory usage: 89 MB
% 8.71/2.05 % (4180253)Instructions burned: 3 (million)
% 8.71/2.05 % (4180259)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3221681242:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi)
% 8.71/2.05 % (4180259)Instruction limit reached!
% 8.71/2.05 % (4180259)------------------------------
% 8.71/2.05 % (4180259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.05 % (4180259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.05 % (4180259)CaDiCaL version: 2.1.3
% 8.71/2.05 % (4180259)Termination reason: Instruction limit
% 8.71/2.05 % (4180259)Termination phase: Saturation
% 8.71/2.05 % (4180259)Time elapsed: 0.002 s
% 8.71/2.05 % (4180259)Peak memory usage: 88 MB
% 8.71/2.05 % (4180259)Instructions burned: 3 (million)
% 8.71/2.05 % (4180261)dis+10_1_si=on:random_seed=4226858074:i=10:ep=R:rtra=on_2993 on theBenchmark for (2993ds/10Mi)
% 8.71/2.05 % (4180260)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=3399045677:i=127:doe=on:rtra=on_2993 on theBenchmark for (2993ds/127Mi)
% 8.71/2.05 % (4180261)Instruction limit reached!
% 8.71/2.05 % (4180261)------------------------------
% 8.71/2.05 % (4180261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.05 % (4180261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.05 % (4180261)CaDiCaL version: 2.1.3
% 8.71/2.05 % (4180261)Termination reason: Instruction limit
% 8.71/2.05 % (4180261)Termination phase: Saturation
% 8.71/2.05 % (4180261)Time elapsed: 0.008 s
% 8.71/2.05 % (4180261)Peak memory usage: 88 MB
% 8.71/2.05 % (4180261)Instructions burned: 10 (million)
% 8.71/2.05 % (4180246)------------------------------
% 8.71/2.05 % (4180246)------------------------------
% 8.71/2.05 % (4180262)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=606712279:i=26:canc=cautious:av=off:rtra=on_2993 on theBenchmark for (2993ds/26Mi)
% 8.71/2.05 % (4180262)Refutation not found, incomplete strategy
% 8.71/2.05 % (4180262)------------------------------
% 8.71/2.05 % (4180262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.71/2.05 % (4180262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/2.05 % (4180262)CaDiCaL version: 2.1.3
% 8.71/2.05 % (4180262)Termination reason: Refutation not found, incomplete strategy
% 8.71/2.05 % (4180262)Time elapsed: 0.003 s
% 8.71/2.05 % (4180262)Peak memory usage: 89 MB
% 8.71/2.05 % (4180262)Instructions burned: 3 (million)
% 8.71/2.05 % (4180267)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=3053169712:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi)
% 9.51/2.26 % (4180265)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=2082982933:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi)
% 9.51/2.26 % (4180264)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=1149406673: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_2993 on theBenchmark for (2993ds/35Mi)
% 9.51/2.26 % (4180267)Instruction limit reached!
% 9.51/2.26 % (4180267)------------------------------
% 9.51/2.26 % (4180267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.26 % (4180267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.26 % (4180267)CaDiCaL version: 2.1.3
% 9.51/2.26 % (4180267)Termination reason: Instruction limit
% 9.51/2.26 % (4180267)Termination phase: Saturation
% 9.51/2.26 % (4180267)Time elapsed: 0.005 s
% 9.51/2.26 % (4180267)Peak memory usage: 88 MB
% 9.51/2.26 % (4180267)Instructions burned: 10 (million)
% 9.51/2.26 % (4180265)Instruction limit reached!
% 9.51/2.26 % (4180265)------------------------------
% 9.51/2.26 % (4180265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.26 % (4180265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.26 % (4180265)CaDiCaL version: 2.1.3
% 9.51/2.26 % (4180265)Termination reason: Instruction limit
% 9.51/2.26 % (4180265)Termination phase: Saturation
% 9.51/2.26 % (4180265)Time elapsed: 0.002 s
% 9.51/2.26 % (4180265)Peak memory usage: 88 MB
% 9.51/2.26 % (4180265)Instructions burned: 2 (million)
% 9.51/2.26 % (4180264)Instruction limit reached!
% 9.51/2.26 % (4180264)------------------------------
% 9.51/2.26 % (4180264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.26 % (4180264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.26 % (4180264)CaDiCaL version: 2.1.3
% 9.51/2.26 % (4180264)Termination reason: Instruction limit
% 9.51/2.26 % (4180264)Termination phase: Saturation
% 9.51/2.26 % (4180264)Time elapsed: 0.028 s
% 9.51/2.26 % (4180264)Peak memory usage: 89 MB
% 9.51/2.26 % (4180264)Instructions burned: 35 (million)
% 9.51/2.26 % (4180260)Instruction limit reached!
% 9.51/2.26 % (4180260)------------------------------
% 9.51/2.26 % (4180260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.26 % (4180260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.26 % (4180260)CaDiCaL version: 2.1.3
% 9.51/2.26 % (4180260)Termination reason: Instruction limit
% 9.51/2.26 % (4180260)Termination phase: Saturation
% 9.51/2.26 % (4180260)Time elapsed: 0.106 s
% 9.51/2.26 % (4180260)Peak memory usage: 116 MB
% 9.51/2.26 % (4180260)Instructions burned: 129 (million)
% 9.51/2.26 % (4180276)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=2972300311:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi)
% 9.51/2.26 % (4180272)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=2685170001:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi)
% 9.51/2.26 % (4180270)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1407030102:i=370:ep=RS:fsr=off:rtra=on_2992 on theBenchmark for (2992ds/370Mi)
% 9.51/2.26 % (4180272)Instruction limit reached!
% 9.51/2.26 % (4180272)------------------------------
% 9.51/2.26 % (4180272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.26 % (4180272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.26 % (4180272)CaDiCaL version: 2.1.3
% 9.51/2.26 % (4180272)Termination reason: Instruction limit
% 9.51/2.26 % (4180272)Termination phase: Saturation
% 9.51/2.26 % (4180272)Time elapsed: 0.031 s
% 9.51/2.26 % (4180272)Peak memory usage: 113 MB
% 9.51/2.26 % (4180272)Instructions burned: 14 (million)
% 9.51/2.26 % (4180277)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=3020497280:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 9.51/2.26 % (4180277)Instruction limit reached!
% 9.51/2.26 % (4180277)------------------------------
% 9.51/2.26 % (4180277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.51/2.26 % (4180277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.51/2.26 % (4180277)CaDiCaL version: 2.1.3
% 10.51/2.58 % (4180277)Termination reason: Instruction limit
% 10.51/2.58 % (4180277)Termination phase: Saturation
% 10.51/2.58 % (4180277)Time elapsed: 0.009 s
% 10.51/2.58 % (4180277)Peak memory usage: 88 MB
% 10.51/2.58 % (4180277)Instructions burned: 11 (million)
% 10.51/2.58 % (4180278)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3903222912:i=71:rtra=on:gtg=exists_top_2991 on theBenchmark for (2991ds/71Mi)
% 10.51/2.58 % (4180276)Instruction limit reached!
% 10.51/2.58 % (4180276)------------------------------
% 10.51/2.58 % (4180276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.58 % (4180276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.58 % (4180276)CaDiCaL version: 2.1.3
% 10.51/2.58 % (4180276)Termination reason: Instruction limit
% 10.51/2.58 % (4180276)Termination phase: Saturation
% 10.51/2.58 % (4180276)Time elapsed: 0.079 s
% 10.51/2.58 % (4180276)Peak memory usage: 117 MB
% 10.51/2.58 % (4180276)Instructions burned: 227 (million)
% 10.51/2.58 % (4180262)------------------------------
% 10.51/2.58 % (4180262)------------------------------
% 10.51/2.58 % (4180279)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=1839523816:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi)
% 10.51/2.58 % (4180278)Instruction limit reached!
% 10.51/2.58 % (4180278)------------------------------
% 10.51/2.58 % (4180278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.58 % (4180278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.58 % (4180278)CaDiCaL version: 2.1.3
% 10.51/2.58 % (4180278)Termination reason: Instruction limit
% 10.51/2.58 % (4180278)Termination phase: Saturation
% 10.51/2.58 % (4180278)Time elapsed: 0.093 s
% 10.51/2.58 % (4180278)Peak memory usage: 133 MB
% 10.51/2.58 % (4180278)Instructions burned: 72 (million)
% 10.51/2.58 % (4180270)Instruction limit reached!
% 10.51/2.58 % (4180270)------------------------------
% 10.51/2.58 % (4180270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.58 % (4180270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.58 % (4180270)CaDiCaL version: 2.1.3
% 10.51/2.58 % (4180270)Termination reason: Instruction limit
% 10.51/2.58 % (4180270)Termination phase: Saturation
% 10.51/2.58 % (4180270)Time elapsed: 0.178 s
% 10.51/2.58 % (4180270)Peak memory usage: 90 MB
% 10.51/2.58 % (4180270)Instructions burned: 370 (million)
% 10.51/2.58 % (4180279)Instruction limit reached!
% 10.51/2.58 % (4180279)------------------------------
% 10.51/2.58 % (4180279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.58 % (4180279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.58 % (4180279)CaDiCaL version: 2.1.3
% 10.51/2.58 % (4180279)Termination reason: Instruction limit
% 10.51/2.58 % (4180279)Termination phase: Saturation
% 10.51/2.58 % (4180279)Time elapsed: 0.057 s
% 10.51/2.58 % (4180279)Peak memory usage: 91 MB
% 10.51/2.58 % (4180279)Instructions burned: 75 (million)
% 10.51/2.58 % (4180283)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=1328852737:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2990 on theBenchmark for (2990ds/294Mi)
% 10.51/2.58 % (4180287)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=2237930576:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi)
% 10.51/2.58 % (4180285)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=3556102199:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi)
% 10.51/2.58 % (4180287)Instruction limit reached!
% 10.51/2.58 % (4180287)------------------------------
% 10.51/2.58 % (4180287)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.51/2.58 % (4180287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.51/2.58 % (4180287)CaDiCaL version: 2.1.3
% 10.51/2.58 % (4180287)Termination reason: Instruction limit
% 10.51/2.58 % (4180287)Termination phase: Saturation
% 10.51/2.58 % (4180287)Time elapsed: 0.073 s
% 10.51/2.58 % (4180287)Peak memory usage: 133 MB
% 10.51/2.58 % (4180287)Instructions burned: 132 (million)
% 10.51/2.58 % (4180289)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1278684557:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2989 on theBenchmark for (2989ds/40Mi)
% 10.51/2.58 % (4180285)Instruction limit reached!
% 10.51/2.58 % (4180285)------------------------------
% 11.31/2.76 % (4180285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180285)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180285)Termination reason: Instruction limit
% 11.31/2.76 % (4180285)Termination phase: Saturation
% 11.31/2.76 % (4180285)Time elapsed: 0.107 s
% 11.31/2.76 % (4180285)Peak memory usage: 116 MB
% 11.31/2.76 % (4180285)Instructions burned: 131 (million)
% 11.31/2.76 % (4180290)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=2212699893:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi)
% 11.31/2.76 % (4180293)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=9503678:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi)
% 11.31/2.76 % (4180291)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=4140321472:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi)
% 11.31/2.76 % (4180289)Instruction limit reached!
% 11.31/2.76 % (4180289)------------------------------
% 11.31/2.76 % (4180289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180289)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180289)Termination reason: Instruction limit
% 11.31/2.76 % (4180289)Termination phase: Saturation
% 11.31/2.76 % (4180289)Time elapsed: 0.070 s
% 11.31/2.76 % (4180289)Peak memory usage: 133 MB
% 11.31/2.76 % (4180289)Instructions burned: 41 (million)
% 11.31/2.76 % (4180283)Instruction limit reached!
% 11.31/2.76 % (4180283)------------------------------
% 11.31/2.76 % (4180283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180283)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180283)Termination reason: Instruction limit
% 11.31/2.76 % (4180283)Termination phase: Saturation
% 11.31/2.76 % (4180283)Time elapsed: 0.195 s
% 11.31/2.76 % (4180283)Peak memory usage: 91 MB
% 11.31/2.76 % (4180283)Instructions burned: 294 (million)
% 11.31/2.76 % (4180296)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=683569718:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2988 on theBenchmark for (2988ds/259Mi)
% 11.31/2.76 % (4180293)Instruction limit reached!
% 11.31/2.76 % (4180293)------------------------------
% 11.31/2.76 % (4180293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180293)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180293)Termination reason: Instruction limit
% 11.31/2.76 % (4180293)Termination phase: Saturation
% 11.31/2.76 % (4180293)Time elapsed: 0.106 s
% 11.31/2.76 % (4180293)Peak memory usage: 116 MB
% 11.31/2.76 % (4180293)Instructions burned: 132 (million)
% 11.31/2.76 % (4180299)dis+10_1_si=on:random_seed=2243360618:s2a=on:i=1000:rtra=on:gtg=exists_all_2987 on theBenchmark for (2987ds/1000Mi)
% 11.31/2.76 % (4180290)Instruction limit reached!
% 11.31/2.76 % (4180290)------------------------------
% 11.31/2.76 % (4180290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180290)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180290)Termination reason: Instruction limit
% 11.31/2.76 % (4180290)Termination phase: Saturation
% 11.31/2.76 % (4180290)Time elapsed: 0.169 s
% 11.31/2.76 % (4180290)Peak memory usage: 94 MB
% 11.31/2.76 % (4180290)Instructions burned: 309 (million)
% 11.31/2.76 % (4180296)Instruction limit reached!
% 11.31/2.76 % (4180296)------------------------------
% 11.31/2.76 % (4180296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180296)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180296)Termination reason: Instruction limit
% 11.31/2.76 % (4180296)Termination phase: Saturation
% 11.31/2.76 % (4180296)Time elapsed: 0.101 s
% 11.31/2.76 % (4180296)Peak memory usage: 118 MB
% 11.31/2.76 % (4180296)Instructions burned: 260 (million)
% 11.31/2.76 % (4180302)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=1051112595:i=383:fsr=off:rtra=on:ev=force_2987 on theBenchmark for (2987ds/383Mi)
% 11.31/2.76 % (4180304)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=4164417544:i=141:doe=on:rtra=on_2987 on theBenchmark for (2987ds/141Mi)
% 11.31/2.76 % (4180305)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=780126125:i=65:nm=16:rtra=on_2986 on theBenchmark for (2986ds/65Mi)
% 11.31/2.76 % (4180305)Refutation not found, incomplete strategy
% 11.31/2.76 % (4180305)------------------------------
% 11.31/2.76 % (4180305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180305)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180305)Termination reason: Refutation not found, incomplete strategy
% 11.31/2.76 % (4180305)Time elapsed: 0.030 s
% 11.31/2.76 % (4180305)Peak memory usage: 116 MB
% 11.31/2.76 % (4180305)Instructions burned: 40 (million)
% 11.31/2.76 % (4180304)Instruction limit reached!
% 11.31/2.76 % (4180304)------------------------------
% 11.31/2.76 % (4180304)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180304)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180304)Termination reason: Instruction limit
% 11.31/2.76 % (4180304)Termination phase: Saturation
% 11.31/2.76 % (4180304)Time elapsed: 0.093 s
% 11.31/2.76 % (4180304)Peak memory usage: 90 MB
% 11.31/2.76 % (4180304)Instructions burned: 143 (million)
% 11.31/2.76 % (4180307)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=4220664761:i=121:nm=16:rtra=on_2986 on theBenchmark for (2986ds/121Mi)
% 11.31/2.76 % (4180308)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=1144720961:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi)
% 11.31/2.76 % (4180291)Instruction limit reached!
% 11.31/2.76 % (4180291)------------------------------
% 11.31/2.76 % (4180291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180291)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180291)Termination reason: Instruction limit
% 11.31/2.76 % (4180291)Termination phase: Saturation
% 11.31/2.76 % (4180291)Time elapsed: 0.358 s
% 11.31/2.76 % (4180291)Peak memory usage: 137 MB
% 11.31/2.76 % (4180291)Instructions burned: 598 (million)
% 11.31/2.76 % (4180307)Instruction limit reached!
% 11.31/2.76 % (4180307)------------------------------
% 11.31/2.76 % (4180307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180307)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180307)Termination reason: Instruction limit
% 11.31/2.76 % (4180307)Termination phase: Saturation
% 11.31/2.76 % (4180307)Time elapsed: 0.076 s
% 11.31/2.76 % (4180307)Peak memory usage: 90 MB
% 11.31/2.76 % (4180307)Instructions burned: 122 (million)
% 11.31/2.76 % (4180302)First to succeed.
% 11.31/2.76 % (4180302)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4180215"
% 11.31/2.76 % (4180308)Instruction limit reached!
% 11.31/2.76 % (4180308)------------------------------
% 11.31/2.76 % (4180308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180308)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180308)Termination reason: Instruction limit
% 11.31/2.76 % (4180308)Termination phase: Saturation
% 11.31/2.76 % (4180308)Time elapsed: 0.094 s
% 11.31/2.76 % (4180308)Peak memory usage: 117 MB
% 11.31/2.76 % (4180308)Instructions burned: 130 (million)
% 11.31/2.76 % (4180305)------------------------------
% 11.31/2.76 % (4180305)------------------------------
% 11.31/2.76 % (4180313)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=2196658077:i=39:ins=3:rtra=on_2984 on theBenchmark for (2984ds/39Mi)
% 11.31/2.76 % (4180313)Instruction limit reached!
% 11.31/2.76 % (4180313)------------------------------
% 11.31/2.76 % (4180313)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180313)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180313)Termination reason: Instruction limit
% 11.31/2.76 % (4180313)Termination phase: Saturation
% 11.31/2.76 % (4180313)Time elapsed: 0.050 s
% 11.31/2.76 % (4180313)Peak memory usage: 115 MB
% 11.31/2.76 % (4180313)Instructions burned: 39 (million)
% 11.31/2.76 % (4180315)dis+1010_1_to=kbo:si=on:random_seed=3321101807:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2983 on theBenchmark for (2983ds/175Mi)
% 11.31/2.76 % (4180316)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=473174561:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2983 on theBenchmark for (2983ds/329Mi)
% 11.31/2.76 % (4180318)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3922751342:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi)
% 11.31/2.76 % (4180317)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3735546780:s2a=on:i=483:doe=on:nm=32:rtra=on_2983 on theBenchmark for (2983ds/483Mi)
% 11.31/2.76 % (4180318)Instruction limit reached!
% 11.31/2.76 % (4180318)------------------------------
% 11.31/2.76 % (4180318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180318)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180318)Termination reason: Instruction limit
% 11.31/2.76 % (4180318)Termination phase: Saturation
% 11.31/2.76 % (4180318)Time elapsed: 0.093 s
% 11.31/2.76 % (4180318)Peak memory usage: 134 MB
% 11.31/2.76 % (4180318)Instructions burned: 215 (million)
% 11.31/2.76 % (4180315)Instruction limit reached!
% 11.31/2.76 % (4180315)------------------------------
% 11.31/2.76 % (4180315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.31/2.76 % (4180315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.31/2.76 % (4180315)CaDiCaL version: 2.1.3
% 11.31/2.76 % (4180315)Termination reason: Instruction limit
% 11.31/2.76 % (4180315)Termination phase: Saturation
% 11.31/2.76 % (4180315)Time elapsed: 0.127 s
% 11.31/2.76 % (4180315)Peak memory usage: 90 MB
% 11.31/2.76 % (4180315)Instructions burned: 176 (million)
% 11.31/2.76 % (4180302)Refutation found. Thanks to Tanya!
% 11.31/2.76 % SZS status Theorem for theBenchmark
% 11.31/2.76 % SZS output start Proof for theBenchmark
% See solution above
% 14.03/2.94 % (4180302)------------------------------
% 14.03/2.94 % (4180302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.03/2.94 % (4180302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.03/2.94 % (4180302)CaDiCaL version: 2.1.3
% 14.03/2.94 % (4180302)Termination reason: Refutation
% 14.03/2.94 % (4180302)Time elapsed: 0.228 s
% 14.03/2.94 % (4180302)Peak memory usage: 96 MB
% 14.03/2.94 % (4180302)Instructions burned: 354 (million)
% 14.03/2.94 % (4180302)------------------------------
% 14.03/2.94 % (4180302)------------------------------
% 14.03/2.94 % (4180215)Success in time 1.915 s
% 14.03/2.94 % Vampire exiting
%------------------------------------------------------------------------------