%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU215+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:52:25 PM UTC 2026
% Result : Theorem 38.76s 6.01s
% Output : Refutation 38.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 11
% Syntax : Number of formulae : 96 ( 27 unt; 5 def)
% Number of atoms : 346 ( 69 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 420 ( 170 ~; 181 |; 44 &)
% ( 9 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 93 ( 87 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( ( in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) ) )
& ( ~ in(X1,relation_dom(X0))
=> ( X2 = apply(X0,X1)
<=> X2 = empty_set ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f60,axiom,
! [X0,X1] :
( ( relation(X0)
& relation(X1) )
=> relation(relation_composition(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_relat_1) ).
fof(f73,axiom,
! [X0,X1] :
( ( relation(X0)
& function(X0)
& relation(X1)
& function(X1) )
=> ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_funct_1) ).
fof(f149,axiom,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_funct_1) ).
fof(f151,axiom,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(relation_composition(X2,X1)))
=> apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_funct_1) ).
fof(f152,conjecture,
! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(X1))
=> apply(relation_composition(X1,X2),X0) = apply(X2,apply(X1,X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t23_funct_1) ).
fof(f153,negated_conjecture,
~ ! [X0,X1] :
( ( relation(X1)
& function(X1) )
=> ! [X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X0,relation_dom(X1))
=> apply(relation_composition(X1,X2),X0) = apply(X2,apply(X1,X0)) ) ) ),
inference(negated_conjecture,[status(cth)],[f152]) ).
fof(f249,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f250,plain,
! [X0] :
( ! [X1,X2] :
( ( ( X2 = apply(X0,X1)
<=> in(ordered_pair(X1,X2),X0) )
| ~ in(X1,relation_dom(X0)) )
& ( ( X2 = apply(X0,X1)
<=> X2 = empty_set )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f249]) ).
fof(f262,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(ennf_transformation,[],[f60]) ).
fof(f263,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(flattening,[],[f262]) ).
fof(f273,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f73]) ).
fof(f274,plain,
! [X0,X1] :
( ( relation(relation_composition(X0,X1))
& function(relation_composition(X0,X1)) )
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f273]) ).
fof(f339,plain,
! [X0,X1] :
( ! [X2] :
( ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) )
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f149]) ).
fof(f340,plain,
! [X0,X1] :
( ! [X2] :
( ( in(X0,relation_dom(relation_composition(X2,X1)))
<=> ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) ) )
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f339]) ).
fof(f342,plain,
! [X0,X1] :
( ! [X2] :
( apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0))
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(ennf_transformation,[],[f151]) ).
fof(f343,plain,
! [X0,X1] :
( ! [X2] :
( apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0))
| ~ in(X0,relation_dom(relation_composition(X2,X1)))
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f342]) ).
fof(f344,plain,
? [X0,X1] :
( ? [X2] :
( apply(relation_composition(X1,X2),X0) != apply(X2,apply(X1,X0))
& in(X0,relation_dom(X1))
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(ennf_transformation,[],[f153]) ).
fof(f345,plain,
? [X0,X1] :
( ? [X2] :
( apply(relation_composition(X1,X2),X0) != apply(X2,apply(X1,X0))
& in(X0,relation_dom(X1))
& relation(X2)
& function(X2) )
& relation(X1)
& function(X1) ),
inference(flattening,[],[f344]) ).
fof(f470,plain,
! [X0] :
( ! [X1,X2] :
( ( ( ( X2 = apply(X0,X1)
| ~ in(ordered_pair(X1,X2),X0) )
& ( in(ordered_pair(X1,X2),X0)
| apply(X0,X1) != X2 ) )
| ~ in(X1,relation_dom(X0)) )
& ( ( ( X2 = apply(X0,X1)
| empty_set != X2 )
& ( X2 = empty_set
| apply(X0,X1) != X2 ) )
| in(X1,relation_dom(X0)) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f250]) ).
fof(f522,plain,
! [X0,X1] :
( ! [X2] :
( ( ( in(X0,relation_dom(relation_composition(X2,X1)))
| ~ in(X0,relation_dom(X2))
| ~ in(apply(X2,X0),relation_dom(X1)) )
& ( ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) )
| ~ in(X0,relation_dom(relation_composition(X2,X1))) ) )
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(nnf_transformation,[],[f340]) ).
fof(f523,plain,
! [X0,X1] :
( ! [X2] :
( ( ( in(X0,relation_dom(relation_composition(X2,X1)))
| ~ in(X0,relation_dom(X2))
| ~ in(apply(X2,X0),relation_dom(X1)) )
& ( ( in(X0,relation_dom(X2))
& in(apply(X2,X0),relation_dom(X1)) )
| ~ in(X0,relation_dom(relation_composition(X2,X1))) ) )
| ~ relation(X2)
| ~ function(X2) )
| ~ relation(X1)
| ~ function(X1) ),
inference(flattening,[],[f522]) ).
fof(f524,plain,
( apply(relation_composition(sK65,sK66),sK64) != apply(sK66,apply(sK65,sK64))
& in(sK64,relation_dom(sK65))
& relation(sK66)
& function(sK66)
& relation(sK65)
& function(sK65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66]),skolemize(X0,sK64),skolemize(X1,sK65),skolemize(X2,sK66)],[f345]) ).
fof(f649,plain,
! [X2,X0,X1] :
( empty_set = X2
| apply(X0,X1) != X2
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f470]) ).
fof(f698,plain,
! [X0,X1] :
( relation(relation_composition(X0,X1))
| ~ relation(X0)
| ~ relation(X1) ),
inference(cnf_transformation,[],[f263]) ).
fof(f711,plain,
! [X0,X1] :
( function(relation_composition(X0,X1))
| ~ relation(X0)
| ~ function(X0)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f274]) ).
fof(f818,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_dom(relation_composition(X2,X1)))
| in(apply(X2,X0),relation_dom(X1))
| ~ relation(X2)
| ~ function(X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f523]) ).
fof(f820,plain,
! [X2,X0,X1] :
( ~ in(apply(X2,X0),relation_dom(X1))
| ~ in(X0,relation_dom(X2))
| in(X0,relation_dom(relation_composition(X2,X1)))
| ~ relation(X2)
| ~ function(X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f523]) ).
fof(f822,plain,
! [X2,X0,X1] :
( ~ in(X0,relation_dom(relation_composition(X2,X1)))
| apply(relation_composition(X2,X1),X0) = apply(X1,apply(X2,X0))
| ~ relation(X2)
| ~ function(X2)
| ~ relation(X1)
| ~ function(X1) ),
inference(cnf_transformation,[],[f343]) ).
fof(f823,plain,
function(sK65),
inference(cnf_transformation,[],[f524]) ).
fof(f824,plain,
relation(sK65),
inference(cnf_transformation,[],[f524]) ).
fof(f825,plain,
function(sK66),
inference(cnf_transformation,[],[f524]) ).
fof(f826,plain,
relation(sK66),
inference(cnf_transformation,[],[f524]) ).
fof(f827,plain,
in(sK64,relation_dom(sK65)),
inference(cnf_transformation,[],[f524]) ).
fof(f828,plain,
apply(relation_composition(sK65,sK66),sK64) != apply(sK66,apply(sK65,sK64)),
inference(cnf_transformation,[],[f524]) ).
fof(f1110,plain,
! [X0,X1] :
( in(X1,relation_dom(X0))
| empty_set = apply(X0,X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f649]) ).
fof(f1133,definition,
sF74 = relation_composition(sK65,sK66),
introduced(definition,[new_symbols(definition,[sF74])],[function_definition]) ).
fof(f1134,plain,
relation_composition(sK65,sK66) = sF74,
inference(reorient_equations,[],[f1133]) ).
fof(f1135,definition,
sF75 = apply(sF74,sK64),
introduced(definition,[new_symbols(definition,[sF75])],[function_definition]) ).
fof(f1136,plain,
apply(sF74,sK64) = sF75,
inference(reorient_equations,[],[f1135]) ).
fof(f1137,definition,
sF76 = apply(sK65,sK64),
introduced(definition,[new_symbols(definition,[sF76])],[function_definition]) ).
fof(f1138,plain,
apply(sK65,sK64) = sF76,
inference(reorient_equations,[],[f1137]) ).
fof(f1139,definition,
sF77 = apply(sK66,sF76),
introduced(definition,[new_symbols(definition,[sF77])],[function_definition]) ).
fof(f1140,plain,
apply(sK66,sF76) = sF77,
inference(reorient_equations,[],[f1139]) ).
fof(f1141,plain,
sF75 != sF77,
inference(definition_folding,[],[f828,f1140,f1138,f1136,f1134]) ).
fof(f1142,definition,
sF78 = relation_dom(sK65),
introduced(definition,[new_symbols(definition,[sF78])],[function_definition]) ).
fof(f1143,plain,
relation_dom(sK65) = sF78,
inference(reorient_equations,[],[f1142]) ).
fof(f1144,plain,
in(sK64,sF78),
inference(definition_folding,[],[f827,f1143]) ).
fof(f1620,plain,
( relation(sF74)
| ~ relation(sK65)
| ~ relation(sK66) ),
inference(superposition,[],[f698,f1134]) ).
fof(f1621,plain,
( relation(sF74)
| ~ relation(sK66) ),
inference(forward_subsumption_resolution,[],[f1620,f824]) ).
fof(f1622,plain,
relation(sF74),
inference(forward_subsumption_resolution,[],[f1621,f826]) ).
fof(f3425,plain,
( function(sF74)
| ~ relation(sK65)
| ~ function(sK65)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(superposition,[],[f711,f1134]) ).
fof(f3430,plain,
( function(sF74)
| ~ function(sK65)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f3425,f824]) ).
fof(f3433,plain,
( function(sF74)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f3430,f823]) ).
fof(f3436,plain,
( function(sF74)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f3433,f826]) ).
fof(f3437,plain,
function(sF74),
inference(forward_subsumption_resolution,[],[f3436,f825]) ).
fof(f7040,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| in(apply(sK65,X0),relation_dom(sK66))
| ~ relation(sK65)
| ~ function(sK65)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(superposition,[],[f818,f1134]) ).
fof(f7047,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| in(apply(sK65,X0),relation_dom(sK66))
| ~ function(sK65)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f7040,f824]) ).
fof(f7059,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| in(apply(sK65,X0),relation_dom(sK66))
| ~ relation(sK66)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f7047,f823]) ).
fof(f7065,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| in(apply(sK65,X0),relation_dom(sK66))
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f7059,f826]) ).
fof(f7067,plain,
! [X0] :
( in(apply(sK65,X0),relation_dom(sK66))
| ~ in(X0,relation_dom(sF74)) ),
inference(forward_subsumption_resolution,[],[f7065,f825]) ).
fof(f7834,plain,
! [X0] :
( ~ in(sF76,relation_dom(X0))
| ~ in(sK64,relation_dom(sK65))
| in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ relation(sK65)
| ~ function(sK65)
| ~ relation(X0)
| ~ function(X0) ),
inference(superposition,[],[f820,f1138]) ).
fof(f7855,plain,
! [X0] :
( ~ in(sF76,relation_dom(X0))
| ~ in(sK64,relation_dom(sK65))
| in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ function(sK65)
| ~ relation(X0)
| ~ function(X0) ),
inference(forward_subsumption_resolution,[],[f7834,f824]) ).
fof(f7868,plain,
! [X0] :
( ~ in(sF76,relation_dom(X0))
| ~ in(sK64,relation_dom(sK65))
| in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ relation(X0)
| ~ function(X0) ),
inference(forward_subsumption_resolution,[],[f7855,f823]) ).
fof(f7878,plain,
! [X0] :
( ~ in(sK64,sF78)
| ~ in(sF76,relation_dom(X0))
| in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ relation(X0)
| ~ function(X0) ),
inference(forward_demodulation,[],[f7868,f1143]) ).
fof(f7884,plain,
! [X0] :
( in(sK64,relation_dom(relation_composition(sK65,X0)))
| ~ in(sF76,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(forward_subsumption_resolution,[],[f7878,f1144]) ).
fof(f8143,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| apply(sF74,X0) = apply(sK66,apply(sK65,X0))
| ~ relation(sK65)
| ~ function(sK65)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(superposition,[],[f822,f1134]) ).
fof(f8150,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| apply(sF74,X0) = apply(sK66,apply(sK65,X0))
| ~ function(sK65)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f8143,f824]) ).
fof(f8164,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| apply(sF74,X0) = apply(sK66,apply(sK65,X0))
| ~ relation(sK66)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f8150,f823]) ).
fof(f8170,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| apply(sF74,X0) = apply(sK66,apply(sK65,X0))
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f8164,f826]) ).
fof(f8171,plain,
! [X0] :
( ~ in(X0,relation_dom(sF74))
| apply(sF74,X0) = apply(sK66,apply(sK65,X0)) ),
inference(forward_subsumption_resolution,[],[f8170,f825]) ).
fof(f13330,plain,
( ~ in(sK64,relation_dom(sF74))
| in(sF76,relation_dom(sK66)) ),
inference(superposition,[],[f7067,f1138]) ).
fof(f14076,plain,
( in(sK64,relation_dom(sF74))
| ~ in(sF76,relation_dom(sK66))
| ~ relation(sK66)
| ~ function(sK66) ),
inference(superposition,[],[f7884,f1134]) ).
fof(f14080,plain,
( in(sK64,relation_dom(sF74))
| ~ in(sF76,relation_dom(sK66))
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f14076,f826]) ).
fof(f14085,plain,
( ~ in(sF76,relation_dom(sK66))
| in(sK64,relation_dom(sF74)) ),
inference(forward_subsumption_resolution,[],[f14080,f825]) ).
fof(f15661,plain,
( in(sF76,relation_dom(sK66))
| empty_set = apply(sF74,sK64)
| ~ relation(sF74)
| ~ function(sF74) ),
inference(resolution,[],[f13330,f1110]) ).
fof(f15663,plain,
( in(sF76,relation_dom(sK66))
| empty_set = apply(sF74,sK64)
| ~ function(sF74) ),
inference(forward_subsumption_resolution,[],[f15661,f1622]) ).
fof(f15664,plain,
( in(sF76,relation_dom(sK66))
| empty_set = apply(sF74,sK64) ),
inference(forward_subsumption_resolution,[],[f15663,f3437]) ).
fof(f15665,plain,
( in(sF76,relation_dom(sK66))
| empty_set = sF75 ),
inference(forward_demodulation,[],[f15664,f1136]) ).
fof(f47167,plain,
( in(sK64,relation_dom(sF74))
| empty_set = sF75 ),
inference(resolution,[],[f14085,f15665]) ).
fof(f47168,plain,
( in(sK64,relation_dom(sF74))
| empty_set = apply(sK66,sF76)
| ~ relation(sK66)
| ~ function(sK66) ),
inference(resolution,[],[f14085,f1110]) ).
fof(f47171,plain,
( in(sK64,relation_dom(sF74))
| empty_set = apply(sK66,sF76)
| ~ function(sK66) ),
inference(forward_subsumption_resolution,[],[f47168,f826]) ).
fof(f47172,plain,
( in(sK64,relation_dom(sF74))
| empty_set = apply(sK66,sF76) ),
inference(forward_subsumption_resolution,[],[f47171,f825]) ).
fof(f47173,plain,
( in(sK64,relation_dom(sF74))
| empty_set = sF77 ),
inference(forward_demodulation,[],[f47172,f1140]) ).
fof(f47241,plain,
( empty_set = sF77
| apply(sK66,apply(sK65,sK64)) = apply(sF74,sK64) ),
inference(resolution,[],[f47173,f8171]) ).
fof(f47268,plain,
( apply(sK66,apply(sK65,sK64)) = sF75
| empty_set = sF77 ),
inference(forward_demodulation,[],[f47241,f1136]) ).
fof(f47269,plain,
( sF75 = apply(sK66,sF76)
| empty_set = sF77 ),
inference(forward_demodulation,[],[f47268,f1138]) ).
fof(f47270,plain,
( sF75 = sF77
| empty_set = sF77 ),
inference(forward_demodulation,[],[f47269,f1140]) ).
fof(f47271,plain,
empty_set = sF77,
inference(forward_subsumption_resolution,[],[f47270,f1141]) ).
fof(f47468,plain,
empty_set != sF75,
inference(superposition,[],[f1141,f47271]) ).
fof(f48683,plain,
( empty_set = sF75
| apply(sK66,apply(sK65,sK64)) = apply(sF74,sK64) ),
inference(resolution,[],[f47167,f8171]) ).
fof(f48724,plain,
apply(sK66,apply(sK65,sK64)) = apply(sF74,sK64),
inference(forward_subsumption_resolution,[],[f48683,f47468]) ).
fof(f48728,plain,
apply(sK66,apply(sK65,sK64)) = sF75,
inference(forward_demodulation,[],[f48724,f1136]) ).
fof(f48729,plain,
sF75 = apply(sK66,sF76),
inference(forward_demodulation,[],[f48728,f1138]) ).
fof(f51768,plain,
sF75 = sF77,
inference(superposition,[],[f1140,f48729]) ).
fof(f51773,plain,
$false,
inference(forward_subsumption_resolution,[],[f51768,f1141]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU215+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n006.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 04:05:26 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.30/2.60 % (3567436)Will run a generic schedule for satisfiability detection.
% 15.30/2.60 % (3567445)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2115478781:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.30/2.60 % (3567442)% WARNING: option uhcvi not known.
% 15.30/2.60 % (3567443)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2524657930:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.30/2.60 % (3567444)dis+10_1_sil=32000:sp=arity:random_seed=3545472741:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.30/2.60 % (3567441)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3496826633_2999 on theBenchmark for (2999ds/0Mi)
% 15.30/2.60 % (3567442)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=966662295:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.30/2.60 % (3567447)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3855475229:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.30/2.60 % (3567446)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1205630677:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.30/2.60 % (3567445)Instruction limit reached!
% 15.30/2.60 % (3567445)------------------------------
% 15.30/2.60 % (3567445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.60 % (3567445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.60 % (3567445)CaDiCaL version: 2.1.3
% 15.30/2.60 % (3567445)Termination reason: Instruction limit
% 15.30/2.60 % (3567445)Termination phase: Saturation
% 15.30/2.60 % (3567445)Time elapsed: 0.039 s
% 15.30/2.60 % (3567445)Peak memory usage: 13 MB
% 15.30/2.60 % (3567445)Instructions burned: 116 (million)
% 15.30/2.60 % (3567455)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3050870999:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.30/2.60 % TRYING [1]
% 15.30/2.60 % TRYING [2]
% 15.30/2.60 % TRYING [1]
% 15.30/2.60 % TRYING [2]
% 15.30/2.60 % (3567444)Instruction limit reached!
% 15.30/2.60 % (3567444)------------------------------
% 15.30/2.60 % (3567444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.60 % (3567444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.60 % (3567444)CaDiCaL version: 2.1.3
% 15.30/2.60 % (3567444)Termination reason: Instruction limit
% 15.30/2.60 % (3567444)Termination phase: Saturation
% 15.30/2.60 % (3567444)Time elapsed: 0.068 s
% 15.30/2.60 % (3567444)Peak memory usage: 13 MB
% 15.30/2.60 % (3567444)Instructions burned: 104 (million)
% 15.30/2.60 % (3567446)Instruction limit reached!
% 15.30/2.60 % (3567446)------------------------------
% 15.30/2.60 % (3567446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.60 % (3567446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.60 % (3567446)CaDiCaL version: 2.1.3
% 15.30/2.60 % (3567446)Termination reason: Instruction limit
% 15.30/2.60 % (3567446)Termination phase: Saturation
% 15.30/2.60 % (3567446)Time elapsed: 0.073 s
% 15.30/2.60 % (3567446)Peak memory usage: 14 MB
% 15.30/2.60 % (3567446)Instructions burned: 132 (million)
% 15.30/2.60 % TRYING [3]
% 15.30/2.60 % TRYING [3]
% 15.30/2.60 % (3567457)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3448528747:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.30/2.60 % (3567458)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=577166415:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.30/2.60 % (3567447)Instruction limit reached!
% 15.30/2.60 % (3567447)------------------------------
% 15.30/2.60 % (3567447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.60 % (3567447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.30/2.60 % (3567447)CaDiCaL version: 2.1.3
% 15.30/2.60 % (3567447)Termination reason: Instruction limit
% 15.30/2.60 % (3567447)Termination phase: Saturation
% 15.30/2.60 % (3567447)Time elapsed: 0.104 s
% 15.30/2.60 % (3567447)Peak memory usage: 14 MB
% 15.30/2.60 % (3567447)Instructions burned: 160 (million)
% 15.30/2.60 % (3567461)ott-21_1_sil=16000:fs=off:random_seed=3021283346:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.30/2.60 % TRYING [4]
% 15.30/2.60 % (3567457)Instruction limit reached!
% 15.30/2.60 % (3567457)------------------------------
% 15.30/2.60 % (3567457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.30/2.60 % (3567457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567457)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567457)Termination reason: Instruction limit
% 38.76/6.01 % (3567457)Termination phase: Saturation
% 38.76/6.01 % (3567457)Time elapsed: 0.078 s
% 38.76/6.01 % (3567457)Peak memory usage: 14 MB
% 38.76/6.01 % (3567457)Instructions burned: 132 (million)
% 38.76/6.01 % (3567455)Instruction limit reached!
% 38.76/6.01 % (3567455)------------------------------
% 38.76/6.01 % (3567455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567455)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567455)Termination reason: Instruction limit
% 38.76/6.01 % (3567455)Termination phase: Finite model building constraint generation
% 38.76/6.01 % (3567455)Time elapsed: 0.141 s
% 38.76/6.01 % (3567455)Peak memory usage: 32 MB
% 38.76/6.01 % (3567455)Instructions burned: 718 (million)
% 38.76/6.01 % (3567463)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=567454599:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 38.76/6.01 % (3567465)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=25324414:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 38.76/6.01 % TRYING [1]
% 38.76/6.01 % TRYING [4]
% 38.76/6.01 % TRYING [2]
% 38.76/6.01 % (3567461)Instruction limit reached!
% 38.76/6.01 % (3567461)------------------------------
% 38.76/6.01 % (3567461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567461)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567461)Termination reason: Instruction limit
% 38.76/6.01 % (3567461)Termination phase: Saturation
% 38.76/6.01 % (3567461)Time elapsed: 0.102 s
% 38.76/6.01 % (3567461)Peak memory usage: 14 MB
% 38.76/6.01 % (3567461)Instructions burned: 180 (million)
% 38.76/6.01 % (3567467)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1614210207:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 38.76/6.01 % TRYING [3]
% 38.76/6.01 % (3567465)Instruction limit reached!
% 38.76/6.01 % (3567465)------------------------------
% 38.76/6.01 % (3567465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567465)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567465)Termination reason: Instruction limit
% 38.76/6.01 % (3567465)Termination phase: Finite model building SAT solving
% 38.76/6.01 % (3567465)Time elapsed: 0.210 s
% 38.76/6.01 % (3567465)Peak memory usage: 33 MB
% 38.76/6.01 % (3567465)Instructions burned: 866 (million)
% 38.76/6.01 % (3567469)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3586639776:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 38.76/6.01 % (3567458)Instruction limit reached!
% 38.76/6.01 % (3567458)------------------------------
% 38.76/6.01 % (3567458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567458)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567458)Termination reason: Instruction limit
% 38.76/6.01 % (3567458)Termination phase: Saturation
% 38.76/6.01 % (3567458)Time elapsed: 0.353 s
% 38.76/6.01 % (3567458)Peak memory usage: 17 MB
% 38.76/6.01 % (3567458)Instructions burned: 685 (million)
% 38.76/6.01 % (3567471)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3981323457:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 38.76/6.01 % (3567463)Instruction limit reached!
% 38.76/6.01 % (3567463)------------------------------
% 38.76/6.01 % (3567463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567463)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567463)Termination reason: Instruction limit
% 38.76/6.01 % (3567463)Termination phase: Saturation
% 38.76/6.01 % (3567463)Time elapsed: 0.339 s
% 38.76/6.01 % (3567463)Peak memory usage: 14 MB
% 38.76/6.01 % (3567463)Instructions burned: 477 (million)
% 38.76/6.01 % (3567473)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4017834011:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 38.76/6.01 % (3567469)Instruction limit reached!
% 38.76/6.01 % (3567469)------------------------------
% 38.76/6.01 % (3567469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567469)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567469)Termination reason: Instruction limit
% 38.76/6.01 % (3567469)Termination phase: Finite model building constraint generation
% 38.76/6.01 % (3567469)Time elapsed: 0.232 s
% 38.76/6.01 % (3567469)Peak memory usage: 101 MB
% 38.76/6.01 % (3567469)Instructions burned: 893 (million)
% 38.76/6.01 % (3567475)fmb+10_1_sil=64000:random_seed=981326968:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 38.76/6.01 % TRYING [1]
% 38.76/6.01 % TRYING [2]
% 38.76/6.01 % TRYING [3]
% 38.76/6.01 % TRYING [5]
% 38.76/6.01 % TRYING [4]
% 38.76/6.01 % (3567471)Instruction limit reached!
% 38.76/6.01 % (3567471)------------------------------
% 38.76/6.01 % (3567471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567471)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567471)Termination reason: Instruction limit
% 38.76/6.01 % (3567471)Termination phase: Saturation
% 38.76/6.01 % (3567471)Time elapsed: 0.466 s
% 38.76/6.01 % (3567471)Peak memory usage: 21 MB
% 38.76/6.01 % (3567471)Instructions burned: 696 (million)
% 38.76/6.01 % (3567477)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3947104726:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 38.76/6.01 % (3567467)Instruction limit reached!
% 38.76/6.01 % (3567467)------------------------------
% 38.76/6.01 % (3567467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567467)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567467)Termination reason: Instruction limit
% 38.76/6.01 % (3567467)Termination phase: Saturation
% 38.76/6.01 % (3567467)Time elapsed: 0.722 s
% 38.76/6.01 % (3567467)Peak memory usage: 26 MB
% 38.76/6.01 % (3567467)Instructions burned: 1179 (million)
% 38.76/6.01 % (3567479)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1834058484:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 38.76/6.01 % TRYING [20]
% 38.76/6.01 % TRYING [8]
% 38.76/6.01 % (3567473)Instruction limit reached!
% 38.76/6.01 % (3567473)------------------------------
% 38.76/6.01 % (3567473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567473)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567473)Termination reason: Instruction limit
% 38.76/6.01 % (3567473)Termination phase: Saturation
% 38.76/6.01 % (3567473)Time elapsed: 0.503 s
% 38.76/6.01 % (3567473)Peak memory usage: 21 MB
% 38.76/6.01 % (3567473)Instructions burned: 879 (million)
% 38.76/6.01 % (3567481)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3107622152:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 38.76/6.01 % (3567479)Instruction limit reached!
% 38.76/6.01 % (3567479)------------------------------
% 38.76/6.01 % (3567479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567479)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567479)Termination reason: Instruction limit
% 38.76/6.01 % (3567479)Termination phase: Finite model building constraint generation
% 38.76/6.01 % (3567479)Time elapsed: 0.318 s
% 38.76/6.01 % (3567479)Peak memory usage: 59 MB
% 38.76/6.01 % (3567479)Instructions burned: 923 (million)
% 38.76/6.01 % (3567483)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1456547890:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 38.76/6.01 % TRYING [5]
% 38.76/6.01 % (3567483)Instruction limit reached!
% 38.76/6.01 % (3567483)------------------------------
% 38.76/6.01 % (3567483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567483)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567483)Termination reason: Instruction limit
% 38.76/6.01 % (3567483)Termination phase: Saturation
% 38.76/6.01 % (3567483)Time elapsed: 0.731 s
% 38.76/6.01 % (3567483)Peak memory usage: 25 MB
% 38.76/6.01 % (3567483)Instructions burned: 1472 (million)
% 38.76/6.01 % (3567485)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3371769811:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 38.76/6.01 % (3567485)Cannot represent all propositional literals internally
% 38.76/6.01 % (3567485)Refutation not found, incomplete strategy
% 38.76/6.01 % (3567485)------------------------------
% 38.76/6.01 % (3567485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567485)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567485)Termination reason: Refutation not found, incomplete strategy
% 38.76/6.01 % (3567485)Time elapsed: 0.047 s
% 38.76/6.01 % (3567485)Peak memory usage: 13 MB
% 38.76/6.01 % (3567485)Instructions burned: 93 (million)
% 38.76/6.01 % (3567485)------------------------------
% 38.76/6.01 % (3567485)------------------------------
% 38.76/6.01 % (3567487)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3016517075:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 38.76/6.01 % TRYING [16]
% 38.76/6.01 % TRYING [6]
% 38.76/6.01 % (3567487)Instruction limit reached!
% 38.76/6.01 % (3567487)------------------------------
% 38.76/6.01 % (3567487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567487)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567487)Termination reason: Instruction limit
% 38.76/6.01 % (3567487)Termination phase: Finite model building constraint generation
% 38.76/6.01 % (3567487)Time elapsed: 0.817 s
% 38.76/6.01 % (3567487)Peak memory usage: 116 MB
% 38.76/6.01 % (3567487)Instructions burned: 2174 (million)
% 38.76/6.01 % (3567489)ott-2_1_sil=16000:newcnf=on:random_seed=2059149571:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 38.76/6.01 % (3567489)Instruction limit reached!
% 38.76/6.01 % (3567489)------------------------------
% 38.76/6.01 % (3567489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567489)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567489)Termination reason: Instruction limit
% 38.76/6.01 % (3567489)Termination phase: Saturation
% 38.76/6.01 % (3567489)Time elapsed: 0.552 s
% 38.76/6.01 % (3567489)Peak memory usage: 22 MB
% 38.76/6.01 % (3567489)Instructions burned: 869 (million)
% 38.76/6.01 % (3567491)ott+10_1_sil=32000:tgt=ground:random_seed=1357488059:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 38.76/6.01 % TRYING [6]
% 38.76/6.01 % (3567481)Instruction limit reached!
% 38.76/6.01 % (3567481)------------------------------
% 38.76/6.01 % (3567481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567481)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567481)Termination reason: Instruction limit
% 38.76/6.01 % (3567481)Termination phase: Saturation
% 38.76/6.01 % (3567481)Time elapsed: 2.982 s
% 38.76/6.01 % (3567481)Peak memory usage: 45 MB
% 38.76/6.01 % (3567481)Instructions burned: 5132 (million)
% 38.76/6.01 % (3567493)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2402405526:i=54282_2959 on theBenchmark for (2959ds/54282Mi)
% 38.76/6.01 % TRYING [1]
% 38.76/6.01 % TRYING [2]
% 38.76/6.01 % TRYING [3]
% 38.76/6.01 % TRYING [4]
% 38.76/6.01 % (3567477)Instruction limit reached!
% 38.76/6.01 % (3567477)------------------------------
% 38.76/6.01 % (3567477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567477)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567477)Termination reason: Instruction limit
% 38.76/6.01 % (3567477)Termination phase: Finite model building constraint generation
% 38.76/6.01 % (3567477)Time elapsed: 3.441 s
% 38.76/6.01 % (3567477)Peak memory usage: 631 MB
% 38.76/6.01 % (3567477)Instructions burned: 9518 (million)
% 38.76/6.01 % (3567495)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3327564724:i=3512:aac=none_2954 on theBenchmark for (2954ds/3512Mi)
% 38.76/6.01 % TRYING [5]
% 38.76/6.01 % (3567491) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3567436-3567491"...
% 38.76/6.01 % (3567491)...printing done.
% 38.76/6.01 % (3567491)Refutation found. Thanks to Tanya!
% 38.76/6.01 % SZS status Theorem for theBenchmark
% 38.76/6.01 % SZS output start Proof for theBenchmark
% See solution above
% 38.76/6.01 % (3567491)------------------------------
% 38.76/6.01 % (3567491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 38.76/6.01 % (3567491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.76/6.01 % (3567491)CaDiCaL version: 2.1.3
% 38.76/6.01 % (3567491)Termination reason: Refutation
% 38.76/6.01 % (3567491)Time elapsed: 1.882 s
% 38.76/6.01 % (3567491)Peak memory usage: 43 MB
% 38.76/6.01 % (3567491)Instructions burned: 3022 (million)
% 38.76/6.01 % (3567436)Success in time 5.577 s
% 38.76/6.01 % Vampire exiting
%------------------------------------------------------------------------------