%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU373+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 : n001.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:53:03 PM UTC 2026
% Result : Theorem 6.16s 1.47s
% Output : Refutation 6.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 7
% Syntax : Number of formulae : 47 ( 13 unt; 1 def)
% Number of atoms : 129 ( 2 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 140 ( 58 ~; 52 |; 8 &)
% ( 5 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 2 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-4 aty)
% Number of variables : 62 ( 0 sgn 59 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f80,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( rel_str(X1)
=> ( subrelstr(X1,X0)
<=> ( subset(the_carrier(X1),the_carrier(X0))
& subset(the_InternalRel(X1),the_InternalRel(X0)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d13_yellow_0) ).
fof(f179,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> ! [X2] :
( net_str(X2,X0)
=> ( subnetstr(X2,X0,X1)
<=> ( subrelstr(X2,X1)
& the_mapping(X0,X2) = relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_yellow_6) ).
fof(f269,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> rel_str(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_waybel_0) ).
fof(f275,axiom,
! [X0] :
( rel_str(X0)
=> ! [X1] :
( subrelstr(X1,X0)
=> rel_str(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_0) ).
fof(f276,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& net_str(X1,X0) )
=> ! [X2] :
( subnetstr(X2,X0,X1)
=> net_str(X2,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_yellow_6) ).
fof(f595,conjecture,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> ! [X2] :
( subnetstr(X2,X0,X1)
=> subset(the_carrier(X2),the_carrier(X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t19_yellow_6) ).
fof(f596,negated_conjecture,
~ ! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> ! [X2] :
( subnetstr(X2,X0,X1)
=> subset(the_carrier(X2),the_carrier(X1)) ) ) ),
inference(negated_conjecture,[status(cth)],[f595]) ).
fof(f946,plain,
! [X0] :
( ! [X1] :
( ( subrelstr(X1,X0)
<=> ( subset(the_carrier(X1),the_carrier(X0))
& subset(the_InternalRel(X1),the_InternalRel(X0)) ) )
| ~ rel_str(X1) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f80]) ).
fof(f1061,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( subnetstr(X2,X0,X1)
<=> ( subrelstr(X2,X1)
& the_mapping(X0,X2) = relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) ) )
| ~ net_str(X2,X0) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f179]) ).
fof(f1148,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f269]) ).
fof(f1153,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ subrelstr(X1,X0) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f275]) ).
fof(f1154,plain,
! [X0,X1] :
( ! [X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f276]) ).
fof(f1155,plain,
! [X0,X1] :
( ! [X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f1154]) ).
fof(f1517,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ subset(the_carrier(X2),the_carrier(X1))
& subnetstr(X2,X0,X1) )
& net_str(X1,X0) )
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f596]) ).
fof(f1932,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ rel_str(X1)
| subset(the_carrier(X1),the_carrier(X0))
| ~ subrelstr(X1,X0) ),
inference(cnf_transformation,[],[f946]) ).
fof(f2345,plain,
! [X2,X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| ~ net_str(X2,X0)
| subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1) ),
inference(cnf_transformation,[],[f1061]) ).
fof(f2442,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| rel_str(X1) ),
inference(cnf_transformation,[],[f1148]) ).
fof(f2447,plain,
! [X0,X1] :
( ~ rel_str(X0)
| ~ subrelstr(X1,X0)
| rel_str(X1) ),
inference(cnf_transformation,[],[f1153]) ).
fof(f2448,plain,
! [X2,X0,X1] :
( ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ subnetstr(X2,X0,X1)
| net_str(X2,X0) ),
inference(cnf_transformation,[],[f1155]) ).
fof(f4054,plain,
subnetstr(sK506,sK504,sK505),
inference(cnf_transformation,[],[f1517]) ).
fof(f4055,plain,
~ subset(the_carrier(sK506),the_carrier(sK505)),
inference(cnf_transformation,[],[f1517]) ).
fof(f4056,plain,
net_str(sK505,sK504),
inference(cnf_transformation,[],[f1517]) ).
fof(f4057,plain,
one_sorted_str(sK504),
inference(cnf_transformation,[],[f1517]) ).
fof(f5930,plain,
! [X0,X1] :
( rel_str(X0)
| rel_str(X1)
| ~ subset(the_carrier(X1),the_carrier(X0))
| ~ subrelstr(X1,X0) ),
inference(consistent_polarity_flipping,[],[f1932]) ).
fof(f6333,plain,
! [X0,X1] :
( ~ rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(consistent_polarity_flipping,[],[f2442]) ).
fof(f6335,plain,
! [X0,X1] :
( ~ rel_str(X1)
| ~ subrelstr(X1,X0)
| rel_str(X0) ),
inference(consistent_polarity_flipping,[],[f2447]) ).
fof(f7579,plain,
subset(the_carrier(sK506),the_carrier(sK505)),
inference(consistent_polarity_flipping,[],[f4055]) ).
fof(f15230,plain,
! [X0,X1] :
( ~ subrelstr(X1,X0)
| ~ subset(the_carrier(X1),the_carrier(X0))
| rel_str(X0) ),
inference(forward_subsumption_resolution,[],[f5930,f6335]) ).
fof(f19352,plain,
! [X2,X0,X1] :
( ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| subrelstr(X2,X1)
| ~ subnetstr(X2,X0,X1) ),
inference(forward_subsumption_resolution,[],[f2345,f2448]) ).
fof(f19353,plain,
! [X0] :
( ~ one_sorted_str(sK504)
| subrelstr(X0,sK505)
| ~ subnetstr(X0,sK504,sK505) ),
inference(resolution,[],[f19352,f4056]) ).
fof(f19356,plain,
! [X0] :
( ~ subnetstr(X0,sK504,sK505)
| subrelstr(X0,sK505) ),
inference(forward_subsumption_resolution,[],[f19353,f4057]) ).
fof(f28037,definition,
( spl538_668
<=> rel_str(sK505) ),
introduced(definition,[new_symbols(definition,[spl538_668])],[avatar_definition]) ).
fof(f28038,plain,
( ~ rel_str(sK505)
| spl538_668 ),
inference(avatar_component_clause,[],[f28037]) ).
fof(f28039,plain,
( rel_str(sK505)
| ~ spl538_668 ),
inference(avatar_component_clause,[],[f28037]) ).
fof(f28052,plain,
( ! [X0] :
( ~ net_str(sK505,X0)
| ~ one_sorted_str(X0) )
| ~ spl538_668 ),
inference(resolution,[],[f28039,f6333]) ).
fof(f28053,plain,
( ~ one_sorted_str(sK504)
| ~ spl538_668 ),
inference(resolution,[],[f28052,f4056]) ).
fof(f28054,plain,
( $false
| ~ spl538_668 ),
inference(forward_subsumption_resolution,[],[f28053,f4057]) ).
fof(f28055,plain,
~ spl538_668,
inference(avatar_contradiction_clause,[],[f28054]) ).
fof(f50308,plain,
subrelstr(sK506,sK505),
inference(resolution,[],[f19356,f4054]) ).
fof(f50392,plain,
( ~ subset(the_carrier(sK506),the_carrier(sK505))
| rel_str(sK505) ),
inference(resolution,[],[f50308,f15230]) ).
fof(f50393,plain,
rel_str(sK505),
inference(forward_subsumption_resolution,[],[f50392,f7579]) ).
fof(f50397,plain,
( $false
| spl538_668 ),
inference(forward_subsumption_resolution,[],[f50393,f28038]) ).
fof(f50398,plain,
spl538_668,
inference(avatar_contradiction_clause,[],[f50397]) ).
cnf(s605,plain,
~ spl538_668,
inference(sat_conversion,[],[f28055]) ).
cnf(s1317,plain,
spl538_668,
inference(sat_conversion,[],[f50398]) ).
cnf(s1321,plain,
$false,
inference(rat,[],[s605,s1317]) ).
fof(f50407,plain,
$false,
inference(avatar_sat_refutation,[],[s1321]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU373+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 28 05:04:33 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.14/0.38 Running first-order model finding
% 0.14/0.38 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
% 6.16/1.47 % (33823)Will run a generic schedule for satisfiability detection.
% 6.16/1.47 % (33829)% WARNING: option uhcvi not known.
% 6.16/1.47 % (33829)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1107712582:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.16/1.47 % (33828)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1949133136_2999 on theBenchmark for (2999ds/0Mi)
% 6.16/1.47 % (33830)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1370692119:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.16/1.47 % (33831)dis+10_1_sil=32000:sp=arity:random_seed=30934244:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.16/1.47 % (33832)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=734806946:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.16/1.47 % (33833)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=274960109:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.16/1.47 % (33834)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3665708043:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.16/1.47 % (33831)Instruction limit reached!
% 6.16/1.47 % (33831)------------------------------
% 6.16/1.47 % (33831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33831)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33831)Termination reason: Instruction limit
% 6.16/1.47 % (33831)Termination phase: Saturation
% 6.16/1.47 % (33831)Time elapsed: 0.055 s
% 6.16/1.47 % (33831)Peak memory usage: 15 MB
% 6.16/1.47 % (33831)Instructions burned: 104 (million)
% 6.16/1.47 % (33832)Instruction limit reached!
% 6.16/1.47 % (33832)------------------------------
% 6.16/1.47 % (33832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33832)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33832)Termination reason: Instruction limit
% 6.16/1.47 % (33832)Termination phase: Blocked clause elimination
% 6.16/1.47 % (33832)Time elapsed: 0.059 s
% 6.16/1.47 % (33832)Peak memory usage: 15 MB
% 6.16/1.47 % (33832)Instructions burned: 116 (million)
% 6.16/1.47 % (33842)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4264831707:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 6.16/1.47 % (33833)Instruction limit reached!
% 6.16/1.47 % (33833)------------------------------
% 6.16/1.47 % (33833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33833)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33833)Termination reason: Instruction limit
% 6.16/1.47 % (33833)Termination phase: Saturation
% 6.16/1.47 % (33833)Time elapsed: 0.075 s
% 6.16/1.47 % (33833)Peak memory usage: 16 MB
% 6.16/1.47 % (33833)Instructions burned: 138 (million)
% 6.16/1.47 % (33843)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3803046914:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 6.16/1.47 % (33834)Instruction limit reached!
% 6.16/1.47 % (33834)------------------------------
% 6.16/1.47 % (33834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33834)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33834)Termination reason: Instruction limit
% 6.16/1.47 % (33834)Termination phase: Saturation
% 6.16/1.47 % (33834)Time elapsed: 0.090 s
% 6.16/1.47 % (33834)Peak memory usage: 17 MB
% 6.16/1.47 % (33834)Instructions burned: 159 (million)
% 6.16/1.47 % (33845)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=1394842553:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.16/1.47 % (33847)ott-21_1_sil=16000:fs=off:random_seed=4152193787:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.16/1.47 % (33843)Instruction limit reached!
% 6.16/1.47 % (33843)------------------------------
% 6.16/1.47 % (33843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33843)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33843)Termination reason: Instruction limit
% 6.16/1.47 % (33843)Termination phase: Blocked clause elimination
% 6.16/1.47 % (33843)Time elapsed: 0.069 s
% 6.16/1.47 % (33843)Peak memory usage: 15 MB
% 6.16/1.47 % (33843)Instructions burned: 131 (million)
% 6.16/1.47 % (33850)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2966706815:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 6.16/1.47 % (33847)Instruction limit reached!
% 6.16/1.47 % (33847)------------------------------
% 6.16/1.47 % (33847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33847)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33847)Termination reason: Instruction limit
% 6.16/1.47 % (33847)Termination phase: Saturation
% 6.16/1.47 % (33847)Time elapsed: 0.094 s
% 6.16/1.47 % (33847)Peak memory usage: 16 MB
% 6.16/1.47 % (33847)Instructions burned: 180 (million)
% 6.16/1.47 % (33852)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=172745018:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.16/1.47 % TRYING [1]
% 6.16/1.47 % TRYING [1]
% 6.16/1.47 % TRYING [2]
% 6.16/1.47 % TRYING [2]
% 6.16/1.47 % TRYING [3]
% 6.16/1.47 % (33842)Instruction limit reached!
% 6.16/1.47 % (33842)------------------------------
% 6.16/1.47 % (33842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33842)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33842)Termination reason: Instruction limit
% 6.16/1.47 % (33842)Termination phase: Finite model building constraint generation
% 6.16/1.47 % (33842)Time elapsed: 0.329 s
% 6.16/1.47 % (33842)Peak memory usage: 35 MB
% 6.16/1.47 % (33842)Instructions burned: 717 (million)
% 6.16/1.47 % TRYING [3]
% 6.16/1.47 % (33854)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=557059290:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 6.16/1.47 % TRYING [1]
% 6.16/1.47 % (33850)Instruction limit reached!
% 6.16/1.47 % (33850)------------------------------
% 6.16/1.47 % (33850)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33850)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33850)Termination reason: Instruction limit
% 6.16/1.47 % (33850)Termination phase: Saturation
% 6.16/1.47 % (33850)Time elapsed: 0.305 s
% 6.16/1.47 % (33850)Peak memory usage: 18 MB
% 6.16/1.47 % (33850)Instructions burned: 477 (million)
% 6.16/1.47 % TRYING [2]
% 6.16/1.47 % (33856)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3481451019:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 6.16/1.47 % (33845)Instruction limit reached!
% 6.16/1.47 % (33845)------------------------------
% 6.16/1.47 % (33845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33845)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33845)Termination reason: Instruction limit
% 6.16/1.47 % (33845)Termination phase: Saturation
% 6.16/1.47 % (33845)Time elapsed: 0.401 s
% 6.16/1.47 % (33845)Peak memory usage: 22 MB
% 6.16/1.47 % (33845)Instructions burned: 685 (million)
% 6.16/1.47 % (33858)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=266712808: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)
% 6.16/1.47 % (33852)Instruction limit reached!
% 6.16/1.47 % (33852)------------------------------
% 6.16/1.47 % (33852)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33852)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33852)Termination reason: Instruction limit
% 6.16/1.47 % (33852)Termination phase: Finite model building SAT solving
% 6.16/1.47 % (33852)Time elapsed: 0.414 s
% 6.16/1.47 % (33852)Peak memory usage: 36 MB
% 6.16/1.47 % (33852)Instructions burned: 866 (million)
% 6.16/1.47 % (33860)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=396933797:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 6.16/1.47 % (33856)Instruction limit reached!
% 6.16/1.47 % (33856)------------------------------
% 6.16/1.47 % (33856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33856)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33856)Termination reason: Instruction limit
% 6.16/1.47 % (33856)Termination phase: Finite model building constraint generation
% 6.16/1.47 % (33856)Time elapsed: 0.437 s
% 6.16/1.47 % (33856)Peak memory usage: 76 MB
% 6.16/1.47 % (33856)Instructions burned: 892 (million)
% 6.16/1.47 % (33858)Instruction limit reached!
% 6.16/1.47 % (33858)------------------------------
% 6.16/1.47 % (33858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33858)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33858)Termination reason: Instruction limit
% 6.16/1.47 % (33858)Termination phase: Saturation
% 6.16/1.47 % (33858)Time elapsed: 0.424 s
% 6.16/1.47 % (33858)Peak memory usage: 27 MB
% 6.16/1.47 % (33858)Instructions burned: 694 (million)
% 6.16/1.47 % (33862)fmb+10_1_sil=64000:random_seed=2828507165:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 6.16/1.47 % (33863)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=489477941:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 6.16/1.47 % (33829) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-33823-33829"...
% 6.16/1.47 % (33829)...printing done.
% 6.16/1.47 % (33829)Refutation found. Thanks to Tanya!
% 6.16/1.47 % SZS status Theorem for theBenchmark
% 6.16/1.47 % SZS output start Proof for theBenchmark
% See solution above
% 6.16/1.47 % (33829)------------------------------
% 6.16/1.47 % (33829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.47 % (33829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.47 % (33829)CaDiCaL version: 2.1.3
% 6.16/1.47 % (33829)Termination reason: Refutation
% 6.16/1.47 % (33829)Time elapsed: 1.002 s
% 6.16/1.47 % (33829)Peak memory usage: 38 MB
% 6.16/1.47 % (33829)Instructions burned: 3028 (million)
% 6.16/1.47 % (33823)Success in time 1.077 s
% 6.16/1.47 % Vampire exiting
%------------------------------------------------------------------------------