%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET129-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:40:14 PM UTC 2026
% Result : Unsatisfiable 3.21s 1.39s
% Output : Refutation 4.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 25
% Syntax : Number of formulae : 106 ( 22 unt; 10 def)
% Number of atoms : 237 ( 23 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 236 ( 105 ~; 121 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 11 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 39 ( 0 sgn 39 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] :
( member(X2,X1)
| ~ member(X2,X0)
| ~ subclass(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_members) ).
fof(f4,axiom,
! [X0] : subclass(X0,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',class_elements_are_sets) ).
fof(f8,axiom,
! [X2,X0,X1] :
( ~ member(X0,unordered_pair(X1,X2))
| X0 = X1
| X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member) ).
fof(f12,axiom,
! [X0] : unordered_pair(X0,X0) = singleton(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_set) ).
fof(f21,axiom,
! [X2,X0,X1] :
( ~ member(X0,intersection(X1,X2))
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection1) ).
fof(f23,axiom,
! [X2,X0,X1] :
( member(X0,intersection(X1,X2))
| ~ member(X0,X2)
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',intersection3) ).
fof(f24,axiom,
! [X0,X1] :
( ~ member(X0,complement(X1))
| ~ member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement1) ).
fof(f25,axiom,
! [X0,X1] :
( member(X0,complement(X1))
| ~ member(X0,universal_class)
| member(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement2) ).
fof(f26,axiom,
! [X0,X1] : complement(intersection(complement(X0),complement(X1))) = union(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union) ).
fof(f69,axiom,
! [X0] :
( X0 = null_class
| intersection(X0,regular(X0)) = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',regularity2) ).
fof(f70,plain,
! [X0] :
( null_class = intersection(X0,regular(X0))
| null_class = X0 ),
inference(reorient_equations,[],[f69]) ).
fof(f101,axiom,
! [X0,X1] : union(singleton(X0),X1) = set_builder(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',definition_of_set_builder) ).
fof(f102,negated_conjecture,
member(u,set_builder(x,set_builder(y,set_builder(z,null_class)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_members_of_built_triple_1) ).
fof(f103,negated_conjecture,
u != x,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_members_of_built_triple_2) ).
fof(f104,negated_conjecture,
u != y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_members_of_built_triple_3) ).
fof(f105,negated_conjecture,
u != z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_members_of_built_triple_4) ).
fof(f189,plain,
! [X0,X1] :
( ~ member(X0,null_class)
| member(X0,X1)
| null_class = X1 ),
inference(superposition,[],[f21,f70]) ).
fof(f215,plain,
! [X2,X0,X1] :
( ~ member(X2,union(X0,X1))
| ~ member(X2,intersection(complement(X0),complement(X1))) ),
inference(superposition,[],[f24,f26]) ).
fof(f273,plain,
! [X0,X1] :
( ~ member(X1,singleton(X0))
| X0 = X1
| X0 = X1 ),
inference(superposition,[],[f8,f12]) ).
fof(f274,plain,
! [X0,X1] :
( ~ member(X1,singleton(X0))
| X0 = X1 ),
inference(duplicate_literal_removal,[],[f273]) ).
fof(f671,plain,
! [X2,X0,X1] :
( ~ member(X2,set_builder(X0,X1))
| ~ member(X2,intersection(complement(singleton(X0)),complement(X1))) ),
inference(superposition,[],[f215,f101]) ).
fof(f821,definition,
( spl0_47
<=> null_class = complement(null_class) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f823,plain,
( null_class = complement(null_class)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f821]) ).
fof(f2978,plain,
~ member(u,intersection(complement(singleton(x)),complement(set_builder(y,set_builder(z,null_class))))),
inference(resolution,[],[f671,f102]) ).
fof(f2981,plain,
( ~ member(u,complement(set_builder(y,set_builder(z,null_class))))
| ~ member(u,complement(singleton(x))) ),
inference(resolution,[],[f2978,f23]) ).
fof(f2990,definition,
( spl0_147
<=> member(u,null_class) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f2991,plain,
( member(u,null_class)
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f2990]) ).
fof(f3000,definition,
( spl0_149
<=> member(u,complement(singleton(x))) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f3002,plain,
( ~ member(u,complement(singleton(x)))
| spl0_149 ),
inference(avatar_component_clause,[],[f3000]) ).
fof(f3004,definition,
( spl0_150
<=> member(u,complement(set_builder(y,set_builder(z,null_class)))) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f3006,plain,
( ~ member(u,complement(set_builder(y,set_builder(z,null_class))))
| spl0_150 ),
inference(avatar_component_clause,[],[f3004]) ).
fof(f3007,plain,
( ~ spl0_149
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f2981,f3004,f3000]) ).
fof(f3028,plain,
( ~ member(u,universal_class)
| member(u,set_builder(y,set_builder(z,null_class)))
| spl0_150 ),
inference(resolution,[],[f3006,f25]) ).
fof(f3031,definition,
( spl0_151
<=> member(u,set_builder(y,set_builder(z,null_class))) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f3033,plain,
( member(u,set_builder(y,set_builder(z,null_class)))
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f3031]) ).
fof(f3035,definition,
( spl0_152
<=> member(u,universal_class) ),
introduced(definition,[new_symbols(definition,[spl0_152])],[avatar_definition]) ).
fof(f3036,plain,
( member(u,universal_class)
| ~ spl0_152 ),
inference(avatar_component_clause,[],[f3035]) ).
fof(f3037,plain,
( ~ member(u,universal_class)
| spl0_152 ),
inference(avatar_component_clause,[],[f3035]) ).
fof(f3038,plain,
( spl0_151
| ~ spl0_152
| spl0_150 ),
inference(avatar_split_clause,[],[f3028,f3004,f3035,f3031]) ).
fof(f3043,plain,
( ! [X0] :
( ~ member(u,X0)
| ~ subclass(X0,universal_class) )
| spl0_152 ),
inference(resolution,[],[f3037,f1]) ).
fof(f3044,plain,
( ! [X0] : ~ member(u,X0)
| spl0_152 ),
inference(forward_subsumption_resolution,[],[f3043,f4]) ).
fof(f3047,plain,
( $false
| spl0_152 ),
inference(resolution,[],[f3044,f102]) ).
fof(f3075,plain,
spl0_152,
inference(avatar_contradiction_clause,[],[f3047]) ).
fof(f3079,plain,
( ~ member(u,universal_class)
| member(u,singleton(x))
| spl0_149 ),
inference(resolution,[],[f3002,f25]) ).
fof(f3081,plain,
( member(u,singleton(x))
| spl0_149
| ~ spl0_152 ),
inference(forward_subsumption_resolution,[],[f3079,f3036]) ).
fof(f3092,plain,
( u = x
| spl0_149
| ~ spl0_152 ),
inference(resolution,[],[f3081,f274]) ).
fof(f3093,plain,
( $false
| spl0_149
| ~ spl0_152 ),
inference(forward_subsumption_resolution,[],[f3092,f103]) ).
fof(f3094,plain,
( spl0_149
| ~ spl0_152 ),
inference(avatar_contradiction_clause,[],[f3093]) ).
fof(f3153,plain,
( ~ member(u,intersection(complement(singleton(y)),complement(set_builder(z,null_class))))
| ~ spl0_151 ),
inference(resolution,[],[f3033,f671]) ).
fof(f3533,plain,
( ~ member(u,complement(set_builder(z,null_class)))
| ~ member(u,complement(singleton(y)))
| ~ spl0_151 ),
inference(resolution,[],[f3153,f23]) ).
fof(f3538,definition,
( spl0_173
<=> member(u,complement(singleton(y))) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f3540,plain,
( ~ member(u,complement(singleton(y)))
| spl0_173 ),
inference(avatar_component_clause,[],[f3538]) ).
fof(f3542,definition,
( spl0_174
<=> member(u,complement(set_builder(z,null_class))) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f3544,plain,
( ~ member(u,complement(set_builder(z,null_class)))
| spl0_174 ),
inference(avatar_component_clause,[],[f3542]) ).
fof(f3545,plain,
( ~ spl0_173
| ~ spl0_174
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f3533,f3031,f3542,f3538]) ).
fof(f3566,plain,
( ~ member(u,universal_class)
| member(u,singleton(y))
| spl0_173 ),
inference(resolution,[],[f3540,f25]) ).
fof(f3568,plain,
( member(u,singleton(y))
| ~ spl0_152
| spl0_173 ),
inference(forward_subsumption_resolution,[],[f3566,f3036]) ).
fof(f3570,plain,
( u = y
| ~ spl0_152
| spl0_173 ),
inference(resolution,[],[f3568,f274]) ).
fof(f3571,plain,
( $false
| ~ spl0_152
| spl0_173 ),
inference(forward_subsumption_resolution,[],[f3570,f104]) ).
fof(f3572,plain,
( ~ spl0_152
| spl0_173 ),
inference(avatar_contradiction_clause,[],[f3571]) ).
fof(f3840,plain,
( ~ member(u,universal_class)
| member(u,set_builder(z,null_class))
| spl0_174 ),
inference(resolution,[],[f3544,f25]) ).
fof(f3842,plain,
( member(u,set_builder(z,null_class))
| ~ spl0_152
| spl0_174 ),
inference(forward_subsumption_resolution,[],[f3840,f3036]) ).
fof(f3848,plain,
( ~ member(u,intersection(complement(singleton(z)),complement(null_class)))
| ~ spl0_152
| spl0_174 ),
inference(resolution,[],[f3842,f671]) ).
fof(f3897,plain,
( ~ member(u,complement(null_class))
| ~ member(u,complement(singleton(z)))
| ~ spl0_152
| spl0_174 ),
inference(resolution,[],[f3848,f23]) ).
fof(f3902,definition,
( spl0_223
<=> member(u,complement(singleton(z))) ),
introduced(definition,[new_symbols(definition,[spl0_223])],[avatar_definition]) ).
fof(f3904,plain,
( ~ member(u,complement(singleton(z)))
| spl0_223 ),
inference(avatar_component_clause,[],[f3902]) ).
fof(f3906,definition,
( spl0_224
<=> member(u,complement(null_class)) ),
introduced(definition,[new_symbols(definition,[spl0_224])],[avatar_definition]) ).
fof(f3908,plain,
( ~ member(u,complement(null_class))
| spl0_224 ),
inference(avatar_component_clause,[],[f3906]) ).
fof(f3909,plain,
( ~ spl0_223
| ~ spl0_224
| ~ spl0_152
| spl0_174 ),
inference(avatar_split_clause,[],[f3897,f3542,f3035,f3906,f3902]) ).
fof(f3911,plain,
( ~ member(u,universal_class)
| member(u,singleton(z))
| spl0_223 ),
inference(resolution,[],[f3904,f25]) ).
fof(f3913,plain,
( member(u,singleton(z))
| ~ spl0_152
| spl0_223 ),
inference(forward_subsumption_resolution,[],[f3911,f3036]) ).
fof(f3916,plain,
( u = z
| ~ spl0_152
| spl0_223 ),
inference(resolution,[],[f3913,f274]) ).
fof(f3917,plain,
( $false
| ~ spl0_152
| spl0_223 ),
inference(forward_subsumption_resolution,[],[f3916,f105]) ).
fof(f3918,plain,
( ~ spl0_152
| spl0_223 ),
inference(avatar_contradiction_clause,[],[f3917]) ).
fof(f3919,plain,
( ~ member(u,universal_class)
| member(u,null_class)
| spl0_224 ),
inference(resolution,[],[f3908,f25]) ).
fof(f3921,plain,
( member(u,null_class)
| ~ spl0_152
| spl0_224 ),
inference(forward_subsumption_resolution,[],[f3919,f3036]) ).
fof(f3950,plain,
( spl0_147
| ~ spl0_152
| spl0_224 ),
inference(avatar_split_clause,[],[f3921,f3906,f3035,f2990]) ).
fof(f3952,plain,
( ! [X0] :
( member(u,X0)
| null_class = X0 )
| ~ spl0_147 ),
inference(resolution,[],[f2991,f189]) ).
fof(f3983,plain,
( null_class = complement(null_class)
| ~ spl0_147
| spl0_224 ),
inference(resolution,[],[f3952,f3908]) ).
fof(f4030,plain,
( spl0_47
| ~ spl0_147
| spl0_224 ),
inference(avatar_split_clause,[],[f3983,f3906,f2990,f821]) ).
fof(f4031,plain,
( ~ member(u,null_class)
| ~ spl0_47
| spl0_224 ),
inference(superposition,[],[f3908,f823]) ).
fof(f4074,plain,
( $false
| ~ spl0_47
| ~ spl0_147
| spl0_224 ),
inference(forward_subsumption_resolution,[],[f4031,f2991]) ).
fof(f4075,plain,
( ~ spl0_47
| ~ spl0_147
| spl0_224 ),
inference(avatar_contradiction_clause,[],[f4074]) ).
cnf(s120,plain,
( ~ spl0_149
| ~ spl0_150 ),
inference(sat_conversion,[],[f3007]) ).
cnf(s121,plain,
( spl0_150
| spl0_151
| ~ spl0_152 ),
inference(sat_conversion,[],[f3038]) ).
cnf(s122,plain,
spl0_152,
inference(sat_conversion,[],[f3075]) ).
cnf(s123,plain,
( spl0_149
| ~ spl0_152 ),
inference(sat_conversion,[],[f3094]) ).
cnf(s152,plain,
( ~ spl0_151
| ~ spl0_173
| ~ spl0_174 ),
inference(sat_conversion,[],[f3545]) ).
cnf(s154,plain,
( ~ spl0_152
| spl0_173 ),
inference(sat_conversion,[],[f3572]) ).
cnf(s188,plain,
( ~ spl0_152
| spl0_174
| ~ spl0_223
| ~ spl0_224 ),
inference(sat_conversion,[],[f3909]) ).
cnf(s189,plain,
( ~ spl0_152
| spl0_223 ),
inference(sat_conversion,[],[f3918]) ).
cnf(s198,plain,
( spl0_147
| ~ spl0_152
| spl0_224 ),
inference(sat_conversion,[],[f3950]) ).
cnf(s211,plain,
( spl0_47
| ~ spl0_147
| spl0_224 ),
inference(sat_conversion,[],[f4030]) ).
cnf(s213,plain,
( ~ spl0_47
| ~ spl0_147
| spl0_224 ),
inference(sat_conversion,[],[f4075]) ).
cnf(s214,plain,
spl0_223,
inference(rat,[],[s189,s122]) ).
cnf(s215,plain,
spl0_173,
inference(rat,[],[s154,s122]) ).
cnf(s216,plain,
spl0_149,
inference(rat,[],[s123,s122]) ).
cnf(s217,plain,
( spl0_150
| spl0_151 ),
inference(rat,[],[s121,s122]) ).
cnf(s218,plain,
~ spl0_150,
inference(rat,[],[s120,s216]) ).
cnf(s219,plain,
spl0_151,
inference(rat,[],[s217,s218]) ).
cnf(s220,plain,
~ spl0_174,
inference(rat,[],[s152,s215,s219]) ).
cnf(s221,plain,
~ spl0_224,
inference(rat,[],[s188,s122,s214,s220]) ).
cnf(s222,plain,
spl0_147,
inference(rat,[],[s198,s122,s221]) ).
cnf(s223,plain,
~ spl0_47,
inference(rat,[],[s213,s221,s222]) ).
cnf(s224,plain,
$false,
inference(rat,[],[s211,s221,s222,s223]) ).
fof(f4076,plain,
$false,
inference(avatar_sat_refutation,[],[s224]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET129-6 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n018.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 00:53:40 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.43 Running first-order theorem proving
% 0.12/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.21/1.39 % (2894861)Input is clausal, will run a generic CNF schedule.
% 3.21/1.39 % (2894870)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1651974819:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.21/1.39 % (2894866)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1578445890:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.21/1.39 % (2894867)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1222525221:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.21/1.39 % (2894869)lrs+10_1_sil=8000:sp=occurrence:random_seed=3208188368:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.21/1.39 % (2894868)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2754608147:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.21/1.39 % (2894871)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3370881504:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.21/1.39 % (2894869)Refutation not found, incomplete strategy
% 3.21/1.39 % (2894869)------------------------------
% 3.21/1.39 % (2894869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.39 % (2894869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.39 % (2894869)CaDiCaL version: 2.1.3
% 3.21/1.39 % (2894869)Termination reason: Refutation not found, incomplete strategy
% 3.21/1.39 % (2894869)Time elapsed: 0.003 s
% 3.21/1.39 % (2894869)Peak memory usage: 88 MB
% 3.21/1.39 % (2894869)Instructions burned: 2 (million)
% 3.21/1.39 % (2894872)dis-21_1_sil=8000:lcm=predicate:random_seed=3118482132:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.21/1.39 % (2894870)Instruction limit reached!
% 3.21/1.39 % (2894870)------------------------------
% 3.21/1.39 % (2894870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.39 % (2894870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.39 % (2894870)CaDiCaL version: 2.1.3
% 3.21/1.39 % (2894870)Termination reason: Instruction limit
% 3.21/1.39 % (2894870)Termination phase: Saturation
% 3.21/1.39 % (2894870)Time elapsed: 0.038 s
% 3.21/1.39 % (2894870)Peak memory usage: 89 MB
% 3.21/1.39 % (2894870)Instructions burned: 117 (million)
% 3.21/1.39 % (2894872)Instruction limit reached!
% 3.21/1.39 % (2894872)------------------------------
% 3.21/1.39 % (2894872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.39 % (2894872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.39 % (2894872)CaDiCaL version: 2.1.3
% 3.21/1.39 % (2894872)Termination reason: Instruction limit
% 3.21/1.39 % (2894872)Termination phase: Saturation
% 3.21/1.39 % (2894872)Time elapsed: 0.065 s
% 3.21/1.39 % (2894872)Peak memory usage: 89 MB
% 3.21/1.39 % (2894872)Instructions burned: 118 (million)
% 3.21/1.39 % (2894880)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=481494220:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 3.21/1.39 % (2894880)Refutation not found, incomplete strategy
% 3.21/1.39 % (2894880)------------------------------
% 3.21/1.39 % (2894880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.39 % (2894880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.39 % (2894880)CaDiCaL version: 2.1.3
% 3.21/1.39 % (2894880)Termination reason: Refutation not found, incomplete strategy
% 3.21/1.39 % (2894880)Time elapsed: 0.002 s
% 3.21/1.39 % (2894880)Peak memory usage: 88 MB
% 3.21/1.39 % (2894880)Instructions burned: 3 (million)
% 3.21/1.39 % (2894871)First to succeed.
% 3.21/1.39 % (2894871)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2894861"
% 3.21/1.39 % (2894881)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3835181194:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 3.21/1.39 % (2894880)------------------------------
% 3.21/1.39 % (2894880)------------------------------
% 3.21/1.39 % (2894869)------------------------------
% 3.21/1.39 % (2894869)------------------------------
% 3.21/1.39 % (2894881)Instruction limit reached!
% 3.21/1.39 % (2894881)------------------------------
% 3.21/1.39 % (2894881)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.39 % (2894881)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.39 % (2894881)CaDiCaL version: 2.1.3
% 3.21/1.39 % (2894881)Termination reason: Instruction limit
% 3.21/1.39 % (2894881)Termination phase: Saturation
% 3.21/1.39 % (2894881)Time elapsed: 0.093 s
% 3.21/1.39 % (2894881)Peak memory usage: 90 MB
% 3.21/1.39 % (2894881)Instructions burned: 189 (million)
% 3.21/1.39 % (2894884)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=216777332:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 3.21/1.39 % (2894884)Refutation not found, incomplete strategy
% 3.21/1.39 % (2894884)------------------------------
% 3.21/1.39 % (2894884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.21/1.39 % (2894884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/1.39 % (2894884)CaDiCaL version: 2.1.3
% 3.21/1.39 % (2894884)Termination reason: Refutation not found, incomplete strategy
% 3.21/1.39 % (2894884)Time elapsed: 0.002 s
% 3.21/1.39 % (2894884)Peak memory usage: 87 MB
% 3.21/1.39 % (2894884)Instructions burned: 3 (million)
% 3.21/1.39 % (2894871)Refutation found. Thanks to Tanya!
% 3.21/1.39 % SZS status Unsatisfiable for theBenchmark
% 3.21/1.39 % SZS output start Proof for theBenchmark
% See solution above
% 4.18/1.49 % (2894871)------------------------------
% 4.18/1.49 % (2894871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.49 % (2894871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.49 % (2894871)CaDiCaL version: 2.1.3
% 4.18/1.49 % (2894871)Termination reason: Refutation
% 4.18/1.49 % (2894871)Time elapsed: 0.120 s
% 4.18/1.49 % (2894871)Peak memory usage: 91 MB
% 4.18/1.49 % (2894871)Instructions burned: 160 (million)
% 4.18/1.49 % (2894871)------------------------------
% 4.18/1.49 % (2894871)------------------------------
% 4.18/1.49 % (2894861)Success in time 0.524 s
% 4.18/1.49 % Vampire exiting
%------------------------------------------------------------------------------