%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU327+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 : 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:52:53 PM UTC 2026
% Result : Theorem 36.09s 5.69s
% Output : Refutation 36.09s
% 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(f26,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> element(union_of_subsets(X0,X1),powerset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k5_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
=> meet_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_complement(X0,union_of_subsets(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t11_tops_2) ).
fof(f49,negated_conjecture,
~ ! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( X1 != empty_set
=> meet_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_complement(X0,union_of_subsets(X0,X1)) ) ),
inference(negated_conjecture,[status(cth)],[f48]) ).
fof(f54,axiom,
! [X0,X1] :
( element(X1,powerset(powerset(X0)))
=> ( X1 != empty_set
=> subset_difference(X0,cast_to_subset(X0),union_of_subsets(X0,X1)) = meet_of_subsets(X0,complements_of_subsets(X0,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t47_setfam_1) ).
fof(f89,plain,
! [X0,X1] :
( subset_complement(X0,X1) = set_difference(X0,X1)
| ~ element(X1,powerset(X0)) ),
inference(ennf_transformation,[],[f18]) ).
fof(f91,plain,
! [X0,X1] :
( element(union_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f26]) ).
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] :
( meet_of_subsets(X0,complements_of_subsets(X0,X1)) != subset_complement(X0,union_of_subsets(X0,X1))
& X1 != empty_set
& element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f49]) ).
fof(f109,plain,
? [X0,X1] :
( meet_of_subsets(X0,complements_of_subsets(X0,X1)) != subset_complement(X0,union_of_subsets(X0,X1))
& X1 != empty_set
& element(X1,powerset(powerset(X0))) ),
inference(flattening,[],[f108]) ).
fof(f114,plain,
! [X0,X1] :
( subset_difference(X0,cast_to_subset(X0),union_of_subsets(X0,X1)) = meet_of_subsets(X0,complements_of_subsets(X0,X1))
| empty_set = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(ennf_transformation,[],[f54]) ).
fof(f115,plain,
! [X0,X1] :
( subset_difference(X0,cast_to_subset(X0),union_of_subsets(X0,X1)) = meet_of_subsets(X0,complements_of_subsets(X0,X1))
| empty_set = X1
| ~ element(X1,powerset(powerset(X0))) ),
inference(flattening,[],[f114]) ).
fof(f126,plain,
( meet_of_subsets(sK4,complements_of_subsets(sK4,sK5)) != subset_complement(sK4,union_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(f156,plain,
! [X0,X1] :
( element(union_of_subsets(X0,X1),powerset(X0))
| ~ element(X1,powerset(powerset(X0))) ),
inference(cnf_transformation,[],[f91]) ).
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,
meet_of_subsets(sK4,complements_of_subsets(sK4,sK5)) != subset_complement(sK4,union_of_subsets(sK4,sK5)),
inference(cnf_transformation,[],[f126]) ).
fof(f206,plain,
! [X0,X1] :
( ~ element(X1,powerset(powerset(X0)))
| empty_set = X1
| meet_of_subsets(X0,complements_of_subsets(X0,X1)) = subset_difference(X0,cast_to_subset(X0),union_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 = meet_of_subsets(sK4,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f216,plain,
meet_of_subsets(sK4,sF6) = sF7,
inference(reorient_equations,[],[f215]) ).
fof(f217,definition,
sF8 = union_of_subsets(sK4,sK5),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f218,plain,
union_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(f645,plain,
( element(sF8,powerset(sK4))
| ~ element(sK5,powerset(powerset(sK4))) ),
inference(superposition,[],[f156,f218]) ).
fof(f649,plain,
( element(sF8,sF10)
| ~ element(sK5,powerset(powerset(sK4))) ),
inference(forward_demodulation,[],[f645,f223]) ).
fof(f651,plain,
( ~ element(sK5,powerset(sF10))
| element(sF8,sF10) ),
inference(forward_demodulation,[],[f649,f223]) ).
fof(f652,plain,
( ~ element(sK5,sF11)
| element(sF8,sF10) ),
inference(forward_demodulation,[],[f651,f225]) ).
fof(f653,plain,
element(sF8,sF10),
inference(forward_subsumption_resolution,[],[f652,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
| meet_of_subsets(sK4,complements_of_subsets(sK4,X0)) = subset_difference(sK4,cast_to_subset(sK4),union_of_subsets(sK4,X0)) ),
inference(superposition,[],[f206,f223]) ).
fof(f854,plain,
! [X0] :
( ~ element(X0,sF11)
| empty_set = X0
| meet_of_subsets(sK4,complements_of_subsets(sK4,X0)) = subset_difference(sK4,cast_to_subset(sK4),union_of_subsets(sK4,X0)) ),
inference(forward_demodulation,[],[f851,f225]) ).
fof(f865,plain,
! [X0] :
( ~ element(X0,sF11)
| meet_of_subsets(sK4,complements_of_subsets(sK4,X0)) = subset_difference(sK4,sK4,union_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,f653]) ).
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,
( meet_of_subsets(sK4,complements_of_subsets(sK4,sK5)) = subset_difference(sK4,sK4,union_of_subsets(sK4,sK5))
| empty_set = sK5 ),
inference(resolution,[],[f865,f226]) ).
fof(f4307,plain,
meet_of_subsets(sK4,complements_of_subsets(sK4,sK5)) = subset_difference(sK4,sK4,union_of_subsets(sK4,sK5)),
inference(forward_subsumption_resolution,[],[f4302,f200]) ).
fof(f4313,plain,
meet_of_subsets(sK4,complements_of_subsets(sK4,sK5)) = subset_difference(sK4,sK4,sF8),
inference(forward_demodulation,[],[f4307,f218]) ).
fof(f4315,plain,
meet_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,f653]) ).
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 : SEU327+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.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 04:49:18 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.54/4.37 % (26296)Will run a generic schedule for satisfiability detection.
% 27.54/4.37 % (26302)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1456012794_2999 on theBenchmark for (2999ds/0Mi)
% 27.54/4.37 % TRYING [1]
% 27.54/4.37 % (26303)% WARNING: option uhcvi not known.
% 27.54/4.37 % TRYING [2]
% 27.54/4.37 % TRYING [3]
% 27.54/4.37 % TRYING [4]
% 27.54/4.37 % (26303)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2623157589:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 27.54/4.37 % (26304)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=31126149:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 27.54/4.37 % (26305)dis+10_1_sil=32000:sp=arity:random_seed=1957559609:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 27.54/4.37 % (26306)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3832851495:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 27.54/4.37 % (26307)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3200608411:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 27.54/4.37 % (26308)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2679774827:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 27.54/4.37 % TRYING [5]
% 27.54/4.37 % TRYING [6]
% 27.54/4.37 % TRYING [7]
% 27.54/4.37 % (26305)Instruction limit reached!
% 27.54/4.37 % (26305)------------------------------
% 27.54/4.37 % (26305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.54/4.37 % (26305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.54/4.37 % (26305)CaDiCaL version: 2.1.3
% 27.54/4.37 % (26305)Termination reason: Instruction limit
% 27.54/4.37 % (26305)Termination phase: Saturation
% 27.54/4.37 % (26305)Time elapsed: 0.067 s
% 27.54/4.37 % (26305)Peak memory usage: 12 MB
% 27.54/4.37 % (26305)Instructions burned: 103 (million)
% 27.54/4.37 % (26306)Instruction limit reached!
% 27.54/4.37 % (26306)------------------------------
% 27.54/4.37 % (26306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.54/4.37 % (26306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.54/4.37 % (26306)CaDiCaL version: 2.1.3
% 27.54/4.37 % (26306)Termination reason: Instruction limit
% 27.54/4.37 % (26306)Termination phase: Saturation
% 27.54/4.37 % (26306)Time elapsed: 0.071 s
% 27.54/4.37 % (26306)Peak memory usage: 13 MB
% 27.54/4.37 % (26306)Instructions burned: 117 (million)
% 27.54/4.37 % (26307)Instruction limit reached!
% 27.54/4.37 % (26307)------------------------------
% 27.54/4.37 % (26307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.54/4.37 % (26307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.54/4.37 % (26307)CaDiCaL version: 2.1.3
% 27.54/4.37 % (26307)Termination reason: Instruction limit
% 27.54/4.37 % (26307)Termination phase: Saturation
% 27.54/4.37 % (26307)Time elapsed: 0.081 s
% 27.54/4.37 % (26307)Peak memory usage: 13 MB
% 27.54/4.37 % (26307)Instructions burned: 132 (million)
% 27.54/4.37 % (26316)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1607771704:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 27.54/4.37 % (26317)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2558131036:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 27.54/4.37 % TRYING [1]
% 27.54/4.37 % TRYING [2]
% 27.54/4.37 % TRYING [3]
% 27.54/4.37 % TRYING [4]
% 27.54/4.37 % (26318)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=1294009576:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 27.54/4.37 % TRYING [5]
% 27.54/4.37 % (26308)Instruction limit reached!
% 27.54/4.37 % (26308)------------------------------
% 27.54/4.37 % (26308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.54/4.37 % (26308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.54/4.37 % (26308)CaDiCaL version: 2.1.3
% 27.54/4.37 % (26308)Termination reason: Instruction limit
% 27.54/4.37 % (26308)Termination phase: Saturation
% 27.54/4.37 % (26308)Time elapsed: 0.108 s
% 27.54/4.37 % (26308)Peak memory usage: 14 MB
% 27.54/4.37 % (26308)Instructions burned: 159 (million)
% 27.54/4.37 % (26322)ott-21_1_sil=16000:fs=off:random_seed=392711083:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 27.54/4.37 % TRYING [6]
% 27.54/4.37 % (26317)Instruction limit reached!
% 27.54/4.37 % (26317)------------------------------
% 27.54/4.37 % (26317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.54/4.37 % (26317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26317)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26317)Termination reason: Instruction limit
% 36.09/5.69 % (26317)Termination phase: Saturation
% 36.09/5.69 % (26317)Time elapsed: 0.086 s
% 36.09/5.69 % (26317)Peak memory usage: 13 MB
% 36.09/5.69 % (26317)Instructions burned: 132 (million)
% 36.09/5.69 % (26324)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2116941111:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 36.09/5.69 % TRYING [7]
% 36.09/5.69 % (26322)Instruction limit reached!
% 36.09/5.69 % (26322)------------------------------
% 36.09/5.69 % (26322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26322)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26322)Termination reason: Instruction limit
% 36.09/5.69 % (26322)Termination phase: Saturation
% 36.09/5.69 % (26322)Time elapsed: 0.094 s
% 36.09/5.69 % (26322)Peak memory usage: 13 MB
% 36.09/5.69 % (26322)Instructions burned: 182 (million)
% 36.09/5.69 % (26326)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3383414891:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 36.09/5.69 % TRYING [1]
% 36.09/5.69 % TRYING [2]
% 36.09/5.69 % TRYING [3]
% 36.09/5.69 % TRYING [4]
% 36.09/5.69 % TRYING [8]
% 36.09/5.69 % TRYING [5]
% 36.09/5.69 % TRYING [6]
% 36.09/5.69 % (26316)Instruction limit reached!
% 36.09/5.69 % (26316)------------------------------
% 36.09/5.69 % (26316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26316)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26316)Termination reason: Instruction limit
% 36.09/5.69 % (26316)Termination phase: Finite model building SAT solving
% 36.09/5.69 % (26316)Time elapsed: 0.352 s
% 36.09/5.69 % (26316)Peak memory usage: 24 MB
% 36.09/5.69 % (26316)Instructions burned: 715 (million)
% 36.09/5.69 % TRYING [7]
% 36.09/5.69 % (26328)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2700052971:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 36.09/5.69 % (26318)Instruction limit reached!
% 36.09/5.69 % (26318)------------------------------
% 36.09/5.69 % (26318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26318)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26318)Termination reason: Instruction limit
% 36.09/5.69 % (26318)Termination phase: Saturation
% 36.09/5.69 % (26318)Time elapsed: 0.409 s
% 36.09/5.69 % (26318)Peak memory usage: 19 MB
% 36.09/5.69 % (26318)Instructions burned: 685 (million)
% 36.09/5.69 % (26324)Instruction limit reached!
% 36.09/5.69 % (26324)------------------------------
% 36.09/5.69 % (26324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26324)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26324)Termination reason: Instruction limit
% 36.09/5.69 % (26324)Termination phase: Saturation
% 36.09/5.69 % (26324)Time elapsed: 0.328 s
% 36.09/5.69 % (26324)Peak memory usage: 14 MB
% 36.09/5.69 % (26324)Instructions burned: 477 (million)
% 36.09/5.69 % (26330)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1965614084:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 36.09/5.69 % (26331)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=1977257106: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)
% 36.09/5.69 % TRYING [14]
% 36.09/5.69 % (26326)Instruction limit reached!
% 36.09/5.69 % (26326)------------------------------
% 36.09/5.69 % (26326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26326)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26326)Termination reason: Instruction limit
% 36.09/5.69 % (26326)Termination phase: Finite model building SAT solving
% 36.09/5.69 % (26326)Time elapsed: 0.349 s
% 36.09/5.69 % (26326)Peak memory usage: 21 MB
% 36.09/5.69 % (26326)Instructions burned: 867 (million)
% 36.09/5.69 % (26334)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3571466439:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 36.09/5.69 % (26330)Instruction limit reached!
% 36.09/5.69 % (26330)------------------------------
% 36.09/5.69 % (26330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26330)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26330)Termination reason: Instruction limit
% 36.09/5.69 % (26330)Termination phase: Finite model building constraint generation
% 36.09/5.69 % (26330)Time elapsed: 0.396 s
% 36.09/5.69 % (26330)Peak memory usage: 71 MB
% 36.09/5.69 % (26330)Instructions burned: 889 (million)
% 36.09/5.69 % (26336)fmb+10_1_sil=64000:random_seed=1800286756:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 36.09/5.69 % TRYING [1]
% 36.09/5.69 % TRYING [2]
% 36.09/5.69 % TRYING [3]
% 36.09/5.69 % TRYING [4]
% 36.09/5.69 % (26331)Instruction limit reached!
% 36.09/5.69 % (26331)------------------------------
% 36.09/5.69 % (26331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26331)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26331)Termination reason: Instruction limit
% 36.09/5.69 % (26331)Termination phase: Saturation
% 36.09/5.69 % (26331)Time elapsed: 0.434 s
% 36.09/5.69 % (26331)Peak memory usage: 21 MB
% 36.09/5.69 % (26331)Instructions burned: 693 (million)
% 36.09/5.69 % (26338)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3401657599:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 36.09/5.69 % TRYING [20]
% 36.09/5.69 % TRYING [5]
% 36.09/5.69 % TRYING [6]
% 36.09/5.69 % (26334)Instruction limit reached!
% 36.09/5.69 % (26334)------------------------------
% 36.09/5.69 % (26334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26334)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26334)Termination reason: Instruction limit
% 36.09/5.69 % (26334)Termination phase: Saturation
% 36.09/5.69 % (26334)Time elapsed: 0.530 s
% 36.09/5.69 % (26334)Peak memory usage: 19 MB
% 36.09/5.69 % (26334)Instructions burned: 880 (million)
% 36.09/5.69 % (26328)Instruction limit reached!
% 36.09/5.69 % (26328)------------------------------
% 36.09/5.69 % (26328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26328)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26328)Termination reason: Instruction limit
% 36.09/5.69 % (26328)Termination phase: Saturation
% 36.09/5.69 % (26328)Time elapsed: 0.688 s
% 36.09/5.69 % (26328)Peak memory usage: 25 MB
% 36.09/5.69 % (26328)Instructions burned: 1180 (million)
% 36.09/5.69 % (26340)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4276985081:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 36.09/5.69 % TRYING [7]
% 36.09/5.69 % TRYING [8]
% 36.09/5.69 % (26341)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1239098896:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 36.09/5.69 % (26340)Instruction limit reached!
% 36.09/5.69 % (26340)------------------------------
% 36.09/5.69 % (26340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26340)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26340)Termination reason: Instruction limit
% 36.09/5.69 % (26340)Termination phase: Finite model building SAT solving
% 36.09/5.69 % (26340)Time elapsed: 0.511 s
% 36.09/5.69 % (26340)Peak memory usage: 36 MB
% 36.09/5.69 % (26340)Instructions burned: 921 (million)
% 36.09/5.69 % TRYING [8]
% 36.09/5.69 % (26344)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2898499588:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi)
% 36.09/5.69 % (26344)Instruction limit reached!
% 36.09/5.69 % (26344)------------------------------
% 36.09/5.69 % (26344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26344)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26344)Termination reason: Instruction limit
% 36.09/5.69 % (26344)Termination phase: Saturation
% 36.09/5.69 % (26344)Time elapsed: 0.792 s
% 36.09/5.69 % (26344)Peak memory usage: 27 MB
% 36.09/5.69 % (26344)Instructions burned: 1473 (million)
% 36.09/5.69 % (26346)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4065579727:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 36.09/5.69 % TRYING [77]
% 36.09/5.69 % (26341)Instruction limit reached!
% 36.09/5.69 % (26341)------------------------------
% 36.09/5.69 % (26341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26341)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26341)Termination reason: Instruction limit
% 36.09/5.69 % (26341)Termination phase: Saturation
% 36.09/5.69 % (26341)Time elapsed: 2.760 s
% 36.09/5.69 % (26341)Peak memory usage: 40 MB
% 36.09/5.69 % (26341)Instructions burned: 5132 (million)
% 36.09/5.69 % (26348)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=221370672:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 36.09/5.69 % TRYING [16]
% 36.09/5.69 % TRYING [9]
% 36.09/5.69 % (26348)Instruction limit reached!
% 36.09/5.69 % (26348)------------------------------
% 36.09/5.69 % (26348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26348)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26348)Termination reason: Instruction limit
% 36.09/5.69 % (26348)Termination phase: Finite model building constraint generation
% 36.09/5.69 % (26348)Time elapsed: 0.750 s
% 36.09/5.69 % (26348)Peak memory usage: 143 MB
% 36.09/5.69 % (26348)Instructions burned: 2177 (million)
% 36.09/5.69 % (26350)ott-2_1_sil=16000:newcnf=on:random_seed=2870674301:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2952 on theBenchmark for (2952ds/869Mi)
% 36.09/5.69 % (26346)Instruction limit reached!
% 36.09/5.69 % (26346)------------------------------
% 36.09/5.69 % (26346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.69 % (26346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.69 % (26346)CaDiCaL version: 2.1.3
% 36.09/5.69 % (26346)Termination reason: Instruction limit
% 36.09/5.69 % (26346)Termination phase: Finite model building constraint generation
% 36.09/5.69 % (26346)Time elapsed: 2.329 s
% 36.09/5.69 % (26346)Peak memory usage: 436 MB
% 36.09/5.69 % (26346)Instructions burned: 6325 (million)
% 36.09/5.69 % (26352)ott+10_1_sil=32000:tgt=ground:random_seed=1512664422:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 36.09/5.69 % (26352) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-26296-26352"...
% 36.09/5.69 % (26352)...printing done.
% 36.09/5.69 % (26352)Refutation found. Thanks to Tanya!
% 36.09/5.69 % SZS status Theorem for theBenchmark
% 36.09/5.69 % SZS output start Proof for theBenchmark
% See solution above
% 36.09/5.70 % (26352)------------------------------
% 36.09/5.70 % (26352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 36.09/5.70 % (26352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.09/5.70 % (26352)CaDiCaL version: 2.1.3
% 36.09/5.70 % (26352)Termination reason: Refutation
% 36.09/5.70 % (26352)Time elapsed: 0.244 s
% 36.09/5.70 % (26352)Peak memory usage: 16 MB
% 36.09/5.70 % (26352)Instructions burned: 421 (million)
% 36.09/5.70 % (26296)Success in time 5.286 s
% 36.09/5.70 % Vampire exiting
%------------------------------------------------------------------------------