%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM924_30 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:06 PM UTC 2026
% Result : Unsatisfiable 8.68s 1.93s
% Output : Refutation 8.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 25
% Syntax : Number of formulae : 153 ( 126 unt; 0 typ; 2 def)
% Number of atoms : 190 ( 89 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 85 ( 48 ~; 30 |; 1 &)
% ( 4 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of types : 20 ( 19 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 3 prp; 0-5 aty)
% Number of functors : 111 ( 111 usr; 28 con; 0-3 aty)
% Number of variables : 93 ( 0 sgn 93 !; 0 ?; 93 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
bool: $tType ).
tff(type_def_6,type,
int: $tType ).
tff(type_def_7,type,
nat: $tType ).
tff(type_def_8,type,
real: $tType ).
tff(type_def_9,type,
fun_bool_bool: $tType ).
tff(type_def_10,type,
fun_bo1549164019l_bool: $tType ).
tff(type_def_11,type,
fun_int_bool: $tType ).
tff(type_def_12,type,
fun_int_int: $tType ).
tff(type_def_13,type,
fun_in531499254l_bool: $tType ).
tff(type_def_14,type,
fun_int_fun_int_bool: $tType ).
tff(type_def_15,type,
fun_nat_bool: $tType ).
tff(type_def_16,type,
fun_nat_int: $tType ).
tff(type_def_17,type,
fun_nat_nat: $tType ).
tff(type_def_18,type,
fun_nat_real: $tType ).
tff(type_def_19,type,
fun_nat_fun_nat_bool: $tType ).
tff(type_def_20,type,
fun_real_bool: $tType ).
tff(type_def_21,type,
fun_real_real: $tType ).
tff(type_def_22,type,
fun_re413263731l_bool: $tType ).
tff(type_def_23,type,
product_prod_int_int: $tType ).
tff(func_def_0,type,
cOMBB_1652995168ol_int: ( fun_bo1549164019l_bool * fun_int_bool ) > fun_in531499254l_bool ).
tff(func_def_1,type,
cOMBC_int_int_bool: ( fun_int_fun_int_bool * int ) > fun_int_bool ).
tff(func_def_2,type,
cOMBS_int_bool_bool: ( fun_in531499254l_bool * fun_int_bool ) > fun_int_bool ).
tff(func_def_3,type,
div_mod_int: int > fun_int_int ).
tff(func_def_4,type,
div_mod_nat: nat > fun_nat_nat ).
tff(func_def_5,type,
minus_minus_int: int > fun_int_int ).
tff(func_def_6,type,
minus_minus_nat: nat > fun_nat_nat ).
tff(func_def_7,type,
minus_minus_real: real > fun_real_real ).
tff(func_def_8,type,
one_one_int: int ).
tff(func_def_9,type,
one_one_nat: nat ).
tff(func_def_10,type,
one_one_real: real ).
tff(func_def_11,type,
plus_plus_int: int > fun_int_int ).
tff(func_def_12,type,
plus_plus_nat: nat > fun_nat_nat ).
tff(func_def_13,type,
plus_plus_real: real > fun_real_real ).
tff(func_def_14,type,
times_times_int: int > fun_int_int ).
tff(func_def_15,type,
times_times_nat: nat > fun_nat_nat ).
tff(func_def_16,type,
times_times_real: real > fun_real_real ).
tff(func_def_17,type,
zero_zero_int: int ).
tff(func_def_18,type,
zero_zero_nat: nat ).
tff(func_def_19,type,
zero_zero_real: real ).
tff(func_def_20,type,
multInv: ( int * int ) > int ).
tff(func_def_21,type,
d22set: int > fun_int_bool ).
tff(func_def_22,type,
zfact: int > int ).
tff(func_def_23,type,
zcong: ( int * int ) > fun_int_bool ).
tff(func_def_24,type,
zprime: fun_int_bool ).
tff(func_def_25,type,
bit0: int > int ).
tff(func_def_26,type,
bit1: int > int ).
tff(func_def_27,type,
min: int ).
tff(func_def_28,type,
pls: int ).
tff(func_def_29,type,
number_number_of_int: int > int ).
tff(func_def_30,type,
number_number_of_nat: int > nat ).
tff(func_def_31,type,
number267125858f_real: int > real ).
tff(func_def_32,type,
ord_less_int: fun_int_fun_int_bool ).
tff(func_def_33,type,
ord_less_nat: fun_nat_fun_nat_bool ).
tff(func_def_34,type,
ord_less_real: fun_re413263731l_bool ).
tff(func_def_35,type,
ord_less_eq_int: fun_int_fun_int_bool ).
tff(func_def_36,type,
ord_less_eq_nat: fun_nat_fun_nat_bool ).
tff(func_def_37,type,
ord_less_eq_real: fun_re413263731l_bool ).
tff(func_def_38,type,
power_power_int: int > fun_nat_int ).
tff(func_def_39,type,
power_power_nat: nat > fun_nat_nat ).
tff(func_def_40,type,
power_power_real: real > fun_nat_real ).
tff(func_def_41,type,
product_Pair_int_int: ( int * int ) > product_prod_int_int ).
tff(func_def_42,type,
legendre: ( int * int ) > int ).
tff(func_def_43,type,
quadRes: int > fun_int_bool ).
tff(func_def_44,type,
sr: int > fun_int_bool ).
tff(func_def_45,type,
standardRes: ( int * int ) > int ).
tff(func_def_46,type,
dvd_dvd_int: fun_int_fun_int_bool ).
tff(func_def_47,type,
dvd_dvd_nat: fun_nat_fun_nat_bool ).
tff(func_def_48,type,
dvd_dvd_real: fun_re413263731l_bool ).
tff(func_def_49,type,
collect_int: fun_int_bool > fun_int_bool ).
tff(func_def_50,type,
twoSqu820444569sum2sq: fun_int_bool ).
tff(func_def_51,type,
twoSqu949963151sum2sq: product_prod_int_int > int ).
tff(func_def_52,type,
inv: ( int * int ) > int ).
tff(func_def_53,type,
wset: ( int * int ) > fun_int_bool ).
tff(func_def_54,type,
fconj: fun_bo1549164019l_bool ).
tff(func_def_55,type,
hAPP_bool_bool: ( fun_bool_bool * bool ) > bool ).
tff(func_def_56,type,
hAPP_b589554111l_bool: ( fun_bo1549164019l_bool * bool ) > fun_bool_bool ).
tff(func_def_57,type,
hAPP_int_bool: ( fun_int_bool * int ) > bool ).
tff(func_def_58,type,
hAPP_int_int: ( fun_int_int * int ) > int ).
tff(func_def_59,type,
hAPP_i68813070l_bool: ( fun_in531499254l_bool * int ) > fun_bool_bool ).
tff(func_def_60,type,
hAPP_i1948725293t_bool: ( fun_int_fun_int_bool * int ) > fun_int_bool ).
tff(func_def_61,type,
hAPP_nat_bool: ( fun_nat_bool * nat ) > bool ).
tff(func_def_62,type,
hAPP_nat_int: ( fun_nat_int * nat ) > int ).
tff(func_def_63,type,
hAPP_nat_nat: ( fun_nat_nat * nat ) > nat ).
tff(func_def_64,type,
hAPP_nat_real: ( fun_nat_real * nat ) > real ).
tff(func_def_65,type,
hAPP_n1699378549t_bool: ( fun_nat_fun_nat_bool * nat ) > fun_nat_bool ).
tff(func_def_66,type,
hAPP_real_bool: ( fun_real_bool * real ) > bool ).
tff(func_def_67,type,
hAPP_real_real: ( fun_real_real * real ) > real ).
tff(func_def_68,type,
hAPP_r1134773055l_bool: ( fun_re413263731l_bool * real ) > fun_real_bool ).
tff(func_def_69,type,
member_int: ( int * fun_int_bool ) > bool ).
tff(func_def_70,type,
m: int ).
tff(func_def_71,type,
s1: int ).
tff(func_def_72,type,
s: int ).
tff(func_def_73,type,
t: int ).
tff(func_def_74,type,
sK0: int ).
tff(func_def_75,type,
sK1: int ).
tff(func_def_76,type,
sK2: int ).
tff(func_def_77,type,
sK3: int > int ).
tff(func_def_78,type,
sK4: int ).
tff(func_def_79,type,
sK5: ( int * int * int ) > int ).
tff(func_def_80,type,
sK6: ( int * int ) > int ).
tff(func_def_81,type,
sK7: ( real * nat ) > real ).
tff(func_def_82,type,
sK8: ( real * nat ) > real ).
tff(func_def_83,type,
sK9: ( nat * nat ) > nat ).
tff(func_def_84,type,
sK10: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_85,type,
sK11: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_86,type,
sK12: ( nat * fun_nat_bool ) > nat ).
tff(func_def_87,type,
sK13: int > int ).
tff(func_def_88,type,
sK14: ( fun_int_bool * int ) > int ).
tff(func_def_89,type,
sK15: ( fun_int_bool * int ) > int ).
tff(func_def_90,type,
sK16: ( int * int ) > int ).
tff(func_def_91,type,
sK17: int > int ).
tff(func_def_92,type,
sK18: int > int ).
tff(func_def_93,type,
sK19: ( fun_int_bool * int ) > int ).
tff(func_def_94,type,
sK20: fun_int_bool > int ).
tff(func_def_95,type,
sK21: ( fun_int_bool * int ) > int ).
tff(func_def_96,type,
sK22: ( fun_int_bool * int ) > int ).
tff(func_def_97,type,
sK23: ( fun_int_bool * int ) > int ).
tff(func_def_98,type,
sK24: fun_nat_nat > nat ).
tff(func_def_99,type,
sK25: fun_nat_nat > nat ).
tff(func_def_100,type,
sK26: ( nat * fun_nat_bool ) > nat ).
tff(func_def_101,type,
sK27: ( nat * nat ) > nat ).
tff(func_def_102,type,
sK28: ( int * int ) > int ).
tff(func_def_103,type,
sK29: ( fun_int_bool * int * int ) > int ).
tff(func_def_104,type,
sK30: ( fun_int_bool * int * int ) > int ).
tff(func_def_105,type,
sK31: ( fun_int_bool * int * int ) > int ).
tff(func_def_106,type,
sK32: ( fun_int_bool * int * int ) > int ).
tff(func_def_107,type,
sK34: ( int * int ) > int ).
tff(func_def_108,type,
sK35: ( nat * nat ) > nat ).
tff(func_def_109,type,
sK36: ( fun_nat_bool * nat * nat ) > nat ).
tff(func_def_110,type,
sK37: ( fun_nat_bool * nat * nat ) > nat ).
tff(pred_def_1,type,
hBOOL: bool > $o ).
tff(pred_def_2,type,
sP33: ( int * int * int * int * fun_int_bool ) > $o ).
tff(f1,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),zero_zero_int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__096t_A_060_A0_096) ).
tff(f4,axiom,
hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_t) ).
tff(f7,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),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_6_p0) ).
tff(f35,axiom,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_number__of__is__id) ).
tff(f36,axiom,
! [X0: int,X1: int] : ( hAPP_int_int(times_times_int(X0),X1) = hAPP_int_int(times_times_int(X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_zmult__commute) ).
tff(f51,axiom,
! [X0: int,X1: int] :
( 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_50_zless__le) ).
tff(f88,axiom,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_nat__1__add__1) ).
tff(f93,axiom,
! [X0: int] : ( hAPP_int_int(times_times_int(one_one_int),X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_zmult__1) ).
tff(f110,axiom,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(plus_plus_int(X0),one_one_int)),X1))
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_add1__zle__eq) ).
tff(f134,axiom,
! [X0: int,X1: int,X2: int] : ( hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)) = hAPP_int_int(plus_plus_int(X1),hAPP_int_int(plus_plus_int(X0),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_zadd__left__commute) ).
tff(f135,axiom,
! [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(X0),X1) = hAPP_int_int(plus_plus_int(X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_zadd__commute) ).
tff(f173,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_Pls__def) ).
tff(f180,axiom,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),pls) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_add__Pls__right) ).
tff(f183,axiom,
! [X0: int] : ( bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_Bit0__def) ).
tff(f199,axiom,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),number_number_of_int(bit0(bit1(pls)))) = hAPP_int_int(plus_plus_int(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_semiring__mult__2__right) ).
tff(f204,axiom,
! [X0: int] : ( hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls)))) = hAPP_int_int(times_times_int(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_power2__eq__square) ).
tff(f237,axiom,
! [X0: int] : ( 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_236_Bit1__def) ).
tff(f328,axiom,
! [X0: int,X1: int,X2: int] : ( hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)) = hAPP_int_int(times_times_int(X1),hAPP_int_int(times_times_int(X0),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_327_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J) ).
tff(f416,axiom,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_415_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J) ).
tff(f677,axiom,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X1))
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),zero_zero_int))
=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),zero_zero_int)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_676_mult__pos__neg) ).
tff(f688,axiom,
! [X0: int] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),X0)),zero_zero_int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_687_not__square__less__zero) ).
tff(f1069,axiom,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1068__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096) ).
tff(f1202,axiom,
! [X0: fun_int_fun_int_bool,X1: int,X2: int] : ( hAPP_int_bool(cOMBC_int_int_bool(X0,X1),X2) = hAPP_int_bool(hAPP_i1948725293t_bool(X0,X2),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_COMBC_000tc__Int__Oint_000tc__Int__Oint_000tc__HOL__Obool_U) ).
tff(f1562,plain,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),zero_zero_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),zero_zero_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X1)) ),
inference(ennf_transformation,[],[f677]) ).
tff(f1563,plain,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),zero_zero_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),zero_zero_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X1)) ),
inference(flattening,[],[f1562]) ).
tff(f2077,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),zero_zero_int)),
inference(cnf_transformation,[],[f1]) ).
tff(f2080,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int),
inference(cnf_transformation,[],[f4]) ).
tff(f2083,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),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,[],[f7]) ).
tff(f2123,plain,
! [X0: int] : ( number_number_of_int(X0) = X0 ),
inference(cnf_transformation,[],[f35]) ).
tff(f2124,plain,
! [X0: int,X1: int] : ( hAPP_int_int(times_times_int(X0),X1) = hAPP_int_int(times_times_int(X1),X0) ),
inference(cnf_transformation,[],[f36]) ).
tff(f2147,plain,
! [X0: int,X1: int] :
( 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,[],[f51]) ).
tff(f2208,plain,
number_number_of_nat(bit0(bit1(pls))) = hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat),
inference(cnf_transformation,[],[f88]) ).
tff(f2214,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(one_one_int),X0) = X0 ),
inference(cnf_transformation,[],[f93]) ).
tff(f2242,plain,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(plus_plus_int(X0),one_one_int)),X1)) ),
inference(cnf_transformation,[],[f110]) ).
tff(f2274,plain,
! [X2: int,X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)) = hAPP_int_int(plus_plus_int(X1),hAPP_int_int(plus_plus_int(X0),X2)) ),
inference(cnf_transformation,[],[f134]) ).
tff(f2275,plain,
! [X0: int,X1: int] : ( hAPP_int_int(plus_plus_int(X0),X1) = hAPP_int_int(plus_plus_int(X1),X0) ),
inference(cnf_transformation,[],[f135]) ).
tff(f2327,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f173]) ).
tff(f2338,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),pls) = X0 ),
inference(cnf_transformation,[],[f180]) ).
tff(f2341,plain,
! [X0: int] : ( bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0) ),
inference(cnf_transformation,[],[f183]) ).
tff(f2357,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),number_number_of_int(bit0(bit1(pls)))) ),
inference(cnf_transformation,[],[f199]) ).
tff(f2362,plain,
! [X0: int] : ( hAPP_nat_int(power_power_int(X0),number_number_of_nat(bit0(bit1(pls)))) = hAPP_int_int(times_times_int(X0),X0) ),
inference(cnf_transformation,[],[f204]) ).
tff(f2406,plain,
! [X0: int] : ( bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0) ),
inference(cnf_transformation,[],[f237]) ).
tff(f2521,plain,
! [X2: int,X0: int,X1: int] : ( hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(X1),X2)) = hAPP_int_int(times_times_int(X1),hAPP_int_int(times_times_int(X0),X2)) ),
inference(cnf_transformation,[],[f328]) ).
tff(f2628,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),X0) ),
inference(cnf_transformation,[],[f416]) ).
tff(f2955,plain,
! [X0: int,X1: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X1))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),zero_zero_int))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),zero_zero_int)) ),
inference(cnf_transformation,[],[f1563]) ).
tff(f2988,plain,
! [X0: int] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),X0)),zero_zero_int)),
inference(cnf_transformation,[],[f688]) ).
tff(f3516,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t) = twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)),
inference(cnf_transformation,[],[f1069]) ).
tff(f3722,plain,
! [X2: int,X0: fun_int_fun_int_bool,X1: int] : ( hAPP_int_bool(cOMBC_int_int_bool(X0,X1),X2) = hAPP_int_bool(hAPP_i1948725293t_bool(X0,X2),X1) ),
inference(cnf_transformation,[],[f1202]) ).
tff(f3726,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),pls)),
inference(definition_unfolding,[],[f2077,f2327]) ).
tff(f3728,plain,
hAPP_int_int(times_times_int(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)),t) = hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),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))))),one_one_int),
inference(definition_unfolding,[],[f2080,f2341,f2341,f2406,f2341,f2406]) ).
tff(f3730,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),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))),
inference(definition_unfolding,[],[f2083,f2327,f2341,f2341,f2406]) ).
tff(f3803,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = 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,[],[f2208,f2341,f2406]) ).
tff(f3898,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),number_number_of_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)))) ),
inference(definition_unfolding,[],[f2357,f2341,f2406]) ).
tff(f3903,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = 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)))) ),
inference(definition_unfolding,[],[f2362,f2341,f2406]) ).
tff(f4124,plain,
! [X0: int,X1: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),X1))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),pls)) ),
inference(definition_unfolding,[],[f2955,f2327,f2327,f2327]) ).
tff(f4138,plain,
! [X0: int] : ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),X0)),pls)),
inference(definition_unfolding,[],[f2988,f2327]) ).
tff(f4234,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(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)),t),
inference(definition_unfolding,[],[f3516,f2341,f2341,f2406]) ).
tff(f4512,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),pls)),
inference(consistent_polarity_flipping,[],[f3726]) ).
tff(f4516,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),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))),
inference(consistent_polarity_flipping,[],[f3730]) ).
tff(f4554,plain,
! [X0: int,X1: int] :
( ~ 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(consistent_polarity_flipping,[],[f2147]) ).
tff(f4629,plain,
! [X0: int,X1: int] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(plus_plus_int(X0),one_one_int)),X1)) ),
inference(consistent_polarity_flipping,[],[f2242]) ).
tff(f5013,plain,
! [X0: int,X1: int] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),X1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),pls)) ),
inference(consistent_polarity_flipping,[],[f4124]) ).
tff(f5046,plain,
! [X0: int] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),X0)),pls)),
inference(consistent_polarity_flipping,[],[f4138]) ).
tff(f6571,plain,
! [X0: int,X1: int] :
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_eq_int,X0),X1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X0)) ),
inference(superposition,[],[f4554,f3722]) ).
tff(f9646,plain,
! [X0: int] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(X0),X0)),one_one_int)),pls)),
inference(resolution,[],[f4629,f5046]) ).
tff(f9648,plain,
! [X0: int] : hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_eq_int,pls),hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(X0),X0)),one_one_int))),
inference(forward_demodulation,[],[f9646,f3722]) ).
tff(f9656,plain,
! [X0: int] : hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_eq_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(X0),X0)))),
inference(forward_demodulation,[],[f9648,f2275]) ).
tff(f22650,plain,
! [X0: int,X1: int] :
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),hAPP_int_int(times_times_int(X1),X0)))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),X1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f5013,f3722]) ).
tff(f25915,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),
inference(forward_demodulation,[],[f3803,f2628]) ).
tff(f25916,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls))),
inference(forward_demodulation,[],[f25915,f2338]) ).
tff(f25917,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))),
inference(forward_demodulation,[],[f25916,f2124]) ).
tff(f25918,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(times_times_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))),
inference(forward_demodulation,[],[f25917,f2338]) ).
tff(f25919,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),
inference(forward_demodulation,[],[f25918,f2214]) ).
tff(f35329,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),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(forward_demodulation,[],[f3898,f2123]) ).
tff(f35330,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))) ),
inference(forward_demodulation,[],[f35329,f2628]) ).
tff(f35331,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls))) ),
inference(forward_demodulation,[],[f35330,f2338]) ).
tff(f35332,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))) ),
inference(forward_demodulation,[],[f35331,f2124]) ).
tff(f35333,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),hAPP_int_int(times_times_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))) ),
inference(forward_demodulation,[],[f35332,f2338]) ).
tff(f35334,plain,
! [X0: int] : ( hAPP_int_int(plus_plus_int(X0),X0) = hAPP_int_int(times_times_int(X0),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)) ),
inference(forward_demodulation,[],[f35333,f2214]) ).
tff(f35999,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))) ),
inference(forward_demodulation,[],[f3903,f2628]) ).
tff(f36000,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls)))) ),
inference(forward_demodulation,[],[f35999,f2338]) ).
tff(f36001,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))) ),
inference(forward_demodulation,[],[f36000,f2124]) ).
tff(f36002,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),pls)))) ),
inference(forward_demodulation,[],[f36001,f35334]) ).
tff(f36003,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))) ),
inference(forward_demodulation,[],[f36002,f2274]) ).
tff(f36004,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),pls)))) ),
inference(forward_demodulation,[],[f36003,f2338]) ).
tff(f36005,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int))) ),
inference(forward_demodulation,[],[f36004,f2338]) ).
tff(f36006,plain,
! [X0: int] : ( hAPP_int_int(times_times_int(X0),X0) = hAPP_nat_int(power_power_int(X0),hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat)) ),
inference(forward_demodulation,[],[f36005,f25919]) ).
tff(f52349,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_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)))),
inference(forward_demodulation,[],[f4516,f2275]) ).
tff(f52350,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),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)))))))),
inference(forward_demodulation,[],[f52349,f2124]) ).
tff(f52351,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),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))))))),
inference(forward_demodulation,[],[f52350,f2123]) ).
tff(f52352,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_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))))))),
inference(forward_demodulation,[],[f52351,f2628]) ).
tff(f52353,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))))),
inference(forward_demodulation,[],[f52352,f2628]) ).
tff(f52354,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls))))))),
inference(forward_demodulation,[],[f52353,f2338]) ).
tff(f52355,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),
inference(forward_demodulation,[],[f52354,f2124]) ).
tff(f52356,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),
inference(forward_demodulation,[],[f52355,f2521]) ).
tff(f52357,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),
inference(forward_demodulation,[],[f52356,f35334]) ).
tff(f52358,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),one_one_int))))))),
inference(forward_demodulation,[],[f52357,f2274]) ).
tff(f52359,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))))),
inference(forward_demodulation,[],[f52358,f2275]) ).
tff(f52360,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))))),
inference(forward_demodulation,[],[f52359,f2338]) ).
tff(f52361,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))))),
inference(forward_demodulation,[],[f52360,f2521]) ).
tff(f52362,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),
inference(forward_demodulation,[],[f52361,f2214]) ).
tff(f55199,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_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))),t),
inference(forward_demodulation,[],[f4234,f2275]) ).
tff(f55200,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),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))))))),t),
inference(forward_demodulation,[],[f55199,f2124]) ).
tff(f55201,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),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)))))),t),
inference(forward_demodulation,[],[f55200,f2123]) ).
tff(f55202,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_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)))))),t),
inference(forward_demodulation,[],[f55201,f2628]) ).
tff(f55203,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))))),t),
inference(forward_demodulation,[],[f55202,f2628]) ).
tff(f55204,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls)))))),t),
inference(forward_demodulation,[],[f55203,f2338]) ).
tff(f55205,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),t),
inference(forward_demodulation,[],[f55204,f2124]) ).
tff(f55206,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),t),
inference(forward_demodulation,[],[f55205,f2521]) ).
tff(f55207,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),t),
inference(forward_demodulation,[],[f55206,f35334]) ).
tff(f55208,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),one_one_int)))))),t),
inference(forward_demodulation,[],[f55207,f2274]) ).
tff(f55209,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),t),
inference(forward_demodulation,[],[f55208,f2275]) ).
tff(f55210,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(times_times_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),t),
inference(forward_demodulation,[],[f55209,f2338]) ).
tff(f55211,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),t),
inference(forward_demodulation,[],[f55210,f2521]) ).
tff(f55212,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),t),
inference(forward_demodulation,[],[f55211,f2214]) ).
tff(f55913,plain,
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),pls)) ),
inference(superposition,[],[f22650,f55212]) ).
tff(f55921,plain,
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),pls)) ),
inference(forward_subsumption_resolution,[],[f55913,f52362]) ).
tff(f55973,plain,
~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)))),
inference(forward_subsumption_resolution,[],[f55921,f4512]) ).
tff(f55975,definition,
( spl38_395
<=> hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_eq_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)))) ),
introduced(definition,[new_symbols(definition,[spl38_395])],[avatar_definition]) ).
tff(f55976,plain,
( hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_eq_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int))))
| ~ spl38_395 ),
inference(avatar_component_clause,[],[f55975]) ).
tff(f55977,plain,
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_eq_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int))))
| spl38_395 ),
inference(avatar_component_clause,[],[f55975]) ).
tff(f59218,plain,
hAPP_int_int(times_times_int(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)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),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(forward_demodulation,[],[f3728,f2275]) ).
tff(f59219,plain,
hAPP_int_int(times_times_int(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(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),
inference(forward_demodulation,[],[f59218,f2628]) ).
tff(f59220,plain,
hAPP_int_int(times_times_int(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(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),pls))))),
inference(forward_demodulation,[],[f59219,f2338]) ).
tff(f59221,plain,
hAPP_int_int(times_times_int(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(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))),
inference(forward_demodulation,[],[f59220,f2124]) ).
tff(f59222,plain,
hAPP_int_int(times_times_int(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(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(one_one_int),pls))))),
inference(forward_demodulation,[],[f59221,f35334]) ).
tff(f59223,plain,
hAPP_int_int(times_times_int(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(one_one_int),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),
inference(forward_demodulation,[],[f59222,f2274]) ).
tff(f59224,plain,
hAPP_int_int(times_times_int(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(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),pls))),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),pls))))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),pls))))),
inference(forward_demodulation,[],[f59223,f2338]) ).
tff(f59225,plain,
hAPP_int_int(times_times_int(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(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),
inference(forward_demodulation,[],[f59224,f2338]) ).
tff(f59226,plain,
hAPP_int_int(times_times_int(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(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(power_power_int(s),hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat))),
inference(forward_demodulation,[],[f59225,f25919]) ).
tff(f59227,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(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(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),t),
inference(forward_demodulation,[],[f59226,f36006]) ).
tff(f59228,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m))),t),
inference(forward_demodulation,[],[f59227,f2275]) ).
tff(f59229,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),t),
inference(forward_demodulation,[],[f59228,f2124]) ).
tff(f59230,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))),t),
inference(forward_demodulation,[],[f59229,f2123]) ).
tff(f59231,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),one_one_int))))),t),
inference(forward_demodulation,[],[f59230,f2274]) ).
tff(f59232,plain,
hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),t) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)),
inference(forward_demodulation,[],[f59231,f2275]) ).
tff(f59233,plain,
twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)),
inference(forward_demodulation,[],[f59232,f55212]) ).
tff(f59701,definition,
( spl38_484
<=> hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)))) ),
introduced(definition,[new_symbols(definition,[spl38_484])],[avatar_definition]) ).
tff(f59703,plain,
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int))))
| spl38_484 ),
inference(avatar_component_clause,[],[f59701]) ).
tff(f64538,plain,
~ spl38_484,
inference(avatar_split_clause,[],[f55973,f59701]) ).
tff(f69741,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int))),pls))
| ~ spl38_395 ),
inference(resolution,[],[f6571,f55976]) ).
tff(f69771,plain,
( hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int))))
| ~ spl38_395 ),
inference(forward_demodulation,[],[f69741,f3722]) ).
tff(f69775,plain,
( $false
| ~ spl38_395
| spl38_484 ),
inference(forward_subsumption_resolution,[],[f69771,f59703]) ).
tff(f69776,plain,
( ~ spl38_395
| spl38_484 ),
inference(avatar_contradiction_clause,[],[f69775]) ).
tff(f73841,plain,
hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_eq_int,pls),twoSqu949963151sum2sq(product_Pair_int_int(s,one_one_int)))),
inference(superposition,[],[f9656,f59233]) ).
tff(f73842,plain,
( $false
| spl38_395 ),
inference(forward_subsumption_resolution,[],[f73841,f55977]) ).
tff(f73843,plain,
spl38_395,
inference(avatar_contradiction_clause,[],[f73842]) ).
cnf(s1249,plain,
~ spl38_484,
inference(sat_conversion,[],[f64538]) ).
cnf(s1404,plain,
( ~ spl38_395
| spl38_484 ),
inference(sat_conversion,[],[f69776]) ).
cnf(s1433,plain,
spl38_395,
inference(sat_conversion,[],[f73843]) ).
cnf(s1437,plain,
spl38_484,
inference(rat,[],[s1404,s1433]) ).
cnf(s1443,plain,
$false,
inference(rat,[],[s1249,s1437]) ).
tff(f73864,plain,
$false,
inference(avatar_sat_refutation,[],[s1443]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924_30 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n001.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 21:47:01 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/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
% 8.68/1.93 % (3987844)Will run a generic schedule for satisfiability detection.
% 8.68/1.93 % (3987892)% WARNING: option uhcvi not known.
% 8.68/1.93 % (3987892)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3901518093:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 8.68/1.93 % (3987891)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2993600913_2999 on theBenchmark for (2999ds/0Mi)
% 8.68/1.93 % (3987893)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1705777440:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 8.68/1.93 % (3987895)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3211442331:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 8.68/1.93 % (3987894)dis+10_1_sil=32000:sp=arity:random_seed=1371585410:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 8.68/1.93 % (3987896)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3308964539:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 8.68/1.93 % (3987897)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2746057020:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 8.68/1.93 % (3987894)Instruction limit reached!
% 8.68/1.93 % (3987894)------------------------------
% 8.68/1.93 % (3987894)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987894)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987894)Termination reason: Instruction limit
% 8.68/1.93 % (3987894)Termination phase: Saturation
% 8.68/1.93 % (3987894)Time elapsed: 0.047 s
% 8.68/1.93 % (3987894)Peak memory usage: 13 MB
% 8.68/1.93 % (3987894)Instructions burned: 105 (million)
% 8.68/1.93 % (3987895)Instruction limit reached!
% 8.68/1.93 % (3987895)------------------------------
% 8.68/1.93 % (3987895)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987895)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987895)Termination reason: Instruction limit
% 8.68/1.93 % (3987895)Termination phase: Property scanning
% 8.68/1.93 % (3987895)Time elapsed: 0.053 s
% 8.68/1.93 % (3987895)Peak memory usage: 13 MB
% 8.68/1.93 % (3987895)Instructions burned: 117 (million)
% 8.68/1.93 % (3987896)Instruction limit reached!
% 8.68/1.93 % (3987896)------------------------------
% 8.68/1.93 % (3987896)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987896)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987896)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987896)Termination reason: Instruction limit
% 8.68/1.93 % (3987896)Termination phase: Saturation
% 8.68/1.93 % (3987896)Time elapsed: 0.067 s
% 8.68/1.93 % (3987896)Peak memory usage: 14 MB
% 8.68/1.93 % (3987896)Instructions burned: 132 (million)
% 8.68/1.93 % (3987905)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3752548517:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.68/1.93 % (3987906)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1345091805:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 8.68/1.93 % (3987897)Instruction limit reached!
% 8.68/1.93 % (3987897)------------------------------
% 8.68/1.93 % (3987897)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987897)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987897)Termination reason: Instruction limit
% 8.68/1.93 % (3987897)Termination phase: Saturation
% 8.68/1.93 % (3987897)Time elapsed: 0.081 s
% 8.68/1.93 % (3987897)Peak memory usage: 15 MB
% 8.68/1.93 % (3987897)Instructions burned: 160 (million)
% 8.68/1.93 % (3987907)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=1116200581:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 8.68/1.93 % (3987910)ott-21_1_sil=16000:fs=off:random_seed=1884825503:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.68/1.93 % (3987906)Instruction limit reached!
% 8.68/1.93 % (3987906)------------------------------
% 8.68/1.93 % (3987906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987906)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987906)Termination reason: Instruction limit
% 8.68/1.93 % (3987906)Termination phase: Property scanning
% 8.68/1.93 % (3987906)Time elapsed: 0.059 s
% 8.68/1.93 % (3987906)Peak memory usage: 13 MB
% 8.68/1.93 % (3987906)Instructions burned: 133 (million)
% 8.68/1.93 % (3987913)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3587480456:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 8.68/1.93 % (3987910)Instruction limit reached!
% 8.68/1.93 % (3987910)------------------------------
% 8.68/1.93 % (3987910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987910)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987910)Termination reason: Instruction limit
% 8.68/1.93 % (3987910)Termination phase: Saturation
% 8.68/1.93 % (3987910)Time elapsed: 0.081 s
% 8.68/1.93 % (3987910)Peak memory usage: 14 MB
% 8.68/1.93 % (3987910)Instructions burned: 180 (million)
% 8.68/1.93 % (3987915)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1680672458:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.68/1.93 % (3987905)Instruction limit reached!
% 8.68/1.93 % (3987905)------------------------------
% 8.68/1.93 % (3987905)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987905)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987905)Termination reason: Instruction limit
% 8.68/1.93 % (3987905)Termination phase: Finite model building preprocessing
% 8.68/1.93 % (3987905)Time elapsed: 0.337 s
% 8.68/1.93 % (3987905)Peak memory usage: 21 MB
% 8.68/1.93 % (3987905)Instructions burned: 714 (million)
% 8.68/1.93 % (3987917)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=254032901:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 8.68/1.93 % (3987913)Instruction limit reached!
% 8.68/1.93 % (3987913)------------------------------
% 8.68/1.93 % (3987913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987913)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987913)Termination reason: Instruction limit
% 8.68/1.93 % (3987913)Termination phase: Saturation
% 8.68/1.93 % (3987913)Time elapsed: 0.289 s
% 8.68/1.93 % (3987913)Peak memory usage: 16 MB
% 8.68/1.93 % (3987913)Instructions burned: 477 (million)
% 8.68/1.93 % (3987919)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=785259108:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 8.68/1.93 % (3987907)Instruction limit reached!
% 8.68/1.93 % (3987907)------------------------------
% 8.68/1.93 % (3987907)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987907)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987907)Termination reason: Instruction limit
% 8.68/1.93 % (3987907)Termination phase: Saturation
% 8.68/1.93 % (3987907)Time elapsed: 0.414 s
% 8.68/1.93 % (3987907)Peak memory usage: 20 MB
% 8.68/1.93 % (3987907)Instructions burned: 685 (million)
% 8.68/1.93 % (3987921)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=4178644352:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 8.68/1.93 % (3987915)Instruction limit reached!
% 8.68/1.93 % (3987915)------------------------------
% 8.68/1.93 % (3987915)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987915)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987915)Termination reason: Instruction limit
% 8.68/1.93 % (3987915)Termination phase: Finite model building preprocessing
% 8.68/1.93 % (3987915)Time elapsed: 0.414 s
% 8.68/1.93 % (3987915)Peak memory usage: 23 MB
% 8.68/1.93 % (3987915)Instructions burned: 866 (million)
% 8.68/1.93 % (3987923)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=769787491:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 8.68/1.93 % (3987919)Instruction limit reached!
% 8.68/1.93 % (3987919)------------------------------
% 8.68/1.93 % (3987919)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987919)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987919)Termination reason: Instruction limit
% 8.68/1.93 % (3987919)Termination phase: Finite model building preprocessing
% 8.68/1.93 % (3987919)Time elapsed: 0.429 s
% 8.68/1.93 % (3987919)Peak memory usage: 23 MB
% 8.68/1.93 % (3987919)Instructions burned: 890 (million)
% 8.68/1.93 % (3987925)fmb+10_1_sil=64000:random_seed=292364620:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 8.68/1.93 % (3987921)Instruction limit reached!
% 8.68/1.93 % (3987921)------------------------------
% 8.68/1.93 % (3987921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987921)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987921)Termination reason: Instruction limit
% 8.68/1.93 % (3987921)Termination phase: Saturation
% 8.68/1.93 % (3987921)Time elapsed: 0.416 s
% 8.68/1.93 % (3987921)Peak memory usage: 18 MB
% 8.68/1.93 % (3987921)Instructions burned: 692 (million)
% 8.68/1.93 % (3987927)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4260782186:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 8.68/1.93 % (3987923)Instruction limit reached!
% 8.68/1.93 % (3987923)------------------------------
% 8.68/1.93 % (3987923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987923)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987923)Termination reason: Instruction limit
% 8.68/1.93 % (3987923)Termination phase: Saturation
% 8.68/1.93 % (3987923)Time elapsed: 0.477 s
% 8.68/1.93 % (3987923)Peak memory usage: 19 MB
% 8.68/1.93 % (3987923)Instructions burned: 879 (million)
% 8.68/1.93 % (3987917)Instruction limit reached!
% 8.68/1.93 % (3987917)------------------------------
% 8.68/1.93 % (3987917)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987917)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987917)Termination reason: Instruction limit
% 8.68/1.93 % (3987917)Termination phase: Saturation
% 8.68/1.93 % (3987917)Time elapsed: 0.693 s
% 8.68/1.93 % (3987917)Peak memory usage: 23 MB
% 8.68/1.93 % (3987917)Instructions burned: 1179 (million)
% 8.68/1.93 % (3987929)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2411193187:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 8.68/1.93 % (3987930)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3365136779:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 8.68/1.93 % (3987892) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3987844-3987892"...
% 8.68/1.93 % (3987892)...printing done.
% 8.68/1.93 % (3987892)Refutation found. Thanks to Tanya!
% 8.68/1.93 % SZS status Unsatisfiable for theBenchmark
% 8.68/1.93 % SZS output start Proof for theBenchmark
% See solution above
% 8.68/1.93 % (3987892)------------------------------
% 8.68/1.93 % (3987892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.68/1.93 % (3987892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.68/1.93 % (3987892)CaDiCaL version: 2.1.3
% 8.68/1.93 % (3987892)Termination reason: Refutation
% 8.68/1.93 % (3987892)Time elapsed: 1.417 s
% 8.68/1.93 % (3987892)Peak memory usage: 40 MB
% 8.68/1.93 % (3987892)Instructions burned: 4653 (million)
% 8.68/1.93 % (3987844)Success in time 1.521 s
% 8.68/1.93 % Vampire exiting
%------------------------------------------------------------------------------