%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM925+7 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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:26:11 PM UTC 2026
% Result : Theorem 5.26s 1.31s
% Output : Refutation 5.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 30
% Syntax : Number of formulae : 115 ( 85 unt; 13 def)
% Number of atoms : 159 ( 99 equ)
% Maximal formula atoms : 7 ( 1 avg)
% Number of connectives : 88 ( 44 ~; 31 |; 4 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 3 prp; 0-2 aty)
% Number of functors : 34 ( 34 usr; 17 con; 0-4 aty)
% Number of variables : 62 ( 0 sgn 62 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f58,axiom,
! [X0] : ti(int,succ(X0)) = succ(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_Int_Osucc_res) ).
fof(f98,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_n1pos) ).
fof(f130,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_rel__simps_I2_J) ).
fof(f145,axiom,
! [X0,X1] : plus_plus(int,X0,X1) = plus_plus(int,X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_zadd__commute) ).
fof(f171,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_Pls__def) ).
fof(f176,axiom,
! [X0] : bit0(X0) = plus_plus(int,X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_Bit0__def) ).
fof(f190,axiom,
! [X0] : bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_Bit1__def) ).
fof(f263,axiom,
! [X0] :
( ring_11004092258visors(X0)
=> ! [X1,X2] :
( ti(X0,X2) != zero_zero(X0)
=> hAPP(nat,X0,power_power(X0,X2),X1) != zero_zero(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_field__power__not__zero) ).
fof(f420,axiom,
! [X0] :
( group_add(X0)
=> ! [X1] : minus_minus(X0,X1,X1) = zero_zero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_322_diff__self) ).
fof(f617,axiom,
! [X0] : succ(X0) = plus_plus(int,X0,one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_519_succ__def) ).
fof(f874,axiom,
succ(min) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_776_succ__Min) ).
fof(f875,axiom,
! [X0] : minus_minus(int,X0,min) = succ(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_777_diff__bin__simps_I2_J) ).
fof(f914,axiom,
! [X0] : hBOOL(hAPP(int,bool,zcong(X0,zero_zero(int)),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_816_zcong__id) ).
fof(f975,axiom,
! [X0,X1] :
( ( hBOOL(hAPP(int,bool,zcong(X0,zero_zero(int)),X1))
=> legendre(X0,X1) = zero_zero(int) )
& ( ~ hBOOL(hAPP(int,bool,zcong(X0,zero_zero(int)),X1))
=> ( ( hBOOL(hAPP(int,bool,quadRes(X1),X0))
=> legendre(X0,X1) = one_one(int) )
& ( ~ hBOOL(hAPP(int,bool,quadRes(X1),X0))
=> legendre(X0,X1) = number_number_of(int,min) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_877_Legendre__def) ).
fof(f1104,axiom,
ring_11004092258visors(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring__1__no__zero__divisors) ).
fof(f1136,axiom,
group_add(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Groups_Ogroup__add) ).
fof(f1251,conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1252,negated_conjecture,
~ ( hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) ),
inference(negated_conjecture,[status(cth)],[f1251]) ).
fof(f1260,plain,
zero_zero(int) = hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))),
inference(flattening,[],[f1252]) ).
fof(f1404,plain,
! [X0] :
( ! [X1,X2] :
( hAPP(nat,X0,power_power(X0,X2),X1) != zero_zero(X0)
| zero_zero(X0) = ti(X0,X2) )
| ~ ring_11004092258visors(X0) ),
inference(ennf_transformation,[],[f263]) ).
fof(f1585,plain,
! [X0] :
( ! [X1] : minus_minus(X0,X1,X1) = zero_zero(X0)
| ~ group_add(X0) ),
inference(ennf_transformation,[],[f420]) ).
fof(f2096,plain,
! [X0,X1] :
( ( legendre(X0,X1) = zero_zero(int)
| ~ hBOOL(hAPP(int,bool,zcong(X0,zero_zero(int)),X1)) )
& ( ( ( legendre(X0,X1) = one_one(int)
| ~ hBOOL(hAPP(int,bool,quadRes(X1),X0)) )
& ( legendre(X0,X1) = number_number_of(int,min)
| hBOOL(hAPP(int,bool,quadRes(X1),X0)) ) )
| hBOOL(hAPP(int,bool,zcong(X0,zero_zero(int)),X1)) ) ),
inference(ennf_transformation,[],[f975]) ).
fof(f2674,plain,
! [X0] : succ(X0) = ti(int,succ(X0)),
inference(cnf_transformation,[],[f58]) ).
fof(f2715,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(cnf_transformation,[],[f98]) ).
fof(f2756,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(cnf_transformation,[],[f130]) ).
fof(f2780,plain,
! [X0,X1] : plus_plus(int,X0,X1) = plus_plus(int,X1,X0),
inference(cnf_transformation,[],[f145]) ).
fof(f2824,plain,
pls = zero_zero(int),
inference(cnf_transformation,[],[f171]) ).
fof(f2829,plain,
! [X0] : bit0(X0) = plus_plus(int,X0,X0),
inference(cnf_transformation,[],[f176]) ).
fof(f2845,plain,
! [X0] : bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
inference(cnf_transformation,[],[f190]) ).
fof(f2960,plain,
! [X2,X0,X1] :
( zero_zero(X0) != hAPP(nat,X0,power_power(X0,X2),X1)
| zero_zero(X0) = ti(X0,X2)
| ~ ring_11004092258visors(X0) ),
inference(cnf_transformation,[],[f1404]) ).
fof(f3183,plain,
! [X0,X1] :
( ~ group_add(X0)
| zero_zero(X0) = minus_minus(X0,X1,X1) ),
inference(cnf_transformation,[],[f1585]) ).
fof(f3478,plain,
! [X0] : succ(X0) = plus_plus(int,X0,one_one(int)),
inference(cnf_transformation,[],[f617]) ).
fof(f3826,plain,
pls = succ(min),
inference(cnf_transformation,[],[f874]) ).
fof(f3827,plain,
! [X0] : succ(X0) = minus_minus(int,X0,min),
inference(cnf_transformation,[],[f875]) ).
fof(f3884,plain,
! [X0] : hBOOL(hAPP(int,bool,zcong(X0,zero_zero(int)),X0)),
inference(cnf_transformation,[],[f914]) ).
fof(f3984,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,zcong(X0,zero_zero(int)),X1))
| legendre(X0,X1) = zero_zero(int) ),
inference(cnf_transformation,[],[f2096]) ).
fof(f4191,plain,
ring_11004092258visors(int),
inference(cnf_transformation,[],[f1104]) ).
fof(f4223,plain,
group_add(int),
inference(cnf_transformation,[],[f1136]) ).
fof(f4338,plain,
zero_zero(int) = hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))),
inference(cnf_transformation,[],[f1260]) ).
fof(f4344,plain,
! [X0] : plus_plus(int,X0,one_one(int)) = ti(int,plus_plus(int,X0,one_one(int))),
inference(definition_unfolding,[],[f2674,f3478,f3478]) ).
fof(f4555,plain,
pls = plus_plus(int,min,one_one(int)),
inference(definition_unfolding,[],[f3826,f3478]) ).
fof(f4556,plain,
! [X0] : plus_plus(int,X0,one_one(int)) = minus_minus(int,X0,min),
inference(definition_unfolding,[],[f3827,f3478]) ).
fof(f4600,plain,
zero_zero(int) = hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))),
inference(definition_unfolding,[],[f4338,f2829,f2845]) ).
fof(f4703,definition,
sF45 = zero_zero(int),
introduced(definition,[new_symbols(definition,[sF45])],[function_definition]) ).
fof(f4704,plain,
zero_zero(int) = sF45,
inference(reorient_equations,[],[f4703]) ).
fof(f4705,definition,
sF46 = one_one(int),
introduced(definition,[new_symbols(definition,[sF46])],[function_definition]) ).
fof(f4706,plain,
one_one(int) = sF46,
inference(reorient_equations,[],[f4705]) ).
fof(f4707,definition,
sF47 = semiring_1_of_nat(int),
introduced(definition,[new_symbols(definition,[sF47])],[function_definition]) ).
fof(f4708,plain,
semiring_1_of_nat(int) = sF47,
inference(reorient_equations,[],[f4707]) ).
fof(f4709,definition,
sF48 = hAPP(nat,int,sF47,n),
introduced(definition,[new_symbols(definition,[sF48])],[function_definition]) ).
fof(f4710,plain,
hAPP(nat,int,sF47,n) = sF48,
inference(reorient_equations,[],[f4709]) ).
fof(f4711,definition,
sF49 = plus_plus(int,sF46,sF48),
introduced(definition,[new_symbols(definition,[sF49])],[function_definition]) ).
fof(f4712,plain,
plus_plus(int,sF46,sF48) = sF49,
inference(reorient_equations,[],[f4711]) ).
fof(f4713,definition,
sF50 = power_power(int,sF49),
introduced(definition,[new_symbols(definition,[sF50])],[function_definition]) ).
fof(f4714,plain,
power_power(int,sF49) = sF50,
inference(reorient_equations,[],[f4713]) ).
fof(f4715,definition,
sF51 = plus_plus(int,sF46,pls),
introduced(definition,[new_symbols(definition,[sF51])],[function_definition]) ).
fof(f4716,plain,
plus_plus(int,sF46,pls) = sF51,
inference(reorient_equations,[],[f4715]) ).
fof(f4717,definition,
sF52 = plus_plus(int,sF51,pls),
introduced(definition,[new_symbols(definition,[sF52])],[function_definition]) ).
fof(f4718,plain,
plus_plus(int,sF51,pls) = sF52,
inference(reorient_equations,[],[f4717]) ).
fof(f4719,definition,
sF53 = plus_plus(int,sF52,sF52),
introduced(definition,[new_symbols(definition,[sF53])],[function_definition]) ).
fof(f4720,plain,
plus_plus(int,sF52,sF52) = sF53,
inference(reorient_equations,[],[f4719]) ).
fof(f4721,definition,
sF54 = number_number_of(nat,sF53),
introduced(definition,[new_symbols(definition,[sF54])],[function_definition]) ).
fof(f4722,plain,
number_number_of(nat,sF53) = sF54,
inference(reorient_equations,[],[f4721]) ).
fof(f4723,definition,
sF55 = hAPP(nat,int,sF50,sF54),
introduced(definition,[new_symbols(definition,[sF55])],[function_definition]) ).
fof(f4724,plain,
hAPP(nat,int,sF50,sF54) = sF55,
inference(reorient_equations,[],[f4723]) ).
fof(f4725,plain,
sF45 = sF55,
inference(definition_folding,[],[f4600,f4724,f4722,f4720,f4718,f4716,f4706,f4718,f4716,f4706,f4714,f4712,f4710,f4708,f4706,f4704]) ).
fof(f4742,plain,
pls = minus_minus(int,min,min),
inference(forward_demodulation,[],[f4555,f4556]) ).
fof(f4834,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(forward_demodulation,[],[f2715,f2824]) ).
fof(f4835,plain,
! [X0] : minus_minus(int,X0,min) = ti(int,minus_minus(int,X0,min)),
inference(forward_demodulation,[],[f4344,f4556]) ).
fof(f4839,plain,
pls = sF45,
inference(forward_demodulation,[],[f4704,f2824]) ).
fof(f4842,plain,
sF45 = hAPP(nat,int,sF50,sF54),
inference(forward_demodulation,[],[f4724,f4725]) ).
fof(f4918,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),plus_plus(int,one_one(int),hAPP(nat,int,sF47,n)))),
inference(forward_demodulation,[],[f4834,f4708]) ).
fof(f4922,plain,
sF45 = minus_minus(int,min,min),
inference(forward_demodulation,[],[f4839,f4742]) ).
fof(f4990,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),plus_plus(int,one_one(int),sF48))),
inference(forward_demodulation,[],[f4918,f4710]) ).
fof(f5050,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),plus_plus(int,sF48,one_one(int)))),
inference(forward_demodulation,[],[f4990,f2780]) ).
fof(f5108,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),minus_minus(int,sF48,min))),
inference(forward_demodulation,[],[f5050,f4556]) ).
fof(f5155,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),minus_minus(int,min,min)),minus_minus(int,sF48,min))),
inference(forward_demodulation,[],[f5108,f4742]) ).
fof(f6363,plain,
! [X0] : zero_zero(int) = minus_minus(int,X0,X0),
inference(resolution,[],[f3183,f4223]) ).
fof(f6373,plain,
! [X0,X1] : minus_minus(int,X0,X0) = minus_minus(int,X1,X1),
inference(superposition,[],[f6363,f6363]) ).
fof(f6776,plain,
! [X0] : plus_plus(int,one_one(int),X0) = minus_minus(int,X0,min),
inference(superposition,[],[f2780,f4556]) ).
fof(f6785,plain,
! [X0] : minus_minus(int,X0,min) = plus_plus(int,sF46,X0),
inference(forward_demodulation,[],[f6776,f4706]) ).
fof(f7265,plain,
sF49 = minus_minus(int,sF48,min),
inference(superposition,[],[f4712,f6785]) ).
fof(f7608,plain,
sF49 = ti(int,sF49),
inference(superposition,[],[f4835,f7265]) ).
fof(f12231,plain,
! [X0] : zero_zero(int) = legendre(X0,X0),
inference(resolution,[],[f3984,f3884]) ).
fof(f12418,plain,
! [X0] : pls = legendre(X0,X0),
inference(superposition,[],[f2824,f12231]) ).
fof(f12431,plain,
! [X0,X1] : minus_minus(int,X1,X1) = legendre(X0,X0),
inference(superposition,[],[f6363,f12231]) ).
fof(f18814,plain,
! [X0] :
( zero_zero(int) != hAPP(nat,int,sF50,X0)
| zero_zero(int) = ti(int,sF49)
| ~ ring_11004092258visors(int) ),
inference(superposition,[],[f2960,f4714]) ).
fof(f18829,plain,
! [X0] :
( zero_zero(int) != hAPP(nat,int,sF50,X0)
| zero_zero(int) = ti(int,sF49) ),
inference(forward_subsumption_resolution,[],[f18814,f4191]) ).
fof(f18835,plain,
! [X0] :
( pls != hAPP(nat,int,sF50,X0)
| zero_zero(int) = ti(int,sF49) ),
inference(forward_demodulation,[],[f18829,f2824]) ).
fof(f18840,plain,
! [X0] :
( minus_minus(int,min,min) != hAPP(nat,int,sF50,X0)
| zero_zero(int) = ti(int,sF49) ),
inference(forward_demodulation,[],[f18835,f4742]) ).
fof(f18843,plain,
! [X0] :
( zero_zero(int) = sF49
| minus_minus(int,min,min) != hAPP(nat,int,sF50,X0) ),
inference(forward_demodulation,[],[f18840,f7608]) ).
fof(f18846,plain,
! [X0] :
( pls = sF49
| minus_minus(int,min,min) != hAPP(nat,int,sF50,X0) ),
inference(forward_demodulation,[],[f18843,f2824]) ).
fof(f18848,plain,
! [X0] :
( sF49 = minus_minus(int,min,min)
| minus_minus(int,min,min) != hAPP(nat,int,sF50,X0) ),
inference(forward_demodulation,[],[f18846,f4742]) ).
fof(f18850,definition,
( spl56_160
<=> ! [X0] : minus_minus(int,min,min) != hAPP(nat,int,sF50,X0) ),
introduced(definition,[new_symbols(definition,[spl56_160])],[avatar_definition]) ).
fof(f18851,plain,
( ! [X0] : minus_minus(int,min,min) != hAPP(nat,int,sF50,X0)
| ~ spl56_160 ),
inference(avatar_component_clause,[],[f18850]) ).
fof(f18853,definition,
( spl56_161
<=> sF49 = minus_minus(int,min,min) ),
introduced(definition,[new_symbols(definition,[spl56_161])],[avatar_definition]) ).
fof(f18855,plain,
( sF49 = minus_minus(int,min,min)
| ~ spl56_161 ),
inference(avatar_component_clause,[],[f18853]) ).
fof(f18856,plain,
( spl56_160
| spl56_161 ),
inference(avatar_split_clause,[],[f18848,f18853,f18850]) ).
fof(f18857,plain,
( sF45 != minus_minus(int,min,min)
| ~ spl56_160 ),
inference(superposition,[],[f18851,f4842]) ).
fof(f18858,plain,
( $false
| ~ spl56_160 ),
inference(forward_subsumption_resolution,[],[f18857,f4922]) ).
fof(f18859,plain,
~ spl56_160,
inference(avatar_contradiction_clause,[],[f18858]) ).
fof(f18883,plain,
( ! [X0] : sF49 = minus_minus(int,X0,X0)
| ~ spl56_161 ),
inference(superposition,[],[f6373,f18855]) ).
fof(f18894,plain,
( ! [X0] : sF49 = legendre(X0,X0)
| ~ spl56_161 ),
inference(superposition,[],[f12431,f18855]) ).
fof(f21070,plain,
( pls = sF49
| ~ spl56_161 ),
inference(superposition,[],[f12418,f18894]) ).
fof(f21217,plain,
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),sF49),sF49))
| ~ spl56_161 ),
inference(superposition,[],[f2756,f21070]) ).
fof(f27765,plain,
! [X0] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),minus_minus(int,X0,X0)),minus_minus(int,sF48,min))),
inference(superposition,[],[f5155,f6373]) ).
fof(f27776,plain,
! [X0] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),minus_minus(int,X0,X0)),sF49)),
inference(forward_demodulation,[],[f27765,f7265]) ).
fof(f27799,plain,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),sF49),sF49))
| ~ spl56_161 ),
inference(forward_demodulation,[],[f27776,f18883]) ).
fof(f27822,plain,
( $false
| ~ spl56_161 ),
inference(forward_subsumption_resolution,[],[f27799,f21217]) ).
fof(f27823,plain,
~ spl56_161,
inference(avatar_contradiction_clause,[],[f27822]) ).
cnf(s156,plain,
( spl56_160
| spl56_161 ),
inference(sat_conversion,[],[f18856]) ).
cnf(s157,plain,
~ spl56_160,
inference(sat_conversion,[],[f18859]) ).
cnf(s191,plain,
~ spl56_161,
inference(sat_conversion,[],[f27823]) ).
cnf(s192,plain,
$false,
inference(rat,[],[s156,s191,s157]) ).
fof(f27829,plain,
$false,
inference(avatar_sat_refutation,[],[s192]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.40 % Computer : n004.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 21:43:04 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.44 Running first-order model finding
% 0.13/0.44 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
% 5.26/1.31 % (3902155)Will run a generic schedule for satisfiability detection.
% 5.26/1.31 % (3902168)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=360069894:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.26/1.31 % (3902163)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4057604437_2999 on theBenchmark for (2999ds/0Mi)
% 5.26/1.31 % (3902164)% WARNING: option uhcvi not known.
% 5.26/1.31 % (3902165)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=31305141:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.26/1.31 % (3902164)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1338336836:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.26/1.31 % (3902167)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3123542986:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.26/1.31 % (3902166)dis+10_1_sil=32000:sp=arity:random_seed=1030767419:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.26/1.31 % (3902169)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=180363825:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.26/1.31 % (3902168)Instruction limit reached!
% 5.26/1.31 % (3902168)------------------------------
% 5.26/1.31 % (3902168)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902168)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902168)Termination reason: Instruction limit
% 5.26/1.31 % (3902168)Termination phase: Saturation
% 5.26/1.31 % (3902168)Time elapsed: 0.046 s
% 5.26/1.31 % (3902168)Peak memory usage: 14 MB
% 5.26/1.31 % (3902168)Instructions burned: 133 (million)
% 5.26/1.31 % (3902177)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1962988493:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 5.26/1.31 % (3902167)Instruction limit reached!
% 5.26/1.31 % (3902167)------------------------------
% 5.26/1.31 % (3902167)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902167)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902167)Termination reason: Instruction limit
% 5.26/1.31 % (3902167)Termination phase: Blocked clause elimination
% 5.26/1.31 % (3902167)Time elapsed: 0.078 s
% 5.26/1.31 % (3902167)Peak memory usage: 13 MB
% 5.26/1.31 % (3902167)Instructions burned: 116 (million)
% 5.26/1.31 % (3902166)Instruction limit reached!
% 5.26/1.31 % (3902166)------------------------------
% 5.26/1.31 % (3902166)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902166)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902166)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902166)Termination reason: Instruction limit
% 5.26/1.31 % (3902166)Termination phase: Property scanning
% 5.26/1.31 % (3902166)Time elapsed: 0.086 s
% 5.26/1.31 % (3902166)Peak memory usage: 13 MB
% 5.26/1.31 % (3902166)Instructions burned: 104 (million)
% 5.26/1.31 % (3902180)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3175088460:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.26/1.31 % (3902181)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=3493039265:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.26/1.31 % (3902169)Instruction limit reached!
% 5.26/1.31 % (3902169)------------------------------
% 5.26/1.31 % (3902169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902169)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902169)Termination reason: Instruction limit
% 5.26/1.31 % (3902169)Termination phase: Saturation
% 5.26/1.31 % (3902169)Time elapsed: 0.136 s
% 5.26/1.31 % (3902169)Peak memory usage: 14 MB
% 5.26/1.31 % (3902169)Instructions burned: 159 (million)
% 5.26/1.31 % (3902184)ott-21_1_sil=16000:fs=off:random_seed=2011288732:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 5.26/1.31 % (3902180)Instruction limit reached!
% 5.26/1.31 % (3902180)------------------------------
% 5.26/1.31 % (3902180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902180)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902180)Termination reason: Instruction limit
% 5.26/1.31 % (3902180)Termination phase: Blocked clause elimination
% 5.26/1.31 % (3902180)Time elapsed: 0.103 s
% 5.26/1.31 % (3902180)Peak memory usage: 13 MB
% 5.26/1.31 % (3902180)Instructions burned: 132 (million)
% 5.26/1.31 % (3902189)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1827404356:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 5.26/1.31 % (3902184)Instruction limit reached!
% 5.26/1.31 % (3902184)------------------------------
% 5.26/1.31 % (3902184)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902184)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902184)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902184)Termination reason: Instruction limit
% 5.26/1.31 % (3902184)Termination phase: Saturation
% 5.26/1.31 % (3902184)Time elapsed: 0.150 s
% 5.26/1.31 % (3902184)Peak memory usage: 14 MB
% 5.26/1.31 % (3902184)Instructions burned: 180 (million)
% 5.26/1.31 % (3902177)Instruction limit reached!
% 5.26/1.31 % (3902177)------------------------------
% 5.26/1.31 % (3902177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902177)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902177)Termination reason: Instruction limit
% 5.26/1.31 % (3902177)Termination phase: Finite model building preprocessing
% 5.26/1.31 % (3902177)Time elapsed: 0.287 s
% 5.26/1.31 % (3902177)Peak memory usage: 19 MB
% 5.26/1.31 % (3902177)Instructions burned: 716 (million)
% 5.26/1.31 % (3902192)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3625071758:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 5.26/1.31 % (3902194)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=631123862:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 5.26/1.31 % (3902189)Instruction limit reached!
% 5.26/1.31 % (3902189)------------------------------
% 5.26/1.31 % (3902189)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902189)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902189)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902189)Termination reason: Instruction limit
% 5.26/1.31 % (3902189)Termination phase: Saturation
% 5.26/1.31 % (3902189)Time elapsed: 0.356 s
% 5.26/1.31 % (3902189)Peak memory usage: 16 MB
% 5.26/1.31 % (3902189)Instructions burned: 477 (million)
% 5.26/1.31 % (3902201)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3891218552:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 5.26/1.31 % (3902181)Instruction limit reached!
% 5.26/1.31 % (3902181)------------------------------
% 5.26/1.31 % (3902181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902181)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902181)Termination reason: Instruction limit
% 5.26/1.31 % (3902181)Termination phase: Saturation
% 5.26/1.31 % (3902181)Time elapsed: 0.619 s
% 5.26/1.31 % (3902181)Peak memory usage: 19 MB
% 5.26/1.31 % (3902181)Instructions burned: 684 (million)
% 5.26/1.31 % (3902194) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3902155-3902194"...
% 5.26/1.31 % (3902194)...printing done.
% 5.26/1.31 % (3902194)Refutation found. Thanks to Tanya!
% 5.26/1.31 % SZS status Theorem for theBenchmark
% 5.26/1.31 % SZS output start Proof for theBenchmark
% See solution above
% 5.26/1.31 % (3902194)------------------------------
% 5.26/1.31 % (3902194)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.26/1.31 % (3902194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.31 % (3902194)CaDiCaL version: 2.1.3
% 5.26/1.31 % (3902194)Termination reason: Refutation
% 5.26/1.31 % (3902194)Time elapsed: 0.422 s
% 5.26/1.31 % (3902194)Peak memory usage: 23 MB
% 5.26/1.31 % (3902194)Instructions burned: 1022 (million)
% 5.26/1.31 % (3902155)Success in time 0.866 s
% 5.26/1.31 % Vampire exiting
%------------------------------------------------------------------------------