%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SEU307+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 30.42s 5.71s
% Output : Refutation 30.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 36 ( 20 unt; 0 def)
% Number of atoms : 60 ( 27 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 41 ( 17 ~; 13 |; 3 &)
% ( 2 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 44 ( 42 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f86,axiom,
! [X0] : cast_to_subset(X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_subset_1) ).
fof(f132,axiom,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k2_subset_1) ).
fof(f243,axiom,
! [X0,X1] :
( set_difference(X0,X1) = empty_set
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l32_xboole_1) ).
fof(f284,axiom,
! [X0,X1,X2] :
( ( element(X1,powerset(X0))
& element(X2,powerset(X0)) )
=> subset_intersection2(X0,X1,X2) = set_intersection2(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f332,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f347,conjecture,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_intersection2(the_carrier(X0),X1,cast_as_carrier_subset(X0)) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_pre_topc) ).
fof(f348,negated_conjecture,
~ ! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( element(X1,powerset(the_carrier(X0)))
=> subset_intersection2(the_carrier(X0),X1,cast_as_carrier_subset(X0)) = X1 ) ),
inference(negated_conjecture,[status(cth)],[f347]) ).
fof(f416,axiom,
! [X0] : set_difference(X0,empty_set) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_boole) ).
fof(f418,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(f436,axiom,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f769,plain,
! [X0,X1,X2] :
( subset_intersection2(X0,X1,X2) = set_intersection2(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(ennf_transformation,[],[f284]) ).
fof(f770,plain,
! [X0,X1,X2] :
( subset_intersection2(X0,X1,X2) = set_intersection2(X1,X2)
| ~ element(X1,powerset(X0))
| ~ element(X2,powerset(X0)) ),
inference(flattening,[],[f769]) ).
fof(f837,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f332]) ).
fof(f858,plain,
? [X0] :
( ? [X1] :
( subset_intersection2(the_carrier(X0),X1,cast_as_carrier_subset(X0)) != X1
& element(X1,powerset(the_carrier(X0))) )
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f348]) ).
fof(f1290,plain,
! [X0] : cast_to_subset(X0) = X0,
inference(cnf_transformation,[],[f86]) ).
fof(f1406,plain,
! [X0] : element(cast_to_subset(X0),powerset(X0)),
inference(cnf_transformation,[],[f132]) ).
fof(f1575,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| empty_set = set_difference(X0,X1) ),
inference(cnf_transformation,[],[f243]) ).
fof(f1687,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| subset_intersection2(X0,X1,X2) = set_intersection2(X1,X2) ),
inference(cnf_transformation,[],[f770]) ).
fof(f2249,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f837]) ).
fof(f2271,plain,
element(sK313,powerset(the_carrier(sK312))),
inference(cnf_transformation,[],[f858]) ).
fof(f2272,plain,
sK313 != subset_intersection2(the_carrier(sK312),sK313,cast_as_carrier_subset(sK312)),
inference(cnf_transformation,[],[f858]) ).
fof(f2273,plain,
one_sorted_str(sK312),
inference(cnf_transformation,[],[f858]) ).
fof(f2381,plain,
! [X0] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[],[f416]) ).
fof(f2384,plain,
! [X0,X1] :
( ~ element(X0,powerset(X1))
| subset(X0,X1) ),
inference(cnf_transformation,[],[f418]) ).
fof(f2412,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1)),
inference(cnf_transformation,[],[f436]) ).
fof(f2694,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(X0))
| ~ element(X1,powerset(X0))
| subset_intersection2(X0,X1,X2) = set_difference(X1,set_difference(X1,X2)) ),
inference(definition_unfolding,[],[f1687,f2412]) ).
fof(f3135,plain,
! [X0] : element(X0,powerset(X0)),
inference(forward_demodulation,[],[f1406,f1290]) ).
fof(f3308,plain,
the_carrier(sK312) = cast_as_carrier_subset(sK312),
inference(resolution,[],[f2249,f2273]) ).
fof(f3309,plain,
sK313 != subset_intersection2(the_carrier(sK312),sK313,the_carrier(sK312)),
inference(superposition,[],[f2272,f3308]) ).
fof(f3653,plain,
subset(sK313,the_carrier(sK312)),
inference(resolution,[],[f2384,f2271]) ).
fof(f3732,plain,
empty_set = set_difference(sK313,the_carrier(sK312)),
inference(resolution,[],[f1575,f3653]) ).
fof(f20526,plain,
! [X0] :
( ~ element(X0,powerset(the_carrier(sK312)))
| subset_intersection2(the_carrier(sK312),sK313,X0) = set_difference(sK313,set_difference(sK313,X0)) ),
inference(resolution,[],[f2694,f2271]) ).
fof(f54549,plain,
subset_intersection2(the_carrier(sK312),sK313,the_carrier(sK312)) = set_difference(sK313,set_difference(sK313,the_carrier(sK312))),
inference(resolution,[],[f20526,f3135]) ).
fof(f54581,plain,
subset_intersection2(the_carrier(sK312),sK313,the_carrier(sK312)) = set_difference(sK313,empty_set),
inference(forward_demodulation,[],[f54549,f3732]) ).
fof(f54586,plain,
sK313 = subset_intersection2(the_carrier(sK312),sK313,the_carrier(sK312)),
inference(forward_demodulation,[],[f54581,f2381]) ).
fof(f54590,plain,
$false,
inference(forward_subsumption_resolution,[],[f54586,f3309]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU307+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.17/0.43 % Computer : n026.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 28 04:40:41 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.22/0.48 Running first-order model finding
% 0.22/0.48 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
% 18.10/3.13 % (3463096)Will run a generic schedule for satisfiability detection.
% 18.10/3.13 % (3463101)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1145673181_2999 on theBenchmark for (2999ds/0Mi)
% 18.10/3.13 % (3463106)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2564207777:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 18.10/3.13 % (3463102)% WARNING: option uhcvi not known.
% 18.10/3.13 % (3463103)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=918722064:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 18.10/3.13 % (3463102)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1543134105:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 18.10/3.13 % (3463105)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1590646693:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 18.10/3.13 % (3463104)dis+10_1_sil=32000:sp=arity:random_seed=2349203095:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 18.10/3.13 % (3463107)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3954055752:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 18.10/3.13 % (3463106)Instruction limit reached!
% 18.10/3.13 % (3463106)------------------------------
% 18.10/3.13 % (3463106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/3.13 % (3463106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.13 % (3463106)CaDiCaL version: 2.1.3
% 18.10/3.13 % (3463106)Termination reason: Instruction limit
% 18.10/3.13 % (3463106)Termination phase: Saturation
% 18.10/3.13 % (3463106)Time elapsed: 0.108 s
% 18.10/3.13 % (3463106)Peak memory usage: 15 MB
% 18.10/3.13 % (3463106)Instructions burned: 131 (million)
% 18.10/3.13 % (3463104)Instruction limit reached!
% 18.10/3.13 % (3463104)------------------------------
% 18.10/3.13 % (3463104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/3.13 % (3463104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.13 % (3463104)CaDiCaL version: 2.1.3
% 18.10/3.13 % (3463104)Termination reason: Instruction limit
% 18.10/3.13 % (3463104)Termination phase: Saturation
% 18.10/3.13 % (3463104)Time elapsed: 0.103 s
% 18.10/3.13 % (3463104)Peak memory usage: 14 MB
% 18.10/3.13 % (3463104)Instructions burned: 103 (million)
% 18.10/3.13 % (3463105)Instruction limit reached!
% 18.10/3.13 % (3463105)------------------------------
% 18.10/3.13 % (3463105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/3.13 % (3463105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.13 % (3463105)CaDiCaL version: 2.1.3
% 18.10/3.13 % (3463105)Termination reason: Instruction limit
% 18.10/3.13 % (3463105)Termination phase: Saturation
% 18.10/3.13 % (3463105)Time elapsed: 0.104 s
% 18.10/3.13 % (3463105)Peak memory usage: 13 MB
% 18.10/3.13 % (3463105)Instructions burned: 117 (million)
% 18.10/3.13 % TRYING [1]
% 18.10/3.13 % TRYING [2]
% 18.10/3.13 % (3463115)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3003293259:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 18.10/3.13 % (3463116)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3067927405:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 18.10/3.13 % (3463117)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=1792628632:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 18.10/3.13 % (3463107)Instruction limit reached!
% 18.10/3.13 % (3463107)------------------------------
% 18.10/3.13 % (3463107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/3.13 % (3463107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.10/3.13 % (3463107)CaDiCaL version: 2.1.3
% 18.10/3.13 % (3463107)Termination reason: Instruction limit
% 18.10/3.13 % (3463107)Termination phase: Saturation
% 18.10/3.13 % (3463107)Time elapsed: 0.165 s
% 18.10/3.13 % (3463107)Peak memory usage: 15 MB
% 18.10/3.13 % (3463107)Instructions burned: 159 (million)
% 18.10/3.13 % TRYING [3]
% 18.10/3.13 % (3463121)ott-21_1_sil=16000:fs=off:random_seed=158876498:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 18.10/3.13 % (3463116)Instruction limit reached!
% 18.10/3.13 % (3463116)------------------------------
% 18.10/3.13 % (3463116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.10/3.13 % (3463116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463116)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463116)Termination reason: Instruction limit
% 30.42/5.70 % (3463116)Termination phase: Saturation
% 30.42/5.70 % (3463116)Time elapsed: 0.128 s
% 30.42/5.70 % (3463116)Peak memory usage: 14 MB
% 30.42/5.70 % (3463116)Instructions burned: 132 (million)
% 30.42/5.70 % (3463123)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=398182800:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 30.42/5.70 % TRYING [1]
% 30.42/5.70 % TRYING [2]
% 30.42/5.70 % (3463121)Instruction limit reached!
% 30.42/5.70 % (3463121)------------------------------
% 30.42/5.70 % (3463121)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463121)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463121)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463121)Termination reason: Instruction limit
% 30.42/5.70 % (3463121)Termination phase: Saturation
% 30.42/5.70 % (3463121)Time elapsed: 0.175 s
% 30.42/5.70 % (3463121)Peak memory usage: 15 MB
% 30.42/5.70 % (3463121)Instructions burned: 180 (million)
% 30.42/5.70 % (3463125)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3088666206:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 30.42/5.70 % TRYING [3]
% 30.42/5.70 % TRYING [4]
% 30.42/5.70 % TRYING [1]
% 30.42/5.70 % (3463115)Instruction limit reached!
% 30.42/5.70 % (3463115)------------------------------
% 30.42/5.70 % (3463115)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463115)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463115)Termination reason: Instruction limit
% 30.42/5.70 % (3463115)Termination phase: Finite model building constraint generation
% 30.42/5.70 % (3463115)Time elapsed: 0.556 s
% 30.42/5.70 % (3463115)Peak memory usage: 46 MB
% 30.42/5.70 % (3463115)Instructions burned: 714 (million)
% 30.42/5.70 % TRYING [2]
% 30.42/5.70 % (3463127)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1494987700:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 30.42/5.70 % (3463117)Instruction limit reached!
% 30.42/5.70 % (3463117)------------------------------
% 30.42/5.70 % (3463117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463117)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463117)Termination reason: Instruction limit
% 30.42/5.70 % (3463117)Termination phase: Saturation
% 30.42/5.70 % (3463117)Time elapsed: 0.614 s
% 30.42/5.70 % (3463117)Peak memory usage: 23 MB
% 30.42/5.70 % (3463117)Instructions burned: 684 (million)
% 30.42/5.70 % (3463129)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1386971586:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 30.42/5.70 % (3463123)Instruction limit reached!
% 30.42/5.70 % (3463123)------------------------------
% 30.42/5.70 % (3463123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463123)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463123)Termination reason: Instruction limit
% 30.42/5.70 % (3463123)Termination phase: Saturation
% 30.42/5.70 % (3463123)Time elapsed: 0.514 s
% 30.42/5.70 % (3463123)Peak memory usage: 16 MB
% 30.42/5.70 % (3463123)Instructions burned: 477 (million)
% 30.42/5.70 % (3463131)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=3459107930:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 30.42/5.70 % TRYING [3]
% 30.42/5.70 % (3463125)Instruction limit reached!
% 30.42/5.70 % (3463125)------------------------------
% 30.42/5.70 % (3463125)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463125)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463125)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463125)Termination reason: Instruction limit
% 30.42/5.70 % (3463125)Termination phase: Finite model building constraint generation
% 30.42/5.70 % (3463125)Time elapsed: 0.731 s
% 30.42/5.70 % (3463125)Peak memory usage: 32 MB
% 30.42/5.70 % (3463125)Instructions burned: 866 (million)
% 30.42/5.70 % (3463133)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3424626960:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 30.42/5.70 % (3463131)Instruction limit reached!
% 30.42/5.70 % (3463131)------------------------------
% 30.42/5.70 % (3463131)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463131)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463131)Termination reason: Instruction limit
% 30.42/5.70 % (3463131)Termination phase: Saturation
% 30.42/5.70 % (3463131)Time elapsed: 0.679 s
% 30.42/5.70 % (3463131)Peak memory usage: 25 MB
% 30.42/5.70 % (3463131)Instructions burned: 692 (million)
% 30.42/5.70 % (3463135)fmb+10_1_sil=64000:random_seed=2985959400:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 30.42/5.70 % (3463129)Instruction limit reached!
% 30.42/5.70 % (3463129)------------------------------
% 30.42/5.70 % (3463129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463129)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463129)Termination reason: Instruction limit
% 30.42/5.70 % (3463129)Termination phase: Finite model building constraint generation
% 30.42/5.70 % (3463129)Time elapsed: 0.827 s
% 30.42/5.70 % (3463129)Peak memory usage: 94 MB
% 30.42/5.70 % (3463129)Instructions burned: 889 (million)
% 30.42/5.70 % (3463137)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2531427683:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 30.42/5.70 % TRYING [1]
% 30.42/5.70 % TRYING [2]
% 30.42/5.70 % (3463137)Cannot represent all propositional literals internally
% 30.42/5.70 % (3463137)Refutation not found, incomplete strategy
% 30.42/5.70 % (3463137)------------------------------
% 30.42/5.70 % (3463137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463137)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463137)Termination reason: Refutation not found, incomplete strategy
% 30.42/5.70 % (3463137)Time elapsed: 0.178 s
% 30.42/5.70 % (3463137)Peak memory usage: 16 MB
% 30.42/5.70 % (3463137)Instructions burned: 253 (million)
% 30.42/5.70 % (3463137)------------------------------
% 30.42/5.70 % (3463137)------------------------------
% 30.42/5.70 % (3463133)Instruction limit reached!
% 30.42/5.70 % (3463133)------------------------------
% 30.42/5.70 % (3463133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463133)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463133)Termination reason: Instruction limit
% 30.42/5.70 % (3463133)Termination phase: Saturation
% 30.42/5.70 % (3463133)Time elapsed: 0.678 s
% 30.42/5.70 % (3463133)Peak memory usage: 22 MB
% 30.42/5.70 % (3463133)Instructions burned: 880 (million)
% 30.42/5.70 % (3463141)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4182778839:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 30.42/5.70 % (3463127)Instruction limit reached!
% 30.42/5.70 % (3463127)------------------------------
% 30.42/5.70 % (3463127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463127)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463127)Termination reason: Instruction limit
% 30.42/5.70 % (3463127)Termination phase: Saturation
% 30.42/5.70 % (3463127)Time elapsed: 1.164 s
% 30.42/5.70 % (3463127)Peak memory usage: 29 MB
% 30.42/5.70 % (3463127)Instructions burned: 1179 (million)
% 30.42/5.70 % (3463143)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1626179292:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 30.42/5.70 % (3463145)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1410727208:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi)
% 30.42/5.70 % TRYING [3]
% 30.42/5.70 % TRYING [8]
% 30.42/5.70 % (3463141)Instruction limit reached!
% 30.42/5.70 % (3463141)------------------------------
% 30.42/5.70 % (3463141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.70 % (3463141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.70 % (3463141)CaDiCaL version: 2.1.3
% 30.42/5.70 % (3463141)Termination reason: Instruction limit
% 30.42/5.70 % (3463141)Termination phase: Finite model building constraint generation
% 30.42/5.70 % (3463141)Time elapsed: 0.697 s
% 30.42/5.70 % (3463141)Peak memory usage: 56 MB
% 30.42/5.70 % (3463141)Instructions burned: 921 (million)
% 30.42/5.70 % (3463147)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=655611094:i=6324_2973 on theBenchmark for (2973ds/6324Mi)
% 30.42/5.71 % TRYING [5]
% 30.42/5.71 % (3463147)Cannot represent all propositional literals internally
% 30.42/5.71 % (3463147)Refutation not found, incomplete strategy
% 30.42/5.71 % (3463147)------------------------------
% 30.42/5.71 % (3463147)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.71 % (3463147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.71 % (3463147)CaDiCaL version: 2.1.3
% 30.42/5.71 % (3463147)Termination reason: Refutation not found, incomplete strategy
% 30.42/5.71 % (3463147)Time elapsed: 0.255 s
% 30.42/5.71 % (3463147)Peak memory usage: 16 MB
% 30.42/5.71 % (3463147)Instructions burned: 285 (million)
% 30.42/5.71 % (3463147)------------------------------
% 30.42/5.71 % (3463147)------------------------------
% 30.42/5.71 % (3463149)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2358087145:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 30.42/5.71 % (3463145)Instruction limit reached!
% 30.42/5.71 % (3463145)------------------------------
% 30.42/5.71 % (3463145)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.71 % (3463145)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.71 % (3463145)CaDiCaL version: 2.1.3
% 30.42/5.71 % (3463145)Termination reason: Instruction limit
% 30.42/5.71 % (3463145)Termination phase: Saturation
% 30.42/5.71 % (3463145)Time elapsed: 1.397 s
% 30.42/5.71 % (3463145)Peak memory usage: 28 MB
% 30.42/5.71 % (3463145)Instructions burned: 1472 (million)
% 30.42/5.71 % (3463151)ott-2_1_sil=16000:newcnf=on:random_seed=998038701:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2966 on theBenchmark for (2966ds/869Mi)
% 30.42/5.71 % TRYING [4]
% 30.42/5.71 % (3463151)Instruction limit reached!
% 30.42/5.71 % (3463151)------------------------------
% 30.42/5.71 % (3463151)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.71 % (3463151)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.71 % (3463151)CaDiCaL version: 2.1.3
% 30.42/5.71 % (3463151)Termination reason: Instruction limit
% 30.42/5.71 % (3463151)Termination phase: Saturation
% 30.42/5.71 % (3463151)Time elapsed: 0.741 s
% 30.42/5.71 % (3463151)Peak memory usage: 18 MB
% 30.42/5.71 % (3463151)Instructions burned: 870 (million)
% 30.42/5.71 % (3463153)ott+10_1_sil=32000:tgt=ground:random_seed=43138828:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi)
% 30.42/5.71 % (3463149)Cannot represent all propositional literals internally
% 30.42/5.71 % (3463149)Refutation not found, incomplete strategy
% 30.42/5.71 % (3463149)------------------------------
% 30.42/5.71 % (3463149)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.71 % (3463149)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.71 % (3463149)CaDiCaL version: 2.1.3
% 30.42/5.71 % (3463149)Termination reason: Refutation not found, incomplete strategy
% 30.42/5.71 % (3463149)Time elapsed: 1.295 s
% 30.42/5.71 % (3463149)Peak memory usage: 31 MB
% 30.42/5.71 % (3463149)Instructions burned: 1478 (million)
% 30.42/5.71 % (3463149)------------------------------
% 30.42/5.71 % (3463149)------------------------------
% 30.42/5.71 % (3463155)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3468982542:i=54282_2957 on theBenchmark for (2957ds/54282Mi)
% 30.42/5.71 % TRYING [1]
% 30.42/5.71 % TRYING [2]
% 30.42/5.71 % TRYING [3]
% 30.42/5.71 % (3463143) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3463096-3463143"...
% 30.42/5.71 % (3463143)...printing done.
% 30.42/5.71 % (3463143)Refutation found. Thanks to Tanya!
% 30.42/5.71 % SZS status Theorem for theBenchmark
% 30.42/5.71 % SZS output start Proof for theBenchmark
% See solution above
% 30.42/5.71 % (3463143)------------------------------
% 30.42/5.71 % (3463143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.42/5.71 % (3463143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.42/5.71 % (3463143)CaDiCaL version: 2.1.3
% 30.42/5.71 % (3463143)Termination reason: Refutation
% 30.42/5.71 % (3463143)Time elapsed: 3.173 s
% 30.42/5.71 % (3463143)Peak memory usage: 40 MB
% 30.42/5.71 % (3463143)Instructions burned: 3472 (million)
% 30.42/5.71 % (3463096)Success in time 5.209 s
% 30.42/5.71 % Vampire exiting
%------------------------------------------------------------------------------