%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU225+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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:29 PM UTC 2026
% Result : Theorem 7.11s 1.57s
% Output : Refutation 7.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 12
% Syntax : Number of formulae : 87 ( 22 unt; 6 def)
% Number of atoms : 246 ( 50 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 258 ( 99 ~; 107 |; 29 &)
% ( 11 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 4 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 77 ( 0 sgn 71 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,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/sandbox/benchmark/theBenchmark.p',d4_funct_1) ).
fof(f69,axiom,
! [X0,X1] :
( relation(X0)
=> relation(relation_dom_restriction(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k7_relat_1) ).
fof(f91,axiom,
! [X0,X1] :
( ( relation(X0)
& function(X0) )
=> ( relation(relation_dom_restriction(X0,X1))
& function(relation_dom_restriction(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc4_funct_1) ).
fof(f221,axiom,
! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X1,relation_dom(relation_dom_restriction(X2,X0)))
=> apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t70_funct_1) ).
fof(f223,conjecture,
! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X1,X0)
=> apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t72_funct_1) ).
fof(f224,negated_conjecture,
~ ! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X1,X0)
=> apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1) ) ),
inference(negated_conjecture,[status(cth)],[f223]) ).
fof(f229,axiom,
! [X0,X1,X2] :
( relation(X2)
=> ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
<=> ( in(X0,X1)
& in(X0,relation_dom(X2)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t86_relat_1) ).
fof(f270,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,[],[f28]) ).
fof(f271,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,[],[f270]) ).
fof(f295,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(ennf_transformation,[],[f69]) ).
fof(f313,plain,
! [X0,X1] :
( ( relation(relation_dom_restriction(X0,X1))
& function(relation_dom_restriction(X0,X1)) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f91]) ).
fof(f314,plain,
! [X0,X1] :
( ( relation(relation_dom_restriction(X0,X1))
& function(relation_dom_restriction(X0,X1)) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f313]) ).
fof(f442,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,relation_dom(relation_dom_restriction(X2,X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f221]) ).
fof(f443,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,relation_dom(relation_dom_restriction(X2,X0)))
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f442]) ).
fof(f444,plain,
? [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) != apply(X2,X1)
& in(X1,X0)
& relation(X2)
& function(X2) ),
inference(ennf_transformation,[],[f224]) ).
fof(f445,plain,
? [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) != apply(X2,X1)
& in(X1,X0)
& relation(X2)
& function(X2) ),
inference(flattening,[],[f444]) ).
fof(f448,plain,
! [X0,X1,X2] :
( ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
<=> ( in(X0,X1)
& in(X0,relation_dom(X2)) ) )
| ~ relation(X2) ),
inference(ennf_transformation,[],[f229]) ).
fof(f525,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,[],[f271]) ).
fof(f616,plain,
( apply(relation_dom_restriction(sK80,sK78),sK79) != apply(sK80,sK79)
& in(sK79,sK78)
& relation(sK80)
& function(sK80) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78,sK79,sK80]),skolemize(X0,sK78),skolemize(X1,sK79),skolemize(X2,sK80)],[f445]) ).
fof(f620,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
| ~ in(X0,X1)
| ~ in(X0,relation_dom(X2)) )
& ( ( in(X0,X1)
& in(X0,relation_dom(X2)) )
| ~ in(X0,relation_dom(relation_dom_restriction(X2,X1))) ) )
| ~ relation(X2) ),
inference(nnf_transformation,[],[f448]) ).
fof(f621,plain,
! [X0,X1,X2] :
( ( ( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
| ~ in(X0,X1)
| ~ in(X0,relation_dom(X2)) )
& ( ( in(X0,X1)
& in(X0,relation_dom(X2)) )
| ~ in(X0,relation_dom(relation_dom_restriction(X2,X1))) ) )
| ~ relation(X2) ),
inference(flattening,[],[f620]) ).
fof(f729,plain,
! [X2,X0,X1] :
( empty_set = X2
| apply(X0,X1) != X2
| in(X1,relation_dom(X0))
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f525]) ).
fof(f791,plain,
! [X0,X1] :
( relation(relation_dom_restriction(X0,X1))
| ~ relation(X0) ),
inference(cnf_transformation,[],[f295]) ).
fof(f819,plain,
! [X0,X1] :
( ~ relation(X0)
| function(relation_dom_restriction(X0,X1))
| ~ function(X0) ),
inference(cnf_transformation,[],[f314]) ).
fof(f1028,plain,
! [X2,X0,X1] :
( ~ in(X1,relation_dom(relation_dom_restriction(X2,X0)))
| apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f443]) ).
fof(f1031,plain,
function(sK80),
inference(cnf_transformation,[],[f616]) ).
fof(f1032,plain,
relation(sK80),
inference(cnf_transformation,[],[f616]) ).
fof(f1033,plain,
in(sK79,sK78),
inference(cnf_transformation,[],[f616]) ).
fof(f1034,plain,
apply(relation_dom_restriction(sK80,sK78),sK79) != apply(sK80,sK79),
inference(cnf_transformation,[],[f616]) ).
fof(f1044,plain,
! [X2,X0,X1] :
( in(X0,relation_dom(relation_dom_restriction(X2,X1)))
| ~ in(X0,X1)
| ~ in(X0,relation_dom(X2))
| ~ relation(X2) ),
inference(cnf_transformation,[],[f621]) ).
fof(f1248,plain,
! [X0,X1] :
( in(X1,relation_dom(X0))
| empty_set = apply(X0,X1)
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f729]) ).
fof(f1286,definition,
sF83 = relation_dom_restriction(sK80,sK78),
introduced(definition,[new_symbols(definition,[sF83])],[function_definition]) ).
fof(f1287,plain,
relation_dom_restriction(sK80,sK78) = sF83,
inference(reorient_equations,[],[f1286]) ).
fof(f1288,definition,
sF84 = apply(sF83,sK79),
introduced(definition,[new_symbols(definition,[sF84])],[function_definition]) ).
fof(f1289,plain,
apply(sF83,sK79) = sF84,
inference(reorient_equations,[],[f1288]) ).
fof(f1290,definition,
sF85 = apply(sK80,sK79),
introduced(definition,[new_symbols(definition,[sF85])],[function_definition]) ).
fof(f1291,plain,
apply(sK80,sK79) = sF85,
inference(reorient_equations,[],[f1290]) ).
fof(f1292,plain,
sF84 != sF85,
inference(definition_folding,[],[f1034,f1291,f1289,f1287]) ).
fof(f1396,plain,
( relation(sF83)
| ~ relation(sK80) ),
inference(superposition,[],[f791,f1287]) ).
fof(f1397,plain,
relation(sF83),
inference(forward_subsumption_resolution,[],[f1396,f1032]) ).
fof(f1522,definition,
( spl86_1
<=> function(sF83) ),
introduced(definition,[new_symbols(definition,[spl86_1])],[avatar_definition]) ).
fof(f1523,plain,
( function(sF83)
| ~ spl86_1 ),
inference(avatar_component_clause,[],[f1522]) ).
fof(f1524,plain,
( ~ function(sF83)
| spl86_1 ),
inference(avatar_component_clause,[],[f1522]) ).
fof(f2249,plain,
! [X0] :
( function(relation_dom_restriction(sK80,X0))
| ~ function(sK80) ),
inference(resolution,[],[f819,f1032]) ).
fof(f2251,plain,
! [X0] : function(relation_dom_restriction(sK80,X0)),
inference(forward_subsumption_resolution,[],[f2249,f1031]) ).
fof(f2269,plain,
function(sF83),
inference(superposition,[],[f2251,f1287]) ).
fof(f2270,plain,
( $false
| spl86_1 ),
inference(forward_subsumption_resolution,[],[f2269,f1524]) ).
fof(f2271,plain,
spl86_1,
inference(avatar_contradiction_clause,[],[f2270]) ).
fof(f7296,plain,
! [X0] :
( in(X0,relation_dom(sF83))
| ~ in(X0,sK78)
| ~ in(X0,relation_dom(sK80))
| ~ relation(sK80) ),
inference(superposition,[],[f1044,f1287]) ).
fof(f7300,plain,
! [X0] :
( ~ in(X0,relation_dom(sK80))
| ~ in(X0,sK78)
| in(X0,relation_dom(sF83)) ),
inference(forward_subsumption_resolution,[],[f7296,f1032]) ).
fof(f9223,definition,
( spl86_93
<=> in(sK79,relation_dom(sK80)) ),
introduced(definition,[new_symbols(definition,[spl86_93])],[avatar_definition]) ).
fof(f9224,plain,
( in(sK79,relation_dom(sK80))
| ~ spl86_93 ),
inference(avatar_component_clause,[],[f9223]) ).
fof(f9225,plain,
( ~ in(sK79,relation_dom(sK80))
| spl86_93 ),
inference(avatar_component_clause,[],[f9223]) ).
fof(f9429,plain,
( empty_set = apply(sK80,sK79)
| ~ relation(sK80)
| ~ function(sK80)
| spl86_93 ),
inference(resolution,[],[f9225,f1248]) ).
fof(f9433,plain,
( empty_set = apply(sK80,sK79)
| ~ function(sK80)
| spl86_93 ),
inference(forward_subsumption_resolution,[],[f9429,f1032]) ).
fof(f9434,plain,
( empty_set = apply(sK80,sK79)
| spl86_93 ),
inference(forward_subsumption_resolution,[],[f9433,f1031]) ).
fof(f9774,plain,
! [X0] :
( ~ in(X0,relation_dom(sF83))
| apply(sF83,X0) = apply(sK80,X0)
| ~ relation(sK80)
| ~ function(sK80) ),
inference(superposition,[],[f1028,f1287]) ).
fof(f9776,plain,
! [X0] :
( ~ in(X0,relation_dom(sF83))
| apply(sF83,X0) = apply(sK80,X0)
| ~ function(sK80) ),
inference(forward_subsumption_resolution,[],[f9774,f1032]) ).
fof(f9784,plain,
! [X0] :
( ~ in(X0,relation_dom(sF83))
| apply(sF83,X0) = apply(sK80,X0) ),
inference(forward_subsumption_resolution,[],[f9776,f1031]) ).
fof(f10062,plain,
( empty_set = sF85
| spl86_93 ),
inference(superposition,[],[f1291,f9434]) ).
fof(f10335,plain,
( empty_set != sF84
| spl86_93 ),
inference(superposition,[],[f1292,f10062]) ).
fof(f10809,definition,
( spl86_125
<=> in(sK79,relation_dom(sF83)) ),
introduced(definition,[new_symbols(definition,[spl86_125])],[avatar_definition]) ).
fof(f10810,plain,
( in(sK79,relation_dom(sF83))
| ~ spl86_125 ),
inference(avatar_component_clause,[],[f10809]) ).
fof(f10811,plain,
( ~ in(sK79,relation_dom(sF83))
| spl86_125 ),
inference(avatar_component_clause,[],[f10809]) ).
fof(f19746,plain,
( ~ in(sK79,sK78)
| in(sK79,relation_dom(sF83))
| ~ spl86_93 ),
inference(resolution,[],[f7300,f9224]) ).
fof(f19747,plain,
( in(sK79,relation_dom(sF83))
| ~ spl86_93 ),
inference(forward_subsumption_resolution,[],[f19746,f1033]) ).
fof(f19787,plain,
( $false
| ~ spl86_93
| spl86_125 ),
inference(forward_subsumption_resolution,[],[f19747,f10811]) ).
fof(f19788,plain,
( ~ spl86_93
| spl86_125 ),
inference(avatar_contradiction_clause,[],[f19787]) ).
fof(f21321,plain,
( apply(sK80,sK79) = apply(sF83,sK79)
| ~ spl86_125 ),
inference(resolution,[],[f10810,f9784]) ).
fof(f21339,plain,
( apply(sK80,sK79) = sF84
| ~ spl86_125 ),
inference(forward_demodulation,[],[f21321,f1289]) ).
fof(f21342,plain,
( sF84 = sF85
| ~ spl86_125 ),
inference(superposition,[],[f21339,f1291]) ).
fof(f21356,plain,
( $false
| ~ spl86_125 ),
inference(forward_subsumption_resolution,[],[f21342,f1292]) ).
fof(f21357,plain,
~ spl86_125,
inference(avatar_contradiction_clause,[],[f21356]) ).
fof(f21388,plain,
( empty_set = apply(sF83,sK79)
| ~ relation(sF83)
| ~ function(sF83)
| spl86_125 ),
inference(resolution,[],[f10811,f1248]) ).
fof(f21392,plain,
( empty_set = apply(sF83,sK79)
| ~ function(sF83)
| spl86_125 ),
inference(forward_subsumption_resolution,[],[f21388,f1397]) ).
fof(f21393,plain,
( empty_set = apply(sF83,sK79)
| ~ spl86_1
| spl86_125 ),
inference(forward_subsumption_resolution,[],[f21392,f1523]) ).
fof(f21428,plain,
( empty_set = sF84
| ~ spl86_1
| spl86_125 ),
inference(superposition,[],[f21393,f1289]) ).
fof(f21438,plain,
( $false
| ~ spl86_1
| spl86_93
| spl86_125 ),
inference(forward_subsumption_resolution,[],[f21428,f10335]) ).
fof(f21439,plain,
( ~ spl86_1
| spl86_93
| spl86_125 ),
inference(avatar_contradiction_clause,[],[f21438]) ).
cnf(s18,plain,
spl86_1,
inference(sat_conversion,[],[f2271]) ).
cnf(s204,plain,
( ~ spl86_93
| spl86_125 ),
inference(sat_conversion,[],[f19788]) ).
cnf(s247,plain,
~ spl86_125,
inference(sat_conversion,[],[f21357]) ).
cnf(s250,plain,
( ~ spl86_1
| spl86_93
| spl86_125 ),
inference(sat_conversion,[],[f21439]) ).
cnf(s259,plain,
~ spl86_93,
inference(rat,[],[s204,s247]) ).
cnf(s260,plain,
~ spl86_1,
inference(rat,[],[s250,s247,s259]) ).
cnf(s279,plain,
$false,
inference(rat,[],[s18,s260]) ).
fof(f21440,plain,
$false,
inference(avatar_sat_refutation,[],[s279]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU225+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Mon Sep 28 04:10:00 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.11/1.57 % (2651834)Will run a generic schedule for satisfiability detection.
% 7.11/1.57 % (2651839)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2414678652_2999 on theBenchmark for (2999ds/0Mi)
% 7.11/1.57 % (2651840)% WARNING: option uhcvi not known.
% 7.11/1.57 % (2651841)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2148251905:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.11/1.57 % (2651840)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3248978635:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.11/1.57 % (2651842)dis+10_1_sil=32000:sp=arity:random_seed=3486587743:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.11/1.57 % (2651843)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1160115596:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.11/1.57 % (2651845)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=871164923:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.11/1.57 % (2651844)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=909834455:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.11/1.57 % TRYING [1]
% 7.11/1.57 % TRYING [2]
% 7.11/1.57 % TRYING [3]
% 7.11/1.57 % (2651844)Instruction limit reached!
% 7.11/1.57 % (2651844)------------------------------
% 7.11/1.57 % (2651844)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651844)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651844)Termination reason: Instruction limit
% 7.11/1.57 % (2651844)Termination phase: Saturation
% 7.11/1.57 % (2651844)Time elapsed: 0.067 s
% 7.11/1.57 % (2651844)Peak memory usage: 13 MB
% 7.11/1.57 % (2651844)Instructions burned: 131 (million)
% 7.11/1.57 % (2651842)Instruction limit reached!
% 7.11/1.57 % (2651842)------------------------------
% 7.11/1.57 % (2651842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651842)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651842)Termination reason: Instruction limit
% 7.11/1.57 % (2651842)Termination phase: Saturation
% 7.11/1.57 % (2651842)Time elapsed: 0.069 s
% 7.11/1.57 % (2651842)Peak memory usage: 13 MB
% 7.11/1.57 % (2651842)Instructions burned: 103 (million)
% 7.11/1.57 % (2651843)Instruction limit reached!
% 7.11/1.57 % (2651843)------------------------------
% 7.11/1.57 % (2651843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651843)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651843)Termination reason: Instruction limit
% 7.11/1.57 % (2651843)Termination phase: Saturation
% 7.11/1.57 % (2651843)Time elapsed: 0.070 s
% 7.11/1.57 % (2651843)Peak memory usage: 13 MB
% 7.11/1.57 % (2651843)Instructions burned: 117 (million)
% 7.11/1.57 % (2651853)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1991875846:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.11/1.57 % (2651855)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=1049698205:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.11/1.57 % (2651854)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1000534996:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.11/1.57 % (2651845)Instruction limit reached!
% 7.11/1.57 % (2651845)------------------------------
% 7.11/1.57 % (2651845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651845)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651845)Termination reason: Instruction limit
% 7.11/1.57 % (2651845)Termination phase: Saturation
% 7.11/1.57 % (2651845)Time elapsed: 0.102 s
% 7.11/1.57 % (2651845)Peak memory usage: 14 MB
% 7.11/1.57 % (2651845)Instructions burned: 159 (million)
% 7.11/1.57 % (2651859)ott-21_1_sil=16000:fs=off:random_seed=4109553161:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.11/1.57 % TRYING [4]
% 7.11/1.57 % TRYING [1]
% 7.11/1.57 % TRYING [2]
% 7.11/1.57 % TRYING [3]
% 7.11/1.57 % (2651854)Instruction limit reached!
% 7.11/1.57 % (2651854)------------------------------
% 7.11/1.57 % (2651854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651854)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651854)Termination reason: Instruction limit
% 7.11/1.57 % (2651854)Termination phase: Saturation
% 7.11/1.57 % (2651854)Time elapsed: 0.075 s
% 7.11/1.57 % (2651854)Peak memory usage: 14 MB
% 7.11/1.57 % (2651854)Instructions burned: 131 (million)
% 7.11/1.57 % (2651861)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3826165060:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 7.11/1.57 % (2651859)Instruction limit reached!
% 7.11/1.57 % (2651859)------------------------------
% 7.11/1.57 % (2651859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651859)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651859)Termination reason: Instruction limit
% 7.11/1.57 % (2651859)Termination phase: Saturation
% 7.11/1.57 % (2651859)Time elapsed: 0.102 s
% 7.11/1.57 % (2651859)Peak memory usage: 14 MB
% 7.11/1.57 % (2651859)Instructions burned: 180 (million)
% 7.11/1.57 % (2651863)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2533555940:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 7.11/1.57 % TRYING [4]
% 7.11/1.57 % TRYING [1]
% 7.11/1.57 % TRYING [2]
% 7.11/1.57 % (2651853)Instruction limit reached!
% 7.11/1.57 % (2651853)------------------------------
% 7.11/1.57 % (2651853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651853)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651853)Termination reason: Instruction limit
% 7.11/1.57 % (2651853)Termination phase: Finite model building constraint generation
% 7.11/1.57 % (2651853)Time elapsed: 0.266 s
% 7.11/1.57 % (2651853)Peak memory usage: 33 MB
% 7.11/1.57 % (2651853)Instructions burned: 717 (million)
% 7.11/1.57 % TRYING [3]
% 7.11/1.57 % (2651865)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4000275220:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 7.11/1.57 % (2651855)Instruction limit reached!
% 7.11/1.57 % (2651855)------------------------------
% 7.11/1.57 % (2651855)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651855)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651855)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651855)Termination reason: Instruction limit
% 7.11/1.57 % (2651855)Termination phase: Saturation
% 7.11/1.57 % (2651855)Time elapsed: 0.384 s
% 7.11/1.57 % (2651855)Peak memory usage: 16 MB
% 7.11/1.57 % (2651855)Instructions burned: 684 (million)
% 7.11/1.57 % TRYING [5]
% 7.11/1.57 % (2651867)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=675574259:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 7.11/1.57 % (2651861)Instruction limit reached!
% 7.11/1.57 % (2651861)------------------------------
% 7.11/1.57 % (2651861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651861)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651861)Termination reason: Instruction limit
% 7.11/1.57 % (2651861)Termination phase: Saturation
% 7.11/1.57 % (2651861)Time elapsed: 0.339 s
% 7.11/1.57 % (2651861)Peak memory usage: 14 MB
% 7.11/1.57 % (2651861)Instructions burned: 477 (million)
% 7.11/1.57 % (2651869)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=2472456742:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 7.11/1.57 % (2651863)Instruction limit reached!
% 7.11/1.57 % (2651863)------------------------------
% 7.11/1.57 % (2651863)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651863)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651863)Termination reason: Instruction limit
% 7.11/1.57 % (2651863)Termination phase: Finite model building SAT solving
% 7.11/1.57 % (2651863)Time elapsed: 0.407 s
% 7.11/1.57 % (2651863)Peak memory usage: 35 MB
% 7.11/1.57 % (2651863)Instructions burned: 866 (million)
% 7.11/1.57 % (2651871)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1751859106:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 7.11/1.57 % (2651867)Instruction limit reached!
% 7.11/1.57 % (2651867)------------------------------
% 7.11/1.57 % (2651867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651867)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651867)Termination reason: Instruction limit
% 7.11/1.57 % (2651867)Termination phase: Finite model building constraint generation
% 7.11/1.57 % (2651867)Time elapsed: 0.417 s
% 7.11/1.57 % (2651867)Peak memory usage: 102 MB
% 7.11/1.57 % (2651867)Instructions burned: 891 (million)
% 7.11/1.57 % (2651873)fmb+10_1_sil=64000:random_seed=611191098:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 7.11/1.57 % TRYING [1]
% 7.11/1.57 % TRYING [2]
% 7.11/1.57 % (2651869)Instruction limit reached!
% 7.11/1.57 % (2651869)------------------------------
% 7.11/1.57 % (2651869)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.57 % (2651869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.57 % (2651869)CaDiCaL version: 2.1.3
% 7.11/1.57 % (2651869)Termination reason: Instruction limit
% 7.11/1.57 % (2651869)Termination phase: Saturation
% 7.11/1.57 % (2651869)Time elapsed: 0.453 s
% 7.11/1.57 % (2651869)Peak memory usage: 20 MB
% 7.11/1.57 % (2651869)Instructions burned: 693 (million)
% 7.11/1.57 % (2651875)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=471613867:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 7.11/1.57 % TRYING [3]
% 7.11/1.57 % TRYING [20]
% 7.11/1.57 % (2651865) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2651834-2651865"...
% 7.11/1.57 % (2651865)...printing done.
% 7.11/1.57 % (2651865)Refutation found. Thanks to Tanya!
% 7.11/1.57 % SZS status Theorem for theBenchmark
% 7.11/1.57 % SZS output start Proof for theBenchmark
% See solution above
% 7.11/1.58 % (2651865)------------------------------
% 7.11/1.58 % (2651865)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.11/1.58 % (2651865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.11/1.58 % (2651865)CaDiCaL version: 2.1.3
% 7.11/1.58 % (2651865)Termination reason: Refutation
% 7.11/1.58 % (2651865)Time elapsed: 0.722 s
% 7.11/1.58 % (2651865)Peak memory usage: 26 MB
% 7.11/1.58 % (2651865)Instructions burned: 1161 (million)
% 7.11/1.58 % (2651834)Success in time 1.162 s
% 7.11/1.58 % Vampire exiting
%------------------------------------------------------------------------------