%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM926+3 : 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:12 PM UTC 2026
% Result : Theorem 1.92s 1.03s
% Output : Refutation 1.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 14
% Syntax : Number of formulae : 56 ( 25 unt; 5 def)
% Number of atoms : 114 ( 33 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 99 ( 41 ~; 35 |; 12 &)
% ( 8 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 9 ( 7 usr; 6 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 10 con; 0-2 aty)
% Number of variables : 30 ( 0 sgn 18 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
is_int(one_one_int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_Groups_Oone__class_Oone_000tc__Int__Oint) ).
fof(f25,axiom,
is_int(t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_v_t____) ).
fof(f26,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_tpos) ).
fof(f27,axiom,
( t = one_one_int
=> ? [X0,X1] :
( is_int(X0)
& is_int(X1)
& hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) ) ),
file('/export/starexec/sandbox/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(f28,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(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) ) ),
file('/export/starexec/sandbox/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(f63,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/sandbox/benchmark/theBenchmark.p',fact_37_zless__le) ).
fof(f232,axiom,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_Bit0__def) ).
fof(f279,axiom,
! [X0] : bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_Bit1__def) ).
fof(f1230,conjecture,
? [X0,X1] : hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f1231,negated_conjecture,
~ ? [X0,X1] : hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int),
inference(negated_conjecture,[status(cth)],[f1230]) ).
fof(f1251,plain,
( ? [X0,X1] :
( is_int(X0)
& is_int(X1)
& hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) )
| one_one_int != t ),
inference(ennf_transformation,[],[f27]) ).
fof(f1252,plain,
( ? [X0,X1] :
( is_int(X0)
& is_int(X1)
& hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) = hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(ennf_transformation,[],[f28]) ).
fof(f1254,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,[],[f63]) ).
fof(f1255,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,[],[f1254]) ).
fof(f2203,plain,
! [X0,X1] : hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) != hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int),
inference(ennf_transformation,[],[f1231]) ).
fof(f2204,plain,
is_int(one_one_int),
inference(cnf_transformation,[],[f1]) ).
fof(f2228,plain,
is_int(t),
inference(cnf_transformation,[],[f25]) ).
fof(f2229,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,one_one_int),t)),
inference(cnf_transformation,[],[f26]) ).
fof(f2230,plain,
( one_one_int != t
| hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(sK1),number_number_of_nat(bit0(bit1(pls))))) ),
inference(cnf_transformation,[],[f1251]) ).
fof(f2233,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
| hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK2),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(sK3),number_number_of_nat(bit0(bit1(pls))))) ),
inference(cnf_transformation,[],[f1252]) ).
fof(f2273,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X0)
| X0 = X1
| ~ is_int(X1)
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ),
inference(cnf_transformation,[],[f1255]) ).
fof(f2505,plain,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
inference(cnf_transformation,[],[f232]) ).
fof(f2552,plain,
! [X0] : bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0),
inference(cnf_transformation,[],[f279]) ).
fof(f3912,plain,
! [X0,X1] : hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(bit0(bit1(pls))))) != hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int),
inference(cnf_transformation,[],[f2203]) ).
fof(f3918,plain,
( one_one_int != t
| hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),hAPP_nat_int(power_power_int(sK1),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))) ),
inference(definition_unfolding,[],[f2230,f2505,f2505,f2552,f2505,f2552,f2505,f2552]) ).
fof(f3919,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
| hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK2),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),hAPP_nat_int(power_power_int(sK3),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))) ),
inference(definition_unfolding,[],[f2233,f2505,f2505,f2552,f2505,f2552,f2505,f2552]) ).
fof(f4515,plain,
! [X0,X1] : hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int) != hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),hAPP_nat_int(power_power_int(X1),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),
inference(definition_unfolding,[],[f3912,f2505,f2552,f2505,f2552,f2505,f2505,f2552]) ).
fof(f4765,definition,
( spl42_9
<=> is_int(one_one_int) ),
introduced(definition,[new_symbols(definition,[spl42_9])],[avatar_definition]) ).
fof(f4766,plain,
( is_int(one_one_int)
| ~ spl42_9 ),
inference(avatar_component_clause,[],[f4765]) ).
fof(f4854,definition,
( spl42_26
<=> hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK2),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),hAPP_nat_int(power_power_int(sK3),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))) ),
introduced(definition,[new_symbols(definition,[spl42_26])],[avatar_definition]) ).
fof(f4856,plain,
( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK2),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),hAPP_nat_int(power_power_int(sK3),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))))
| ~ spl42_26 ),
inference(avatar_component_clause,[],[f4854]) ).
fof(f4858,definition,
( spl42_27
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
introduced(definition,[new_symbols(definition,[spl42_27])],[avatar_definition]) ).
fof(f4861,plain,
( spl42_26
| ~ spl42_27 ),
inference(avatar_split_clause,[],[f3919,f4858,f4854]) ).
fof(f4873,definition,
( spl42_30
<=> hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),hAPP_nat_int(power_power_int(sK1),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))) ),
introduced(definition,[new_symbols(definition,[spl42_30])],[avatar_definition]) ).
fof(f4875,plain,
( hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(sK0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),hAPP_nat_int(power_power_int(sK1),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))))
| ~ spl42_30 ),
inference(avatar_component_clause,[],[f4873]) ).
fof(f4877,definition,
( spl42_31
<=> one_one_int = t ),
introduced(definition,[new_symbols(definition,[spl42_31])],[avatar_definition]) ).
fof(f4880,plain,
( spl42_30
| ~ spl42_31 ),
inference(avatar_split_clause,[],[f3918,f4877,f4873]) ).
fof(f4893,plain,
spl42_9,
inference(avatar_split_clause,[],[f2204,f4765]) ).
fof(f18954,plain,
( ~ is_int(one_one_int)
| one_one_int = t
| ~ is_int(t)
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t)) ),
inference(resolution,[],[f2273,f2229]) ).
fof(f18975,plain,
( one_one_int = t
| ~ is_int(t)
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
| ~ spl42_9 ),
inference(forward_subsumption_resolution,[],[f18954,f4766]) ).
fof(f19013,plain,
( $false
| ~ spl42_26 ),
inference(forward_subsumption_resolution,[],[f4856,f4515]) ).
fof(f19014,plain,
~ spl42_26,
inference(avatar_contradiction_clause,[],[f19013]) ).
fof(f19016,plain,
( $false
| ~ spl42_30 ),
inference(forward_subsumption_resolution,[],[f4875,f4515]) ).
fof(f19017,plain,
~ spl42_30,
inference(avatar_contradiction_clause,[],[f19016]) ).
fof(f19018,plain,
( one_one_int = t
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,one_one_int),t))
| ~ spl42_9 ),
inference(forward_subsumption_resolution,[],[f18975,f2228]) ).
fof(f19019,plain,
( spl42_27
| spl42_31
| ~ spl42_9 ),
inference(avatar_split_clause,[],[f19018,f4765,f4877,f4858]) ).
cnf(s31,plain,
( spl42_26
| ~ spl42_27 ),
inference(sat_conversion,[],[f4861]) ).
cnf(s34,plain,
( spl42_30
| ~ spl42_31 ),
inference(sat_conversion,[],[f4880]) ).
cnf(s40,plain,
spl42_9,
inference(sat_conversion,[],[f4893]) ).
cnf(s149,plain,
~ spl42_26,
inference(sat_conversion,[],[f19014]) ).
cnf(s151,plain,
~ spl42_30,
inference(sat_conversion,[],[f19017]) ).
cnf(s152,plain,
( ~ spl42_9
| spl42_27
| spl42_31 ),
inference(sat_conversion,[],[f19019]) ).
cnf(s157,plain,
~ spl42_31,
inference(rat,[],[s34,s151]) ).
cnf(s158,plain,
spl42_27,
inference(rat,[],[s152,s40,s157]) ).
cnf(s161,plain,
$false,
inference(rat,[],[s31,s158,s149]) ).
fof(f19020,plain,
$false,
inference(avatar_sat_refutation,[],[s161]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM926+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 21:44:22 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.40 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
% 1.92/1.03 % (3904433)Will run a generic schedule for satisfiability detection.
% 1.92/1.03 % (3904451)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=113249269_2999 on theBenchmark for (2999ds/0Mi)
% 1.92/1.03 % (3904452)% WARNING: option uhcvi not known.
% 1.92/1.03 % (3904453)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3869375364:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.92/1.03 % (3904454)dis+10_1_sil=32000:sp=arity:random_seed=1291857061:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.92/1.03 % (3904452)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=98072076:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.92/1.03 % (3904455)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1430249285:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.92/1.03 % (3904456)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2613848750:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.92/1.03 % (3904457)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1374517518:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.92/1.03 % (3904454)Instruction limit reached!
% 1.92/1.03 % (3904454)------------------------------
% 1.92/1.03 % (3904454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904454)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904454)Termination reason: Instruction limit
% 1.92/1.03 % (3904454)Termination phase: Saturation
% 1.92/1.03 % (3904454)Time elapsed: 0.047 s
% 1.92/1.03 % (3904454)Peak memory usage: 14 MB
% 1.92/1.03 % (3904454)Instructions burned: 105 (million)
% 1.92/1.03 % (3904455)Instruction limit reached!
% 1.92/1.03 % (3904455)------------------------------
% 1.92/1.03 % (3904455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904455)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904455)Termination reason: Instruction limit
% 1.92/1.03 % (3904455)Termination phase: Blocked clause elimination
% 1.92/1.03 % (3904455)Time elapsed: 0.052 s
% 1.92/1.03 % (3904455)Peak memory usage: 13 MB
% 1.92/1.03 % (3904455)Instructions burned: 116 (million)
% 1.92/1.03 % (3904456)Instruction limit reached!
% 1.92/1.03 % (3904456)------------------------------
% 1.92/1.03 % (3904456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904484)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=938609270:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.92/1.03 % (3904456)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904456)Termination reason: Instruction limit
% 1.92/1.03 % (3904456)Termination phase: Saturation
% 1.92/1.03 % (3904456)Time elapsed: 0.067 s
% 1.92/1.03 % (3904456)Peak memory usage: 14 MB
% 1.92/1.03 % (3904456)Instructions burned: 132 (million)
% 1.92/1.03 % (3904488)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3523706830:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.92/1.03 % (3904457)Instruction limit reached!
% 1.92/1.03 % (3904457)------------------------------
% 1.92/1.03 % (3904457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904457)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904457)Termination reason: Instruction limit
% 1.92/1.03 % (3904457)Termination phase: Saturation
% 1.92/1.03 % (3904457)Time elapsed: 0.082 s
% 1.92/1.03 % (3904457)Peak memory usage: 15 MB
% 1.92/1.03 % (3904457)Instructions burned: 160 (million)
% 1.92/1.03 % (3904495)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=661180110:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.92/1.03 % (3904503)ott-21_1_sil=16000:fs=off:random_seed=382195046:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.92/1.03 % (3904488)Instruction limit reached!
% 1.92/1.03 % (3904488)------------------------------
% 1.92/1.03 % (3904488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904488)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904488)Termination reason: Instruction limit
% 1.92/1.03 % (3904488)Termination phase: Property scanning
% 1.92/1.03 % (3904488)Time elapsed: 0.058 s
% 1.92/1.03 % (3904488)Peak memory usage: 13 MB
% 1.92/1.03 % (3904488)Instructions burned: 131 (million)
% 1.92/1.03 % (3904526)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3977960200:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.92/1.03 % (3904503)Instruction limit reached!
% 1.92/1.03 % (3904503)------------------------------
% 1.92/1.03 % (3904503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904503)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904503)Termination reason: Instruction limit
% 1.92/1.03 % (3904503)Termination phase: Saturation
% 1.92/1.03 % (3904503)Time elapsed: 0.083 s
% 1.92/1.03 % (3904503)Peak memory usage: 15 MB
% 1.92/1.03 % (3904503)Instructions burned: 180 (million)
% 1.92/1.03 % (3904537)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=885090075:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.92/1.03 % (3904484)Instruction limit reached!
% 1.92/1.03 % (3904484)------------------------------
% 1.92/1.03 % (3904484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904484)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904484)Termination reason: Instruction limit
% 1.92/1.03 % (3904484)Termination phase: Finite model building preprocessing
% 1.92/1.03 % (3904484)Time elapsed: 0.337 s
% 1.92/1.03 % (3904484)Peak memory usage: 22 MB
% 1.92/1.03 % (3904484)Instructions burned: 714 (million)
% 1.92/1.03 % (3904565)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=225750735:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 1.92/1.03 % (3904526)Instruction limit reached!
% 1.92/1.03 % (3904526)------------------------------
% 1.92/1.03 % (3904526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904526)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904526)Termination reason: Instruction limit
% 1.92/1.03 % (3904526)Termination phase: Saturation
% 1.92/1.03 % (3904526)Time elapsed: 0.285 s
% 1.92/1.03 % (3904526)Peak memory usage: 16 MB
% 1.92/1.03 % (3904526)Instructions burned: 478 (million)
% 1.92/1.03 % TRYING [1]
% 1.92/1.03 % (3904567)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2575876845:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 1.92/1.03 % (3904495)Instruction limit reached!
% 1.92/1.03 % (3904495)------------------------------
% 1.92/1.03 % (3904495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904495)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904495)Termination reason: Instruction limit
% 1.92/1.03 % (3904495)Termination phase: Saturation
% 1.92/1.03 % (3904495)Time elapsed: 0.389 s
% 1.92/1.03 % (3904495)Peak memory usage: 22 MB
% 1.92/1.03 % (3904495)Instructions burned: 684 (million)
% 1.92/1.03 % TRYING [2]
% 1.92/1.03 % (3904569)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=3340929970: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)
% 1.92/1.03 % (3904452) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3904433-3904452"...
% 1.92/1.03 % (3904452)...printing done.
% 1.92/1.03 % (3904452)Refutation found. Thanks to Tanya!
% 1.92/1.03 % SZS status Theorem for theBenchmark
% 1.92/1.03 % SZS output start Proof for theBenchmark
% See solution above
% 1.92/1.03 % (3904452)------------------------------
% 1.92/1.03 % (3904452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.92/1.03 % (3904452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.92/1.03 % (3904452)CaDiCaL version: 2.1.3
% 1.92/1.03 % (3904452)Termination reason: Refutation
% 1.92/1.03 % (3904452)Time elapsed: 0.512 s
% 1.92/1.03 % (3904452)Peak memory usage: 21 MB
% 1.92/1.03 % (3904452)Instructions burned: 911 (million)
% 1.92/1.03 % (3904433)Success in time 0.619 s
% 1.92/1.03 % Vampire exiting
%------------------------------------------------------------------------------