%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET807+4 : TPTP v9.3.1. Released v3.2.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 12:44:39 PM UTC 2026
% Result : Theorem 6.04s 2.06s
% Output : Refutation 6.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 12
% Syntax : Number of formulae : 78 ( 39 unt; 8 def)
% Number of atoms : 195 ( 14 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 168 ( 51 ~; 48 |; 53 &)
% ( 5 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-2 aty)
% Number of variables : 113 ( 92 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( member(X2,X0)
=> member(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET006+0.ax',subset) ).
fof(f16,axiom,
! [X0,X1] :
( pre_order(X0,X1)
<=> ( ! [X2] :
( member(X2,X1)
=> apply(X0,X2,X2) )
& ! [X2,X3,X4] :
( ( member(X2,X1)
& member(X3,X1)
& member(X4,X1) )
=> ( ( apply(X0,X2,X3)
& apply(X0,X3,X4) )
=> apply(X0,X2,X4) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET006+2.ax',pre_order) ).
fof(f17,axiom,
! [X0,X1] :
( apply(subset_predicate,X0,X1)
<=> subset(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rel_subset) ).
fof(f18,conjecture,
! [X0] : pre_order(subset_predicate,power_set(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thIV18a) ).
fof(f19,negated_conjecture,
~ ! [X0] : pre_order(subset_predicate,power_set(X0)),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f22,plain,
! [X0,X1] :
( pre_order(X0,X1)
<=> ( ! [X2] :
( member(X2,X1)
=> apply(X0,X2,X2) )
& ! [X3,X4,X5] :
( ( member(X3,X1)
& member(X4,X1)
& member(X5,X1) )
=> ( ( apply(X0,X3,X4)
& apply(X0,X4,X5) )
=> apply(X0,X3,X5) ) ) ) ),
inference(rectify,[],[f16]) ).
fof(f23,plain,
! [X0,X1] :
( ( ! [X2] :
( member(X2,X1)
=> apply(X0,X2,X2) )
& ! [X3,X4,X5] :
( ( member(X3,X1)
& member(X4,X1)
& member(X5,X1) )
=> ( ( apply(X0,X3,X4)
& apply(X0,X4,X5) )
=> apply(X0,X3,X5) ) ) )
=> pre_order(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( member(X2,X1)
| ~ member(X2,X0) ) ),
inference(ennf_transformation,[],[f1]) ).
fof(f26,plain,
! [X0,X1] :
( pre_order(X0,X1)
| ? [X2] :
( ~ apply(X0,X2,X2)
& member(X2,X1) )
| ? [X3,X4,X5] :
( ~ apply(X0,X3,X5)
& apply(X0,X3,X4)
& apply(X0,X4,X5)
& member(X3,X1)
& member(X4,X1)
& member(X5,X1) ) ),
inference(ennf_transformation,[],[f23]) ).
fof(f27,plain,
! [X0,X1] :
( pre_order(X0,X1)
| ? [X2] :
( ~ apply(X0,X2,X2)
& member(X2,X1) )
| ? [X3,X4,X5] :
( ~ apply(X0,X3,X5)
& apply(X0,X3,X4)
& apply(X0,X4,X5)
& member(X3,X1)
& member(X4,X1)
& member(X5,X1) ) ),
inference(flattening,[],[f26]) ).
fof(f28,plain,
? [X0] : ~ pre_order(subset_predicate,power_set(X0)),
inference(ennf_transformation,[],[f19]) ).
fof(f29,definition,
! [X0,X1] :
( ? [X3,X4,X5] :
( ~ apply(X0,X3,X5)
& apply(X0,X3,X4)
& apply(X0,X4,X5)
& member(X3,X1)
& member(X4,X1)
& member(X5,X1) )
| ~ sP0(X0,X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f30,plain,
! [X0,X1] :
( pre_order(X0,X1)
| ? [X2] :
( ~ apply(X0,X2,X2)
& member(X2,X1) )
| sP0(X0,X1) ),
inference(definition_folding,[],[f27,f29]) ).
fof(f31,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ member(X2,X1)
& member(X2,X0) ) )
& ( ! [X2] :
( member(X2,X1)
| ~ member(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f24]) ).
fof(f32,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ member(X2,X1)
& member(X2,X0) ) )
& ( ! [X3] :
( member(X3,X1)
| ~ member(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f31]) ).
fof(f33,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ member(sK1(X0,X1),X1)
& member(sK1(X0,X1),X0) ) )
& ( ! [X3] :
( member(X3,X1)
| ~ member(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f32]) ).
fof(f52,plain,
! [X0,X1] :
( ? [X3,X4,X5] :
( ~ apply(X0,X3,X5)
& apply(X0,X3,X4)
& apply(X0,X4,X5)
& member(X3,X1)
& member(X4,X1)
& member(X5,X1) )
| ~ sP0(X0,X1) ),
inference(nnf_transformation,[],[f29]) ).
fof(f53,plain,
! [X0,X1] :
( ? [X2,X3,X4] :
( ~ apply(X0,X2,X4)
& apply(X0,X2,X3)
& apply(X0,X3,X4)
& member(X2,X1)
& member(X3,X1)
& member(X4,X1) )
| ~ sP0(X0,X1) ),
inference(rectify,[],[f52]) ).
fof(f54,plain,
! [X0,X1] :
( ( ~ apply(X0,sK4(X0,X1),sK6(X0,X1))
& apply(X0,sK4(X0,X1),sK5(X0,X1))
& apply(X0,sK5(X0,X1),sK6(X0,X1))
& member(sK4(X0,X1),X1)
& member(sK5(X0,X1),X1)
& member(sK6(X0,X1),X1) )
| ~ sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X2,sK4(X0,X1)),skolemize(X3,sK5(X0,X1)),skolemize(X4,sK6(X0,X1))],[f53]) ).
fof(f55,plain,
! [X0,X1] :
( pre_order(X0,X1)
| ( ~ apply(X0,sK7(X0,X1),sK7(X0,X1))
& member(sK7(X0,X1),X1) )
| sP0(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X2,sK7(X0,X1))],[f30]) ).
fof(f56,plain,
! [X0,X1] :
( ( apply(subset_predicate,X0,X1)
| ~ subset(X0,X1) )
& ( subset(X0,X1)
| ~ apply(subset_predicate,X0,X1) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f57,plain,
~ pre_order(subset_predicate,power_set(sK8)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X0,sK8)],[f28]) ).
fof(f58,plain,
! [X3,X0,X1] :
( ~ subset(X0,X1)
| ~ member(X3,X0)
| member(X3,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f59,plain,
! [X0,X1] :
( member(sK1(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f60,plain,
! [X0,X1] :
( ~ member(sK1(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f33]) ).
fof(f90,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| apply(X0,sK5(X0,X1),sK6(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f91,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| apply(X0,sK4(X0,X1),sK5(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f92,plain,
! [X0,X1] :
( ~ sP0(X0,X1)
| ~ apply(X0,sK4(X0,X1),sK6(X0,X1)) ),
inference(cnf_transformation,[],[f54]) ).
fof(f94,plain,
! [X0,X1] :
( ~ apply(X0,sK7(X0,X1),sK7(X0,X1))
| pre_order(X0,X1)
| sP0(X0,X1) ),
inference(cnf_transformation,[],[f55]) ).
fof(f95,plain,
! [X0,X1] :
( ~ apply(subset_predicate,X0,X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
fof(f96,plain,
! [X0,X1] :
( apply(subset_predicate,X0,X1)
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f56]) ).
fof(f97,plain,
~ pre_order(subset_predicate,power_set(sK8)),
inference(cnf_transformation,[],[f57]) ).
fof(f107,plain,
! [X0] :
( subset(X0,X0)
| subset(X0,X0) ),
inference(resolution,[],[f60,f59]) ).
fof(f109,plain,
! [X0] : subset(X0,X0),
inference(duplicate_literal_removal,[],[f107]) ).
fof(f2931,plain,
! [X0] :
( pre_order(subset_predicate,X0)
| sP0(subset_predicate,X0)
| ~ subset(sK7(subset_predicate,X0),sK7(subset_predicate,X0)) ),
inference(resolution,[],[f94,f96]) ).
fof(f2937,plain,
! [X0] :
( pre_order(subset_predicate,X0)
| sP0(subset_predicate,X0) ),
inference(forward_subsumption_resolution,[],[f2931,f109]) ).
fof(f3718,plain,
sP0(subset_predicate,power_set(sK8)),
inference(resolution,[],[f2937,f97]) ).
fof(f3725,definition,
sF115 = power_set(sK8),
introduced(definition,[new_symbols(definition,[sF115])],[function_definition]) ).
fof(f3726,plain,
power_set(sK8) = sF115,
inference(reorient_equations,[],[f3725]) ).
fof(f4030,plain,
sP0(subset_predicate,sF115),
inference(superposition,[],[f3718,f3726]) ).
fof(f4035,plain,
~ apply(subset_predicate,sK4(subset_predicate,sF115),sK6(subset_predicate,sF115)),
inference(resolution,[],[f4030,f92]) ).
fof(f4036,plain,
apply(subset_predicate,sK4(subset_predicate,sF115),sK5(subset_predicate,sF115)),
inference(resolution,[],[f4030,f91]) ).
fof(f4037,plain,
apply(subset_predicate,sK5(subset_predicate,sF115),sK6(subset_predicate,sF115)),
inference(resolution,[],[f4030,f90]) ).
fof(f4041,definition,
! [X0] : sF125(X0) = sK6(subset_predicate,X0),
introduced(definition,[new_symbols(definition,[sF125])],[function_definition]) ).
fof(f4042,plain,
! [X0] : sK6(subset_predicate,X0) = sF125(X0),
inference(reorient_equations,[],[f4041]) ).
fof(f4043,definition,
! [X0] : sF126(X0) = sK5(subset_predicate,X0),
introduced(definition,[new_symbols(definition,[sF126])],[function_definition]) ).
fof(f4044,plain,
! [X0] : sK5(subset_predicate,X0) = sF126(X0),
inference(reorient_equations,[],[f4043]) ).
fof(f4045,definition,
! [X0] : sF127(X0) = sK4(subset_predicate,X0),
introduced(definition,[new_symbols(definition,[sF127])],[function_definition]) ).
fof(f4046,plain,
! [X0] : sK4(subset_predicate,X0) = sF127(X0),
inference(reorient_equations,[],[f4045]) ).
fof(f4053,plain,
~ subset(sK4(subset_predicate,sF115),sK6(subset_predicate,sF115)),
inference(resolution,[],[f4035,f96]) ).
fof(f4054,plain,
~ subset(sK4(subset_predicate,sF115),sF125(sF115)),
inference(forward_demodulation,[],[f4053,f4042]) ).
fof(f4055,plain,
~ subset(sF127(sF115),sF125(sF115)),
inference(forward_demodulation,[],[f4054,f4046]) ).
fof(f4056,plain,
subset(sK4(subset_predicate,sF115),sK5(subset_predicate,sF115)),
inference(resolution,[],[f4036,f95]) ).
fof(f4059,plain,
subset(sK4(subset_predicate,sF115),sF126(sF115)),
inference(forward_demodulation,[],[f4056,f4044]) ).
fof(f4061,plain,
subset(sF127(sF115),sF126(sF115)),
inference(forward_demodulation,[],[f4059,f4046]) ).
fof(f4065,plain,
! [X0] :
( ~ member(X0,sF127(sF115))
| member(X0,sF126(sF115)) ),
inference(resolution,[],[f4061,f58]) ).
fof(f4066,definition,
sF129 = sF127(sF115),
introduced(definition,[new_symbols(definition,[sF129])],[function_definition]) ).
fof(f4067,plain,
sF127(sF115) = sF129,
inference(reorient_equations,[],[f4066]) ).
fof(f4068,definition,
sF130 = sF126(sF115),
introduced(definition,[new_symbols(definition,[sF130])],[function_definition]) ).
fof(f4069,plain,
sF126(sF115) = sF130,
inference(reorient_equations,[],[f4068]) ).
fof(f4070,plain,
subset(sK5(subset_predicate,sF115),sK6(subset_predicate,sF115)),
inference(resolution,[],[f4037,f95]) ).
fof(f4073,plain,
subset(sK5(subset_predicate,sF115),sF125(sF115)),
inference(forward_demodulation,[],[f4070,f4042]) ).
fof(f4075,plain,
subset(sF126(sF115),sF125(sF115)),
inference(forward_demodulation,[],[f4073,f4044]) ).
fof(f4077,plain,
subset(sF130,sF125(sF115)),
inference(forward_demodulation,[],[f4075,f4069]) ).
fof(f4080,definition,
sF131 = sF125(sF115),
introduced(definition,[new_symbols(definition,[sF131])],[function_definition]) ).
fof(f4081,plain,
sF125(sF115) = sF131,
inference(reorient_equations,[],[f4080]) ).
fof(f4082,plain,
! [X0] :
( ~ member(X0,sF130)
| member(X0,sF125(sF115)) ),
inference(resolution,[],[f4077,f58]) ).
fof(f4083,plain,
! [X0] :
( member(X0,sF131)
| ~ member(X0,sF130) ),
inference(forward_demodulation,[],[f4082,f4081]) ).
fof(f4086,plain,
! [X0] :
( ~ member(sK1(X0,sF131),sF130)
| subset(X0,sF131) ),
inference(resolution,[],[f4083,f60]) ).
fof(f4153,plain,
~ subset(sF129,sF125(sF115)),
inference(superposition,[],[f4055,f4067]) ).
fof(f4154,plain,
~ subset(sF129,sF131),
inference(forward_demodulation,[],[f4153,f4081]) ).
fof(f4967,plain,
! [X0] :
( member(sK1(sF127(sF115),X0),sF126(sF115))
| subset(sF127(sF115),X0) ),
inference(resolution,[],[f4065,f59]) ).
fof(f4980,plain,
! [X0] :
( member(sK1(sF127(sF115),X0),sF130)
| subset(sF127(sF115),X0) ),
inference(forward_demodulation,[],[f4967,f4069]) ).
fof(f4986,plain,
! [X0] :
( member(sK1(sF129,X0),sF130)
| subset(sF127(sF115),X0) ),
inference(forward_demodulation,[],[f4980,f4067]) ).
fof(f4992,plain,
! [X0] :
( member(sK1(sF129,X0),sF130)
| subset(sF129,X0) ),
inference(forward_demodulation,[],[f4986,f4067]) ).
fof(f5487,plain,
( subset(sF129,sF131)
| subset(sF129,sF131) ),
inference(resolution,[],[f4992,f4086]) ).
fof(f5494,plain,
subset(sF129,sF131),
inference(duplicate_literal_removal,[],[f5487]) ).
fof(f5495,plain,
$false,
inference(forward_subsumption_resolution,[],[f5494,f4154]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET807+4 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n018.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Mon Sep 28 02:54:00 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 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
% 6.04/2.06 % (2947546)Will run a generic schedule for satisfiability detection.
% 6.04/2.06 % (2947555)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2971286440:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 6.04/2.06 % (2947552)% WARNING: option uhcvi not known.
% 6.04/2.06 % (2947552)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=948473041:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 6.04/2.06 % (2947551)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=103931747_2999 on theBenchmark for (2999ds/0Mi)
% 6.04/2.06 % (2947553)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3067418872:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 6.04/2.06 % (2947556)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4016029661:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 6.04/2.06 % (2947554)dis+10_1_sil=32000:sp=arity:random_seed=3594531094:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 6.04/2.06 % (2947557)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1173167713:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 6.04/2.06 % TRYING [1]
% 6.04/2.06 % TRYING [2]
% 6.04/2.06 % TRYING [3]
% 6.04/2.06 % TRYING [4]
% 6.04/2.06 % TRYING [5]
% 6.04/2.06 % TRYING [6]
% 6.04/2.06 % (2947555)Instruction limit reached!
% 6.04/2.06 % (2947555)------------------------------
% 6.04/2.06 % (2947555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947555)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947555)Termination reason: Instruction limit
% 6.04/2.06 % (2947555)Termination phase: Saturation
% 6.04/2.06 % (2947555)Time elapsed: 0.038 s
% 6.04/2.06 % (2947555)Peak memory usage: 12 MB
% 6.04/2.06 % (2947555)Instructions burned: 117 (million)
% 6.04/2.06 % (2947565)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=151100350:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.04/2.06 % TRYING [1]
% 6.04/2.06 % TRYING [2]
% 6.04/2.06 % TRYING [7]
% 6.04/2.06 % TRYING [3]
% 6.04/2.06 % TRYING [4]
% 6.04/2.06 % (2947554)Instruction limit reached!
% 6.04/2.06 % (2947554)------------------------------
% 6.04/2.06 % (2947554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947554)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947554)Termination reason: Instruction limit
% 6.04/2.06 % (2947554)Termination phase: Saturation
% 6.04/2.06 % (2947554)Time elapsed: 0.061 s
% 6.04/2.06 % (2947554)Peak memory usage: 12 MB
% 6.04/2.06 % (2947554)Instructions burned: 104 (million)
% 6.04/2.06 % TRYING [5]
% 6.04/2.06 % (2947567)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1282105053:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.04/2.06 % (2947556)Instruction limit reached!
% 6.04/2.06 % (2947556)------------------------------
% 6.04/2.06 % (2947556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947556)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947556)Termination reason: Instruction limit
% 6.04/2.06 % (2947556)Termination phase: Saturation
% 6.04/2.06 % (2947556)Time elapsed: 0.082 s
% 6.04/2.06 % (2947556)Peak memory usage: 14 MB
% 6.04/2.06 % (2947556)Instructions burned: 131 (million)
% 6.04/2.06 % TRYING [6]
% 6.04/2.06 % (2947557)Instruction limit reached!
% 6.04/2.06 % (2947557)------------------------------
% 6.04/2.06 % (2947557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947557)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947557)Termination reason: Instruction limit
% 6.04/2.06 % (2947557)Termination phase: Saturation
% 6.04/2.06 % (2947557)Time elapsed: 0.095 s
% 6.04/2.06 % (2947557)Peak memory usage: 13 MB
% 6.04/2.06 % (2947557)Instructions burned: 159 (million)
% 6.04/2.06 % (2947569)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=808412175:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 6.04/2.06 % TRYING [8]
% 6.04/2.06 % (2947570)ott-21_1_sil=16000:fs=off:random_seed=2730049774:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.04/2.06 % TRYING [7]
% 6.04/2.06 % (2947567)Instruction limit reached!
% 6.04/2.06 % (2947567)------------------------------
% 6.04/2.06 % (2947567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947567)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947567)Termination reason: Instruction limit
% 6.04/2.06 % (2947567)Termination phase: Saturation
% 6.04/2.06 % (2947567)Time elapsed: 0.087 s
% 6.04/2.06 % (2947567)Peak memory usage: 14 MB
% 6.04/2.06 % (2947567)Instructions burned: 131 (million)
% 6.04/2.06 % (2947573)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3928646797:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.04/2.06 % (2947570)Instruction limit reached!
% 6.04/2.06 % (2947570)------------------------------
% 6.04/2.06 % (2947570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947570)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947570)Termination reason: Instruction limit
% 6.04/2.06 % (2947570)Termination phase: Saturation
% 6.04/2.06 % (2947570)Time elapsed: 0.097 s
% 6.04/2.06 % (2947570)Peak memory usage: 14 MB
% 6.04/2.06 % (2947570)Instructions burned: 181 (million)
% 6.04/2.06 % (2947565)Instruction limit reached!
% 6.04/2.06 % (2947565)------------------------------
% 6.04/2.06 % (2947565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947565)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947565)Termination reason: Instruction limit
% 6.04/2.06 % (2947565)Termination phase: Finite model building SAT solving
% 6.04/2.06 % (2947565)Time elapsed: 0.180 s
% 6.04/2.06 % (2947565)Peak memory usage: 26 MB
% 6.04/2.06 % (2947565)Instructions burned: 715 (million)
% 6.04/2.06 % (2947575)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2152895012:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.04/2.06 % TRYING [1]
% 6.04/2.06 % TRYING [2]
% 6.04/2.06 % TRYING [3]
% 6.04/2.06 % (2947576)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1867475501:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 6.04/2.06 % TRYING [4]
% 6.04/2.06 % TRYING [9]
% 6.04/2.06 % TRYING [5]
% 6.04/2.06 % TRYING [6]
% 6.04/2.06 % TRYING [7]
% 6.04/2.06 % (2947569)Instruction limit reached!
% 6.04/2.06 % (2947569)------------------------------
% 6.04/2.06 % (2947569)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947569)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947569)Termination reason: Instruction limit
% 6.04/2.06 % (2947569)Termination phase: Saturation
% 6.04/2.06 % (2947569)Time elapsed: 0.385 s
% 6.04/2.06 % (2947569)Peak memory usage: 18 MB
% 6.04/2.06 % (2947569)Instructions burned: 685 (million)
% 6.04/2.06 % (2947573)Instruction limit reached!
% 6.04/2.06 % (2947573)------------------------------
% 6.04/2.06 % (2947573)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947573)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947573)Termination reason: Instruction limit
% 6.04/2.06 % (2947573)Termination phase: Saturation
% 6.04/2.06 % (2947573)Time elapsed: 0.298 s
% 6.04/2.06 % (2947573)Peak memory usage: 15 MB
% 6.04/2.06 % (2947573)Instructions burned: 478 (million)
% 6.04/2.06 % (2947579)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1368322390:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 6.04/2.06 % (2947580)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=3930698447:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 6.04/2.06 % TRYING [14]
% 6.04/2.06 % (2947575)Instruction limit reached!
% 6.04/2.06 % (2947575)------------------------------
% 6.04/2.06 % (2947575)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947575)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947575)Termination reason: Instruction limit
% 6.04/2.06 % (2947575)Termination phase: Finite model building SAT solving
% 6.04/2.06 % (2947575)Time elapsed: 0.323 s
% 6.04/2.06 % (2947575)Peak memory usage: 20 MB
% 6.04/2.06 % (2947575)Instructions burned: 867 (million)
% 6.04/2.06 % (2947583)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=119735403:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 6.04/2.06 % (2947576)Instruction limit reached!
% 6.04/2.06 % (2947576)------------------------------
% 6.04/2.06 % (2947576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947576)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947576)Termination reason: Instruction limit
% 6.04/2.06 % (2947576)Termination phase: Saturation
% 6.04/2.06 % (2947576)Time elapsed: 0.374 s
% 6.04/2.06 % (2947576)Peak memory usage: 26 MB
% 6.04/2.06 % (2947576)Instructions burned: 1179 (million)
% 6.04/2.06 % (2947585)fmb+10_1_sil=64000:random_seed=3651501847:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 6.04/2.06 % TRYING [1]
% 6.04/2.06 % TRYING [2]
% 6.04/2.06 % TRYING [3]
% 6.04/2.06 % TRYING [4]
% 6.04/2.06 % TRYING [5]
% 6.04/2.06 % TRYING [6]
% 6.04/2.06 % TRYING [7]
% 6.04/2.06 % TRYING [8]
% 6.04/2.06 % TRYING [10]
% 6.04/2.06 % TRYING [9]
% 6.04/2.06 % (2947579)Instruction limit reached!
% 6.04/2.06 % (2947579)------------------------------
% 6.04/2.06 % (2947579)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947579)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947579)Termination reason: Instruction limit
% 6.04/2.06 % (2947579)Termination phase: Finite model building constraint generation
% 6.04/2.06 % (2947579)Time elapsed: 0.379 s
% 6.04/2.06 % (2947579)Peak memory usage: 65 MB
% 6.04/2.06 % (2947579)Instructions burned: 890 (million)
% 6.04/2.06 % (2947580)Instruction limit reached!
% 6.04/2.06 % (2947580)------------------------------
% 6.04/2.06 % (2947580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947580)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947580)Termination reason: Instruction limit
% 6.04/2.06 % (2947580)Termination phase: Saturation
% 6.04/2.06 % (2947580)Time elapsed: 0.404 s
% 6.04/2.06 % (2947580)Peak memory usage: 21 MB
% 6.04/2.06 % (2947580)Instructions burned: 693 (million)
% 6.04/2.06 % (2947587)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4219363163:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 6.04/2.06 % TRYING [20]
% 6.04/2.06 % (2947589)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2521621799:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 6.04/2.06 % TRYING [8]
% 6.04/2.06 % (2947583)Instruction limit reached!
% 6.04/2.06 % (2947583)------------------------------
% 6.04/2.06 % (2947583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947583)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947583)Termination reason: Instruction limit
% 6.04/2.06 % (2947583)Termination phase: Saturation
% 6.04/2.06 % (2947583)Time elapsed: 0.464 s
% 6.04/2.06 % (2947583)Peak memory usage: 21 MB
% 6.04/2.06 % (2947583)Instructions burned: 880 (million)
% 6.04/2.06 % TRYING [10]
% 6.04/2.06 % (2947591)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1580389939:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 6.04/2.06 % TRYING [9]
% 6.04/2.06 % (2947589)Instruction limit reached!
% 6.04/2.06 % (2947589)------------------------------
% 6.04/2.06 % (2947589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947589)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947589)Termination reason: Instruction limit
% 6.04/2.06 % (2947589)Termination phase: Finite model building SAT solving
% 6.04/2.06 % (2947589)Time elapsed: 0.445 s
% 6.04/2.06 % (2947589)Peak memory usage: 34 MB
% 6.04/2.06 % (2947589)Instructions burned: 923 (million)
% 6.04/2.06 % (2947593)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=482312758:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 6.04/2.06 % TRYING [11]
% 6.04/2.06 % (2947593) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2947546-2947593"...
% 6.04/2.06 % (2947593)...printing done.
% 6.04/2.06 % (2947593)Refutation found. Thanks to Tanya!
% 6.04/2.06 % SZS status Theorem for theBenchmark
% 6.04/2.06 % SZS output start Proof for theBenchmark
% See solution above
% 6.04/2.06 % (2947593)------------------------------
% 6.04/2.06 % (2947593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.04/2.06 % (2947593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.04/2.06 % (2947593)CaDiCaL version: 2.1.3
% 6.04/2.06 % (2947593)Termination reason: Refutation
% 6.04/2.06 % (2947593)Time elapsed: 0.174 s
% 6.04/2.06 % (2947593)Peak memory usage: 15 MB
% 6.04/2.06 % (2947593)Instructions burned: 240 (million)
% 6.04/2.06 % (2947546)Success in time 1.633 s
% 6.04/2.06 % Vampire exiting
%------------------------------------------------------------------------------