%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM926+4 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:13 PM UTC 2026
% Result : Theorem 34.91s 10.81s
% Output : Refutation 34.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of formulae : 56 ( 23 unt; 5 def)
% Number of atoms : 123 ( 28 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 110 ( 43 ~; 44 |; 12 &)
% ( 8 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 17 con; 0-2 aty)
% Number of variables : 26 ( 0 sgn 14 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
is_int(one_one_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_Groups_Oone__class_Oone_000tc__Int__Oint) ).
fof(f59,axiom,
is_int(t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_v_t____) ).
fof(f60,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_tpos) ).
fof(f61,axiom,
( t = one_one_int
=> ? [X0,X1] :
( is_int(X0)
& is_int(X1)
& hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(f62,axiom,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
=> ? [X0,X1] :
( is_int(X0)
& is_int(X1)
& hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(f125,axiom,
! [X0,X1] :
( ( is_int(X0)
& is_int(X1) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_zless__le) ).
fof(f5480,conjecture,
? [X0,X1] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f5481,negated_conjecture,
~ ? [X0,X1] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int),
inference(negated_conjecture,[status(cth)],[f5480]) ).
fof(f5542,plain,
( ? [X0,X1] :
( is_int(X0)
& is_int(X1)
& hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) )
| one_one_int != t ),
inference(ennf_transformation,[],[f61]) ).
fof(f5543,plain,
( ? [X0,X1] :
( is_int(X0)
& is_int(X1)
& hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(ennf_transformation,[],[f62]) ).
fof(f5545,plain,
! [X0,X1] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(ennf_transformation,[],[f125]) ).
fof(f5546,plain,
! [X0,X1] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(flattening,[],[f5545]) ).
fof(f9431,plain,
! [X0,X1] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) != hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int),
inference(ennf_transformation,[],[f5481]) ).
fof(f9437,plain,
is_int(one_one_int),
inference(cnf_transformation,[],[f6]) ).
fof(f9490,plain,
is_int(t),
inference(cnf_transformation,[],[f59]) ).
fof(f9491,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
inference(cnf_transformation,[],[f60]) ).
fof(f9492,plain,
( one_one_int != t
| hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) ),
inference(cnf_transformation,[],[f5542]) ).
fof(f9495,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
| hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK2),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK3),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) ),
inference(cnf_transformation,[],[f5543]) ).
fof(f9563,plain,
! [X0,X1] :
( ~ is_int(X1)
| ~ is_int(X0)
| X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ),
inference(cnf_transformation,[],[f5546]) ).
fof(f17172,plain,
! [X0,X1] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) != hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int),
inference(cnf_transformation,[],[f9431]) ).
fof(f19447,plain,
~ is_int(one_one_int),
inference(consistent_polarity_flipping,[],[f9437]) ).
fof(f19500,plain,
~ is_int(t),
inference(consistent_polarity_flipping,[],[f9490]) ).
fof(f19501,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
inference(consistent_polarity_flipping,[],[f9491]) ).
fof(f19506,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
| hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK2),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK3),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) ),
inference(consistent_polarity_flipping,[],[f9495]) ).
fof(f19513,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| is_int(X0)
| X0 = X1
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| is_int(X1) ),
inference(consistent_polarity_flipping,[],[f9563]) ).
fof(f24771,definition,
( spl556_2
<=> is_int(one_one_int) ),
introduced(definition,[new_symbols(definition,[spl556_2])],[avatar_definition]) ).
fof(f24772,plain,
( ~ is_int(one_one_int)
| spl556_2 ),
inference(avatar_component_clause,[],[f24771]) ).
fof(f25097,definition,
( spl556_70
<=> hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK2),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK3),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) ),
introduced(definition,[new_symbols(definition,[spl556_70])],[avatar_definition]) ).
fof(f25099,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK2),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK3),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))))
| ~ spl556_70 ),
inference(avatar_component_clause,[],[f25097]) ).
fof(f25101,definition,
( spl556_71
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
introduced(definition,[new_symbols(definition,[spl556_71])],[avatar_definition]) ).
fof(f25103,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
| ~ spl556_71 ),
inference(avatar_component_clause,[],[f25101]) ).
fof(f25104,plain,
( spl556_70
| spl556_71 ),
inference(avatar_split_clause,[],[f19506,f25101,f25097]) ).
fof(f25116,definition,
( spl556_74
<=> hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))) ),
introduced(definition,[new_symbols(definition,[spl556_74])],[avatar_definition]) ).
fof(f25118,plain,
( hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(bit0,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),m)),one_one_int) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,sK1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))))
| ~ spl556_74 ),
inference(avatar_component_clause,[],[f25116]) ).
fof(f25120,definition,
( spl556_75
<=> one_one_int = t ),
introduced(definition,[new_symbols(definition,[spl556_75])],[avatar_definition]) ).
fof(f25123,plain,
( spl556_74
| ~ spl556_75 ),
inference(avatar_split_clause,[],[f9492,f25120,f25116]) ).
fof(f25136,plain,
~ spl556_2,
inference(avatar_split_clause,[],[f19447,f24771]) ).
fof(f138304,plain,
( is_int(one_one_int)
| one_one_int = t
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t))
| is_int(t)
| ~ spl556_71 ),
inference(resolution,[],[f19513,f25103]) ).
fof(f138321,plain,
( one_one_int = t
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t))
| is_int(t)
| spl556_2
| ~ spl556_71 ),
inference(forward_subsumption_resolution,[],[f138304,f24772]) ).
fof(f138447,plain,
( one_one_int = t
| is_int(t)
| spl556_2
| ~ spl556_71 ),
inference(forward_subsumption_resolution,[],[f138321,f19501]) ).
fof(f138451,plain,
( $false
| ~ spl556_74 ),
inference(forward_subsumption_resolution,[],[f25118,f17172]) ).
fof(f138452,plain,
~ spl556_74,
inference(avatar_contradiction_clause,[],[f138451]) ).
fof(f138454,plain,
( one_one_int = t
| spl556_2
| ~ spl556_71 ),
inference(forward_subsumption_resolution,[],[f138447,f19500]) ).
fof(f138456,plain,
( spl556_75
| spl556_2
| ~ spl556_71 ),
inference(avatar_split_clause,[],[f138454,f25101,f24771,f25120]) ).
fof(f443427,plain,
( $false
| ~ spl556_70 ),
inference(forward_subsumption_resolution,[],[f25099,f17172]) ).
fof(f443428,plain,
~ spl556_70,
inference(avatar_contradiction_clause,[],[f443427]) ).
cnf(s84,plain,
( spl556_70
| spl556_71 ),
inference(sat_conversion,[],[f25104]) ).
cnf(s87,plain,
( spl556_74
| ~ spl556_75 ),
inference(sat_conversion,[],[f25123]) ).
cnf(s93,plain,
~ spl556_2,
inference(sat_conversion,[],[f25136]) ).
cnf(s5314,plain,
~ spl556_74,
inference(sat_conversion,[],[f138452]) ).
cnf(s5316,plain,
( spl556_2
| ~ spl556_71
| spl556_75 ),
inference(sat_conversion,[],[f138456]) ).
cnf(s14816,plain,
~ spl556_70,
inference(sat_conversion,[],[f443428]) ).
cnf(s15161,plain,
~ spl556_75,
inference(rat,[],[s87,s5314]) ).
cnf(s15162,plain,
~ spl556_71,
inference(rat,[],[s5316,s93,s15161]) ).
cnf(s15165,plain,
$false,
inference(rat,[],[s84,s15162,s14816]) ).
fof(f443429,plain,
$false,
inference(avatar_sat_refutation,[],[s15165]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM926+4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n015.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 21:48:16 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.05/4.83 % (2035368)Will run a generic schedule for satisfiability detection.
% 29.05/4.83 % (2035374)% WARNING: option uhcvi not known.
% 29.05/4.83 % (2035374)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2516113129:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi)
% 29.05/4.83 % (2035373)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3832639237_2996 on theBenchmark for (2996ds/0Mi)
% 29.05/4.83 % (2035375)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1936718873:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi)
% 29.05/4.83 % (2035376)dis+10_1_sil=32000:sp=arity:random_seed=1443687843:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi)
% 29.05/4.83 % (2035377)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1362017287:i=116_2996 on theBenchmark for (2996ds/116Mi)
% 29.05/4.83 % (2035378)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=376859450:i=131_2996 on theBenchmark for (2996ds/131Mi)
% 29.05/4.83 % (2035379)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3823591299:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi)
% 29.05/4.83 % (2035376)Instruction limit reached!
% 29.05/4.83 % (2035376)------------------------------
% 29.05/4.83 % (2035376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.05/4.83 % (2035376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.05/4.83 % (2035376)CaDiCaL version: 2.1.3
% 29.05/4.83 % (2035376)Termination reason: Instruction limit
% 29.05/4.83 % (2035376)Termination phase: Preprocessing 3
% 29.05/4.83 % (2035376)Time elapsed: 0.062 s
% 29.05/4.83 % (2035376)Peak memory usage: 19 MB
% 29.05/4.83 % (2035376)Instructions burned: 104 (million)
% 29.05/4.83 % (2035377)Instruction limit reached!
% 29.05/4.83 % (2035377)------------------------------
% 29.05/4.83 % (2035377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.05/4.83 % (2035377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.05/4.83 % (2035377)CaDiCaL version: 2.1.3
% 29.05/4.83 % (2035377)Termination reason: Instruction limit
% 29.05/4.83 % (2035377)Termination phase: NewCNF
% 29.05/4.83 % (2035377)Time elapsed: 0.075 s
% 29.05/4.83 % (2035377)Peak memory usage: 21 MB
% 29.05/4.83 % (2035377)Instructions burned: 117 (million)
% 29.05/4.83 % (2035378)Instruction limit reached!
% 29.05/4.83 % (2035378)------------------------------
% 29.05/4.83 % (2035378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.05/4.83 % (2035378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.05/4.83 % (2035378)CaDiCaL version: 2.1.3
% 29.05/4.83 % (2035378)Termination reason: Instruction limit
% 29.05/4.83 % (2035378)Termination phase: Clausification
% 29.05/4.83 % (2035378)Time elapsed: 0.078 s
% 29.05/4.83 % (2035378)Peak memory usage: 21 MB
% 29.05/4.83 % (2035378)Instructions burned: 132 (million)
% 29.05/4.83 % (2035387)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2474319844:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi)
% 29.05/4.83 % (2035379)Instruction limit reached!
% 29.05/4.83 % (2035379)------------------------------
% 29.05/4.83 % (2035379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.05/4.83 % (2035379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.05/4.83 % (2035379)CaDiCaL version: 2.1.3
% 29.05/4.83 % (2035379)Termination reason: Instruction limit
% 29.05/4.83 % (2035379)Termination phase: Property scanning
% 29.05/4.83 % (2035379)Time elapsed: 0.092 s
% 29.05/4.83 % (2035379)Peak memory usage: 21 MB
% 29.05/4.83 % (2035379)Instructions burned: 161 (million)
% 29.05/4.83 % (2035388)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=226454956:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 29.05/4.83 % (2035389)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=815472981:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 29.05/4.83 % (2035391)ott-21_1_sil=16000:fs=off:random_seed=2029202804:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 29.05/4.83 % (2035388)Instruction limit reached!
% 29.05/4.83 % (2035388)------------------------------
% 29.05/4.83 % (2035388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.05/4.83 % (2035388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.99/9.30 % (2035388)CaDiCaL version: 2.1.3
% 60.99/9.30 % (2035388)Termination reason: Instruction limit
% 60.99/9.30 % (2035388)Termination phase: Clausification
% 60.99/9.30 % (2035388)Time elapsed: 0.075 s
% 60.99/9.30 % (2035388)Peak memory usage: 20 MB
% 60.99/9.30 % (2035388)Instructions burned: 131 (million)
% 60.99/9.30 % (2035395)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2591762865:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 60.99/9.30 % (2035391)Instruction limit reached!
% 60.99/9.30 % (2035391)------------------------------
% 60.99/9.30 % (2035391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.99/9.30 % (2035391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.99/9.30 % (2035391)CaDiCaL version: 2.1.3
% 60.99/9.30 % (2035391)Termination reason: Instruction limit
% 60.99/9.30 % (2035391)Termination phase: Property scanning
% 60.99/9.30 % (2035391)Time elapsed: 0.096 s
% 60.99/9.30 % (2035391)Peak memory usage: 21 MB
% 60.99/9.30 % (2035391)Instructions burned: 181 (million)
% 60.99/9.30 % (2035397)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3364975960:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 60.99/9.30 % (2035395)Instruction limit reached!
% 60.99/9.30 % (2035395)------------------------------
% 60.99/9.30 % (2035395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.99/9.30 % (2035395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.99/9.30 % (2035395)CaDiCaL version: 2.1.3
% 60.99/9.30 % (2035395)Termination reason: Instruction limit
% 60.99/9.30 % (2035395)Termination phase: Saturation
% 60.99/9.30 % (2035395)Time elapsed: 0.217 s
% 60.99/9.30 % (2035395)Peak memory usage: 23 MB
% 60.99/9.30 % (2035395)Instructions burned: 478 (million)
% 60.99/9.30 % (2035387)Instruction limit reached!
% 60.99/9.30 % (2035387)------------------------------
% 60.99/9.30 % (2035387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.99/9.30 % (2035387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.99/9.30 % (2035387)CaDiCaL version: 2.1.3
% 60.99/9.30 % (2035387)Termination reason: Instruction limit
% 60.99/9.30 % (2035387)Termination phase: Finite model building preprocessing
% 60.99/9.30 % (2035387)Time elapsed: 0.330 s
% 60.99/9.30 % (2035387)Peak memory usage: 28 MB
% 60.99/9.30 % (2035387)Instructions burned: 714 (million)
% 60.99/9.30 % (2035389)Instruction limit reached!
% 60.99/9.30 % (2035389)------------------------------
% 60.99/9.30 % (2035389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.99/9.30 % (2035389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.99/9.30 % (2035389)CaDiCaL version: 2.1.3
% 60.99/9.30 % (2035389)Termination reason: Instruction limit
% 60.99/9.30 % (2035389)Termination phase: Saturation
% 60.99/9.30 % (2035389)Time elapsed: 0.320 s
% 60.99/9.30 % (2035389)Peak memory usage: 25 MB
% 60.99/9.30 % (2035389)Instructions burned: 687 (million)
% 60.99/9.30 % (2035399)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3595616939:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 60.99/9.30 % (2035400)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1318032469:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 60.99/9.30 % (2035401)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=2945752928:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 60.99/9.30 % (2035397)Instruction limit reached!
% 60.99/9.30 % (2035397)------------------------------
% 60.99/9.30 % (2035397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.99/9.30 % (2035397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.99/9.30 % (2035397)CaDiCaL version: 2.1.3
% 60.99/9.30 % (2035397)Termination reason: Instruction limit
% 60.99/9.30 % (2035397)Termination phase: Finite model building preprocessing
% 60.99/9.30 % (2035397)Time elapsed: 0.406 s
% 60.99/9.30 % (2035397)Peak memory usage: 32 MB
% 60.99/9.30 % (2035397)Instructions burned: 865 (million)
% 60.99/9.30 % (2035405)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=47016287:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 60.99/9.30 % (2035401)Instruction limit reached!
% 60.99/9.30 % (2035401)------------------------------
% 60.99/9.30 % (2035401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 60.99/9.30 % (2035401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035401)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035401)Termination reason: Instruction limit
% 34.91/10.81 % (2035401)Termination phase: Saturation
% 34.91/10.81 % (2035401)Time elapsed: 0.349 s
% 34.91/10.81 % (2035401)Peak memory usage: 28 MB
% 34.91/10.81 % (2035401)Instructions burned: 693 (million)
% 34.91/10.81 % (2035407)fmb+10_1_sil=64000:random_seed=973575038:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 34.91/10.81 % (2035400)Instruction limit reached!
% 34.91/10.81 % (2035400)------------------------------
% 34.91/10.81 % (2035400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035400)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035400)Termination reason: Instruction limit
% 34.91/10.81 % (2035400)Termination phase: Finite model building preprocessing
% 34.91/10.81 % (2035400)Time elapsed: 0.421 s
% 34.91/10.81 % (2035400)Peak memory usage: 33 MB
% 34.91/10.81 % (2035400)Instructions burned: 889 (million)
% 34.91/10.81 % (2035409)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3071236615:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi)
% 34.91/10.81 % (2035399)Instruction limit reached!
% 34.91/10.81 % (2035399)------------------------------
% 34.91/10.81 % (2035399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035399)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035399)Termination reason: Instruction limit
% 34.91/10.81 % (2035399)Termination phase: Saturation
% 34.91/10.81 % (2035399)Time elapsed: 0.624 s
% 34.91/10.81 % (2035399)Peak memory usage: 29 MB
% 34.91/10.81 % (2035399)Instructions burned: 1179 (million)
% 34.91/10.81 % (2035405)Instruction limit reached!
% 34.91/10.81 % (2035405)------------------------------
% 34.91/10.81 % (2035405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035405)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035405)Termination reason: Instruction limit
% 34.91/10.81 % (2035405)Termination phase: Saturation
% 34.91/10.81 % (2035405)Time elapsed: 0.399 s
% 34.91/10.81 % (2035405)Peak memory usage: 30 MB
% 34.91/10.81 % (2035405)Instructions burned: 879 (million)
% 34.91/10.81 % (2035411)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1508671893:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi)
% 34.91/10.81 % (2035412)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=859797944:i=5131_2985 on theBenchmark for (2985ds/5131Mi)
% 34.91/10.81 % (2035411)Instruction limit reached!
% 34.91/10.81 % (2035411)------------------------------
% 34.91/10.81 % (2035411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035411)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035411)Termination reason: Instruction limit
% 34.91/10.81 % (2035411)Termination phase: Finite model building preprocessing
% 34.91/10.81 % (2035411)Time elapsed: 0.431 s
% 34.91/10.81 % (2035411)Peak memory usage: 32 MB
% 34.91/10.81 % (2035411)Instructions burned: 920 (million)
% 34.91/10.81 % (2035416)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2226926049:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 34.91/10.81 % (2035416)Instruction limit reached!
% 34.91/10.81 % (2035416)------------------------------
% 34.91/10.81 % (2035416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035416)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035416)Termination reason: Instruction limit
% 34.91/10.81 % (2035416)Termination phase: Saturation
% 34.91/10.81 % (2035416)Time elapsed: 0.697 s
% 34.91/10.81 % (2035416)Peak memory usage: 30 MB
% 34.91/10.81 % (2035416)Instructions burned: 1473 (million)
% 34.91/10.81 % (2035418)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3514582149:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 34.91/10.81 % (2035412)Instruction limit reached!
% 34.91/10.81 % (2035412)------------------------------
% 34.91/10.81 % (2035412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035412)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035412)Termination reason: Instruction limit
% 34.91/10.81 % (2035412)Termination phase: Saturation
% 34.91/10.81 % (2035412)Time elapsed: 2.969 s
% 34.91/10.81 % (2035412)Peak memory usage: 61 MB
% 34.91/10.81 % (2035412)Instructions burned: 5132 (million)
% 34.91/10.81 % (2035420)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3194355688:fmbsr=2.30978:i=2174_2956 on theBenchmark for (2956ds/2174Mi)
% 34.91/10.81 % (2035420)Instruction limit reached!
% 34.91/10.81 % (2035420)------------------------------
% 34.91/10.81 % (2035420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035420)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035420)Termination reason: Instruction limit
% 34.91/10.81 % (2035420)Termination phase: Finite model building preprocessing
% 34.91/10.81 % (2035420)Time elapsed: 1.032 s
% 34.91/10.81 % (2035420)Peak memory usage: 49 MB
% 34.91/10.81 % (2035420)Instructions burned: 2175 (million)
% 34.91/10.81 % (2035422)ott-2_1_sil=16000:newcnf=on:random_seed=479669673:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2945 on theBenchmark for (2945ds/869Mi)
% 34.91/10.81 % (2035418)Instruction limit reached!
% 34.91/10.81 % (2035418)------------------------------
% 34.91/10.81 % (2035418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035418)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035418)Termination reason: Instruction limit
% 34.91/10.81 % (2035418)Termination phase: Finite model building preprocessing
% 34.91/10.81 % (2035418)Time elapsed: 3.104 s
% 34.91/10.81 % (2035418)Peak memory usage: 82 MB
% 34.91/10.81 % (2035418)Instructions burned: 6324 (million)
% 34.91/10.81 % Detected minimum model sizes of [3]
% 34.91/10.81 % Detected maximum model sizes of [max]
% 34.91/10.81 % TRYING [3]
% 34.91/10.81 % (2035424)ott+10_1_sil=32000:tgt=ground:random_seed=1740089186:i=5114:av=off_2942 on theBenchmark for (2942ds/5114Mi)
% 34.91/10.81 % Detected minimum model sizes of [3]
% 34.91/10.81 % Detected maximum model sizes of [max]
% 34.91/10.81 % (2035422)Instruction limit reached!
% 34.91/10.81 % (2035422)------------------------------
% 34.91/10.81 % (2035422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035422)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035422)Termination reason: Instruction limit
% 34.91/10.81 % (2035422)Termination phase: Saturation
% 34.91/10.81 % (2035422)Time elapsed: 0.435 s
% 34.91/10.81 % (2035422)Peak memory usage: 28 MB
% 34.91/10.81 % (2035422)Instructions burned: 870 (million)
% 34.91/10.81 % (2035426)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1151949024:i=54282_2940 on theBenchmark for (2940ds/54282Mi)
% 34.91/10.81 % (2035409)Instruction limit reached!
% 34.91/10.81 % (2035409)------------------------------
% 34.91/10.81 % (2035409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035409)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035409)Termination reason: Instruction limit
% 34.91/10.81 % (2035409)Termination phase: Finite model building preprocessing
% 34.91/10.81 % (2035409)Time elapsed: 4.787 s
% 34.91/10.81 % (2035409)Peak memory usage: 156 MB
% 34.91/10.81 % (2035409)Instructions burned: 9517 (million)
% 34.91/10.81 % (2035428)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2374238937:i=3512:aac=none_2939 on theBenchmark for (2939ds/3512Mi)
% 34.91/10.81 % TRYING [3]
% 34.91/10.81 % (2035428)Instruction limit reached!
% 34.91/10.81 % (2035428)------------------------------
% 34.91/10.81 % (2035428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035428)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035428)Termination reason: Instruction limit
% 34.91/10.81 % (2035428)Termination phase: Saturation
% 34.91/10.81 % (2035428)Time elapsed: 2.002 s
% 34.91/10.81 % (2035428)Peak memory usage: 50 MB
% 34.91/10.81 % (2035428)Instructions burned: 3513 (million)
% 34.91/10.81 % (2035430)dis+21_1_sil=32000:sas=cadical:random_seed=2669780076:i=3773:amm=off_2919 on theBenchmark for (2919ds/3773Mi)
% 34.91/10.81 % (2035424)Instruction limit reached!
% 34.91/10.81 % (2035424)------------------------------
% 34.91/10.81 % (2035424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035424)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035424)Termination reason: Instruction limit
% 34.91/10.81 % (2035424)Termination phase: Saturation
% 34.91/10.81 % (2035424)Time elapsed: 3.134 s
% 34.91/10.81 % (2035424)Peak memory usage: 74 MB
% 34.91/10.81 % (2035424)Instructions burned: 5115 (million)
% 34.91/10.81 % (2035432)ott+11_1_sil=16000:gs=on:random_seed=3735869822:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2911 on theBenchmark for (2911ds/2251Mi)
% 34.91/10.81 % (2035432)Instruction limit reached!
% 34.91/10.81 % (2035432)------------------------------
% 34.91/10.81 % (2035432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.81 % (2035432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.81 % (2035432)CaDiCaL version: 2.1.3
% 34.91/10.81 % (2035432)Termination reason: Instruction limit
% 34.91/10.81 % (2035432)Termination phase: Saturation
% 34.91/10.81 % (2035432)Time elapsed: 1.282 s
% 34.91/10.81 % (2035432)Peak memory usage: 53 MB
% 34.91/10.81 % (2035432)Instructions burned: 2251 (million)
% 34.91/10.81 % (2035434)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=43764261:fmbsr=1.6:i=67534_2898 on theBenchmark for (2898ds/67534Mi)
% 34.91/10.81 % (2035374) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2035368-2035374"...
% 34.91/10.81 % (2035374)...printing done.
% 34.91/10.81 % (2035374)Refutation found. Thanks to Tanya!
% 34.91/10.81 % SZS status Theorem for theBenchmark
% 34.91/10.81 % SZS output start Proof for theBenchmark
% See solution above
% 34.91/10.82 % (2035374)------------------------------
% 34.91/10.82 % (2035374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.91/10.82 % (2035374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.91/10.82 % (2035374)CaDiCaL version: 2.1.3
% 34.91/10.82 % (2035374)Termination reason: Refutation
% 34.91/10.82 % (2035374)Time elapsed: 9.873 s
% 34.91/10.82 % (2035374)Peak memory usage: 214 MB
% 34.91/10.82 % (2035374)Instructions burned: 31095 (million)
% 34.91/10.82 % (2035368)Success in time 10.373 s
% 34.91/10.82 % Vampire exiting
%------------------------------------------------------------------------------