%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : HAL003+3 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n019.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 10:18:54 AM UTC 2026
% Result : Theorem 53.83s 8.12s
% Output : Refutation 53.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 8
% Syntax : Number of formulae : 60 ( 13 unt; 3 def)
% Number of atoms : 147 ( 18 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 157 ( 70 ~; 68 |; 12 &)
% ( 3 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 4 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 3 con; 0-3 aty)
% Number of variables : 57 ( 0 sgn 50 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1,X2] :
( ( morphism(X0,X1,X2)
& ! [X3] :
( element(X3,X2)
=> ? [X4] :
( element(X4,X1)
& apply(X0,X4) = X3 ) ) )
=> surjection(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',properties_for_surjection) ).
fof(f10,axiom,
! [X0,X1,X2] :
( ( element(X1,X0)
& element(X2,X0) )
=> element(subtract(X0,X1,X2),X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HAL001+0.ax',subtract_in_domain) ).
fof(f19,axiom,
morphism(g,b,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',g_morphism) ).
fof(f33,axiom,
! [X0] :
( element(X0,e)
=> ? [X1,X2] :
( element(X1,b)
& element(X2,b)
& apply(g,subtract(b,X1,X2)) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',lemma12) ).
fof(f34,conjecture,
surjection(g),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',g_surjection) ).
fof(f35,negated_conjecture,
~ surjection(g),
inference(negated_conjecture,[status(cth)],[f34]) ).
fof(f36,plain,
~ surjection(g),
inference(flattening,[],[f35]) ).
fof(f44,plain,
! [X0,X1,X2] :
( surjection(X0)
| ~ morphism(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ element(X4,X1)
| apply(X0,X4) != X3 )
& element(X3,X2) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f45,plain,
! [X0,X1,X2] :
( surjection(X0)
| ~ morphism(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ element(X4,X1)
| apply(X0,X4) != X3 )
& element(X3,X2) ) ),
inference(flattening,[],[f44]) ).
fof(f54,plain,
! [X0,X1,X2] :
( element(subtract(X0,X1,X2),X0)
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f55,plain,
! [X0,X1,X2] :
( element(subtract(X0,X1,X2),X0)
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(flattening,[],[f54]) ).
fof(f63,plain,
! [X0] :
( ? [X1,X2] :
( element(X1,b)
& element(X2,b)
& apply(g,subtract(b,X1,X2)) = X0 )
| ~ element(X0,e) ),
inference(ennf_transformation,[],[f33]) ).
fof(f66,plain,
! [X0,X1,X2] :
( surjection(X0)
| ~ morphism(X0,X1,X2)
| ( ! [X4] :
( ~ element(X4,X1)
| apply(X0,X4) != sK3(X0,X1,X2) )
& element(sK3(X0,X1,X2),X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X3,sK3(X0,X1,X2))],[f45]) ).
fof(f78,plain,
! [X0] :
( ( element(sK13(X0),b)
& element(sK14(X0),b)
& apply(g,subtract(b,sK13(X0),sK14(X0))) = X0 )
| ~ element(X0,e) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14]),skolemize(X1,sK13(X0)),skolemize(X2,sK14(X0))],[f63]) ).
fof(f88,plain,
! [X2,X0,X1] :
( element(sK3(X0,X1,X2),X2)
| ~ morphism(X0,X1,X2)
| surjection(X0) ),
inference(cnf_transformation,[],[f66]) ).
fof(f89,plain,
! [X2,X0,X1,X4] :
( apply(X0,X4) != sK3(X0,X1,X2)
| ~ morphism(X0,X1,X2)
| ~ element(X4,X1)
| surjection(X0) ),
inference(cnf_transformation,[],[f66]) ).
fof(f102,plain,
! [X2,X0,X1] :
( element(subtract(X0,X1,X2),X0)
| ~ element(X1,X0)
| ~ element(X2,X0) ),
inference(cnf_transformation,[],[f55]) ).
fof(f111,plain,
morphism(g,b,e),
inference(cnf_transformation,[],[f19]) ).
fof(f134,plain,
! [X0] :
( ~ element(X0,e)
| apply(g,subtract(b,sK13(X0),sK14(X0))) = X0 ),
inference(cnf_transformation,[],[f78]) ).
fof(f135,plain,
! [X0] :
( element(sK14(X0),b)
| ~ element(X0,e) ),
inference(cnf_transformation,[],[f78]) ).
fof(f136,plain,
! [X0] :
( element(sK13(X0),b)
| ~ element(X0,e) ),
inference(cnf_transformation,[],[f78]) ).
fof(f137,plain,
~ surjection(g),
inference(cnf_transformation,[],[f36]) ).
fof(f281,plain,
! [X0,X1] :
( ~ morphism(X0,X1,e)
| sK3(X0,X1,e) = apply(g,subtract(b,sK13(sK3(X0,X1,e)),sK14(sK3(X0,X1,e))))
| surjection(X0) ),
inference(resolution,[],[f134,f88]) ).
fof(f1923,plain,
( sK3(g,b,e) = apply(g,subtract(b,sK13(sK3(g,b,e)),sK14(sK3(g,b,e))))
| surjection(g) ),
inference(resolution,[],[f281,f111]) ).
fof(f1924,plain,
sK3(g,b,e) = apply(g,subtract(b,sK13(sK3(g,b,e)),sK14(sK3(g,b,e)))),
inference(forward_subsumption_resolution,[],[f1923,f137]) ).
fof(f2033,definition,
( spl15_53
<=> element(sK3(g,b,e),e) ),
introduced(definition,[new_symbols(definition,[spl15_53])],[avatar_definition]) ).
fof(f2034,plain,
( element(sK3(g,b,e),e)
| ~ spl15_53 ),
inference(avatar_component_clause,[],[f2033]) ).
fof(f2035,plain,
( ~ element(sK3(g,b,e),e)
| spl15_53 ),
inference(avatar_component_clause,[],[f2033]) ).
fof(f2101,plain,
( ~ morphism(g,b,e)
| surjection(g)
| spl15_53 ),
inference(resolution,[],[f2035,f88]) ).
fof(f2102,plain,
( surjection(g)
| spl15_53 ),
inference(forward_subsumption_resolution,[],[f2101,f111]) ).
fof(f2103,plain,
( $false
| spl15_53 ),
inference(forward_subsumption_resolution,[],[f2102,f137]) ).
fof(f2104,plain,
spl15_53,
inference(avatar_contradiction_clause,[],[f2103]) ).
fof(f2459,plain,
! [X0,X1] :
( sK3(g,X0,X1) != sK3(g,b,e)
| ~ morphism(g,X0,X1)
| ~ element(subtract(b,sK13(sK3(g,b,e)),sK14(sK3(g,b,e))),X0)
| surjection(g) ),
inference(superposition,[],[f89,f1924]) ).
fof(f2460,plain,
! [X0,X1] :
( ~ element(subtract(b,sK13(sK3(g,b,e)),sK14(sK3(g,b,e))),X0)
| ~ morphism(g,X0,X1)
| sK3(g,X0,X1) != sK3(g,b,e) ),
inference(forward_subsumption_resolution,[],[f2459,f137]) ).
fof(f33857,definition,
( spl15_472
<=> element(sK13(sK3(g,b,e)),b) ),
introduced(definition,[new_symbols(definition,[spl15_472])],[avatar_definition]) ).
fof(f33858,plain,
( ~ element(sK13(sK3(g,b,e)),b)
| spl15_472 ),
inference(avatar_component_clause,[],[f33857]) ).
fof(f33859,plain,
( element(sK13(sK3(g,b,e)),b)
| ~ spl15_472 ),
inference(avatar_component_clause,[],[f33857]) ).
fof(f33978,plain,
( ~ element(sK3(g,b,e),e)
| spl15_472 ),
inference(resolution,[],[f33858,f136]) ).
fof(f33979,plain,
( $false
| ~ spl15_53
| spl15_472 ),
inference(forward_subsumption_resolution,[],[f33978,f2034]) ).
fof(f33980,plain,
( ~ spl15_53
| spl15_472 ),
inference(avatar_contradiction_clause,[],[f33979]) ).
fof(f34803,definition,
( spl15_480
<=> element(sK14(sK3(g,b,e)),b) ),
introduced(definition,[new_symbols(definition,[spl15_480])],[avatar_definition]) ).
fof(f34804,plain,
( ~ element(sK14(sK3(g,b,e)),b)
| spl15_480 ),
inference(avatar_component_clause,[],[f34803]) ).
fof(f34805,plain,
( element(sK14(sK3(g,b,e)),b)
| ~ spl15_480 ),
inference(avatar_component_clause,[],[f34803]) ).
fof(f34954,plain,
( ~ element(sK3(g,b,e),e)
| spl15_480 ),
inference(resolution,[],[f34804,f135]) ).
fof(f34955,plain,
( $false
| ~ spl15_53
| spl15_480 ),
inference(forward_subsumption_resolution,[],[f34954,f2034]) ).
fof(f34956,plain,
( ~ spl15_53
| spl15_480 ),
inference(avatar_contradiction_clause,[],[f34955]) ).
fof(f36095,plain,
! [X0] :
( ~ morphism(g,b,X0)
| sK3(g,b,e) != sK3(g,b,X0)
| ~ element(sK13(sK3(g,b,e)),b)
| ~ element(sK14(sK3(g,b,e)),b) ),
inference(resolution,[],[f2460,f102]) ).
fof(f36096,plain,
( ! [X0] :
( ~ morphism(g,b,X0)
| sK3(g,b,e) != sK3(g,b,X0)
| ~ element(sK14(sK3(g,b,e)),b) )
| ~ spl15_472 ),
inference(forward_subsumption_resolution,[],[f36095,f33859]) ).
fof(f36097,plain,
( ! [X0] :
( ~ morphism(g,b,X0)
| sK3(g,b,e) != sK3(g,b,X0) )
| ~ spl15_472
| ~ spl15_480 ),
inference(forward_subsumption_resolution,[],[f36096,f34805]) ).
fof(f36098,plain,
( sK3(g,b,e) != sK3(g,b,e)
| ~ spl15_472
| ~ spl15_480 ),
inference(resolution,[],[f36097,f111]) ).
fof(f36099,plain,
( $false
| ~ spl15_472
| ~ spl15_480 ),
inference(trivial_inequality_removal,[],[f36098]) ).
fof(f36100,plain,
( ~ spl15_472
| ~ spl15_480 ),
inference(avatar_contradiction_clause,[],[f36099]) ).
cnf(s57,plain,
spl15_53,
inference(sat_conversion,[],[f2104]) ).
cnf(s374,plain,
( ~ spl15_53
| spl15_472 ),
inference(sat_conversion,[],[f33980]) ).
cnf(s379,plain,
( ~ spl15_53
| spl15_480 ),
inference(sat_conversion,[],[f34956]) ).
cnf(s383,plain,
( ~ spl15_472
| ~ spl15_480 ),
inference(sat_conversion,[],[f36100]) ).
cnf(s384,plain,
spl15_480,
inference(rat,[],[s379,s57]) ).
cnf(s385,plain,
spl15_472,
inference(rat,[],[s374,s57]) ).
cnf(s395,plain,
$false,
inference(rat,[],[s383,s384,s385]) ).
fof(f36101,plain,
$false,
inference(avatar_sat_refutation,[],[s395]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HAL003+3 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.40 % Computer : n019.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sun Sep 27 10:49:04 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 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
% 16.01/2.72 % (2906455)Will run a generic schedule for satisfiability detection.
% 16.01/2.72 % (2906460)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2207654684_2999 on theBenchmark for (2999ds/0Mi)
% 16.01/2.72 % (2906461)% WARNING: option uhcvi not known.
% 16.01/2.72 % TRYING [1]
% 16.01/2.72 % TRYING [2]
% 16.01/2.72 % (2906461)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=904633042:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.01/2.72 % (2906462)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3239015314:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.01/2.72 % (2906463)dis+10_1_sil=32000:sp=arity:random_seed=1148475961:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.01/2.72 % (2906464)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3795259872:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.01/2.72 % (2906465)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3159333803:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.01/2.72 % (2906466)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3957205987:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.01/2.72 % TRYING [3]
% 16.01/2.72 % (2906463)Instruction limit reached!
% 16.01/2.72 % (2906463)------------------------------
% 16.01/2.72 % (2906463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.01/2.72 % (2906463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.01/2.72 % (2906463)CaDiCaL version: 2.1.3
% 16.01/2.72 % (2906463)Termination reason: Instruction limit
% 16.01/2.72 % (2906463)Termination phase: Saturation
% 16.01/2.72 % (2906463)Time elapsed: 0.061 s
% 16.01/2.72 % (2906463)Peak memory usage: 12 MB
% 16.01/2.72 % (2906463)Instructions burned: 105 (million)
% 16.01/2.72 % (2906464)Instruction limit reached!
% 16.01/2.72 % (2906464)------------------------------
% 16.01/2.72 % (2906464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.01/2.72 % (2906464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.01/2.72 % (2906464)CaDiCaL version: 2.1.3
% 16.01/2.72 % (2906464)Termination reason: Instruction limit
% 16.01/2.72 % (2906464)Termination phase: Saturation
% 16.01/2.72 % (2906464)Time elapsed: 0.066 s
% 16.01/2.72 % (2906464)Peak memory usage: 13 MB
% 16.01/2.72 % (2906464)Instructions burned: 117 (million)
% 16.01/2.72 % (2906465)Instruction limit reached!
% 16.01/2.72 % (2906465)------------------------------
% 16.01/2.72 % (2906465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.01/2.72 % (2906465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.01/2.72 % (2906465)CaDiCaL version: 2.1.3
% 16.01/2.72 % (2906465)Termination reason: Instruction limit
% 16.01/2.72 % (2906465)Termination phase: Saturation
% 16.01/2.72 % (2906465)Time elapsed: 0.068 s
% 16.01/2.72 % (2906465)Peak memory usage: 13 MB
% 16.01/2.72 % (2906465)Instructions burned: 132 (million)
% 16.01/2.72 % (2906474)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2498196064:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.01/2.72 % (2906475)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3454554161:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.01/2.72 % TRYING [1]
% 16.01/2.72 % (2906476)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=930930394:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.01/2.72 % TRYING [2]
% 16.01/2.72 % (2906466)Instruction limit reached!
% 16.01/2.72 % (2906466)------------------------------
% 16.01/2.72 % (2906466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.01/2.72 % (2906466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.01/2.72 % (2906466)CaDiCaL version: 2.1.3
% 16.01/2.72 % (2906466)Termination reason: Instruction limit
% 16.01/2.72 % (2906466)Termination phase: Saturation
% 16.01/2.72 % (2906466)Time elapsed: 0.098 s
% 16.01/2.72 % (2906466)Peak memory usage: 15 MB
% 16.01/2.72 % (2906466)Instructions burned: 161 (million)
% 16.01/2.72 % TRYING [3]
% 16.01/2.72 % (2906480)ott-21_1_sil=16000:fs=off:random_seed=1690181104:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.01/2.72 % (2906475)Instruction limit reached!
% 16.01/2.72 % (2906475)------------------------------
% 16.01/2.72 % (2906475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.01/2.72 % (2906475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.31/6.72 % (2906475)CaDiCaL version: 2.1.3
% 44.31/6.72 % (2906475)Termination reason: Instruction limit
% 44.31/6.72 % (2906475)Termination phase: Saturation
% 44.31/6.72 % (2906475)Time elapsed: 0.073 s
% 44.31/6.72 % (2906475)Peak memory usage: 13 MB
% 44.31/6.72 % (2906475)Instructions burned: 132 (million)
% 44.31/6.72 % (2906482)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1848760741:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 44.31/6.72 % (2906480)Instruction limit reached!
% 44.31/6.72 % (2906480)------------------------------
% 44.31/6.72 % (2906480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.31/6.72 % (2906480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.31/6.72 % (2906480)CaDiCaL version: 2.1.3
% 44.31/6.72 % (2906480)Termination reason: Instruction limit
% 44.31/6.72 % (2906480)Termination phase: Saturation
% 44.31/6.72 % (2906480)Time elapsed: 0.093 s
% 44.31/6.72 % (2906480)Peak memory usage: 13 MB
% 44.31/6.72 % (2906480)Instructions burned: 181 (million)
% 44.31/6.72 % TRYING [4]
% 44.31/6.72 % (2906484)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1284658202:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 44.31/6.72 % TRYING [1]
% 44.31/6.72 % TRYING [2]
% 44.31/6.72 % TRYING [3]
% 44.31/6.72 % (2906476)Instruction limit reached!
% 44.31/6.72 % (2906476)------------------------------
% 44.31/6.72 % (2906476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.31/6.72 % (2906476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.31/6.72 % (2906476)CaDiCaL version: 2.1.3
% 44.31/6.72 % (2906476)Termination reason: Instruction limit
% 44.31/6.72 % (2906476)Termination phase: Saturation
% 44.31/6.72 % (2906476)Time elapsed: 0.362 s
% 44.31/6.72 % (2906476)Peak memory usage: 19 MB
% 44.31/6.72 % (2906476)Instructions burned: 686 (million)
% 44.31/6.72 % (2906482)Instruction limit reached!
% 44.31/6.72 % (2906482)------------------------------
% 44.31/6.72 % (2906482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.31/6.72 % (2906482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.31/6.72 % (2906482)CaDiCaL version: 2.1.3
% 44.31/6.72 % (2906482)Termination reason: Instruction limit
% 44.31/6.72 % (2906482)Termination phase: Saturation
% 44.31/6.72 % (2906482)Time elapsed: 0.279 s
% 44.31/6.72 % (2906482)Peak memory usage: 14 MB
% 44.31/6.72 % (2906482)Instructions burned: 477 (million)
% 44.31/6.72 % (2906486)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=117979028:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 44.31/6.72 % (2906487)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=841401990:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 44.31/6.72 % (2906474)Instruction limit reached!
% 44.31/6.72 % (2906474)------------------------------
% 44.31/6.72 % (2906474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.31/6.72 % (2906474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.31/6.72 % (2906474)CaDiCaL version: 2.1.3
% 44.31/6.72 % (2906474)Termination reason: Instruction limit
% 44.31/6.72 % (2906474)Termination phase: Finite model building SAT solving
% 44.31/6.72 % (2906474)Time elapsed: 0.439 s
% 44.31/6.72 % (2906474)Peak memory usage: 21 MB
% 44.31/6.72 % (2906474)Instructions burned: 715 (million)
% 44.31/6.72 % (2906490)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=1508392362: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)
% 44.31/6.72 % TRYING [4]
% 44.31/6.72 % (2906484)Instruction limit reached!
% 44.31/6.72 % (2906484)------------------------------
% 44.31/6.72 % (2906484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.31/6.72 % (2906484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.31/6.72 % (2906484)CaDiCaL version: 2.1.3
% 44.31/6.72 % (2906484)Termination reason: Instruction limit
% 44.31/6.72 % (2906484)Termination phase: Finite model building constraint generation
% 44.31/6.72 % (2906484)Time elapsed: 0.384 s
% 44.31/6.72 % (2906484)Peak memory usage: 26 MB
% 44.31/6.72 % (2906484)Instructions burned: 868 (million)
% 44.31/6.72 % (2906492)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=693457049:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 44.31/6.72 % (2906487)Instruction limit reached!
% 44.31/6.72 % (2906487)------------------------------
% 44.31/6.72 % (2906487)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906487)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906487)Termination reason: Instruction limit
% 53.83/8.12 % (2906487)Termination phase: Finite model building constraint generation
% 53.83/8.12 % (2906487)Time elapsed: 0.410 s
% 53.83/8.12 % (2906487)Peak memory usage: 110 MB
% 53.83/8.12 % (2906487)Instructions burned: 891 (million)
% 53.83/8.12 % (2906494)fmb+10_1_sil=64000:random_seed=2755823059:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 53.83/8.12 % TRYING [1]
% 53.83/8.12 % TRYING [2]
% 53.83/8.12 % (2906490)Instruction limit reached!
% 53.83/8.12 % (2906490)------------------------------
% 53.83/8.12 % (2906490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906490)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906490)Termination reason: Instruction limit
% 53.83/8.12 % (2906490)Termination phase: Saturation
% 53.83/8.12 % (2906490)Time elapsed: 0.405 s
% 53.83/8.12 % (2906490)Peak memory usage: 22 MB
% 53.83/8.12 % (2906490)Instructions burned: 692 (million)
% 53.83/8.12 % TRYING [3]
% 53.83/8.12 % (2906496)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3708874676:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 53.83/8.12 % TRYING [20]
% 53.83/8.12 % (2906492)Instruction limit reached!
% 53.83/8.12 % (2906492)------------------------------
% 53.83/8.12 % (2906492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906492)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906492)Termination reason: Instruction limit
% 53.83/8.12 % (2906492)Termination phase: Saturation
% 53.83/8.12 % (2906492)Time elapsed: 0.514 s
% 53.83/8.12 % (2906492)Peak memory usage: 19 MB
% 53.83/8.12 % (2906492)Instructions burned: 879 (million)
% 53.83/8.12 % (2906486)Instruction limit reached!
% 53.83/8.12 % (2906486)------------------------------
% 53.83/8.12 % (2906486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906486)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906486)Termination reason: Instruction limit
% 53.83/8.12 % (2906486)Termination phase: Saturation
% 53.83/8.12 % (2906486)Time elapsed: 0.685 s
% 53.83/8.12 % (2906486)Peak memory usage: 24 MB
% 53.83/8.12 % (2906486)Instructions burned: 1180 (million)
% 53.83/8.12 % (2906498)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2745013005:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 53.83/8.12 % (2906499)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=947662070:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 53.83/8.12 % TRYING [4]
% 53.83/8.12 % TRYING [8]
% 53.83/8.12 % (2906498)Instruction limit reached!
% 53.83/8.12 % (2906498)------------------------------
% 53.83/8.12 % (2906498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906498)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906498)Termination reason: Instruction limit
% 53.83/8.12 % (2906498)Termination phase: Finite model building constraint generation
% 53.83/8.12 % (2906498)Time elapsed: 0.311 s
% 53.83/8.12 % (2906498)Peak memory usage: 66 MB
% 53.83/8.12 % (2906498)Instructions burned: 921 (million)
% 53.83/8.12 % (2906502)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4268157668:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 53.83/8.12 % (2906502)Instruction limit reached!
% 53.83/8.12 % (2906502)------------------------------
% 53.83/8.12 % (2906502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906502)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906502)Termination reason: Instruction limit
% 53.83/8.12 % (2906502)Termination phase: Saturation
% 53.83/8.12 % (2906502)Time elapsed: 0.697 s
% 53.83/8.12 % (2906502)Peak memory usage: 26 MB
% 53.83/8.12 % (2906502)Instructions burned: 1473 (million)
% 53.83/8.12 % (2906504)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3436276205:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 53.83/8.12 % (2906504)Cannot represent all propositional literals internally
% 53.83/8.12 % (2906504)Refutation not found, incomplete strategy
% 53.83/8.12 % (2906504)------------------------------
% 53.83/8.12 % (2906504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906504)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906504)Termination reason: Refutation not found, incomplete strategy
% 53.83/8.12 % (2906504)Time elapsed: 0.007 s
% 53.83/8.12 % (2906504)Peak memory usage: 10 MB
% 53.83/8.12 % (2906504)Instructions burned: 13 (million)
% 53.83/8.12 % (2906504)------------------------------
% 53.83/8.12 % (2906504)------------------------------
% 53.83/8.12 % (2906506)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3053962678:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 53.83/8.12 % TRYING [16]
% 53.83/8.12 % (2906506)Instruction limit reached!
% 53.83/8.12 % (2906506)------------------------------
% 53.83/8.12 % (2906506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906506)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906506)Termination reason: Instruction limit
% 53.83/8.12 % (2906506)Termination phase: Finite model building constraint generation
% 53.83/8.12 % (2906506)Time elapsed: 0.723 s
% 53.83/8.12 % (2906506)Peak memory usage: 119 MB
% 53.83/8.12 % (2906506)Instructions burned: 2174 (million)
% 53.83/8.12 % (2906508)ott-2_1_sil=16000:newcnf=on:random_seed=2214282646:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 53.83/8.12 % (2906508)Instruction limit reached!
% 53.83/8.12 % (2906508)------------------------------
% 53.83/8.12 % (2906508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906508)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906508)Termination reason: Instruction limit
% 53.83/8.12 % (2906508)Termination phase: Saturation
% 53.83/8.12 % (2906508)Time elapsed: 0.504 s
% 53.83/8.12 % (2906508)Peak memory usage: 20 MB
% 53.83/8.12 % (2906508)Instructions burned: 872 (million)
% 53.83/8.12 % (2906510)ott+10_1_sil=32000:tgt=ground:random_seed=574306485:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 53.83/8.12 % (2906499)Instruction limit reached!
% 53.83/8.12 % (2906499)------------------------------
% 53.83/8.12 % (2906499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906499)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906499)Termination reason: Instruction limit
% 53.83/8.12 % (2906499)Termination phase: Saturation
% 53.83/8.12 % (2906499)Time elapsed: 2.686 s
% 53.83/8.12 % (2906499)Peak memory usage: 38 MB
% 53.83/8.12 % (2906499)Instructions burned: 5131 (million)
% 53.83/8.12 % (2906512)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2508154882:i=54282_2960 on theBenchmark for (2960ds/54282Mi)
% 53.83/8.12 % TRYING [1]
% 53.83/8.12 % TRYING [2]
% 53.83/8.12 % TRYING [3]
% 53.83/8.12 % TRYING [4]
% 53.83/8.12 % (2906496)Instruction limit reached!
% 53.83/8.12 % (2906496)------------------------------
% 53.83/8.12 % (2906496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906496)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906496)Termination reason: Instruction limit
% 53.83/8.12 % (2906496)Termination phase: Finite model building constraint generation
% 53.83/8.12 % (2906496)Time elapsed: 3.303 s
% 53.83/8.12 % (2906496)Peak memory usage: 564 MB
% 53.83/8.12 % (2906496)Instructions burned: 9516 (million)
% 53.83/8.12 % (2906514)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3494717276:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi)
% 53.83/8.12 % (2906514)Instruction limit reached!
% 53.83/8.12 % (2906514)------------------------------
% 53.83/8.12 % (2906514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906514)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906514)Termination reason: Instruction limit
% 53.83/8.12 % (2906514)Termination phase: Saturation
% 53.83/8.12 % (2906514)Time elapsed: 1.803 s
% 53.83/8.12 % (2906514)Peak memory usage: 41 MB
% 53.83/8.12 % (2906514)Instructions burned: 3513 (million)
% 53.83/8.12 % (2906516)dis+21_1_sil=32000:sas=cadical:random_seed=2048612187:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 53.83/8.12 % (2906510)Instruction limit reached!
% 53.83/8.12 % (2906510)------------------------------
% 53.83/8.12 % (2906510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906510)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906510)Termination reason: Instruction limit
% 53.83/8.12 % (2906510)Termination phase: Saturation
% 53.83/8.12 % (2906510)Time elapsed: 2.698 s
% 53.83/8.12 % (2906510)Peak memory usage: 50 MB
% 53.83/8.12 % (2906510)Instructions burned: 5115 (million)
% 53.83/8.12 % (2906518)ott+11_1_sil=16000:gs=on:random_seed=2597522260:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 53.83/8.12 % (2906518)Instruction limit reached!
% 53.83/8.12 % (2906518)------------------------------
% 53.83/8.12 % (2906518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906518)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906518)Termination reason: Instruction limit
% 53.83/8.12 % (2906518)Termination phase: Saturation
% 53.83/8.12 % (2906518)Time elapsed: 1.076 s
% 53.83/8.12 % (2906518)Peak memory usage: 20 MB
% 53.83/8.12 % (2906518)Instructions burned: 2251 (million)
% 53.83/8.12 % (2906520)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3048473530:fmbsr=1.6:i=67534_2926 on theBenchmark for (2926ds/67534Mi)
% 53.83/8.12 % (2906516) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2906455-2906516"...
% 53.83/8.12 % (2906516)...printing done.
% 53.83/8.12 % (2906516)Refutation found. Thanks to Tanya!
% 53.83/8.12 % SZS status Theorem for theBenchmark
% 53.83/8.12 % SZS output start Proof for theBenchmark
% See solution above
% 53.83/8.12 % (2906516)------------------------------
% 53.83/8.12 % (2906516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 53.83/8.12 % (2906516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 53.83/8.12 % (2906516)CaDiCaL version: 2.1.3
% 53.83/8.12 % (2906516)Termination reason: Refutation
% 53.83/8.12 % (2906516)Time elapsed: 1.422 s
% 53.83/8.12 % (2906516)Peak memory usage: 27 MB
% 53.83/8.12 % (2906516)Instructions burned: 2654 (million)
% 53.83/8.12 % (2906455)Success in time 7.678 s
% 53.83/8.12 % Vampire exiting
%------------------------------------------------------------------------------