%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU309+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 : n014.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:49 PM UTC 2026
% Result : Theorem 196.85s 41.29s
% Output : Refutation 196.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 6
% Syntax : Number of formulae : 39 ( 17 unt; 0 def)
% Number of atoms : 68 ( 31 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 50 ( 21 ~; 15 |; 4 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-3 aty)
% Number of variables : 33 ( 31 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f94,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,X1) = set_difference(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f139,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> element(subset_complement(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k3_subset_1) ).
fof(f235,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,subset_complement(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',involutiveness_k3_subset_1) ).
fof(f337,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f361,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t17_pre_topc) ).
fof(f380,conjecture,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t22_pre_topc) ).
fof(f381,negated_conjecture,
~ ! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)) = X1 ) ),
inference(negated_conjecture,[status(cth)],[f380]) ).
fof(f637,plain,
! [X0,X1] :
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f94]) ).
fof(f668,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f139]) ).
fof(f750,plain,
! [X0,X1] :
( subset_complement(X0,subset_complement(X0,X1)) = X1
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f235]) ).
fof(f849,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f337]) ).
fof(f883,plain,
! [X0] :
( ! [X1] :
( subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)
| ~ element(X1,powerset(the_carrier(X0))) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f361]) ).
fof(f908,plain,
? [X0] :
( ? [X1] :
( subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)) != X1
& element(X1,powerset(the_carrier(X0))) )
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f381]) ).
fof(f1515,plain,
( sK334 != subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),sK334))
& element(sK334,powerset(the_carrier(sK333)))
& one_sorted_str(sK333) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK333,sK334]),skolemize(X0,sK333),skolemize(X1,sK334)],[f908]) ).
fof(f1880,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| set_difference(X0,X1) = subset_complement(X0,X1) ),
inference(cnf_transformation,[],[f637]) ).
fof(f1958,plain,
! [X0,X1] :
( element(subset_complement(X0,X1),powerset(X0))
| ~ element(X1,powerset(X0)) ),
inference(cnf_transformation,[],[f668]) ).
fof(f2120,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| subset_complement(X0,subset_complement(X0,X1)) = X1 ),
inference(cnf_transformation,[],[f750]) ).
fof(f2593,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f849]) ).
fof(f2629,plain,
! [X0,X1] :
( ~ element(X1,powerset(the_carrier(X0)))
| subset_complement(the_carrier(X0),X1) = subset_difference(the_carrier(X0),cast_as_carrier_subset(X0),X1)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f883]) ).
fof(f2654,plain,
one_sorted_str(sK333),
inference(cnf_transformation,[],[f1515]) ).
fof(f2655,plain,
element(sK334,powerset(the_carrier(sK333))),
inference(cnf_transformation,[],[f1515]) ).
fof(f2656,plain,
sK334 != subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),sK334)),
inference(cnf_transformation,[],[f1515]) ).
fof(f3812,plain,
the_carrier(sK333) = cast_as_carrier_subset(sK333),
inference(resolution,[],[f2593,f2654]) ).
fof(f3813,plain,
sK334 != subset_difference(the_carrier(sK333),the_carrier(sK333),subset_difference(the_carrier(sK333),the_carrier(sK333),sK334)),
inference(superposition,[],[f2656,f3812]) ).
fof(f10183,plain,
set_difference(the_carrier(sK333),sK334) = subset_complement(the_carrier(sK333),sK334),
inference(resolution,[],[f1880,f2655]) ).
fof(f10434,plain,
sK334 = subset_complement(the_carrier(sK333),subset_complement(the_carrier(sK333),sK334)),
inference(resolution,[],[f2120,f2655]) ).
fof(f10435,plain,
sK334 = subset_complement(the_carrier(sK333),set_difference(the_carrier(sK333),sK334)),
inference(forward_demodulation,[],[f10434,f10183]) ).
fof(f13564,plain,
( element(set_difference(the_carrier(sK333),sK334),powerset(the_carrier(sK333)))
| ~ element(sK334,powerset(the_carrier(sK333))) ),
inference(superposition,[],[f1958,f10183]) ).
fof(f13565,plain,
element(set_difference(the_carrier(sK333),sK334),powerset(the_carrier(sK333))),
inference(forward_subsumption_resolution,[],[f13564,f2655]) ).
fof(f21607,plain,
( subset_complement(the_carrier(sK333),set_difference(the_carrier(sK333),sK334)) = subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),set_difference(the_carrier(sK333),sK334))
| ~ one_sorted_str(sK333) ),
inference(resolution,[],[f2629,f13565]) ).
fof(f21618,plain,
( subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),sK334) = subset_complement(the_carrier(sK333),sK334)
| ~ one_sorted_str(sK333) ),
inference(resolution,[],[f2629,f2655]) ).
fof(f21620,plain,
subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),sK334) = subset_complement(the_carrier(sK333),sK334),
inference(forward_subsumption_resolution,[],[f21618,f2654]) ).
fof(f21624,plain,
subset_complement(the_carrier(sK333),set_difference(the_carrier(sK333),sK334)) = subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),set_difference(the_carrier(sK333),sK334)),
inference(forward_subsumption_resolution,[],[f21607,f2654]) ).
fof(f21628,plain,
subset_difference(the_carrier(sK333),cast_as_carrier_subset(sK333),sK334) = set_difference(the_carrier(sK333),sK334),
inference(forward_demodulation,[],[f21620,f10183]) ).
fof(f21631,plain,
subset_complement(the_carrier(sK333),set_difference(the_carrier(sK333),sK334)) = subset_difference(the_carrier(sK333),the_carrier(sK333),set_difference(the_carrier(sK333),sK334)),
inference(forward_demodulation,[],[f21624,f3812]) ).
fof(f21633,plain,
subset_difference(the_carrier(sK333),the_carrier(sK333),sK334) = set_difference(the_carrier(sK333),sK334),
inference(forward_demodulation,[],[f21628,f3812]) ).
fof(f21634,plain,
sK334 = subset_difference(the_carrier(sK333),the_carrier(sK333),set_difference(the_carrier(sK333),sK334)),
inference(forward_demodulation,[],[f21631,f10435]) ).
fof(f56067,plain,
sK334 != subset_difference(the_carrier(sK333),the_carrier(sK333),set_difference(the_carrier(sK333),sK334)),
inference(superposition,[],[f3813,f21633]) ).
fof(f56069,plain,
$false,
inference(forward_subsumption_resolution,[],[f56067,f21634]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU309+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n014.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 28 04:38:01 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 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
% 8.99/1.95 % (1434203)Will run a generic schedule for satisfiability detection.
% 8.99/1.95 % (1434208)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3568837796_2999 on theBenchmark for (2999ds/0Mi)
% 8.99/1.95 % (1434209)% WARNING: option uhcvi not known.
% 8.99/1.95 % (1434209)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3048655899:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.99/1.95 % (1434210)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2754744990:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.99/1.95 % (1434213)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=575082835:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.99/1.95 % (1434211)dis+10_1_sil=32000:sp=arity:random_seed=24233756:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.99/1.95 % (1434212)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1550919466:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.99/1.95 % (1434214)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4030175042:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.99/1.95 % (1434212)Instruction limit reached!
% 8.99/1.95 % (1434212)------------------------------
% 8.99/1.95 % (1434212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.95 % (1434212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.95 % (1434212)CaDiCaL version: 2.1.3
% 8.99/1.95 % (1434212)Termination reason: Instruction limit
% 8.99/1.95 % (1434212)Termination phase: Saturation
% 8.99/1.95 % (1434212)Time elapsed: 0.057 s
% 8.99/1.95 % (1434212)Peak memory usage: 13 MB
% 8.99/1.95 % (1434212)Instructions burned: 116 (million)
% 8.99/1.95 % (1434211)Instruction limit reached!
% 8.99/1.95 % (1434211)------------------------------
% 8.99/1.95 % (1434211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.95 % (1434211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.95 % (1434211)CaDiCaL version: 2.1.3
% 8.99/1.95 % (1434211)Termination reason: Instruction limit
% 8.99/1.95 % (1434211)Termination phase: Saturation
% 8.99/1.95 % (1434211)Time elapsed: 0.062 s
% 8.99/1.95 % (1434211)Peak memory usage: 14 MB
% 8.99/1.95 % (1434211)Instructions burned: 103 (million)
% 8.99/1.95 % TRYING [1]
% 8.99/1.95 % TRYING [2]
% 8.99/1.95 % (1434213)Instruction limit reached!
% 8.99/1.95 % (1434213)------------------------------
% 8.99/1.95 % (1434213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.95 % (1434213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.95 % (1434213)CaDiCaL version: 2.1.3
% 8.99/1.95 % (1434213)Termination reason: Instruction limit
% 8.99/1.95 % (1434213)Termination phase: Saturation
% 8.99/1.95 % (1434213)Time elapsed: 0.075 s
% 8.99/1.95 % (1434213)Peak memory usage: 15 MB
% 8.99/1.95 % (1434213)Instructions burned: 131 (million)
% 8.99/1.95 % (1434222)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1349266718:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.99/1.95 % (1434223)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3385167718:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.99/1.95 % (1434224)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=2584612228:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.99/1.95 % (1434214)Instruction limit reached!
% 8.99/1.95 % (1434214)------------------------------
% 8.99/1.95 % (1434214)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.95 % (1434214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.99/1.95 % (1434214)CaDiCaL version: 2.1.3
% 8.99/1.95 % (1434214)Termination reason: Instruction limit
% 8.99/1.95 % (1434214)Termination phase: Saturation
% 8.99/1.95 % (1434214)Time elapsed: 0.095 s
% 8.99/1.95 % (1434214)Peak memory usage: 16 MB
% 8.99/1.95 % (1434214)Instructions burned: 159 (million)
% 8.99/1.95 % TRYING [3]
% 8.99/1.95 % (1434228)ott-21_1_sil=16000:fs=off:random_seed=1137944218:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.99/1.95 % (1434223)Instruction limit reached!
% 8.99/1.95 % (1434223)------------------------------
% 8.99/1.95 % (1434223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.99/1.95 % (1434223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.76/6.11 % (1434223)CaDiCaL version: 2.1.3
% 39.76/6.11 % (1434223)Termination reason: Instruction limit
% 39.76/6.11 % (1434223)Termination phase: Saturation
% 39.76/6.11 % (1434223)Time elapsed: 0.074 s
% 39.76/6.11 % (1434223)Peak memory usage: 15 MB
% 39.76/6.11 % (1434223)Instructions burned: 132 (million)
% 39.76/6.11 % (1434230)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3251212710:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 39.76/6.11 % TRYING [1]
% 39.76/6.11 % TRYING [2]
% 39.76/6.11 % (1434228)Instruction limit reached!
% 39.76/6.11 % (1434228)------------------------------
% 39.76/6.11 % (1434228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.76/6.11 % (1434228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.76/6.11 % (1434228)CaDiCaL version: 2.1.3
% 39.76/6.11 % (1434228)Termination reason: Instruction limit
% 39.76/6.11 % (1434228)Termination phase: Saturation
% 39.76/6.11 % (1434228)Time elapsed: 0.097 s
% 39.76/6.11 % (1434228)Peak memory usage: 15 MB
% 39.76/6.11 % (1434228)Instructions burned: 181 (million)
% 39.76/6.11 % (1434232)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1650178908:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 39.76/6.11 % TRYING [3]
% 39.76/6.11 % TRYING [4]
% 39.76/6.11 % TRYING [1]
% 39.76/6.11 % TRYING [2]
% 39.76/6.11 % (1434222)Instruction limit reached!
% 39.76/6.11 % (1434222)------------------------------
% 39.76/6.11 % (1434222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.76/6.11 % (1434222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.76/6.11 % (1434222)CaDiCaL version: 2.1.3
% 39.76/6.11 % (1434222)Termination reason: Instruction limit
% 39.76/6.11 % (1434222)Termination phase: Finite model building constraint generation
% 39.76/6.11 % (1434222)Time elapsed: 0.308 s
% 39.76/6.11 % (1434222)Peak memory usage: 46 MB
% 39.76/6.11 % (1434222)Instructions burned: 714 (million)
% 39.76/6.11 % (1434234)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1858332505:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 39.76/6.11 % (1434224)Instruction limit reached!
% 39.76/6.11 % (1434224)------------------------------
% 39.76/6.11 % (1434224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.76/6.11 % (1434224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.76/6.11 % (1434224)CaDiCaL version: 2.1.3
% 39.76/6.11 % (1434224)Termination reason: Instruction limit
% 39.76/6.11 % (1434224)Termination phase: Saturation
% 39.76/6.11 % (1434224)Time elapsed: 0.388 s
% 39.76/6.11 % (1434224)Peak memory usage: 21 MB
% 39.76/6.11 % (1434224)Instructions burned: 686 (million)
% 39.76/6.11 % (1434230)Instruction limit reached!
% 39.76/6.11 % (1434230)------------------------------
% 39.76/6.11 % (1434230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.76/6.11 % (1434230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.76/6.11 % (1434230)CaDiCaL version: 2.1.3
% 39.76/6.11 % (1434230)Termination reason: Instruction limit
% 39.76/6.11 % (1434230)Termination phase: Saturation
% 39.76/6.11 % (1434230)Time elapsed: 0.326 s
% 39.76/6.11 % (1434230)Peak memory usage: 16 MB
% 39.76/6.11 % (1434230)Instructions burned: 477 (million)
% 39.76/6.11 % (1434236)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4243462930:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 39.76/6.11 % (1434237)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=3081247291: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)
% 39.76/6.11 % TRYING [3]
% 39.76/6.11 % (1434232)Instruction limit reached!
% 39.76/6.11 % (1434232)------------------------------
% 39.76/6.11 % (1434232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 39.76/6.11 % (1434232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.76/6.11 % (1434232)CaDiCaL version: 2.1.3
% 39.76/6.11 % (1434232)Termination reason: Instruction limit
% 39.76/6.11 % (1434232)Termination phase: Finite model building constraint generation
% 39.76/6.11 % (1434232)Time elapsed: 0.413 s
% 39.76/6.11 % (1434232)Peak memory usage: 35 MB
% 39.76/6.11 % (1434232)Instructions burned: 868 (million)
% 39.76/6.11 % (1434240)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=319078548:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 39.76/6.11 % (1434236)Instruction limit reached!
% 39.76/6.11 % (1434236)------------------------------
% 39.76/6.11 % (1434236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.32 % (1434236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.32 % (1434236)CaDiCaL version: 2.1.3
% 91.31/13.32 % (1434236)Termination reason: Instruction limit
% 91.31/13.32 % (1434236)Termination phase: Finite model building constraint generation
% 91.31/13.32 % (1434236)Time elapsed: 0.433 s
% 91.31/13.32 % (1434236)Peak memory usage: 92 MB
% 91.31/13.32 % (1434236)Instructions burned: 893 (million)
% 91.31/13.32 % (1434237)Instruction limit reached!
% 91.31/13.32 % (1434237)------------------------------
% 91.31/13.32 % (1434237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.32 % (1434237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.32 % (1434237)CaDiCaL version: 2.1.3
% 91.31/13.32 % (1434237)Termination reason: Instruction limit
% 91.31/13.32 % (1434237)Termination phase: Saturation
% 91.31/13.32 % (1434237)Time elapsed: 0.416 s
% 91.31/13.32 % (1434237)Peak memory usage: 27 MB
% 91.31/13.32 % (1434237)Instructions burned: 692 (million)
% 91.31/13.32 % (1434242)fmb+10_1_sil=64000:random_seed=4290818257:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 91.31/13.32 % (1434243)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1579809284:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 91.31/13.32 % TRYING [1]
% 91.31/13.32 % TRYING [2]
% 91.31/13.32 % (1434243)Cannot represent all propositional literals internally
% 91.31/13.32 % (1434243)Refutation not found, incomplete strategy
% 91.31/13.32 % (1434243)------------------------------
% 91.31/13.32 % (1434243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.32 % (1434243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.32 % (1434243)CaDiCaL version: 2.1.3
% 91.31/13.32 % (1434243)Termination reason: Refutation not found, incomplete strategy
% 91.31/13.32 % (1434243)Time elapsed: 0.126 s
% 91.31/13.32 % (1434243)Peak memory usage: 16 MB
% 91.31/13.32 % (1434243)Instructions burned: 255 (million)
% 91.31/13.32 % (1434243)------------------------------
% 91.31/13.32 % (1434243)------------------------------
% 91.31/13.32 % (1434240)Instruction limit reached!
% 91.31/13.32 % (1434240)------------------------------
% 91.31/13.32 % (1434240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.32 % (1434240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.32 % (1434240)CaDiCaL version: 2.1.3
% 91.31/13.32 % (1434240)Termination reason: Instruction limit
% 91.31/13.32 % (1434240)Termination phase: Saturation
% 91.31/13.32 % (1434240)Time elapsed: 0.436 s
% 91.31/13.32 % (1434240)Peak memory usage: 22 MB
% 91.31/13.32 % (1434240)Instructions burned: 880 (million)
% 91.31/13.32 % (1434246)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1536435922:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 91.31/13.32 % (1434247)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2292061876:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 91.31/13.32 % (1434234)Instruction limit reached!
% 91.31/13.32 % (1434234)------------------------------
% 91.31/13.32 % (1434234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.32 % (1434234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.32 % (1434234)CaDiCaL version: 2.1.3
% 91.31/13.32 % (1434234)Termination reason: Instruction limit
% 91.31/13.32 % (1434234)Termination phase: Saturation
% 91.31/13.32 % (1434234)Time elapsed: 0.736 s
% 91.31/13.32 % (1434234)Peak memory usage: 29 MB
% 91.31/13.32 % (1434234)Instructions burned: 1180 (million)
% 91.31/13.32 % (1434250)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=254089282:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 91.31/13.32 % TRYING [3]
% 91.31/13.32 % TRYING [8]
% 91.31/13.32 % TRYING [5]
% 91.31/13.32 % (1434246)Instruction limit reached!
% 91.31/13.32 % (1434246)------------------------------
% 91.31/13.32 % (1434246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.31/13.32 % (1434246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.31/13.32 % (1434246)CaDiCaL version: 2.1.3
% 91.31/13.32 % (1434246)Termination reason: Instruction limit
% 91.31/13.32 % (1434246)Termination phase: Finite model building constraint generation
% 91.31/13.32 % (1434246)Time elapsed: 0.350 s
% 91.31/13.32 % (1434246)Peak memory usage: 56 MB
% 91.31/13.32 % (1434246)Instructions burned: 921 (million)
% 91.31/13.32 % (1434252)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2379677738:i=6324_2984 on theBenchmark for (2984ds/6324Mi)
% 201.79/31.14 % (1434252)Cannot represent all propositional literals internally
% 201.79/31.14 % (1434252)Refutation not found, incomplete strategy
% 201.79/31.14 % (1434252)------------------------------
% 201.79/31.14 % (1434252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.79/31.14 % (1434252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.79/31.14 % (1434252)CaDiCaL version: 2.1.3
% 201.79/31.14 % (1434252)Termination reason: Refutation not found, incomplete strategy
% 201.79/31.14 % (1434252)Time elapsed: 0.142 s
% 201.79/31.14 % (1434252)Peak memory usage: 17 MB
% 201.79/31.14 % (1434252)Instructions burned: 286 (million)
% 201.79/31.14 % (1434252)------------------------------
% 201.79/31.14 % (1434252)------------------------------
% 201.79/31.14 % (1434254)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3685767670:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi)
% 201.79/31.14 % (1434250)Instruction limit reached!
% 201.79/31.14 % (1434250)------------------------------
% 201.79/31.14 % (1434250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.79/31.14 % (1434250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.79/31.14 % (1434250)CaDiCaL version: 2.1.3
% 201.79/31.14 % (1434250)Termination reason: Instruction limit
% 201.79/31.14 % (1434250)Termination phase: Saturation
% 201.79/31.14 % (1434250)Time elapsed: 0.770 s
% 201.79/31.14 % (1434250)Peak memory usage: 29 MB
% 201.79/31.14 % (1434250)Instructions burned: 1473 (million)
% 201.79/31.14 % (1434256)ott-2_1_sil=16000:newcnf=on:random_seed=271496110:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2980 on theBenchmark for (2980ds/869Mi)
% 201.79/31.14 % TRYING [4]
% 201.79/31.14 % (1434254)Cannot represent all propositional literals internally
% 201.79/31.14 % (1434254)Refutation not found, incomplete strategy
% 201.79/31.14 % (1434254)------------------------------
% 201.79/31.14 % (1434254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.79/31.14 % (1434254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.79/31.14 % (1434254)CaDiCaL version: 2.1.3
% 201.79/31.14 % (1434254)Termination reason: Refutation not found, incomplete strategy
% 201.79/31.14 % (1434254)Time elapsed: 0.724 s
% 201.79/31.14 % (1434254)Peak memory usage: 31 MB
% 201.79/31.14 % (1434254)Instructions burned: 1484 (million)
% 201.79/31.14 % (1434254)------------------------------
% 201.79/31.14 % (1434254)------------------------------
% 201.79/31.14 % (1434258)ott+10_1_sil=32000:tgt=ground:random_seed=3699048497:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi)
% 201.79/31.14 % (1434256)Instruction limit reached!
% 201.79/31.14 % (1434256)------------------------------
% 201.79/31.14 % (1434256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.79/31.14 % (1434256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.79/31.14 % (1434256)CaDiCaL version: 2.1.3
% 201.79/31.14 % (1434256)Termination reason: Instruction limit
% 201.79/31.14 % (1434256)Termination phase: Saturation
% 201.79/31.14 % (1434256)Time elapsed: 0.446 s
% 201.79/31.14 % (1434256)Peak memory usage: 18 MB
% 201.79/31.14 % (1434256)Instructions burned: 870 (million)
% 201.79/31.14 % (1434260)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2386120382:i=54282_2975 on theBenchmark for (2975ds/54282Mi)
% 201.79/31.14 % TRYING [1]
% 201.79/31.14 % TRYING [2]
% 201.79/31.14 % TRYING [3]
% 201.79/31.14 % TRYING [4]
% 201.79/31.14 % (1434247)Instruction limit reached!
% 201.79/31.14 % (1434247)------------------------------
% 201.79/31.14 % (1434247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.79/31.14 % (1434247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.79/31.14 % (1434247)CaDiCaL version: 2.1.3
% 201.79/31.14 % (1434247)Termination reason: Instruction limit
% 201.79/31.14 % (1434247)Termination phase: Saturation
% 201.79/31.14 % (1434247)Time elapsed: 3.069 s
% 201.79/31.14 % (1434247)Peak memory usage: 50 MB
% 201.79/31.14 % (1434247)Instructions burned: 5132 (million)
% 201.79/31.14 % (1434262)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=575767015:i=3512:aac=none_2957 on theBenchmark for (2957ds/3512Mi)
% 201.79/31.14 % TRYING [5]
% 201.79/31.14 % TRYING [6]
% 201.79/31.14 % (1434258)Instruction limit reached!
% 201.79/31.14 % (1434258)------------------------------
% 201.79/31.14 % (1434258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 201.79/31.14 % (1434258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 201.79/31.14 % (1434258)CaDiCaL version: 2.1.3
% 201.79/31.14 % (1434258)Termination reason: Instruction limit
% 201.79/31.14 % (1434258)Termination phase: Saturation
% 201.79/31.14 % (1434258)Time elapsed: 3.243 s
% 196.85/41.28 % (1434258)Peak memory usage: 68 MB
% 196.85/41.28 % (1434258)Instructions burned: 5115 (million)
% 196.85/41.28 % (1434264)dis+21_1_sil=32000:sas=cadical:random_seed=230545131:i=3773:amm=off_2942 on theBenchmark for (2942ds/3773Mi)
% 196.85/41.28 % (1434262)Instruction limit reached!
% 196.85/41.28 % (1434262)------------------------------
% 196.85/41.28 % (1434262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434262)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434262)Termination reason: Instruction limit
% 196.85/41.28 % (1434262)Termination phase: Saturation
% 196.85/41.28 % (1434262)Time elapsed: 2.152 s
% 196.85/41.28 % (1434262)Peak memory usage: 42 MB
% 196.85/41.28 % (1434262)Instructions burned: 3513 (million)
% 196.85/41.28 % (1434266)ott+11_1_sil=16000:gs=on:random_seed=46625885:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2935 on theBenchmark for (2935ds/2251Mi)
% 196.85/41.28 % TRYING [5]
% 196.85/41.28 % (1434266)Instruction limit reached!
% 196.85/41.28 % (1434266)------------------------------
% 196.85/41.28 % (1434266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434266)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434266)Termination reason: Instruction limit
% 196.85/41.28 % (1434266)Termination phase: Saturation
% 196.85/41.28 % (1434266)Time elapsed: 1.268 s
% 196.85/41.28 % (1434266)Peak memory usage: 31 MB
% 196.85/41.28 % (1434266)Instructions burned: 2253 (million)
% 196.85/41.28 % (1434268)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3145760213:fmbsr=1.6:i=67534_2922 on theBenchmark for (2922ds/67534Mi)
% 196.85/41.28 % (1434264)Instruction limit reached!
% 196.85/41.28 % (1434264)------------------------------
% 196.85/41.28 % (1434264)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434264)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434264)Termination reason: Instruction limit
% 196.85/41.28 % (1434264)Termination phase: Saturation
% 196.85/41.28 % (1434264)Time elapsed: 2.279 s
% 196.85/41.28 % (1434264)Peak memory usage: 48 MB
% 196.85/41.28 % (1434264)Instructions burned: 3773 (million)
% 196.85/41.28 % (1434270)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3656628118:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2919 on theBenchmark for (2919ds/4591Mi)
% 196.85/41.28 % TRYING [7]
% 196.85/41.28 % (1434242)Instruction limit reached!
% 196.85/41.28 % (1434242)------------------------------
% 196.85/41.28 % (1434242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434242)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434242)Termination reason: Instruction limit
% 196.85/41.28 % (1434242)Termination phase: Finite model building constraint generation
% 196.85/41.28 % (1434242)Time elapsed: 9.447 s
% 196.85/41.28 % (1434242)Peak memory usage: 467 MB
% 196.85/41.28 % (1434242)Instructions burned: 22061 (million)
% 196.85/41.28 % (1434270)Instruction limit reached!
% 196.85/41.28 % (1434270)------------------------------
% 196.85/41.28 % (1434270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434270)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434270)Termination reason: Instruction limit
% 196.85/41.28 % (1434270)Termination phase: Saturation
% 196.85/41.28 % (1434270)Time elapsed: 2.476 s
% 196.85/41.28 % (1434270)Peak memory usage: 79 MB
% 196.85/41.28 % (1434270)Instructions burned: 4592 (million)
% 196.85/41.28 % (1434272)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4126841488:i=29340_2894 on theBenchmark for (2894ds/29340Mi)
% 196.85/41.28 % (1434273)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1330181721:i=5211_2894 on theBenchmark for (2894ds/5211Mi)
% 196.85/41.28 % TRYING [6]
% 196.85/41.28 % (1434273)Instruction limit reached!
% 196.85/41.28 % (1434273)------------------------------
% 196.85/41.28 % (1434273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434273)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434273)Termination reason: Instruction limit
% 196.85/41.28 % (1434273)Termination phase: Saturation
% 196.85/41.28 % (1434273)Time elapsed: 2.365 s
% 196.85/41.28 % (1434273)Peak memory usage: 53 MB
% 196.85/41.28 % (1434273)Instructions burned: 5212 (million)
% 196.85/41.28 % (1434276)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2778842028:i=5497:nm=2_2870 on theBenchmark for (2870ds/5497Mi)
% 196.85/41.28 % TRYING [17]
% 196.85/41.28 % (1434276)Instruction limit reached!
% 196.85/41.28 % (1434276)------------------------------
% 196.85/41.28 % (1434276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434276)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434276)Termination reason: Instruction limit
% 196.85/41.28 % (1434276)Termination phase: Finite model building constraint generation
% 196.85/41.28 % (1434276)Time elapsed: 1.922 s
% 196.85/41.28 % (1434276)Peak memory usage: 343 MB
% 196.85/41.28 % (1434276)Instructions burned: 5498 (million)
% 196.85/41.28 % (1434278)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=77772990:fmbsr=2:i=46332_2851 on theBenchmark for (2851ds/46332Mi)
% 196.85/41.28 % TRYING [15]
% 196.85/41.28 % TRYING [7]
% 196.85/41.28 % (1434260)Instruction limit reached!
% 196.85/41.28 % (1434260)------------------------------
% 196.85/41.28 % (1434260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434260)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434260)Termination reason: Instruction limit
% 196.85/41.28 % (1434260)Termination phase: Finite model building constraint generation
% 196.85/41.28 % (1434260)Time elapsed: 19.426 s
% 196.85/41.28 % (1434260)Peak memory usage: 1568 MB
% 196.85/41.28 % (1434260)Instructions burned: 54282 (million)
% 196.85/41.28 % (1434280)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2816620469:i=14071_2778 on theBenchmark for (2778ds/14071Mi)
% 196.85/41.28 % TRYING [12]
% 196.85/41.28 % (1434272)Instruction limit reached!
% 196.85/41.28 % (1434272)------------------------------
% 196.85/41.28 % (1434272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434272)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434272)Termination reason: Instruction limit
% 196.85/41.28 % (1434272)Termination phase: Saturation
% 196.85/41.28 % (1434272)Time elapsed: 13.652 s
% 196.85/41.28 % (1434272)Peak memory usage: 396 MB
% 196.85/41.28 % (1434272)Instructions burned: 29342 (million)
% 196.85/41.28 % (1434282)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2326945440:i=22565:add=on:rawr=on_2757 on theBenchmark for (2757ds/22565Mi)
% 196.85/41.28 % (1434280)Instruction limit reached!
% 196.85/41.28 % (1434280)------------------------------
% 196.85/41.28 % (1434280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434280)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434280)Termination reason: Instruction limit
% 196.85/41.28 % (1434280)Termination phase: Finite model building constraint generation
% 196.85/41.28 % (1434280)Time elapsed: 4.779 s
% 196.85/41.28 % (1434280)Peak memory usage: 776 MB
% 196.85/41.28 % (1434280)Instructions burned: 14073 (million)
% 196.85/41.28 % (1434284)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=402678792:i=8173:av=off_2729 on theBenchmark for (2729ds/8173Mi)
% 196.85/41.28 % (1434278)Instruction limit reached!
% 196.85/41.28 % (1434278)------------------------------
% 196.85/41.28 % (1434278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434278)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434278)Termination reason: Instruction limit
% 196.85/41.28 % (1434278)Termination phase: Finite model building constraint generation
% 196.85/41.28 % (1434278)Time elapsed: 15.582 s
% 196.85/41.28 % (1434278)Peak memory usage: 2238 MB
% 196.85/41.28 % (1434278)Instructions burned: 46334 (million)
% 196.85/41.28 % (1434268)Instruction limit reached!
% 196.85/41.28 % (1434268)------------------------------
% 196.85/41.28 % (1434268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.28 % (1434268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.28 % (1434268)CaDiCaL version: 2.1.3
% 196.85/41.28 % (1434268)Termination reason: Instruction limit
% 196.85/41.28 % (1434268)Termination phase: Finite model building constraint generation
% 196.85/41.28 % (1434268)Time elapsed: 22.987 s
% 196.85/41.29 % (1434268)Peak memory usage: 2850 MB
% 196.85/41.29 % (1434268)Instructions burned: 67536 (million)
% 196.85/41.29 % (1434286)dis+10_16:1_sil=16000:random_seed=3214341543:i=9155:fsr=off_2691 on theBenchmark for (2691ds/9155Mi)
% 196.85/41.29 % (1434288)ott-3_8_sil=64000:random_seed=3037118414:i=20139:bs=on_2688 on theBenchmark for (2688ds/20139Mi)
% 196.85/41.29 % (1434284)Instruction limit reached!
% 196.85/41.29 % (1434284)------------------------------
% 196.85/41.29 % (1434284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.29 % (1434284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.29 % (1434284)CaDiCaL version: 2.1.3
% 196.85/41.29 % (1434284)Termination reason: Instruction limit
% 196.85/41.29 % (1434284)Termination phase: Saturation
% 196.85/41.29 % (1434284)Time elapsed: 5.242 s
% 196.85/41.29 % (1434284)Peak memory usage: 118 MB
% 196.85/41.29 % (1434284)Instructions burned: 8175 (million)
% 196.85/41.29 % (1434290)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3479353058:fmbsr=2:i=32576_2677 on theBenchmark for (2677ds/32576Mi)
% 196.85/41.29 % TRYING [9]
% 196.85/41.29 % (1434286)Instruction limit reached!
% 196.85/41.29 % (1434286)------------------------------
% 196.85/41.29 % (1434286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.29 % (1434286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.29 % (1434286)CaDiCaL version: 2.1.3
% 196.85/41.29 % (1434286)Termination reason: Instruction limit
% 196.85/41.29 % (1434286)Termination phase: Saturation
% 196.85/41.29 % (1434286)Time elapsed: 5.343 s
% 196.85/41.29 % (1434286)Peak memory usage: 93 MB
% 196.85/41.29 % (1434286)Instructions burned: 9155 (million)
% 196.85/41.29 % (1434292)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=451083237:i=11404_2638 on theBenchmark for (2638ds/11404Mi)
% 196.85/41.29 % (1434282)Instruction limit reached!
% 196.85/41.29 % (1434282)------------------------------
% 196.85/41.29 % (1434282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.29 % (1434282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.29 % (1434282)CaDiCaL version: 2.1.3
% 196.85/41.29 % (1434282)Termination reason: Instruction limit
% 196.85/41.29 % (1434282)Termination phase: Saturation
% 196.85/41.29 % (1434282)Time elapsed: 13.323 s
% 196.85/41.29 % (1434282)Peak memory usage: 318 MB
% 196.85/41.29 % (1434282)Instructions burned: 22565 (million)
% 196.85/41.29 % (1434294)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=168754669:i=14134_2623 on theBenchmark for (2623ds/14134Mi)
% 196.85/41.29 % (1434294) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1434203-1434294"...
% 196.85/41.29 % (1434294)...printing done.
% 196.85/41.29 % (1434294)Refutation found. Thanks to Tanya!
% 196.85/41.29 % SZS status Theorem for theBenchmark
% 196.85/41.29 % SZS output start Proof for theBenchmark
% See solution above
% 196.85/41.29 % (1434294)------------------------------
% 196.85/41.29 % (1434294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 196.85/41.29 % (1434294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 196.85/41.29 % (1434294)CaDiCaL version: 2.1.3
% 196.85/41.29 % (1434294)Termination reason: Refutation
% 196.85/41.29 % (1434294)Time elapsed: 2.743 s
% 196.85/41.29 % (1434294)Peak memory usage: 52 MB
% 196.85/41.29 % (1434294)Instructions burned: 4378 (million)
% 196.85/41.29 % (1434203)Success in time 40.868 s
% 196.85/41.29 % Vampire exiting
%------------------------------------------------------------------------------