%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET042-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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:42:46 PM UTC 2026
% Result : Unsatisfiable 208.19s 40.27s
% Output : Refutation 208.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 16
% Syntax : Number of formulae : 66 ( 16 unt; 5 def)
% Number of atoms : 158 ( 14 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 180 ( 88 ~; 87 |; 0 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 6 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 37 ( 0 sgn 37 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( little_set(X0)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',a2) ).
fof(f9,axiom,
! [X0] : singleton_set(X0) = non_ordered_pair(X0,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',singleton_set) ).
fof(f10,axiom,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(singleton_set(X0),non_ordered_pair(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',ordered_pair) ).
fof(f15,axiom,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| X0 != ordered_pair(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate4) ).
fof(f16,plain,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| ordered_pair(X1,X2) != X0 ),
inference(reorient_equations,[],[f15]) ).
fof(f49,axiom,
! [X2,X0,X1] :
( member(X0,cross_product(X1,X2))
| ~ little_set(X0)
| ~ ordered_pair_predicate(X0)
| ~ member(first(X0),X1)
| ~ member(second(X0),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',cross_product4) ).
fof(f167,axiom,
! [X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| first(ordered_pair(X0,X1)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_first) ).
fof(f168,axiom,
! [X0,X1] :
( ~ little_set(X0)
| ~ little_set(X1)
| second(ordered_pair(X0,X1)) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_second) ).
fof(f173,axiom,
! [X0] :
( ~ ordered_pair_predicate(X0)
| little_set(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pairs_are_small2) ).
fof(f189,axiom,
member(a,set_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',member_of_set_a) ).
fof(f190,axiom,
member(b,set_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',member_of_set_b) ).
fof(f191,negated_conjecture,
~ member(ordered_pair(a,b),cross_product(set_a,set_b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_ordered_pair_is_in_cross_product) ).
fof(f193,plain,
! [X0,X1] : ordered_pair(X0,X1) = non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1)),
inference(definition_unfolding,[],[f10,f9]) ).
fof(f196,plain,
! [X2,X0,X1] :
( ordered_pair_predicate(X0)
| ~ little_set(X1)
| ~ little_set(X2)
| non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)) != X0 ),
inference(definition_unfolding,[],[f16,f193]) ).
fof(f222,plain,
! [X0,X1] :
( ~ little_set(X1)
| ~ little_set(X0)
| first(non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1))) = X0 ),
inference(definition_unfolding,[],[f167,f193]) ).
fof(f223,plain,
! [X0,X1] :
( ~ little_set(X1)
| ~ little_set(X0)
| second(non_ordered_pair(non_ordered_pair(X0,X0),non_ordered_pair(X0,X1))) = X1 ),
inference(definition_unfolding,[],[f168,f193]) ).
fof(f230,plain,
~ member(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)),cross_product(set_a,set_b)),
inference(definition_unfolding,[],[f191,f193]) ).
fof(f233,plain,
! [X2,X1] :
( ordered_pair_predicate(non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)))
| ~ little_set(X1)
| ~ little_set(X2) ),
inference(equality_resolution,[],[f196]) ).
fof(f253,plain,
! [X2,X0,X1] :
( member(X0,cross_product(X1,X2))
| ~ ordered_pair_predicate(X0)
| ~ member(first(X0),X1)
| ~ member(second(X0),X2) ),
inference(forward_subsumption_resolution,[],[f49,f173]) ).
fof(f1488,definition,
( spl0_29
<=> ordered_pair_predicate(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f1489,plain,
( ordered_pair_predicate(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f1488]) ).
fof(f1490,plain,
( ~ ordered_pair_predicate(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)))
| spl0_29 ),
inference(avatar_component_clause,[],[f1488]) ).
fof(f3453,plain,
( ~ ordered_pair_predicate(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)))
| ~ member(first(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_a)
| ~ member(second(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_b) ),
inference(resolution,[],[f253,f230]) ).
fof(f3490,plain,
( ~ member(first(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_a)
| ~ member(second(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_b)
| ~ spl0_29 ),
inference(forward_subsumption_resolution,[],[f3453,f1489]) ).
fof(f3492,definition,
( spl0_75
<=> member(second(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_b) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f3494,plain,
( ~ member(second(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_b)
| spl0_75 ),
inference(avatar_component_clause,[],[f3492]) ).
fof(f3496,definition,
( spl0_76
<=> member(first(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_a) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f3498,plain,
( ~ member(first(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b))),set_a)
| spl0_76 ),
inference(avatar_component_clause,[],[f3496]) ).
fof(f3499,plain,
( ~ spl0_75
| ~ spl0_76
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f3490,f1488,f3496,f3492]) ).
fof(f4114,definition,
( spl0_101
<=> little_set(a) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f4115,plain,
( little_set(a)
| ~ spl0_101 ),
inference(avatar_component_clause,[],[f4114]) ).
fof(f4116,plain,
( ~ little_set(a)
| spl0_101 ),
inference(avatar_component_clause,[],[f4114]) ).
fof(f4122,definition,
( spl0_103
<=> little_set(b) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f4123,plain,
( little_set(b)
| ~ spl0_103 ),
inference(avatar_component_clause,[],[f4122]) ).
fof(f4124,plain,
( ~ little_set(b)
| spl0_103 ),
inference(avatar_component_clause,[],[f4122]) ).
fof(f4148,plain,
( ! [X0] : ~ member(a,X0)
| spl0_101 ),
inference(resolution,[],[f4116,f1]) ).
fof(f4155,plain,
( $false
| spl0_101 ),
inference(resolution,[],[f4148,f189]) ).
fof(f4173,plain,
spl0_101,
inference(avatar_contradiction_clause,[],[f4155]) ).
fof(f4189,plain,
( ! [X0] :
( ~ little_set(X0)
| second(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,X0))) = X0 )
| ~ spl0_101 ),
inference(resolution,[],[f4115,f223]) ).
fof(f4191,plain,
( ! [X0] :
( ~ little_set(X0)
| a = first(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,X0))) )
| ~ spl0_101 ),
inference(resolution,[],[f4115,f222]) ).
fof(f4195,plain,
( ! [X0] : ~ member(b,X0)
| spl0_103 ),
inference(resolution,[],[f4124,f1]) ).
fof(f4228,plain,
( $false
| spl0_103 ),
inference(resolution,[],[f4195,f190]) ).
fof(f4246,plain,
spl0_103,
inference(avatar_contradiction_clause,[],[f4228]) ).
fof(f4867,plain,
( b = second(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)))
| ~ spl0_101
| ~ spl0_103 ),
inference(resolution,[],[f4189,f4123]) ).
fof(f5312,plain,
( a = first(non_ordered_pair(non_ordered_pair(a,a),non_ordered_pair(a,b)))
| ~ spl0_101
| ~ spl0_103 ),
inference(resolution,[],[f4191,f4123]) ).
fof(f5674,plain,
( ~ member(a,set_a)
| spl0_76
| ~ spl0_101
| ~ spl0_103 ),
inference(superposition,[],[f3498,f5312]) ).
fof(f5690,plain,
( $false
| spl0_76
| ~ spl0_101
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f5674,f189]) ).
fof(f5691,plain,
( spl0_76
| ~ spl0_101
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f5690]) ).
fof(f5696,plain,
( ~ member(b,set_b)
| spl0_75
| ~ spl0_101
| ~ spl0_103 ),
inference(forward_demodulation,[],[f3494,f4867]) ).
fof(f5698,plain,
( $false
| spl0_75
| ~ spl0_101
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f5696,f190]) ).
fof(f5699,plain,
( spl0_75
| ~ spl0_101
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f5698]) ).
fof(f8051,plain,
( ~ little_set(a)
| ~ little_set(b)
| spl0_29 ),
inference(resolution,[],[f1490,f233]) ).
fof(f8057,plain,
( ~ little_set(b)
| spl0_29
| ~ spl0_101 ),
inference(forward_subsumption_resolution,[],[f8051,f4115]) ).
fof(f8058,plain,
( $false
| spl0_29
| ~ spl0_101
| ~ spl0_103 ),
inference(forward_subsumption_resolution,[],[f8057,f4123]) ).
fof(f8059,plain,
( spl0_29
| ~ spl0_101
| ~ spl0_103 ),
inference(avatar_contradiction_clause,[],[f8058]) ).
cnf(s71,plain,
( ~ spl0_29
| ~ spl0_75
| ~ spl0_76 ),
inference(sat_conversion,[],[f3499]) ).
cnf(s119,plain,
spl0_101,
inference(sat_conversion,[],[f4173]) ).
cnf(s122,plain,
spl0_103,
inference(sat_conversion,[],[f4246]) ).
cnf(s169,plain,
( spl0_76
| ~ spl0_101
| ~ spl0_103 ),
inference(sat_conversion,[],[f5691]) ).
cnf(s170,plain,
( spl0_75
| ~ spl0_101
| ~ spl0_103 ),
inference(sat_conversion,[],[f5699]) ).
cnf(s252,plain,
( spl0_29
| ~ spl0_101
| ~ spl0_103 ),
inference(sat_conversion,[],[f8059]) ).
cnf(s255,plain,
spl0_29,
inference(rat,[],[s252,s122,s119]) ).
cnf(s256,plain,
spl0_75,
inference(rat,[],[s170,s122,s119]) ).
cnf(s257,plain,
spl0_76,
inference(rat,[],[s169,s122,s119]) ).
cnf(s275,plain,
$false,
inference(rat,[],[s71,s257,s256,s255]) ).
fof(f8060,plain,
$false,
inference(avatar_sat_refutation,[],[s275]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET042-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.42 % Computer : n017.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.42 % DateTime : Mon Sep 28 00:16:05 UTC 2026
% 0.14/0.42 % CPUTime :
% 0.14/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.14/0.47 Running first-order model finding
% 0.14/0.47 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
% 14.29/2.76 % (3102487)Will run a generic schedule for satisfiability detection.
% 14.29/2.76 % (3102492)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3752919873_2999 on theBenchmark for (2999ds/0Mi)
% 14.29/2.76 % (3102493)% WARNING: option uhcvi not known.
% 14.29/2.76 % (3102494)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1605240763:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.29/2.76 % (3102495)dis+10_1_sil=32000:sp=arity:random_seed=2416210447:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.29/2.76 % (3102497)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2688002149:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.29/2.76 % (3102498)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2514465174:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.29/2.76 % (3102496)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1423110219:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.29/2.76 % (3102493)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=79636324:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.29/2.76 % TRYING [1]
% 14.29/2.76 % TRYING [2]
% 14.29/2.76 % TRYING [3]
% 14.29/2.76 % (3102495)Instruction limit reached!
% 14.29/2.76 % (3102495)------------------------------
% 14.29/2.76 % (3102495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.76 % (3102495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.76 % (3102495)CaDiCaL version: 2.1.3
% 14.29/2.76 % (3102495)Termination reason: Instruction limit
% 14.29/2.76 % (3102495)Termination phase: Saturation
% 14.29/2.76 % (3102495)Time elapsed: 0.102 s
% 14.29/2.76 % (3102495)Peak memory usage: 12 MB
% 14.29/2.76 % (3102495)Instructions burned: 103 (million)
% 14.29/2.76 % (3102496)Instruction limit reached!
% 14.29/2.76 % (3102496)------------------------------
% 14.29/2.76 % (3102496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.76 % (3102496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.76 % (3102496)CaDiCaL version: 2.1.3
% 14.29/2.76 % (3102496)Termination reason: Instruction limit
% 14.29/2.76 % (3102496)Termination phase: Saturation
% 14.29/2.76 % (3102496)Time elapsed: 0.108 s
% 14.29/2.76 % (3102496)Peak memory usage: 13 MB
% 14.29/2.76 % (3102496)Instructions burned: 116 (million)
% 14.29/2.76 % (3102506)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=693894354:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.29/2.76 % (3102497)Instruction limit reached!
% 14.29/2.76 % (3102497)------------------------------
% 14.29/2.76 % (3102497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.76 % (3102497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.76 % (3102497)CaDiCaL version: 2.1.3
% 14.29/2.76 % (3102497)Termination reason: Instruction limit
% 14.29/2.76 % (3102497)Termination phase: Saturation
% 14.29/2.76 % (3102497)Time elapsed: 0.126 s
% 14.29/2.76 % (3102497)Peak memory usage: 13 MB
% 14.29/2.76 % (3102497)Instructions burned: 132 (million)
% 14.29/2.76 % (3102507)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1865312532:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.29/2.76 % (3102509)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=3381584898:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.29/2.76 % TRYING [1]
% 14.29/2.76 % TRYING [2]
% 14.29/2.76 % (3102498)Instruction limit reached!
% 14.29/2.76 % (3102498)------------------------------
% 14.29/2.76 % (3102498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.76 % (3102498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.29/2.76 % (3102498)CaDiCaL version: 2.1.3
% 14.29/2.76 % (3102498)Termination reason: Instruction limit
% 14.29/2.76 % (3102498)Termination phase: Saturation
% 14.29/2.76 % (3102498)Time elapsed: 0.169 s
% 14.29/2.76 % (3102498)Peak memory usage: 13 MB
% 14.29/2.76 % (3102498)Instructions burned: 160 (million)
% 14.29/2.76 % TRYING [3]
% 14.29/2.76 % (3102512)ott-21_1_sil=16000:fs=off:random_seed=355604095:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 14.29/2.76 % TRYING [4]
% 14.29/2.76 % (3102507)Instruction limit reached!
% 14.29/2.76 % (3102507)------------------------------
% 14.29/2.76 % (3102507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.29/2.76 % (3102507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/8.59 % (3102507)CaDiCaL version: 2.1.3
% 56.96/8.59 % (3102507)Termination reason: Instruction limit
% 56.96/8.59 % (3102507)Termination phase: Saturation
% 56.96/8.59 % (3102507)Time elapsed: 0.141 s
% 56.96/8.59 % (3102507)Peak memory usage: 13 MB
% 56.96/8.59 % (3102507)Instructions burned: 132 (million)
% 56.96/8.59 % (3102514)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1090447627:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 56.96/8.59 % (3102512)Instruction limit reached!
% 56.96/8.59 % (3102512)------------------------------
% 56.96/8.59 % (3102512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.96/8.59 % (3102512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/8.59 % (3102512)CaDiCaL version: 2.1.3
% 56.96/8.59 % (3102512)Termination reason: Instruction limit
% 56.96/8.59 % (3102512)Termination phase: Saturation
% 56.96/8.59 % (3102512)Time elapsed: 0.170 s
% 56.96/8.59 % (3102512)Peak memory usage: 13 MB
% 56.96/8.59 % (3102512)Instructions burned: 180 (million)
% 56.96/8.59 % (3102516)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2097044268:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 56.96/8.59 % TRYING [1]
% 56.96/8.59 % TRYING [2]
% 56.96/8.59 % TRYING [3]
% 56.96/8.59 % (3102506)Instruction limit reached!
% 56.96/8.59 % (3102506)------------------------------
% 56.96/8.59 % (3102506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.96/8.59 % (3102506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/8.59 % (3102506)CaDiCaL version: 2.1.3
% 56.96/8.59 % (3102506)Termination reason: Instruction limit
% 56.96/8.59 % (3102506)Termination phase: Finite model building constraint generation
% 56.96/8.59 % (3102506)Time elapsed: 0.496 s
% 56.96/8.59 % (3102506)Peak memory usage: 39 MB
% 56.96/8.59 % (3102506)Instructions burned: 715 (million)
% 56.96/8.59 % (3102518)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4178913310:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 56.96/8.59 % (3102514)Instruction limit reached!
% 56.96/8.59 % (3102514)------------------------------
% 56.96/8.59 % (3102514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.96/8.59 % (3102514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/8.59 % (3102514)CaDiCaL version: 2.1.3
% 56.96/8.59 % (3102514)Termination reason: Instruction limit
% 56.96/8.59 % (3102514)Termination phase: Saturation
% 56.96/8.59 % (3102514)Time elapsed: 0.483 s
% 56.96/8.59 % (3102514)Peak memory usage: 14 MB
% 56.96/8.59 % (3102514)Instructions burned: 477 (million)
% 56.96/8.59 % (3102509)Instruction limit reached!
% 56.96/8.59 % (3102509)------------------------------
% 56.96/8.59 % (3102509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.96/8.59 % (3102509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/8.59 % (3102509)CaDiCaL version: 2.1.3
% 56.96/8.59 % (3102509)Termination reason: Instruction limit
% 56.96/8.59 % (3102509)Termination phase: Saturation
% 56.96/8.59 % (3102509)Time elapsed: 0.677 s
% 56.96/8.59 % (3102509)Peak memory usage: 19 MB
% 56.96/8.59 % (3102509)Instructions burned: 684 (million)
% 56.96/8.59 % (3102520)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3111883364:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 56.96/8.59 % (3102520)Cannot represent all propositional literals internally
% 56.96/8.59 % (3102520)Refutation not found, incomplete strategy
% 56.96/8.59 % (3102520)------------------------------
% 56.96/8.59 % (3102520)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 56.96/8.59 % (3102520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.96/8.59 % (3102521)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=4155623361: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)
% 56.96/8.59 % (3102520)CaDiCaL version: 2.1.3
% 56.96/8.59 % (3102520)Termination reason: Refutation not found, incomplete strategy
% 56.96/8.59 % (3102520)Time elapsed: 0.030 s
% 56.96/8.59 % (3102520)Peak memory usage: 11 MB
% 56.96/8.59 % (3102520)Instructions burned: 31 (million)
% 56.96/8.59 % (3102520)------------------------------
% 56.96/8.59 % (3102520)------------------------------
% 56.96/8.59 % (3102524)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3388562369:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 144.38/20.85 % (3102516)Instruction limit reached!
% 144.38/20.85 % (3102516)------------------------------
% 144.38/20.85 % (3102516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.38/20.85 % (3102516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.38/20.85 % (3102516)CaDiCaL version: 2.1.3
% 144.38/20.85 % (3102516)Termination reason: Instruction limit
% 144.38/20.85 % (3102516)Termination phase: Finite model building SAT solving
% 144.38/20.85 % (3102516)Time elapsed: 0.643 s
% 144.38/20.85 % (3102516)Peak memory usage: 40 MB
% 144.38/20.85 % (3102516)Instructions burned: 867 (million)
% 144.38/20.85 % (3102526)fmb+10_1_sil=64000:random_seed=869853947:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 144.38/20.85 % TRYING [1]
% 144.38/20.85 % TRYING [2]
% 144.38/20.85 % TRYING [3]
% 144.38/20.85 % (3102521)Instruction limit reached!
% 144.38/20.85 % (3102521)------------------------------
% 144.38/20.85 % (3102521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.38/20.85 % (3102521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.38/20.85 % (3102521)CaDiCaL version: 2.1.3
% 144.38/20.85 % (3102521)Termination reason: Instruction limit
% 144.38/20.85 % (3102521)Termination phase: Saturation
% 144.38/20.85 % (3102521)Time elapsed: 0.683 s
% 144.38/20.85 % (3102521)Peak memory usage: 22 MB
% 144.38/20.85 % (3102521)Instructions burned: 692 (million)
% 144.38/20.85 % (3102528)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3567042702:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 144.38/20.85 % (3102528)Cannot represent all propositional literals internally
% 144.38/20.85 % (3102528)Refutation not found, incomplete strategy
% 144.38/20.85 % (3102528)------------------------------
% 144.38/20.85 % (3102528)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.38/20.85 % (3102528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.38/20.85 % (3102528)CaDiCaL version: 2.1.3
% 144.38/20.85 % (3102528)Termination reason: Refutation not found, incomplete strategy
% 144.38/20.85 % (3102528)Time elapsed: 0.038 s
% 144.38/20.85 % (3102528)Peak memory usage: 11 MB
% 144.38/20.85 % (3102528)Instructions burned: 34 (million)
% 144.38/20.85 % (3102528)------------------------------
% 144.38/20.85 % (3102528)------------------------------
% 144.38/20.85 % (3102530)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2079589223:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 144.38/20.85 % (3102524)Instruction limit reached!
% 144.38/20.85 % (3102524)------------------------------
% 144.38/20.85 % (3102524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.38/20.85 % (3102524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.38/20.85 % (3102524)CaDiCaL version: 2.1.3
% 144.38/20.85 % (3102524)Termination reason: Instruction limit
% 144.38/20.85 % (3102524)Termination phase: Saturation
% 144.38/20.85 % (3102524)Time elapsed: 0.774 s
% 144.38/20.85 % (3102524)Peak memory usage: 19 MB
% 144.38/20.85 % (3102524)Instructions burned: 879 (million)
% 144.38/20.85 % TRYING [8]
% 144.38/20.85 % (3102532)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=771617018:i=5131_2982 on theBenchmark for (2982ds/5131Mi)
% 144.38/20.85 % (3102518)Instruction limit reached!
% 144.38/20.85 % (3102518)------------------------------
% 144.38/20.85 % (3102518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.38/20.85 % (3102518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.38/20.85 % (3102518)CaDiCaL version: 2.1.3
% 144.38/20.85 % (3102518)Termination reason: Instruction limit
% 144.38/20.85 % (3102518)Termination phase: Saturation
% 144.38/20.85 % (3102518)Time elapsed: 1.119 s
% 144.38/20.85 % (3102518)Peak memory usage: 27 MB
% 144.38/20.85 % (3102518)Instructions burned: 1179 (million)
% 144.38/20.85 % (3102534)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3989793445:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 144.38/20.85 % (3102530)Instruction limit reached!
% 144.38/20.85 % (3102530)------------------------------
% 144.38/20.85 % (3102530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 144.38/20.85 % (3102530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.38/20.85 % (3102530)CaDiCaL version: 2.1.3
% 144.38/20.85 % (3102530)Termination reason: Instruction limit
% 144.38/20.85 % (3102530)Termination phase: Finite model building constraint generation
% 144.38/20.85 % (3102530)Time elapsed: 0.535 s
% 144.38/20.85 % (3102530)Peak memory usage: 75 MB
% 144.38/20.85 % (3102530)Instructions burned: 921 (million)
% 144.38/20.85 % (3102536)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3108621:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 275.10/39.23 % (3102536)Cannot represent all propositional literals internally
% 275.10/39.23 % (3102536)Refutation not found, incomplete strategy
% 275.10/39.23 % (3102536)------------------------------
% 275.10/39.23 % (3102536)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 275.10/39.23 % (3102536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.10/39.23 % (3102536)CaDiCaL version: 2.1.3
% 275.10/39.23 % (3102536)Termination reason: Refutation not found, incomplete strategy
% 275.10/39.23 % (3102536)Time elapsed: 0.033 s
% 275.10/39.23 % (3102536)Peak memory usage: 11 MB
% 275.10/39.23 % (3102536)Instructions burned: 35 (million)
% 275.10/39.23 % (3102536)------------------------------
% 275.10/39.23 % (3102536)------------------------------
% 275.10/39.23 % (3102538)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=613958853:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 275.10/39.23 % TRYING [4]
% 275.10/39.23 % (3102538)Cannot represent all propositional literals internally
% 275.10/39.23 % (3102538)Refutation not found, incomplete strategy
% 275.10/39.23 % (3102538)------------------------------
% 275.10/39.23 % (3102538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 275.10/39.23 % (3102538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.10/39.23 % (3102538)CaDiCaL version: 2.1.3
% 275.10/39.23 % (3102538)Termination reason: Refutation not found, incomplete strategy
% 275.10/39.23 % (3102538)Time elapsed: 0.197 s
% 275.10/39.23 % (3102538)Peak memory usage: 13 MB
% 275.10/39.23 % (3102538)Instructions burned: 204 (million)
% 275.10/39.23 % (3102538)------------------------------
% 275.10/39.23 % (3102538)------------------------------
% 275.10/39.23 % (3102540)ott-2_1_sil=16000:newcnf=on:random_seed=3382394542:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2974 on theBenchmark for (2974ds/869Mi)
% 275.10/39.23 % (3102534)Instruction limit reached!
% 275.10/39.23 % (3102534)------------------------------
% 275.10/39.23 % (3102534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 275.10/39.23 % (3102534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.10/39.23 % (3102534)CaDiCaL version: 2.1.3
% 275.10/39.23 % (3102534)Termination reason: Instruction limit
% 275.10/39.23 % (3102534)Termination phase: Saturation
% 275.10/39.23 % (3102534)Time elapsed: 1.442 s
% 275.10/39.23 % (3102534)Peak memory usage: 30 MB
% 275.10/39.23 % (3102534)Instructions burned: 1472 (million)
% 275.10/39.23 % (3102542)ott+10_1_sil=32000:tgt=ground:random_seed=1305433006:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi)
% 275.10/39.23 % (3102540)Instruction limit reached!
% 275.10/39.23 % (3102540)------------------------------
% 275.10/39.23 % (3102540)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 275.10/39.23 % (3102540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.10/39.23 % (3102540)CaDiCaL version: 2.1.3
% 275.10/39.23 % (3102540)Termination reason: Instruction limit
% 275.10/39.23 % (3102540)Termination phase: Saturation
% 275.10/39.23 % (3102540)Time elapsed: 0.847 s
% 275.10/39.23 % (3102540)Peak memory usage: 21 MB
% 275.10/39.23 % (3102540)Instructions burned: 869 (million)
% 275.10/39.23 % (3102544)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1245599122:i=54282_2965 on theBenchmark for (2965ds/54282Mi)
% 275.10/39.23 % TRYING [1]
% 275.10/39.23 % TRYING [2]
% 275.10/39.23 % TRYING [3]
% 275.10/39.23 % TRYING [5]
% 275.10/39.23 % TRYING [4]
% 275.10/39.23 % (3102532)Instruction limit reached!
% 275.10/39.23 % (3102532)------------------------------
% 275.10/39.23 % (3102532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 275.10/39.23 % (3102532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.10/39.23 % (3102532)CaDiCaL version: 2.1.3
% 275.10/39.23 % (3102532)Termination reason: Instruction limit
% 275.10/39.23 % (3102532)Termination phase: Saturation
% 275.10/39.23 % (3102532)Time elapsed: 4.549 s
% 275.10/39.23 % (3102532)Peak memory usage: 50 MB
% 275.10/39.23 % (3102532)Instructions burned: 5132 (million)
% 275.10/39.23 % (3102548)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3426499453:i=3512:aac=none_2937 on theBenchmark for (2937ds/3512Mi)
% 275.10/39.23 % (3102542)Instruction limit reached!
% 275.10/39.23 % (3102542)------------------------------
% 275.10/39.23 % (3102542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 275.10/39.23 % (3102542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.10/39.23 % (3102542)CaDiCaL version: 2.1.3
% 275.10/39.23 % (3102542)Termination reason: Instruction limit
% 208.19/40.27 % (3102542)Termination phase: Saturation
% 208.19/40.27 % (3102542)Time elapsed: 4.787 s
% 208.19/40.27 % (3102542)Peak memory usage: 74 MB
% 208.19/40.27 % (3102542)Instructions burned: 5114 (million)
% 208.19/40.27 % (3102550)dis+21_1_sil=32000:sas=cadical:random_seed=1705893529:i=3773:amm=off_2918 on theBenchmark for (2918ds/3773Mi)
% 208.19/40.27 % (3102548)Instruction limit reached!
% 208.19/40.27 % (3102548)------------------------------
% 208.19/40.27 % (3102548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102548)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102548)Termination reason: Instruction limit
% 208.19/40.27 % (3102548)Termination phase: Saturation
% 208.19/40.27 % (3102548)Time elapsed: 3.162 s
% 208.19/40.27 % (3102548)Peak memory usage: 37 MB
% 208.19/40.27 % (3102548)Instructions burned: 3512 (million)
% 208.19/40.27 % (3102552)ott+11_1_sil=16000:gs=on:random_seed=491168113:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2905 on theBenchmark for (2905ds/2251Mi)
% 208.19/40.27 % TRYING [5]
% 208.19/40.27 % (3102552)Instruction limit reached!
% 208.19/40.27 % (3102552)------------------------------
% 208.19/40.27 % (3102552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102552)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102552)Termination reason: Instruction limit
% 208.19/40.27 % (3102552)Termination phase: Saturation
% 208.19/40.27 % (3102552)Time elapsed: 1.846 s
% 208.19/40.27 % (3102552)Peak memory usage: 15 MB
% 208.19/40.27 % (3102552)Instructions burned: 2251 (million)
% 208.19/40.27 % (3102554)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=109735567:fmbsr=1.6:i=67534_2886 on theBenchmark for (2886ds/67534Mi)
% 208.19/40.27 % (3102550)Instruction limit reached!
% 208.19/40.27 % (3102550)------------------------------
% 208.19/40.27 % (3102550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102550)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102550)Termination reason: Instruction limit
% 208.19/40.27 % (3102550)Termination phase: Saturation
% 208.19/40.27 % (3102550)Time elapsed: 3.469 s
% 208.19/40.27 % (3102550)Peak memory usage: 50 MB
% 208.19/40.27 % (3102550)Instructions burned: 3774 (million)
% 208.19/40.27 % (3102556)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1693391209:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2883 on theBenchmark for (2883ds/4591Mi)
% 208.19/40.27 % (3102556)Instruction limit reached!
% 208.19/40.27 % (3102556)------------------------------
% 208.19/40.27 % (3102556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102556)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102556)Termination reason: Instruction limit
% 208.19/40.27 % (3102556)Termination phase: Saturation
% 208.19/40.27 % (3102556)Time elapsed: 3.650 s
% 208.19/40.27 % (3102556)Peak memory usage: 38 MB
% 208.19/40.27 % (3102556)Instructions burned: 4591 (million)
% 208.19/40.27 % (3102562)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4260600796:i=29340_2846 on theBenchmark for (2846ds/29340Mi)
% 208.19/40.27 % (3102526)Instruction limit reached!
% 208.19/40.27 % (3102526)------------------------------
% 208.19/40.27 % (3102526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102526)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102526)Termination reason: Instruction limit
% 208.19/40.27 % (3102526)Termination phase: Finite model building constraint generation
% 208.19/40.27 % (3102526)Time elapsed: 15.030 s
% 208.19/40.27 % (3102526)Peak memory usage: 336 MB
% 208.19/40.27 % (3102526)Instructions burned: 22062 (million)
% 208.19/40.27 % (3102564)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2681733965:i=5211_2837 on theBenchmark for (2837ds/5211Mi)
% 208.19/40.27 % TRYING [7]
% 208.19/40.27 % (3102564)Instruction limit reached!
% 208.19/40.27 % (3102564)------------------------------
% 208.19/40.27 % (3102564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102564)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102564)Termination reason: Instruction limit
% 208.19/40.27 % (3102564)Termination phase: Saturation
% 208.19/40.27 % (3102564)Time elapsed: 4.119 s
% 208.19/40.27 % (3102564)Peak memory usage: 45 MB
% 208.19/40.27 % (3102564)Instructions burned: 5211 (million)
% 208.19/40.27 % (3102570)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=936993960:i=5497:nm=2_2796 on theBenchmark for (2796ds/5497Mi)
% 208.19/40.27 % (3102570)Cannot represent all propositional literals internally
% 208.19/40.27 % (3102570)Refutation not found, incomplete strategy
% 208.19/40.27 % (3102570)------------------------------
% 208.19/40.27 % (3102570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102570)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102570)Termination reason: Refutation not found, incomplete strategy
% 208.19/40.27 % (3102570)Time elapsed: 0.032 s
% 208.19/40.27 % (3102570)Peak memory usage: 11 MB
% 208.19/40.27 % (3102570)Instructions burned: 35 (million)
% 208.19/40.27 % (3102570)------------------------------
% 208.19/40.27 % (3102570)------------------------------
% 208.19/40.27 % (3102574)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3784522415:fmbsr=2:i=46332_2795 on theBenchmark for (2795ds/46332Mi)
% 208.19/40.27 % (3102574)Cannot represent all propositional literals internally
% 208.19/40.27 % (3102574)Refutation not found, incomplete strategy
% 208.19/40.27 % (3102574)------------------------------
% 208.19/40.27 % (3102574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102574)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102574)Termination reason: Refutation not found, incomplete strategy
% 208.19/40.27 % (3102574)Time elapsed: 0.020 s
% 208.19/40.27 % (3102574)Peak memory usage: 11 MB
% 208.19/40.27 % (3102574)Instructions burned: 37 (million)
% 208.19/40.27 % (3102574)------------------------------
% 208.19/40.27 % (3102574)------------------------------
% 208.19/40.27 % (3102576)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1803090798:i=14071_2795 on theBenchmark for (2795ds/14071Mi)
% 208.19/40.27 % TRYING [12]
% 208.19/40.27 % (3102576)Instruction limit reached!
% 208.19/40.27 % (3102576)------------------------------
% 208.19/40.27 % (3102576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102576)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102576)Termination reason: Instruction limit
% 208.19/40.27 % (3102576)Termination phase: Finite model building constraint generation
% 208.19/40.27 % (3102576)Time elapsed: 9.106 s
% 208.19/40.27 % (3102576)Peak memory usage: 1036 MB
% 208.19/40.27 % (3102576)Instructions burned: 14072 (million)
% 208.19/40.27 % (3102677)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3762515008:i=22565:add=on:rawr=on_2702 on theBenchmark for (2702ds/22565Mi)
% 208.19/40.27 % TRYING [6]
% 208.19/40.27 % (3102544)Instruction limit reached!
% 208.19/40.27 % (3102544)------------------------------
% 208.19/40.27 % (3102544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102544)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102544)Termination reason: Instruction limit
% 208.19/40.27 % (3102544)Termination phase: Finite model building constraint generation
% 208.19/40.27 % (3102544)Time elapsed: 30.307 s
% 208.19/40.27 % (3102544)Peak memory usage: 1592 MB
% 208.19/40.27 % (3102544)Instructions burned: 54282 (million)
% 208.19/40.27 % (3102736)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3435842238:i=8173:av=off_2660 on theBenchmark for (2660ds/8173Mi)
% 208.19/40.27 % (3102562)Instruction limit reached!
% 208.19/40.27 % (3102562)------------------------------
% 208.19/40.27 % (3102562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102562)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102562)Termination reason: Instruction limit
% 208.19/40.27 % (3102562)Termination phase: Saturation
% 208.19/40.27 % (3102562)Time elapsed: 20.570 s
% 208.19/40.27 % (3102562)Peak memory usage: 593 MB
% 208.19/40.27 % (3102562)Instructions burned: 29341 (million)
% 208.19/40.27 % (3102738)dis+10_16:1_sil=16000:random_seed=3732668765:i=9155:fsr=off_2639 on theBenchmark for (2639ds/9155Mi)
% 208.19/40.27 % (3102736)Instruction limit reached!
% 208.19/40.27 % (3102736)------------------------------
% 208.19/40.27 % (3102736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102736)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102736)Termination reason: Instruction limit
% 208.19/40.27 % (3102736)Termination phase: Saturation
% 208.19/40.27 % (3102736)Time elapsed: 4.758 s
% 208.19/40.27 % (3102736)Peak memory usage: 130 MB
% 208.19/40.27 % (3102736)Instructions burned: 8174 (million)
% 208.19/40.27 % (3102740)ott-3_8_sil=64000:random_seed=2997840117:i=20139:bs=on_2612 on theBenchmark for (2612ds/20139Mi)
% 208.19/40.27 % (3102740) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3102487-3102740"...
% 208.19/40.27 % (3102740)...printing done.
% 208.19/40.27 % (3102740)Refutation found. Thanks to Tanya!
% 208.19/40.27 % SZS status Unsatisfiable for theBenchmark
% 208.19/40.27 % SZS output start Proof for theBenchmark
% See solution above
% 208.19/40.27 % (3102740)------------------------------
% 208.19/40.27 % (3102740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 208.19/40.27 % (3102740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 208.19/40.27 % (3102740)CaDiCaL version: 2.1.3
% 208.19/40.27 % (3102740)Termination reason: Refutation
% 208.19/40.27 % (3102740)Time elapsed: 0.497 s
% 208.19/40.27 % (3102740)Peak memory usage: 18 MB
% 208.19/40.27 % (3102740)Instructions burned: 789 (million)
% 208.19/40.27 % (3102487)Success in time 39.785 s
% 208.19/40.27 % Vampire exiting
%------------------------------------------------------------------------------