%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR109+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 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 09:45:21 AM UTC 2026
% Result : Theorem 24.84s 4.84s
% Output : Refutation 24.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 5
% Syntax : Number of formulae : 61 ( 28 unt; 0 def)
% Number of atoms : 151 ( 0 equ)
% Maximal formula atoms : 22 ( 2 avg)
% Number of connectives : 155 ( 65 ~; 42 |; 44 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 14 con; 0-0 aty)
% Number of variables : 56 ( 36 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_26) ).
fof(f27,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+1.ax',kb_SUMO_27) ).
fof(f26088,axiom,
s__subclass(s__Reptile,s__Animal),
file('/export/starexec/sandbox/benchmark/Axioms/CSR003+4.ax',kb_SUMO_9340) ).
fof(f37983,axiom,
( s__subclass(s__Reptile,s__Animal)
=> ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f37984,conjecture,
s__instance(s__Creature50_1,s__Reptile),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_SUMO_MILO) ).
fof(f37985,negated_conjecture,
~ s__instance(s__Creature50_1,s__Reptile),
inference(negated_conjecture,[status(cth)],[f37984]) ).
fof(f37998,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(flattening,[],[f37985]) ).
fof(f38253,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26]) ).
fof(f38254,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f27]) ).
fof(f38255,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f38254]) ).
fof(f48354,plain,
( ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass)
& s__instance(X2,s__SetOrClass)
& s__instance(X3,s__SetOrClass)
& s__instance(X4,s__SetOrClass)
& s__instance(X5,s__SetOrClass)
& s__instance(X6,s__SetOrClass)
& s__instance(X7,s__SetOrClass)
& s__instance(X8,s__SetOrClass)
& s__instance(X9,s__SetOrClass)
& s__subclass(X0,X1)
& s__subclass(X1,X2)
& s__subclass(X2,X3)
& s__subclass(X3,X4)
& s__subclass(X4,X5)
& s__subclass(X5,X6)
& s__subclass(X6,X7)
& s__subclass(X7,X8)
& s__subclass(X8,X9)
& s__subclass(X9,s__Reptile)
& s__instance(s__Creature50_1,X0) )
| ~ s__subclass(s__Reptile,s__Animal) ),
inference(ennf_transformation,[],[f37983]) ).
fof(f48384,plain,
! [X0,X1] :
( s__instance(X1,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f38253]) ).
fof(f48385,plain,
! [X0,X1] :
( s__instance(X0,s__SetOrClass)
| ~ s__subclass(X0,X1) ),
inference(cnf_transformation,[],[f38253]) ).
fof(f48386,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(cnf_transformation,[],[f38255]) ).
fof(f77666,plain,
s__subclass(s__Reptile,s__Animal),
inference(cnf_transformation,[],[f26088]) ).
fof(f89561,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__instance(s__Creature50_1,sK1443) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89562,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1452,s__Reptile) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89563,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1451,sK1452) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89564,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1450,sK1451) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89565,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1449,sK1450) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89566,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1448,sK1449) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89567,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1447,sK1448) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89568,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1446,sK1447) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89569,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1445,sK1446) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89570,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1444,sK1445) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89571,plain,
( ~ s__subclass(s__Reptile,s__Animal)
| s__subclass(sK1443,sK1444) ),
inference(cnf_transformation,[],[f48354]) ).
fof(f89582,plain,
~ s__instance(s__Creature50_1,s__Reptile),
inference(cnf_transformation,[],[f37998]) ).
fof(f90108,plain,
s__instance(s__Creature50_1,sK1443),
inference(forward_subsumption_resolution,[],[f89561,f77666]) ).
fof(f90109,plain,
s__subclass(sK1452,s__Reptile),
inference(forward_subsumption_resolution,[],[f89562,f77666]) ).
fof(f90110,plain,
s__subclass(sK1451,sK1452),
inference(forward_subsumption_resolution,[],[f89563,f77666]) ).
fof(f90111,plain,
s__subclass(sK1450,sK1451),
inference(forward_subsumption_resolution,[],[f89564,f77666]) ).
fof(f90112,plain,
s__subclass(sK1449,sK1450),
inference(forward_subsumption_resolution,[],[f89565,f77666]) ).
fof(f90113,plain,
s__subclass(sK1448,sK1449),
inference(forward_subsumption_resolution,[],[f89566,f77666]) ).
fof(f90114,plain,
s__subclass(sK1447,sK1448),
inference(forward_subsumption_resolution,[],[f89567,f77666]) ).
fof(f90115,plain,
s__subclass(sK1446,sK1447),
inference(forward_subsumption_resolution,[],[f89568,f77666]) ).
fof(f90116,plain,
s__subclass(sK1445,sK1446),
inference(forward_subsumption_resolution,[],[f89569,f77666]) ).
fof(f90117,plain,
s__subclass(sK1444,sK1445),
inference(forward_subsumption_resolution,[],[f89570,f77666]) ).
fof(f90118,plain,
s__subclass(sK1443,sK1444),
inference(forward_subsumption_resolution,[],[f89571,f77666]) ).
fof(f137427,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__SetOrClass)
| ~ s__instance(X2,X0)
| ~ s__subclass(X0,X1)
| s__instance(X2,X1) ),
inference(forward_subsumption_resolution,[],[f48386,f48384]) ).
fof(f137428,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f137427,f48385]) ).
fof(f137515,plain,
! [X0] :
( ~ s__subclass(X0,s__Reptile)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f137428,f89582]) ).
fof(f137540,plain,
~ s__instance(s__Creature50_1,sK1452),
inference(resolution,[],[f137515,f90109]) ).
fof(f137548,plain,
! [X0] :
( ~ s__subclass(X0,sK1452)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f137540,f137428]) ).
fof(f141655,plain,
~ s__instance(s__Creature50_1,sK1451),
inference(resolution,[],[f137548,f90110]) ).
fof(f141664,plain,
! [X0] :
( ~ s__subclass(X0,sK1451)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141655,f137428]) ).
fof(f141681,plain,
~ s__instance(s__Creature50_1,sK1450),
inference(resolution,[],[f141664,f90111]) ).
fof(f141690,plain,
! [X0] :
( ~ s__subclass(X0,sK1450)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141681,f137428]) ).
fof(f141706,plain,
~ s__instance(s__Creature50_1,sK1449),
inference(resolution,[],[f141690,f90112]) ).
fof(f141715,plain,
! [X0] :
( ~ s__subclass(X0,sK1449)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141706,f137428]) ).
fof(f141729,plain,
~ s__instance(s__Creature50_1,sK1448),
inference(resolution,[],[f141715,f90113]) ).
fof(f141738,plain,
! [X0] :
( ~ s__subclass(X0,sK1448)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141729,f137428]) ).
fof(f141752,plain,
~ s__instance(s__Creature50_1,sK1447),
inference(resolution,[],[f141738,f90114]) ).
fof(f141761,plain,
! [X0] :
( ~ s__subclass(X0,sK1447)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141752,f137428]) ).
fof(f141775,plain,
~ s__instance(s__Creature50_1,sK1446),
inference(resolution,[],[f141761,f90115]) ).
fof(f141784,plain,
! [X0] :
( ~ s__subclass(X0,sK1446)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141775,f137428]) ).
fof(f141799,plain,
~ s__instance(s__Creature50_1,sK1445),
inference(resolution,[],[f141784,f90116]) ).
fof(f141808,plain,
! [X0] :
( ~ s__subclass(X0,sK1445)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141799,f137428]) ).
fof(f141826,plain,
~ s__instance(s__Creature50_1,sK1444),
inference(resolution,[],[f141808,f90117]) ).
fof(f141828,plain,
! [X0] :
( ~ s__subclass(X0,sK1444)
| ~ s__instance(s__Creature50_1,X0) ),
inference(resolution,[],[f141826,f137428]) ).
fof(f141838,plain,
~ s__instance(s__Creature50_1,sK1443),
inference(resolution,[],[f141828,f90118]) ).
fof(f141839,plain,
$false,
inference(forward_subsumption_resolution,[],[f141838,f90108]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR109+2 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n018.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 23:02:40 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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
% 23.94/4.14 % (3879722)Will run a generic schedule for satisfiability detection.
% 23.94/4.14 % (3879728)% WARNING: option uhcvi not known.
% 23.94/4.14 % (3879728)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2143151490:i=135531:add=off:rawr=on_2993 on theBenchmark for (2993ds/135531Mi)
% 23.94/4.14 % (3879727)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3911481040_2993 on theBenchmark for (2993ds/0Mi)
% 23.94/4.14 % (3879729)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1358665321:i=88024:add=on:rawr=on_2993 on theBenchmark for (2993ds/88024Mi)
% 23.94/4.14 % (3879730)dis+10_1_sil=32000:sp=arity:random_seed=196087070:i=103:fgj=on_2993 on theBenchmark for (2993ds/103Mi)
% 23.94/4.14 % (3879731)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2098280750:i=116_2993 on theBenchmark for (2993ds/116Mi)
% 23.94/4.14 % (3879732)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=838965830:i=131_2993 on theBenchmark for (2993ds/131Mi)
% 23.94/4.14 % (3879733)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=993602318:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2993 on theBenchmark for (2993ds/159Mi)
% 23.94/4.14 % (3879730)Instruction limit reached!
% 23.94/4.14 % (3879730)------------------------------
% 23.94/4.14 % (3879730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/4.14 % (3879730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/4.14 % (3879730)CaDiCaL version: 2.1.3
% 23.94/4.14 % (3879730)Termination reason: Instruction limit
% 23.94/4.14 % (3879730)Termination phase: Preprocessing 2
% 23.94/4.14 % (3879730)Time elapsed: 0.088 s
% 23.94/4.14 % (3879730)Peak memory usage: 51 MB
% 23.94/4.14 % (3879730)Instructions burned: 103 (million)
% 23.94/4.14 % (3879732)Instruction limit reached!
% 23.94/4.14 % (3879732)------------------------------
% 23.94/4.14 % (3879732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/4.14 % (3879732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/4.14 % (3879732)CaDiCaL version: 2.1.3
% 23.94/4.14 % (3879732)Termination reason: Instruction limit
% 23.94/4.14 % (3879732)Termination phase: Naming
% 23.94/4.14 % (3879732)Time elapsed: 0.094 s
% 23.94/4.14 % (3879732)Peak memory usage: 52 MB
% 23.94/4.14 % (3879732)Instructions burned: 131 (million)
% 23.94/4.14 % (3879731)Instruction limit reached!
% 23.94/4.14 % (3879731)------------------------------
% 23.94/4.14 % (3879731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/4.14 % (3879731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/4.14 % (3879731)CaDiCaL version: 2.1.3
% 23.94/4.14 % (3879731)Termination reason: Instruction limit
% 23.94/4.14 % (3879731)Termination phase: NewCNF
% 23.94/4.14 % (3879731)Time elapsed: 0.101 s
% 23.94/4.14 % (3879731)Peak memory usage: 53 MB
% 23.94/4.14 % (3879731)Instructions burned: 116 (million)
% 23.94/4.14 % (3879741)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3803938367:i=714:nm=2_2992 on theBenchmark for (2992ds/714Mi)
% 23.94/4.14 % (3879733)Instruction limit reached!
% 23.94/4.14 % (3879733)------------------------------
% 23.94/4.14 % (3879733)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/4.14 % (3879733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/4.14 % (3879733)CaDiCaL version: 2.1.3
% 23.94/4.14 % (3879733)Termination reason: Instruction limit
% 23.94/4.14 % (3879733)Termination phase: Preprocessing 3
% 23.94/4.14 % (3879733)Time elapsed: 0.112 s
% 23.94/4.14 % (3879733)Peak memory usage: 52 MB
% 23.94/4.14 % (3879733)Instructions burned: 161 (million)
% 23.94/4.14 % (3879742)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3433713130:i=131:bd=preordered:fsd=on_2992 on theBenchmark for (2992ds/131Mi)
% 23.94/4.14 % (3879743)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=1191074513:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2992 on theBenchmark for (2992ds/684Mi)
% 23.94/4.14 % (3879746)ott-21_1_sil=16000:fs=off:random_seed=1122138389:i=180:av=off:fsr=off_2992 on theBenchmark for (2992ds/180Mi)
% 23.94/4.14 % (3879742)Instruction limit reached!
% 23.94/4.14 % (3879742)------------------------------
% 23.94/4.14 % (3879742)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 23.94/4.14 % (3879742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.94/4.14 % (3879742)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879742)Termination reason: Instruction limit
% 24.84/4.83 % (3879742)Termination phase: Naming
% 24.84/4.83 % (3879742)Time elapsed: 0.093 s
% 24.84/4.83 % (3879742)Peak memory usage: 51 MB
% 24.84/4.83 % (3879742)Instructions burned: 134 (million)
% 24.84/4.83 % (3879749)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=582707456:i=477:bd=all_2991 on theBenchmark for (2991ds/477Mi)
% 24.84/4.83 % (3879746)Instruction limit reached!
% 24.84/4.83 % (3879746)------------------------------
% 24.84/4.83 % (3879746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879746)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879746)Termination reason: Instruction limit
% 24.84/4.83 % (3879746)Termination phase: Preprocessing 3
% 24.84/4.83 % (3879746)Time elapsed: 0.124 s
% 24.84/4.83 % (3879746)Peak memory usage: 52 MB
% 24.84/4.83 % (3879746)Instructions burned: 181 (million)
% 24.84/4.83 % (3879751)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1252467212:fmbsr=1.3:i=865:ins=25_2990 on theBenchmark for (2990ds/865Mi)
% 24.84/4.83 % (3879743)Instruction limit reached!
% 24.84/4.83 % (3879743)------------------------------
% 24.84/4.83 % (3879743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879743)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879743)Termination reason: Instruction limit
% 24.84/4.83 % (3879743)Termination phase: NewCNF
% 24.84/4.83 % (3879743)Time elapsed: 0.323 s
% 24.84/4.83 % (3879743)Peak memory usage: 61 MB
% 24.84/4.83 % (3879743)Instructions burned: 684 (million)
% 24.84/4.83 % (3879753)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1314074553:i=1179_2988 on theBenchmark for (2988ds/1179Mi)
% 24.84/4.83 % (3879741)Instruction limit reached!
% 24.84/4.83 % (3879741)------------------------------
% 24.84/4.83 % (3879741)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879741)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879741)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879741)Termination reason: Instruction limit
% 24.84/4.83 % (3879741)Termination phase: Clausification
% 24.84/4.83 % (3879741)Time elapsed: 0.392 s
% 24.84/4.83 % (3879741)Peak memory usage: 85 MB
% 24.84/4.83 % (3879741)Instructions burned: 715 (million)
% 24.84/4.83 % (3879749)Instruction limit reached!
% 24.84/4.83 % (3879749)------------------------------
% 24.84/4.83 % (3879749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879749)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879749)Termination reason: Instruction limit
% 24.84/4.83 % (3879749)Termination phase: Property scanning
% 24.84/4.83 % (3879749)Time elapsed: 0.272 s
% 24.84/4.83 % (3879749)Peak memory usage: 58 MB
% 24.84/4.83 % (3879749)Instructions burned: 477 (million)
% 24.84/4.83 % (3879755)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2555922252:i=889:ins=1_2988 on theBenchmark for (2988ds/889Mi)
% 24.84/4.83 % (3879756)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=2543500776:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2988 on theBenchmark for (2988ds/692Mi)
% 24.84/4.83 % (3879751)Instruction limit reached!
% 24.84/4.83 % (3879751)------------------------------
% 24.84/4.83 % (3879751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879751)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879751)Termination reason: Instruction limit
% 24.84/4.83 % (3879751)Termination phase: Property scanning
% 24.84/4.83 % (3879751)Time elapsed: 0.455 s
% 24.84/4.83 % (3879751)Peak memory usage: 89 MB
% 24.84/4.83 % (3879751)Instructions burned: 865 (million)
% 24.84/4.83 % (3879759)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=735841974:i=879:kws=inv_precedence:fsr=off_2985 on theBenchmark for (2985ds/879Mi)
% 24.84/4.83 % (3879756)Instruction limit reached!
% 24.84/4.83 % (3879756)------------------------------
% 24.84/4.83 % (3879756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879756)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879756)Termination reason: Instruction limit
% 24.84/4.83 % (3879756)Termination phase: NewCNF
% 24.84/4.83 % (3879756)Time elapsed: 0.313 s
% 24.84/4.83 % (3879756)Peak memory usage: 61 MB
% 24.84/4.83 % (3879756)Instructions burned: 692 (million)
% 24.84/4.83 % (3879761)fmb+10_1_sil=64000:random_seed=969677988:i=22061:nm=2:gsp=on_2984 on theBenchmark for (2984ds/22061Mi)
% 24.84/4.83 % (3879755)Instruction limit reached!
% 24.84/4.83 % (3879755)------------------------------
% 24.84/4.83 % (3879755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879755)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879755)Termination reason: Instruction limit
% 24.84/4.83 % (3879755)Termination phase: Property scanning
% 24.84/4.83 % (3879755)Time elapsed: 0.455 s
% 24.84/4.83 % (3879755)Peak memory usage: 89 MB
% 24.84/4.83 % (3879755)Instructions burned: 891 (million)
% 24.84/4.83 % (3879763)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1377663975:i=9515:nm=5_2983 on theBenchmark for (2983ds/9515Mi)
% 24.84/4.83 % (3879753)Instruction limit reached!
% 24.84/4.83 % (3879753)------------------------------
% 24.84/4.83 % (3879753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879753)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879753)Termination reason: Instruction limit
% 24.84/4.83 % (3879753)Termination phase: Saturation
% 24.84/4.83 % (3879753)Time elapsed: 0.627 s
% 24.84/4.83 % (3879753)Peak memory usage: 72 MB
% 24.84/4.83 % (3879753)Instructions burned: 1180 (million)
% 24.84/4.83 % (3879765)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=829554949:fmbsr=1.7:i=920_2982 on theBenchmark for (2982ds/920Mi)
% 24.84/4.83 % (3879759)Instruction limit reached!
% 24.84/4.83 % (3879759)------------------------------
% 24.84/4.83 % (3879759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879759)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879759)Termination reason: Instruction limit
% 24.84/4.83 % (3879759)Termination phase: Property scanning
% 24.84/4.83 % (3879759)Time elapsed: 0.397 s
% 24.84/4.83 % (3879759)Peak memory usage: 62 MB
% 24.84/4.83 % (3879759)Instructions burned: 880 (million)
% 24.84/4.83 % (3879767)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2493777055:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 24.84/4.83 % (3879765)Instruction limit reached!
% 24.84/4.83 % (3879765)------------------------------
% 24.84/4.83 % (3879765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.83 % (3879765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.83 % (3879765)CaDiCaL version: 2.1.3
% 24.84/4.83 % (3879765)Termination reason: Instruction limit
% 24.84/4.83 % (3879765)Termination phase: Property scanning
% 24.84/4.83 % (3879765)Time elapsed: 0.488 s
% 24.84/4.83 % (3879765)Peak memory usage: 89 MB
% 24.84/4.83 % (3879765)Instructions burned: 921 (million)
% 24.84/4.83 % (3879769)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4129197861:i=1472:ins=7:fdi=8:gsp=on_2977 on theBenchmark for (2977ds/1472Mi)
% 24.84/4.83 % (3879769)Instruction limit reached!
% 24.84/4.83 % (3879769)------------------------------
% 24.84/4.84 % (3879769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.84 % (3879769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.84 % (3879769)CaDiCaL version: 2.1.3
% 24.84/4.84 % (3879769)Termination reason: Instruction limit
% 24.84/4.84 % (3879769)Termination phase: Saturation
% 24.84/4.84 % (3879769)Time elapsed: 0.791 s
% 24.84/4.84 % (3879769)Peak memory usage: 79 MB
% 24.84/4.84 % (3879769)Instructions burned: 1473 (million)
% 24.84/4.84 % (3879771)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2571063715:i=6324_2968 on theBenchmark for (2968ds/6324Mi)
% 24.84/4.84 % Detected minimum model sizes of [447]
% 24.84/4.84 % Detected maximum model sizes of [max]
% 24.84/4.84 % (3879727)Cannot represent all propositional literals internally
% 24.84/4.84 % (3879727)Refutation not found, incomplete strategy
% 24.84/4.84 % (3879727)------------------------------
% 24.84/4.84 % (3879727)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.84 % (3879727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.84 % (3879727)CaDiCaL version: 2.1.3
% 24.84/4.84 % (3879727)Termination reason: Refutation not found, incomplete strategy
% 24.84/4.84 % (3879727)Time elapsed: 3.258 s
% 24.84/4.84 % (3879727)Peak memory usage: 177 MB
% 24.84/4.84 % (3879727)Instructions burned: 6917 (million)
% 24.84/4.84 % (3879727)------------------------------
% 24.84/4.84 % (3879727)------------------------------
% 24.84/4.84 % (3879773)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=921658591:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 24.84/4.84 % Detected minimum model sizes of [447]
% 24.84/4.84 % Detected maximum model sizes of [max]
% 24.84/4.84 % (3879761)Cannot represent all propositional literals internally
% 24.84/4.84 % (3879761)Refutation not found, incomplete strategy
% 24.84/4.84 % (3879761)------------------------------
% 24.84/4.84 % (3879761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.84 % (3879761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.84 % (3879761)CaDiCaL version: 2.1.3
% 24.84/4.84 % (3879761)Termination reason: Refutation not found, incomplete strategy
% 24.84/4.84 % (3879761)Time elapsed: 2.582 s
% 24.84/4.84 % (3879761)Peak memory usage: 153 MB
% 24.84/4.84 % (3879761)Instructions burned: 5782 (million)
% 24.84/4.84 % (3879761)------------------------------
% 24.84/4.84 % (3879761)------------------------------
% 24.84/4.84 % (3879775)ott-2_1_sil=16000:newcnf=on:random_seed=2838457773:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 24.84/4.84 % Detected minimum model sizes of [447]
% 24.84/4.84 % Detected maximum model sizes of [max]
% 24.84/4.84 % (3879763)Cannot represent all propositional literals internally
% 24.84/4.84 % (3879763)Refutation not found, incomplete strategy
% 24.84/4.84 % (3879763)------------------------------
% 24.84/4.84 % (3879763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.84 % (3879763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.84 % (3879763)CaDiCaL version: 2.1.3
% 24.84/4.84 % (3879763)Termination reason: Refutation not found, incomplete strategy
% 24.84/4.84 % (3879763)Time elapsed: 2.684 s
% 24.84/4.84 % (3879763)Peak memory usage: 157 MB
% 24.84/4.84 % (3879763)Instructions burned: 5979 (million)
% 24.84/4.84 % (3879763)------------------------------
% 24.84/4.84 % (3879763)------------------------------
% 24.84/4.84 % (3879777)ott+10_1_sil=32000:tgt=ground:random_seed=2242809305:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 24.84/4.84 % (3879767) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3879722-3879767"...
% 24.84/4.84 % (3879767)...printing done.
% 24.84/4.84 % (3879767)Refutation found. Thanks to Tanya!
% 24.84/4.84 % SZS status Theorem for theBenchmark
% 24.84/4.84 % SZS output start Proof for theBenchmark
% See solution above
% 24.84/4.88 % (3879767)------------------------------
% 24.84/4.88 % (3879767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 24.84/4.88 % (3879767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 24.84/4.88 % (3879767)CaDiCaL version: 2.1.3
% 24.84/4.88 % (3879767)Termination reason: Refutation
% 24.84/4.88 % (3879767)Time elapsed: 2.659 s
% 24.84/4.88 % (3879767)Peak memory usage: 105 MB
% 24.84/4.88 % (3879767)Instructions burned: 5023 (million)
% 24.84/4.88 % (3879722)Success in time 4.616 s
% 24.84/4.88 % Vampire exiting
%------------------------------------------------------------------------------