%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : NUM924+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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 : Theorem 21.40s 3.55s
% Output : Refutation 21.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 24
% Syntax : Number of formulae : 161 ( 118 unt; 2 def)
% Number of atoms : 224 ( 85 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 114 ( 51 ~; 54 |; 0 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 17 ( 3 avg)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-2 aty)
% Number of variables : 118 ( 0 sgn 118 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__096t_A_060_A0_096) ).
fof(f29,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/sandbox2/benchmark/theBenchmark.p',fact_3_t) ).
fof(f32,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/sandbox2/benchmark/theBenchmark.p',fact_6_p0) ).
fof(f52,axiom,
! [X0] : hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(bit1(pls)),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_26_add__special_I2_J) ).
fof(f61,axiom,
! [X0,X1] : hAPP_int_int(times_times_int(X0),X1) = hAPP_int_int(times_times_int(X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_35_zmult__commute) ).
fof(f113,axiom,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_nat__1__add__1) ).
fof(f158,axiom,
! [X0,X1,X2] : hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(X0),X1)),X2) = hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_zadd__assoc) ).
fof(f159,axiom,
! [X0,X1,X2] : 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/sandbox2/benchmark/theBenchmark.p',fact_133_zadd__left__commute) ).
fof(f160,axiom,
! [X0,X1] : hAPP_int_int(plus_plus_int(X0),X1) = hAPP_int_int(plus_plus_int(X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_134_zadd__commute) ).
fof(f186,axiom,
one_one_int = number_number_of_int(bit1(pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_160_one__is__num__one) ).
fof(f198,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_172_Pls__def) ).
fof(f208,axiom,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_Bit0__def) ).
fof(f213,axiom,
! [X0] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),number_number_of_int(X0)) = number_number_of_int(bit0(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_187_double__number__of__Bit0) ).
fof(f229,axiom,
! [X0] : 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/sandbox2/benchmark/theBenchmark.p',fact_203_power2__eq__square) ).
fof(f262,axiom,
! [X0] : bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_236_Bit1__def) ).
fof(f393,axiom,
! [X0] : hAPP_int_int(times_times_int(X0),zero_zero_int) = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_367_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J) ).
fof(f441,axiom,
! [X0] : 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/sandbox2/benchmark/theBenchmark.p',fact_415_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J) ).
fof(f685,axiom,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),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),hAPP_int_int(times_times_int(X1),X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_659_mult__neg__neg) ).
fof(f688,axiom,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),zero_zero_int))
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X0))
=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),zero_zero_int)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_662_mult__neg__pos) ).
fof(f690,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X2),zero_zero_int))
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X2),X0)),hAPP_int_int(times_times_int(X2),X1)))
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_664_mult__less__cancel__left__neg) ).
fof(f1227,axiom,
! [X0,X1,X2] : hAPP_int_bool(cOMBC_int_int_bool(X0,X1),X2) = hAPP_int_bool(hAPP_i1948725293t_bool(X0,X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_COMBC_1_1_COMBC_000tc__Int__Oint_000tc__Int__Oint_000tc__HOL__Obool_U) ).
fof(f1230,conjecture,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1231,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(negated_conjecture,[status(cth)],[f1230]) ).
fof(f1235,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(flattening,[],[f1231]) ).
fof(f1643,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(times_times_int(X1),X0)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),zero_zero_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),zero_zero_int)) ),
inference(ennf_transformation,[],[f685]) ).
fof(f1644,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(times_times_int(X1),X0)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),zero_zero_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),zero_zero_int)) ),
inference(flattening,[],[f1643]) ).
fof(f1649,plain,
! [X0,X1] :
( 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,zero_zero_int),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),zero_zero_int)) ),
inference(ennf_transformation,[],[f688]) ).
fof(f1650,plain,
! [X0,X1] :
( 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,zero_zero_int),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),zero_zero_int)) ),
inference(flattening,[],[f1649]) ).
fof(f1652,plain,
! [X0,X1,X2] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X2),X0)),hAPP_int_int(times_times_int(X2),X1)))
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X0)) )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X2),zero_zero_int)) ),
inference(ennf_transformation,[],[f690]) ).
fof(f2227,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),zero_zero_int)),
inference(cnf_transformation,[],[f26]) ).
fof(f2230,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,[],[f29]) ).
fof(f2233,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,[],[f32]) ).
fof(f2265,plain,
! [X0] : hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(bit1(pls)),X0)),
inference(cnf_transformation,[],[f52]) ).
fof(f2275,plain,
! [X0,X1] : hAPP_int_int(times_times_int(X0),X1) = hAPP_int_int(times_times_int(X1),X0),
inference(cnf_transformation,[],[f61]) ).
fof(f2359,plain,
number_number_of_nat(bit0(bit1(pls))) = hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat),
inference(cnf_transformation,[],[f113]) ).
fof(f2424,plain,
! [X2,X0,X1] : hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(X0),X1)),X2) = hAPP_int_int(plus_plus_int(X0),hAPP_int_int(plus_plus_int(X1),X2)),
inference(cnf_transformation,[],[f158]) ).
fof(f2425,plain,
! [X2,X0,X1] : 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,[],[f159]) ).
fof(f2426,plain,
! [X0,X1] : hAPP_int_int(plus_plus_int(X0),X1) = hAPP_int_int(plus_plus_int(X1),X0),
inference(cnf_transformation,[],[f160]) ).
fof(f2460,plain,
one_one_int = number_number_of_int(bit1(pls)),
inference(cnf_transformation,[],[f186]) ).
fof(f2478,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f198]) ).
fof(f2492,plain,
! [X0] : bit0(X0) = hAPP_int_int(plus_plus_int(X0),X0),
inference(cnf_transformation,[],[f208]) ).
fof(f2497,plain,
! [X0] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),number_number_of_int(X0)) = number_number_of_int(bit0(X0)),
inference(cnf_transformation,[],[f213]) ).
fof(f2513,plain,
! [X0] : 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,[],[f229]) ).
fof(f2557,plain,
! [X0] : bit1(X0) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),X0)),X0),
inference(cnf_transformation,[],[f262]) ).
fof(f2718,plain,
! [X0] : zero_zero_int = hAPP_int_int(times_times_int(X0),zero_zero_int),
inference(cnf_transformation,[],[f393]) ).
fof(f2781,plain,
! [X0] : 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,[],[f441]) ).
fof(f3091,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),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),hAPP_int_int(times_times_int(X1),X0))) ),
inference(cnf_transformation,[],[f1644]) ).
fof(f3094,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),zero_zero_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X0))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),zero_zero_int)) ),
inference(cnf_transformation,[],[f1650]) ).
fof(f3098,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X2),zero_zero_int))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X2),X0)),hAPP_int_int(times_times_int(X2),X1))) ),
inference(cnf_transformation,[],[f1652]) ).
fof(f3902,plain,
! [X2,X0,X1] : hAPP_int_bool(cOMBC_int_int_bool(X0,X1),X2) = hAPP_int_bool(hAPP_i1948725293t_bool(X0,X2),X1),
inference(cnf_transformation,[],[f1227]) ).
fof(f3905,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(cnf_transformation,[],[f1235]) ).
fof(f3911,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),pls)),
inference(definition_unfolding,[],[f2227,f2478]) ).
fof(f3913,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,[],[f2230,f2492,f2492,f2557,f2492,f2557]) ).
fof(f3915,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,[],[f2233,f2478,f2492,f2492,f2557]) ).
fof(f3947,plain,
! [X0] : hAPP_int_int(plus_plus_int(one_one_int),number_number_of_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)),X0)),
inference(definition_unfolding,[],[f2265,f2557]) ).
fof(f3988,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,[],[f2359,f2492,f2557]) ).
fof(f4043,plain,
one_one_int = number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),
inference(definition_unfolding,[],[f2460,f2557]) ).
fof(f4072,plain,
! [X0] : hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(X0),X0)),
inference(definition_unfolding,[],[f2497,f2492]) ).
fof(f4088,plain,
! [X0] : 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,[],[f2513,f2492,f2557]) ).
fof(f4189,plain,
! [X0] : pls = hAPP_int_int(times_times_int(X0),pls),
inference(definition_unfolding,[],[f2718,f2478,f2478]) ).
fof(f4302,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),pls))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(times_times_int(X1),X0))) ),
inference(definition_unfolding,[],[f3091,f2478,f2478,f2478]) ).
fof(f4303,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),pls))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),X0))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),pls)) ),
inference(definition_unfolding,[],[f3094,f2478,f2478,f2478]) ).
fof(f4304,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X2),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X2),X0)),hAPP_int_int(times_times_int(X2),X1))) ),
inference(definition_unfolding,[],[f3098,f2478]) ).
fof(f4522,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,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)),pls)),
inference(definition_unfolding,[],[f3905,f2492,f2557,f2478]) ).
fof(f4714,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),pls)),
inference(consistent_polarity_flipping,[],[f3911]) ).
fof(f4718,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,[],[f3915]) ).
fof(f5197,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(times_times_int(X1),X0)))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),pls)) ),
inference(consistent_polarity_flipping,[],[f4302]) ).
fof(f5200,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X1),X0)),pls)) ),
inference(consistent_polarity_flipping,[],[f4303]) ).
fof(f5203,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X0))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X2),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X2),X0)),hAPP_int_int(times_times_int(X2),X1))) ),
inference(consistent_polarity_flipping,[],[f4304]) ).
fof(f5866,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,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)),pls)),
inference(consistent_polarity_flipping,[],[f4522]) ).
fof(f6752,plain,
one_one_int = number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),pls))),
inference(forward_demodulation,[],[f4043,f2426]) ).
fof(f6753,plain,
one_one_int = number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int))),
inference(forward_demodulation,[],[f6752,f2426]) ).
fof(f16273,plain,
! [X0] : hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(pls),X0))),
inference(forward_demodulation,[],[f3947,f2424]) ).
fof(f16274,plain,
! [X0] : hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),X0))),
inference(forward_demodulation,[],[f16273,f2425]) ).
fof(f16275,plain,
! [X0] : hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),X0)))),
inference(forward_demodulation,[],[f16274,f2424]) ).
fof(f16276,plain,
! [X0] : hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(X0)) = number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),X0)))),
inference(forward_demodulation,[],[f16275,f2425]) ).
fof(f31062,plain,
! [X0,X1] :
( ~ 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,X1),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),X0)) ),
inference(forward_demodulation,[],[f5200,f3902]) ).
fof(f35367,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(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))),
inference(forward_demodulation,[],[f3988,f2425]) ).
fof(f35368,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),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls)))),
inference(forward_demodulation,[],[f35367,f2424]) ).
fof(f35369,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_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)),pls)))),
inference(forward_demodulation,[],[f35368,f2425]) ).
fof(f35370,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))),
inference(forward_demodulation,[],[f35369,f2426]) ).
fof(f35371,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_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),pls)),pls))))),
inference(forward_demodulation,[],[f35370,f2425]) ).
fof(f35372,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),pls)))))),
inference(forward_demodulation,[],[f35371,f2426]) ).
fof(f35373,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),pls)))))),
inference(forward_demodulation,[],[f35372,f2425]) ).
fof(f35374,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),one_one_int)))))),
inference(forward_demodulation,[],[f35373,f2426]) ).
fof(f35375,plain,
hAPP_nat_nat(plus_plus_nat(one_one_nat),one_one_nat) = number_number_of_nat(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),
inference(forward_demodulation,[],[f35374,f2425]) ).
fof(f45276,plain,
! [X0] :
( 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(X0),pls)),hAPP_int_int(times_times_int(X0),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(resolution,[],[f5203,f5866]) ).
fof(f45308,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45276,f2426]) ).
fof(f45325,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45308,f2425]) ).
fof(f45333,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls)))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45325,f2424]) ).
fof(f45338,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_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)),pls)))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45333,f2425]) ).
fof(f45341,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45338,f2426]) ).
fof(f45344,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_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),pls)),pls))))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45341,f2425]) ).
fof(f45347,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),pls)))))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45344,f2426]) ).
fof(f45350,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),pls)))))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45347,f2425]) ).
fof(f45351,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),one_one_int)))))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45350,f2426]) ).
fof(f45352,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45351,f2425]) ).
fof(f45353,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(X0),pls)),hAPP_int_int(times_times_int(X0),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))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45352,f35375]) ).
fof(f45354,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(times_times_int(X0),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))))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45353,f4189]) ).
fof(f50688,plain,
! [X0] : 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(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls)))),
inference(forward_demodulation,[],[f4088,f2425]) ).
fof(f50689,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))),
inference(forward_demodulation,[],[f50688,f2424]) ).
fof(f50690,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_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)),pls))))),
inference(forward_demodulation,[],[f50689,f2425]) ).
fof(f50691,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))))),
inference(forward_demodulation,[],[f50690,f2426]) ).
fof(f50692,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_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),pls)),pls)))))),
inference(forward_demodulation,[],[f50691,f2425]) ).
fof(f50693,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),pls))))))),
inference(forward_demodulation,[],[f50692,f2426]) ).
fof(f50694,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),pls))))))),
inference(forward_demodulation,[],[f50693,f2425]) ).
fof(f50695,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),one_one_int))))))),
inference(forward_demodulation,[],[f50694,f2426]) ).
fof(f50696,plain,
! [X0] : 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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))))),
inference(forward_demodulation,[],[f50695,f2425]) ).
fof(f50697,plain,
! [X0] : 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,[],[f50696,f35375]) ).
fof(f73810,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,[],[f4718,f2426]) ).
fof(f73811,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,[],[f73810,f2275]) ).
fof(f73812,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)),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(forward_demodulation,[],[f73811,f4072]) ).
fof(f73813,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)),number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)))))))),
inference(forward_demodulation,[],[f73812,f4072]) ).
fof(f73814,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)),number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),pls))))))))),
inference(forward_demodulation,[],[f73813,f2426]) ).
fof(f73815,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)),number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int))))))))),
inference(forward_demodulation,[],[f73814,f2426]) ).
fof(f73816,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)),one_one_int)))))),
inference(forward_demodulation,[],[f73815,f6753]) ).
fof(f73817,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(one_one_int),one_one_int)))))),
inference(forward_demodulation,[],[f73816,f2781]) ).
fof(f73818,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(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))),
inference(forward_demodulation,[],[f73817,f2781]) ).
fof(f73819,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(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),one_one_int)))))),
inference(forward_demodulation,[],[f73818,f2425]) ).
fof(f73820,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,[],[f73819,f2426]) ).
fof(f76004,definition,
( spl38_1542
<=> hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)))) ),
introduced(definition,[new_symbols(definition,[spl38_1542])],[avatar_definition]) ).
fof(f80482,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,[],[f3913,f2426]) ).
fof(f80483,plain,
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(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))) = 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(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))),m)),one_one_int)),t),
inference(forward_demodulation,[],[f80482,f2425]) ).
fof(f80484,plain,
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(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))) = 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(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))),m))),t),
inference(forward_demodulation,[],[f80483,f2426]) ).
fof(f80485,plain,
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(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))) = 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(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))))),t),
inference(forward_demodulation,[],[f80484,f2275]) ).
fof(f80486,plain,
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(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))) = 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)),number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls))))))),t),
inference(forward_demodulation,[],[f80485,f4072]) ).
fof(f80487,plain,
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(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls)))))) = 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)),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls)),pls)))))))),t),
inference(forward_demodulation,[],[f80486,f2424]) ).
fof(f80488,plain,
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(pls),hAPP_int_int(plus_plus_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)),pls)))))) = 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)),number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_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)),pls)))))))),t),
inference(forward_demodulation,[],[f80487,f2425]) ).
fof(f80489,plain,
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(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),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),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)),number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))))))),t),
inference(forward_demodulation,[],[f80488,f2426]) ).
fof(f80490,plain,
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(pls),hAPP_int_int(plus_plus_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),pls)),pls))))))) = 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)),number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_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),pls)),pls))))))))),t),
inference(forward_demodulation,[],[f80489,f2425]) ).
fof(f80491,plain,
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(pls),hAPP_int_int(plus_plus_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),pls)),pls))))))) = 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(one_one_int),number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),pls)),pls))))))),t),
inference(forward_demodulation,[],[f80490,f16276]) ).
fof(f80492,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),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),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(one_one_int),number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),pls)))))))),t),
inference(forward_demodulation,[],[f80491,f2426]) ).
fof(f80493,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),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(one_one_int),number_number_of_int(hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int)))))))),t),
inference(forward_demodulation,[],[f80492,f2426]) ).
fof(f80494,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),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(one_one_int),one_one_int))))),t),
inference(forward_demodulation,[],[f80493,f6753]) ).
fof(f80495,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int)))))))) = hAPP_int_int(times_times_int(t),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(one_one_int),one_one_int))))),
inference(forward_demodulation,[],[f80494,f2275]) ).
fof(f80496,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int)))))))) = hAPP_int_int(times_times_int(t),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))))),
inference(forward_demodulation,[],[f80495,f2781]) ).
fof(f80497,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int)))))))) = hAPP_int_int(times_times_int(t),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))))),
inference(forward_demodulation,[],[f80496,f2425]) ).
fof(f80498,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),one_one_int)))))))) = hAPP_int_int(times_times_int(t),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,[],[f80497,f2426]) ).
fof(f80499,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(pls),one_one_int)))))))) = hAPP_int_int(times_times_int(t),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,[],[f80498,f2425]) ).
fof(f80500,plain,
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(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(pls),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))))))) = hAPP_int_int(times_times_int(t),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,[],[f80499,f2425]) ).
fof(f80501,plain,
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))) = hAPP_int_int(times_times_int(t),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,[],[f80500,f35375]) ).
fof(f80502,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(t),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,[],[f80501,f50697]) ).
fof(f80607,plain,
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,t),pls))
| 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(superposition,[],[f31062,f80502]) ).
fof(f80627,plain,
( ~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))))
| 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_subsumption_resolution,[],[f80607,f4714]) ).
fof(f80772,plain,
~ hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)))),
inference(forward_subsumption_resolution,[],[f80627,f73820]) ).
fof(f80841,plain,
~ spl38_1542,
inference(avatar_split_clause,[],[f80772,f76004]) ).
fof(f87257,plain,
! [X0] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(times_times_int(X0),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f45354,f50697]) ).
fof(f87259,plain,
! [X0] :
( 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(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),pls))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(resolution,[],[f87257,f5197]) ).
fof(f87314,plain,
! [X0] :
( 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(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),pls)) ),
inference(duplicate_literal_removal,[],[f87259]) ).
fof(f87320,definition,
( spl38_1967
<=> ! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
introduced(definition,[new_symbols(definition,[spl38_1967])],[avatar_definition]) ).
fof(f87321,plain,
( ! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls))
| ~ spl38_1967 ),
inference(avatar_component_clause,[],[f87320]) ).
fof(f87348,plain,
! [X0] :
( hBOOL(hAPP_int_bool(cOMBC_int_int_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),pls)) ),
inference(forward_demodulation,[],[f87314,f3902]) ).
fof(f87371,plain,
( spl38_1967
| spl38_1542 ),
inference(avatar_split_clause,[],[f87348,f76004,f87320]) ).
fof(f87399,plain,
( $false
| ~ spl38_1967 ),
inference(backward_subsumption_resolution,[],[f4714,f87321]) ).
fof(f87453,plain,
~ spl38_1967,
inference(avatar_contradiction_clause,[],[f87399]) ).
cnf(s2325,plain,
~ spl38_1542,
inference(sat_conversion,[],[f80841]) ).
cnf(s2648,plain,
( spl38_1542
| spl38_1967 ),
inference(sat_conversion,[],[f87371]) ).
cnf(s2650,plain,
~ spl38_1967,
inference(sat_conversion,[],[f87453]) ).
cnf(s2658,plain,
spl38_1542,
inference(rat,[],[s2648,s2650]) ).
cnf(s2662,plain,
$false,
inference(rat,[],[s2325,s2658]) ).
fof(f87507,plain,
$false,
inference(avatar_sat_refutation,[],[s2662]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.37 % Computer : n002.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 21:43:51 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.41 Running first-order model finding
% 0.12/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.01/2.52 % (3915262)Will run a generic schedule for satisfiability detection.
% 14.01/2.52 % (3915271)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2308334476:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.01/2.52 % (3915268)% WARNING: option uhcvi not known.
% 14.01/2.52 % (3915267)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3144745807_2999 on theBenchmark for (2999ds/0Mi)
% 14.01/2.52 % (3915268)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1929844951:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.01/2.52 % (3915269)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3047515997:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.01/2.52 % (3915270)dis+10_1_sil=32000:sp=arity:random_seed=669596520:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.01/2.52 % (3915272)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2748044080:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.01/2.52 % (3915273)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3577055340:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.01/2.52 % (3915271)Instruction limit reached!
% 14.01/2.52 % (3915271)------------------------------
% 14.01/2.52 % (3915271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.01/2.52 % (3915271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.01/2.52 % (3915271)CaDiCaL version: 2.1.3
% 14.01/2.52 % (3915271)Termination reason: Instruction limit
% 14.01/2.52 % (3915271)Termination phase: Property scanning
% 14.01/2.52 % (3915271)Time elapsed: 0.030 s
% 14.01/2.52 % (3915271)Peak memory usage: 13 MB
% 14.01/2.52 % (3915271)Instructions burned: 119 (million)
% 14.01/2.52 % (3915281)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4032104812:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.01/2.52 % (3915270)Instruction limit reached!
% 14.01/2.52 % (3915270)------------------------------
% 14.01/2.52 % (3915270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.01/2.52 % (3915270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.01/2.52 % (3915270)CaDiCaL version: 2.1.3
% 14.01/2.52 % (3915270)Termination reason: Instruction limit
% 14.01/2.52 % (3915270)Termination phase: Saturation
% 14.01/2.52 % (3915270)Time elapsed: 0.047 s
% 14.01/2.52 % (3915270)Peak memory usage: 14 MB
% 14.01/2.52 % (3915270)Instructions burned: 104 (million)
% 14.01/2.52 % (3915272)Instruction limit reached!
% 14.01/2.52 % (3915272)------------------------------
% 14.01/2.52 % (3915272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.01/2.52 % (3915272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.01/2.52 % (3915272)CaDiCaL version: 2.1.3
% 14.01/2.52 % (3915272)Termination reason: Instruction limit
% 14.01/2.52 % (3915272)Termination phase: Saturation
% 14.01/2.52 % (3915272)Time elapsed: 0.065 s
% 14.01/2.52 % (3915272)Peak memory usage: 14 MB
% 14.01/2.52 % (3915272)Instructions burned: 133 (million)
% 14.01/2.52 % (3915283)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1823015067:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.01/2.52 % (3915273)Instruction limit reached!
% 14.01/2.52 % (3915273)------------------------------
% 14.01/2.52 % (3915273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.01/2.52 % (3915273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.01/2.52 % (3915273)CaDiCaL version: 2.1.3
% 14.01/2.52 % (3915273)Termination reason: Instruction limit
% 14.01/2.52 % (3915273)Termination phase: Saturation
% 14.01/2.52 % (3915273)Time elapsed: 0.083 s
% 14.01/2.52 % (3915273)Peak memory usage: 15 MB
% 14.01/2.52 % (3915273)Instructions burned: 159 (million)
% 14.01/2.52 % (3915284)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=2356987491:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.01/2.52 % (3915287)ott-21_1_sil=16000:fs=off:random_seed=544237602:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.01/2.52 % (3915283)Instruction limit reached!
% 14.01/2.52 % (3915283)------------------------------
% 14.01/2.52 % (3915283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.01/2.52 % (3915283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915283)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915283)Termination reason: Instruction limit
% 21.40/3.55 % (3915283)Termination phase: Property scanning
% 21.40/3.55 % (3915283)Time elapsed: 0.058 s
% 21.40/3.55 % (3915283)Peak memory usage: 14 MB
% 21.40/3.55 % (3915283)Instructions burned: 131 (million)
% 21.40/3.55 % (3915289)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2097602910:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 21.40/3.55 % (3915287)Instruction limit reached!
% 21.40/3.55 % (3915287)------------------------------
% 21.40/3.55 % (3915287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915287)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915287)Termination reason: Instruction limit
% 21.40/3.55 % (3915287)Termination phase: Saturation
% 21.40/3.55 % (3915287)Time elapsed: 0.081 s
% 21.40/3.55 % (3915287)Peak memory usage: 14 MB
% 21.40/3.55 % (3915287)Instructions burned: 182 (million)
% 21.40/3.55 % (3915291)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2111099659:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 21.40/3.55 % (3915281)Instruction limit reached!
% 21.40/3.55 % (3915281)------------------------------
% 21.40/3.55 % (3915281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915281)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915281)Termination reason: Instruction limit
% 21.40/3.55 % (3915281)Termination phase: Finite model building preprocessing
% 21.40/3.55 % (3915281)Time elapsed: 0.181 s
% 21.40/3.55 % (3915281)Peak memory usage: 22 MB
% 21.40/3.55 % (3915281)Instructions burned: 718 (million)
% 21.40/3.55 % (3915293)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2070894697:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 21.40/3.55 % (3915289)Instruction limit reached!
% 21.40/3.55 % (3915289)------------------------------
% 21.40/3.55 % (3915289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915289)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915289)Termination reason: Instruction limit
% 21.40/3.55 % (3915289)Termination phase: Saturation
% 21.40/3.55 % (3915289)Time elapsed: 0.279 s
% 21.40/3.55 % (3915289)Peak memory usage: 15 MB
% 21.40/3.55 % (3915289)Instructions burned: 477 (million)
% 21.40/3.55 % (3915284)Instruction limit reached!
% 21.40/3.55 % (3915284)------------------------------
% 21.40/3.55 % (3915284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915284)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915284)Termination reason: Instruction limit
% 21.40/3.55 % (3915284)Termination phase: Saturation
% 21.40/3.55 % (3915284)Time elapsed: 0.353 s
% 21.40/3.55 % (3915284)Peak memory usage: 19 MB
% 21.40/3.55 % (3915284)Instructions burned: 686 (million)
% 21.40/3.55 % (3915295)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3615976307:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 21.40/3.55 % (3915296)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=252683443: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)
% 21.40/3.55 % (3915293)Instruction limit reached!
% 21.40/3.55 % (3915293)------------------------------
% 21.40/3.55 % (3915293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915293)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915293)Termination reason: Instruction limit
% 21.40/3.55 % (3915293)Termination phase: Saturation
% 21.40/3.55 % (3915293)Time elapsed: 0.362 s
% 21.40/3.55 % (3915293)Peak memory usage: 25 MB
% 21.40/3.55 % (3915293)Instructions burned: 1180 (million)
% 21.40/3.55 % (3915299)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=557412548:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 21.40/3.55 % (3915291)Instruction limit reached!
% 21.40/3.55 % (3915291)------------------------------
% 21.40/3.55 % (3915291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915291)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915291)Termination reason: Instruction limit
% 21.40/3.55 % (3915291)Termination phase: Finite model building preprocessing
% 21.40/3.55 % (3915291)Time elapsed: 0.412 s
% 21.40/3.55 % (3915291)Peak memory usage: 23 MB
% 21.40/3.55 % (3915291)Instructions burned: 865 (million)
% 21.40/3.55 % (3915301)fmb+10_1_sil=64000:random_seed=57247690:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 21.40/3.55 % TRYING [1]
% 21.40/3.55 % (3915296)Instruction limit reached!
% 21.40/3.55 % (3915296)------------------------------
% 21.40/3.55 % (3915296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915296)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915296)Termination reason: Instruction limit
% 21.40/3.55 % (3915296)Termination phase: Saturation
% 21.40/3.55 % (3915296)Time elapsed: 0.390 s
% 21.40/3.55 % (3915296)Peak memory usage: 22 MB
% 21.40/3.55 % (3915296)Instructions burned: 693 (million)
% 21.40/3.55 % (3915299)Instruction limit reached!
% 21.40/3.55 % (3915299)------------------------------
% 21.40/3.55 % (3915299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915299)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915299)Termination reason: Instruction limit
% 21.40/3.55 % (3915299)Termination phase: Saturation
% 21.40/3.55 % (3915299)Time elapsed: 0.251 s
% 21.40/3.55 % (3915299)Peak memory usage: 21 MB
% 21.40/3.55 % (3915299)Instructions burned: 880 (million)
% 21.40/3.55 % (3915303)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2258086727:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 21.40/3.55 % (3915304)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1310455962:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 21.40/3.55 % (3915295)Instruction limit reached!
% 21.40/3.55 % (3915295)------------------------------
% 21.40/3.55 % (3915295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915295)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915295)Termination reason: Instruction limit
% 21.40/3.55 % (3915295)Termination phase: Finite model building preprocessing
% 21.40/3.55 % (3915295)Time elapsed: 0.433 s
% 21.40/3.55 % (3915295)Peak memory usage: 24 MB
% 21.40/3.55 % (3915295)Instructions burned: 891 (million)
% 21.40/3.55 % TRYING [2]
% 21.40/3.55 % (3915307)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3813716681:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 21.40/3.55 % (3915304)Instruction limit reached!
% 21.40/3.55 % (3915304)------------------------------
% 21.40/3.55 % (3915304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915304)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915304)Termination reason: Instruction limit
% 21.40/3.55 % (3915304)Termination phase: Finite model building preprocessing
% 21.40/3.55 % (3915304)Time elapsed: 0.236 s
% 21.40/3.55 % (3915304)Peak memory usage: 23 MB
% 21.40/3.55 % (3915304)Instructions burned: 920 (million)
% 21.40/3.55 % (3915309)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3463524420:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 21.40/3.55 % TRYING [3]
% 21.40/3.55 % TRYING [1]
% 21.40/3.55 % (3915309)Instruction limit reached!
% 21.40/3.55 % (3915309)------------------------------
% 21.40/3.55 % (3915309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915309)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915309)Termination reason: Instruction limit
% 21.40/3.55 % (3915309)Termination phase: Saturation
% 21.40/3.55 % (3915309)Time elapsed: 0.423 s
% 21.40/3.55 % (3915309)Peak memory usage: 30 MB
% 21.40/3.55 % (3915309)Instructions burned: 1475 (million)
% 21.40/3.55 % TRYING [2]
% 21.40/3.55 % (3915311)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=716297733:i=6324_2983 on theBenchmark for (2983ds/6324Mi)
% 21.40/3.55 % TRYING [20]
% 21.40/3.55 % TRYING [4]
% 21.40/3.55 % (3915311)Cannot represent all propositional literals internally
% 21.40/3.55 % (3915311)Refutation not found, incomplete strategy
% 21.40/3.55 % (3915311)------------------------------
% 21.40/3.55 % (3915311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915311)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915311)Termination reason: Refutation not found, incomplete strategy
% 21.40/3.55 % (3915311)Time elapsed: 0.461 s
% 21.40/3.55 % (3915311)Peak memory usage: 37 MB
% 21.40/3.55 % (3915311)Instructions burned: 1770 (million)
% 21.40/3.55 % (3915311)------------------------------
% 21.40/3.55 % (3915311)------------------------------
% 21.40/3.55 % (3915313)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3987943311:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 21.40/3.55 % TRYING [3]
% 21.40/3.55 % (3915313)Instruction limit reached!
% 21.40/3.55 % (3915313)------------------------------
% 21.40/3.55 % (3915313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915313)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915313)Termination reason: Instruction limit
% 21.40/3.55 % (3915313)Termination phase: Finite model building preprocessing
% 21.40/3.55 % (3915313)Time elapsed: 0.556 s
% 21.40/3.55 % (3915313)Peak memory usage: 32 MB
% 21.40/3.55 % (3915313)Instructions burned: 2178 (million)
% 21.40/3.55 % (3915315)ott-2_1_sil=16000:newcnf=on:random_seed=2054734895:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2973 on theBenchmark for (2973ds/869Mi)
% 21.40/3.55 % (3915315)Instruction limit reached!
% 21.40/3.55 % (3915315)------------------------------
% 21.40/3.55 % (3915315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915315)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915315)Termination reason: Instruction limit
% 21.40/3.55 % (3915315)Termination phase: Saturation
% 21.40/3.55 % (3915315)Time elapsed: 0.250 s
% 21.40/3.55 % (3915315)Peak memory usage: 23 MB
% 21.40/3.55 % (3915315)Instructions burned: 871 (million)
% 21.40/3.55 % (3915317)ott+10_1_sil=32000:tgt=ground:random_seed=3583957949:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 21.40/3.55 % (3915268) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3915262-3915268"...
% 21.40/3.55 % (3915268)...printing done.
% 21.40/3.55 % (3915268)Refutation found. Thanks to Tanya!
% 21.40/3.55 % SZS status Theorem for theBenchmark
% 21.40/3.55 % SZS output start Proof for theBenchmark
% See solution above
% 21.40/3.55 % (3915268)------------------------------
% 21.40/3.55 % (3915268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.40/3.55 % (3915268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.40/3.55 % (3915268)CaDiCaL version: 2.1.3
% 21.40/3.55 % (3915268)Termination reason: Refutation
% 21.40/3.55 % (3915268)Time elapsed: 2.997 s
% 21.40/3.55 % (3915268)Peak memory usage: 54 MB
% 21.40/3.55 % (3915268)Instructions burned: 5434 (million)
% 21.40/3.55 % (3915262)Success in time 3.131 s
% 21.40/3.55 % Vampire exiting
%------------------------------------------------------------------------------