%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU328+1 : 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 : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:52:53 PM UTC 2026
% Result : Theorem 32.28s 5.64s
% Output : Refutation 32.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 13
% Syntax : Number of formulae : 64 ( 34 unt; 6 def)
% Number of atoms : 111 ( 62 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 84 ( 37 ~; 31 |; 7 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 51 ( 47 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
! [X0] : cast_to_subset(X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_subset_1) ).
fof(f18,axiom,
! [X0,X1] :
( element(X1,powerset(X0))
=> subset_complement(X0,X1) = set_difference(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_subset_1) ).
fof(f22,axiom,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_subset_1) ).
fof(f27,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(meet_of_subsets(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_setfam_1) ).
fof(f46,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X0))
& element(X2,powerset(X0)) )
=> subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k6_subset_1) ).
fof(f48,conjecture,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( X1 != empty_set
=> union_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_complement(X0,meet_of_subsets(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_tops_2) ).
fof(f49,negated_conjecture,
~ ! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( X1 != empty_set
=> union_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_complement(X0,meet_of_subsets(X0,X1)) ) ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f54,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( X1 != empty_set
=> union_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_difference(X0,cast_to_subset(X0),meet_of_subsets(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_setfam_1) ).
fof(f89,plain,
! [X0,X1] :
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f18]) ).
fof(f92,plain,
! [X0,X1] :
( element(meet_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f27]) ).
fof(f106,plain,
! [X0,X1,X2] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(ennf_transformation,[],[f46]) ).
fof(f107,plain,
! [X0,X1,X2] :
( subset_difference(X0,X1,X2) = set_difference(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(flattening,[],[f106]) ).
fof(f108,plain,
? [X0,X1] :
( union_of_subsets(X0,complements_of_subsets(X0,X1)) != subset_complement(X0,meet_of_subsets(X0,X1))
& X1 != empty_set
& element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f49]) ).
fof(f109,plain,
? [X0,X1] :
( union_of_subsets(X0,complements_of_subsets(X0,X1)) != subset_complement(X0,meet_of_subsets(X0,X1))
& X1 != empty_set
& element(X1,powerset(powerset(X0))) ),
inference(flattening,[],[f108]) ).
fof(f114,plain,
! [X0,X1] :
( union_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_difference(X0,cast_to_subset(X0),meet_of_subsets(X0,X1))
| empty_set = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f54]) ).
fof(f115,plain,
! [X0,X1] :
( union_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_difference(X0,cast_to_subset(X0),meet_of_subsets(X0,X1))
| empty_set = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(flattening,[],[f114]) ).
fof(f126,plain,
( union_of_subsets(sK4,complements_of_subsets(sK4,sK5)) != subset_complement(sK4,meet_of_subsets(sK4,sK5))
& empty_set != sK5
& element(sK5,powerset(powerset(sK4))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X0,sK4),skolemize(X1,sK5)],[f109]) ).
fof(f152,plain,
! [X0] : cast_to_subset(X0) = X0,
inference(cnf_transformation,[],[f17]) ).
fof(f153,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| subset_complement(X0,X1) = set_difference(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
fof(f154,plain,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
inference(cnf_transformation,[],[f22]) ).
fof(f157,plain,
! [X0,X1] :
( element(meet_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f92]) ).
fof(f197,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| subset_difference(X0,X1,X2) = set_difference(X1,X2) ),
inference(cnf_transformation,[],[f107]) ).
fof(f199,plain,
element(sK5,powerset(powerset(sK4))),
inference(cnf_transformation,[],[f126]) ).
fof(f200,plain,
empty_set != sK5,
inference(cnf_transformation,[],[f126]) ).
fof(f201,plain,
union_of_subsets(sK4,complements_of_subsets(sK4,sK5)) != subset_complement(sK4,meet_of_subsets(sK4,sK5)),
inference(cnf_transformation,[],[f126]) ).
fof(f206,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| empty_set = X1
| union_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_difference(X0,cast_to_subset(X0),meet_of_subsets(X0,X1)) ),
inference(cnf_transformation,[],[f115]) ).
fof(f213,definition,
sF6 = complements_of_subsets(sK4,sK5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f214,plain,
complements_of_subsets(sK4,sK5) = sF6,
inference(reorient_equations,[],[f213]) ).
fof(f215,definition,
sF7 = union_of_subsets(sK4,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f216,plain,
union_of_subsets(sK4,sF6) = sF7,
inference(reorient_equations,[],[f215]) ).
fof(f217,definition,
sF8 = meet_of_subsets(sK4,sK5),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f218,plain,
meet_of_subsets(sK4,sK5) = sF8,
inference(reorient_equations,[],[f217]) ).
fof(f219,definition,
sF9 = subset_complement(sK4,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f220,plain,
subset_complement(sK4,sF8) = sF9,
inference(reorient_equations,[],[f219]) ).
fof(f221,plain,
sF7 != sF9,
inference(definition_folding,[],[f201,f220,f218,f216,f214]) ).
fof(f222,definition,
sF10 = powerset(sK4),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f223,plain,
powerset(sK4) = sF10,
inference(reorient_equations,[],[f222]) ).
fof(f224,definition,
sF11 = powerset(sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f225,plain,
powerset(sF10) = sF11,
inference(reorient_equations,[],[f224]) ).
fof(f226,plain,
element(sK5,sF11),
inference(definition_folding,[],[f199,f225,f223]) ).
fof(f252,plain,
element(cast_to_subset(sK4),sF10),
inference(superposition,[],[f154,f223]) ).
fof(f255,plain,
element(sK4,sF10),
inference(forward_demodulation,[],[f252,f152]) ).
fof(f617,plain,
! [X0] :
( ~ element(X0,sF10)
| subset_complement(sK4,X0) = set_difference(sK4,X0) ),
inference(superposition,[],[f153,f223]) ).
fof(f675,plain,
( element(sF8,powerset(sK4))
| ~ element(sK5,powerset(powerset(sK4))) ),
inference(superposition,[],[f157,f218]) ).
fof(f679,plain,
( element(sF8,sF10)
| ~ element(sK5,powerset(powerset(sK4))) ),
inference(forward_demodulation,[],[f675,f223]) ).
fof(f681,plain,
( ~ element(sK5,powerset(sF10))
| element(sF8,sF10) ),
inference(forward_demodulation,[],[f679,f223]) ).
fof(f682,plain,
( ~ element(sK5,sF11)
| element(sF8,sF10) ),
inference(forward_demodulation,[],[f681,f225]) ).
fof(f683,plain,
element(sF8,sF10),
inference(forward_subsumption_resolution,[],[f682,f226]) ).
fof(f833,plain,
! [X0,X1] :
( ~ element(X1,sF10)
| ~ element(X0,sF10)
| subset_difference(sK4,X1,X0) = set_difference(X1,X0) ),
inference(superposition,[],[f197,f223]) ).
fof(f851,plain,
! [X0] :
( ~ element(X0,powerset(sF10))
| empty_set = X0
| union_of_subsets(sK4,complements_of_subsets(sK4,X0)) = subset_difference(sK4,cast_to_subset(sK4),meet_of_subsets(sK4,X0)) ),
inference(superposition,[],[f206,f223]) ).
fof(f854,plain,
! [X0] :
( ~ element(X0,sF11)
| empty_set = X0
| union_of_subsets(sK4,complements_of_subsets(sK4,X0)) = subset_difference(sK4,cast_to_subset(sK4),meet_of_subsets(sK4,X0)) ),
inference(forward_demodulation,[],[f851,f225]) ).
fof(f865,plain,
! [X0] :
( ~ element(X0,sF11)
| union_of_subsets(sK4,complements_of_subsets(sK4,X0)) = subset_difference(sK4,sK4,meet_of_subsets(sK4,X0))
| empty_set = X0 ),
inference(forward_demodulation,[],[f854,f152]) ).
fof(f1788,plain,
subset_complement(sK4,sF8) = set_difference(sK4,sF8),
inference(resolution,[],[f617,f683]) ).
fof(f1790,plain,
sF9 = set_difference(sK4,sF8),
inference(forward_demodulation,[],[f1788,f220]) ).
fof(f3608,plain,
! [X0] :
( ~ element(X0,sF10)
| set_difference(sK4,X0) = subset_difference(sK4,sK4,X0) ),
inference(resolution,[],[f833,f255]) ).
fof(f4302,plain,
( union_of_subsets(sK4,complements_of_subsets(sK4,sK5)) = subset_difference(sK4,sK4,meet_of_subsets(sK4,sK5))
| empty_set = sK5 ),
inference(resolution,[],[f865,f226]) ).
fof(f4307,plain,
union_of_subsets(sK4,complements_of_subsets(sK4,sK5)) = subset_difference(sK4,sK4,meet_of_subsets(sK4,sK5)),
inference(forward_subsumption_resolution,[],[f4302,f200]) ).
fof(f4313,plain,
union_of_subsets(sK4,complements_of_subsets(sK4,sK5)) = subset_difference(sK4,sK4,sF8),
inference(forward_demodulation,[],[f4307,f218]) ).
fof(f4315,plain,
union_of_subsets(sK4,sF6) = subset_difference(sK4,sK4,sF8),
inference(forward_demodulation,[],[f4313,f214]) ).
fof(f4316,plain,
sF7 = subset_difference(sK4,sK4,sF8),
inference(forward_demodulation,[],[f4315,f216]) ).
fof(f13822,plain,
set_difference(sK4,sF8) = subset_difference(sK4,sK4,sF8),
inference(resolution,[],[f3608,f683]) ).
fof(f13825,plain,
sF7 = set_difference(sK4,sF8),
inference(forward_demodulation,[],[f13822,f4316]) ).
fof(f13836,plain,
sF7 = sF9,
inference(superposition,[],[f1790,f13825]) ).
fof(f13852,plain,
$false,
inference(forward_subsumption_resolution,[],[f13836,f221]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU328+1 : 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.38 % Computer : n006.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 04:43:26 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 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
% 16.77/2.92 % (3585956)Will run a generic schedule for satisfiability detection.
% 16.77/2.92 % (3585961)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=970751761_2999 on theBenchmark for (2999ds/0Mi)
% 16.77/2.92 % TRYING [1]
% 16.77/2.92 % TRYING [2]
% 16.77/2.92 % TRYING [3]
% 16.77/2.92 % TRYING [4]
% 16.77/2.92 % (3585964)dis+10_1_sil=32000:sp=arity:random_seed=1889143395:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.77/2.92 % (3585963)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=326452545:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.77/2.92 % (3585965)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4158756487:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.77/2.92 % (3585966)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=372102560:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.77/2.92 % (3585967)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2675587613:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.77/2.92 % TRYING [5]
% 16.77/2.92 % (3585962)% WARNING: option uhcvi not known.
% 16.77/2.92 % (3585962)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1529766310:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.77/2.93 % TRYING [6]
% 16.77/2.93 % TRYING [7]
% 16.77/2.93 % (3585964)Instruction limit reached!
% 16.77/2.93 % (3585964)------------------------------
% 16.77/2.93 % (3585964)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.77/2.93 % (3585964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/2.93 % (3585964)CaDiCaL version: 2.1.3
% 16.77/2.93 % (3585964)Termination reason: Instruction limit
% 16.77/2.93 % (3585964)Termination phase: Saturation
% 16.77/2.93 % (3585964)Time elapsed: 0.067 s
% 16.77/2.93 % (3585964)Peak memory usage: 12 MB
% 16.77/2.93 % (3585964)Instructions burned: 104 (million)
% 16.77/2.93 % (3585965)Instruction limit reached!
% 16.77/2.93 % (3585965)------------------------------
% 16.77/2.93 % (3585965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.77/2.93 % (3585965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/2.93 % (3585965)CaDiCaL version: 2.1.3
% 16.77/2.93 % (3585965)Termination reason: Instruction limit
% 16.77/2.93 % (3585965)Termination phase: Saturation
% 16.77/2.93 % (3585965)Time elapsed: 0.071 s
% 16.77/2.93 % (3585965)Peak memory usage: 13 MB
% 16.77/2.93 % (3585965)Instructions burned: 117 (million)
% 16.77/2.93 % (3585966)Instruction limit reached!
% 16.77/2.93 % (3585966)------------------------------
% 16.77/2.93 % (3585966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.77/2.93 % (3585966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/2.93 % (3585966)CaDiCaL version: 2.1.3
% 16.77/2.93 % (3585966)Termination reason: Instruction limit
% 16.77/2.93 % (3585966)Termination phase: Saturation
% 16.77/2.93 % (3585966)Time elapsed: 0.080 s
% 16.77/2.93 % (3585966)Peak memory usage: 13 MB
% 16.77/2.93 % (3585966)Instructions burned: 131 (million)
% 16.77/2.93 % (3585975)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3901437337:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.77/2.93 % (3585976)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1844657025:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.77/2.93 % TRYING [1]
% 16.77/2.93 % TRYING [2]
% 16.77/2.93 % TRYING [3]
% 16.77/2.93 % TRYING [4]
% 16.77/2.93 % (3585977)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=1691430645:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.77/2.93 % TRYING [5]
% 16.77/2.93 % (3585967)Instruction limit reached!
% 16.77/2.93 % (3585967)------------------------------
% 16.77/2.93 % (3585967)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.77/2.93 % (3585967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.77/2.93 % (3585967)CaDiCaL version: 2.1.3
% 16.77/2.93 % (3585967)Termination reason: Instruction limit
% 16.77/2.93 % (3585967)Termination phase: Saturation
% 16.77/2.93 % (3585967)Time elapsed: 0.110 s
% 16.77/2.93 % (3585967)Peak memory usage: 14 MB
% 16.77/2.93 % (3585967)Instructions burned: 160 (million)
% 16.77/2.93 % (3585981)ott-21_1_sil=16000:fs=off:random_seed=556858980:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.77/2.93 % TRYING [6]
% 16.77/2.93 % (3585976)Instruction limit reached!
% 16.77/2.93 % (3585976)------------------------------
% 16.77/2.93 % (3585976)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.63 % (3585976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.63 % (3585976)CaDiCaL version: 2.1.3
% 32.28/5.63 % (3585976)Termination reason: Instruction limit
% 32.28/5.63 % (3585976)Termination phase: Saturation
% 32.28/5.63 % (3585976)Time elapsed: 0.081 s
% 32.28/5.63 % (3585976)Peak memory usage: 13 MB
% 32.28/5.63 % (3585976)Instructions burned: 131 (million)
% 32.28/5.63 % (3585983)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2198835380:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 32.28/5.63 % TRYING [7]
% 32.28/5.63 % (3585981)Instruction limit reached!
% 32.28/5.63 % (3585981)------------------------------
% 32.28/5.63 % (3585981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.63 % (3585981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.63 % (3585981)CaDiCaL version: 2.1.3
% 32.28/5.63 % (3585981)Termination reason: Instruction limit
% 32.28/5.63 % (3585981)Termination phase: Saturation
% 32.28/5.63 % (3585981)Time elapsed: 0.093 s
% 32.28/5.63 % (3585981)Peak memory usage: 13 MB
% 32.28/5.64 % (3585981)Instructions burned: 180 (million)
% 32.28/5.64 % (3585985)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2880772140:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 32.28/5.64 % TRYING [1]
% 32.28/5.64 % TRYING [2]
% 32.28/5.64 % TRYING [3]
% 32.28/5.64 % TRYING [4]
% 32.28/5.64 % TRYING [8]
% 32.28/5.64 % TRYING [5]
% 32.28/5.64 % TRYING [6]
% 32.28/5.64 % (3585975)Instruction limit reached!
% 32.28/5.64 % (3585975)------------------------------
% 32.28/5.64 % (3585975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585975)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585975)Termination reason: Instruction limit
% 32.28/5.64 % (3585975)Termination phase: Finite model building SAT solving
% 32.28/5.64 % (3585975)Time elapsed: 0.355 s
% 32.28/5.64 % (3585975)Peak memory usage: 24 MB
% 32.28/5.64 % (3585975)Instructions burned: 716 (million)
% 32.28/5.64 % TRYING [7]
% 32.28/5.64 % (3585987)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=170636476:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 32.28/5.64 % (3585977)Instruction limit reached!
% 32.28/5.64 % (3585977)------------------------------
% 32.28/5.64 % (3585977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585977)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585977)Termination reason: Instruction limit
% 32.28/5.64 % (3585977)Termination phase: Saturation
% 32.28/5.64 % (3585977)Time elapsed: 0.391 s
% 32.28/5.64 % (3585977)Peak memory usage: 18 MB
% 32.28/5.64 % (3585977)Instructions burned: 685 (million)
% 32.28/5.64 % (3585989)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3769694777:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 32.28/5.64 % (3585983)Instruction limit reached!
% 32.28/5.64 % (3585983)------------------------------
% 32.28/5.64 % (3585983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585983)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585983)Termination reason: Instruction limit
% 32.28/5.64 % (3585983)Termination phase: Saturation
% 32.28/5.64 % (3585983)Time elapsed: 0.338 s
% 32.28/5.64 % (3585983)Peak memory usage: 14 MB
% 32.28/5.64 % (3585983)Instructions burned: 478 (million)
% 32.28/5.64 % (3585991)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=646635785: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)
% 32.28/5.64 % TRYING [14]
% 32.28/5.64 % (3585985)Instruction limit reached!
% 32.28/5.64 % (3585985)------------------------------
% 32.28/5.64 % (3585985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585985)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585985)Termination reason: Instruction limit
% 32.28/5.64 % (3585985)Termination phase: Finite model building SAT solving
% 32.28/5.64 % (3585985)Time elapsed: 0.342 s
% 32.28/5.64 % (3585985)Peak memory usage: 21 MB
% 32.28/5.64 % (3585985)Instructions burned: 865 (million)
% 32.28/5.64 % (3585993)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3495176938:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 32.28/5.64 % (3585989)Instruction limit reached!
% 32.28/5.64 % (3585989)------------------------------
% 32.28/5.64 % (3585989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585989)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585989)Termination reason: Instruction limit
% 32.28/5.64 % (3585989)Termination phase: Finite model building constraint generation
% 32.28/5.64 % (3585989)Time elapsed: 0.389 s
% 32.28/5.64 % (3585989)Peak memory usage: 71 MB
% 32.28/5.64 % (3585989)Instructions burned: 889 (million)
% 32.28/5.64 % (3585991)Instruction limit reached!
% 32.28/5.64 % (3585991)------------------------------
% 32.28/5.64 % (3585991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585991)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585991)Termination reason: Instruction limit
% 32.28/5.64 % (3585991)Termination phase: Saturation
% 32.28/5.64 % (3585991)Time elapsed: 0.354 s
% 32.28/5.64 % (3585991)Peak memory usage: 20 MB
% 32.28/5.64 % (3585991)Instructions burned: 693 (million)
% 32.28/5.64 % (3585995)fmb+10_1_sil=64000:random_seed=322279100:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 32.28/5.64 % (3585996)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4050644793:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 32.28/5.64 % TRYING [1]
% 32.28/5.64 % TRYING [2]
% 32.28/5.64 % TRYING [20]
% 32.28/5.64 % TRYING [3]
% 32.28/5.64 % TRYING [4]
% 32.28/5.64 % TRYING [5]
% 32.28/5.64 % TRYING [6]
% 32.28/5.64 % (3585993)Instruction limit reached!
% 32.28/5.64 % (3585993)------------------------------
% 32.28/5.64 % (3585993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585993)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585993)Termination reason: Instruction limit
% 32.28/5.64 % (3585993)Termination phase: Saturation
% 32.28/5.64 % (3585993)Time elapsed: 0.527 s
% 32.28/5.64 % (3585993)Peak memory usage: 19 MB
% 32.28/5.64 % (3585993)Instructions burned: 880 (million)
% 32.28/5.64 % TRYING [7]
% 32.28/5.64 % (3585987)Instruction limit reached!
% 32.28/5.64 % (3585987)------------------------------
% 32.28/5.64 % (3585987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585987)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585987)Termination reason: Instruction limit
% 32.28/5.64 % (3585987)Termination phase: Saturation
% 32.28/5.64 % (3585987)Time elapsed: 0.683 s
% 32.28/5.64 % (3585987)Peak memory usage: 25 MB
% 32.28/5.64 % (3585987)Instructions burned: 1181 (million)
% 32.28/5.64 % (3585999)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=356964690:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 32.28/5.64 % TRYING [8]
% 32.28/5.64 % (3586000)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1060369522:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 32.28/5.64 % TRYING [8]
% 32.28/5.64 % (3585999)Instruction limit reached!
% 32.28/5.64 % (3585999)------------------------------
% 32.28/5.64 % (3585999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3585999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3585999)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3585999)Termination reason: Instruction limit
% 32.28/5.64 % (3585999)Termination phase: Finite model building SAT solving
% 32.28/5.64 % (3585999)Time elapsed: 0.491 s
% 32.28/5.64 % (3585999)Peak memory usage: 36 MB
% 32.28/5.64 % (3585999)Instructions burned: 920 (million)
% 32.28/5.64 % (3586003)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1745059123:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 32.28/5.64 % (3586003)Instruction limit reached!
% 32.28/5.64 % (3586003)------------------------------
% 32.28/5.64 % (3586003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3586003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3586003)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3586003)Termination reason: Instruction limit
% 32.28/5.64 % (3586003)Termination phase: Saturation
% 32.28/5.64 % (3586003)Time elapsed: 0.782 s
% 32.28/5.64 % (3586003)Peak memory usage: 27 MB
% 32.28/5.64 % (3586003)Instructions burned: 1472 (million)
% 32.28/5.64 % (3586005)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1281896792:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 32.28/5.64 % TRYING [77]
% 32.28/5.64 % (3586000)Instruction limit reached!
% 32.28/5.64 % (3586000)------------------------------
% 32.28/5.64 % (3586000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3586000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3586000)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3586000)Termination reason: Instruction limit
% 32.28/5.64 % (3586000)Termination phase: Saturation
% 32.28/5.64 % (3586000)Time elapsed: 2.743 s
% 32.28/5.64 % (3586000)Peak memory usage: 40 MB
% 32.28/5.64 % (3586000)Instructions burned: 5131 (million)
% 32.28/5.64 % (3586007)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1919358478:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 32.28/5.64 % TRYING [16]
% 32.28/5.64 % TRYING [9]
% 32.28/5.64 % (3586007)Instruction limit reached!
% 32.28/5.64 % (3586007)------------------------------
% 32.28/5.64 % (3586007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3586007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3586007)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3586007)Termination reason: Instruction limit
% 32.28/5.64 % (3586007)Termination phase: Finite model building constraint generation
% 32.28/5.64 % (3586007)Time elapsed: 0.748 s
% 32.28/5.64 % (3586007)Peak memory usage: 143 MB
% 32.28/5.64 % (3586007)Instructions burned: 2174 (million)
% 32.28/5.64 % (3586009)ott-2_1_sil=16000:newcnf=on:random_seed=4002121806:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2952 on theBenchmark for (2952ds/869Mi)
% 32.28/5.64 % (3586005)Instruction limit reached!
% 32.28/5.64 % (3586005)------------------------------
% 32.28/5.64 % (3586005)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3586005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3586005)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3586005)Termination reason: Instruction limit
% 32.28/5.64 % (3586005)Termination phase: Finite model building constraint generation
% 32.28/5.64 % (3586005)Time elapsed: 2.312 s
% 32.28/5.64 % (3586005)Peak memory usage: 436 MB
% 32.28/5.64 % (3586005)Instructions burned: 6324 (million)
% 32.28/5.64 % (3586011)ott+10_1_sil=32000:tgt=ground:random_seed=3064790282:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 32.28/5.64 % (3586011) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3585956-3586011"...
% 32.28/5.64 % (3586011)...printing done.
% 32.28/5.64 % (3586011)Refutation found. Thanks to Tanya!
% 32.28/5.64 % SZS status Theorem for theBenchmark
% 32.28/5.64 % SZS output start Proof for theBenchmark
% See solution above
% 32.28/5.64 % (3586011)------------------------------
% 32.28/5.64 % (3586011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 32.28/5.64 % (3586011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.28/5.64 % (3586011)CaDiCaL version: 2.1.3
% 32.28/5.64 % (3586011)Termination reason: Refutation
% 32.28/5.64 % (3586011)Time elapsed: 0.243 s
% 32.28/5.64 % (3586011)Peak memory usage: 16 MB
% 32.28/5.64 % (3586011)Instructions burned: 421 (million)
% 32.28/5.64 % (3585956)Success in time 5.215 s
% 32.28/5.64 % Vampire exiting
%------------------------------------------------------------------------------