%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM924+8 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:17:32 PM UTC 2026
% Result : Theorem 35.35s 6.57s
% Output : Refutation 36.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 30
% Syntax : Number of formulae : 143 ( 104 unt; 0 def)
% Number of atoms : 190 ( 124 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 80 ( 33 ~; 37 |; 5 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 11 con; 0-4 aty)
% Number of variables : 155 ( 155 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f265,axiom,
! [X0,X1,X2,X3] : hAPP(X0,X1,X2,ti(X0,X3)) = hAPP(X0,X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_hAPP_arg2) ).
fof(f266,axiom,
! [X0,X1,X2,X3] : ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_hAPP_res) ).
fof(f275,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__096_I4_A_K_Am_A_L_A1_J_A_K_At_A_060_A_I4_A_K_Am_A_L_A1_J_A_K_A0_096) ).
fof(f276,axiom,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_t) ).
fof(f295,axiom,
! [X0] : hAPP(int,int,number_number_of(int),X0) = ti(int,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_number__of__is__id) ).
fof(f296,axiom,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_zmult__commute) ).
fof(f307,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_rel__simps_I19_J) ).
fof(f334,axiom,
hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),one_one(nat)),one_one(nat)) = hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_nat__1__add__1) ).
fof(f335,axiom,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),X0) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_mult__Pls) ).
fof(f336,axiom,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,X0)),X1) = hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_mult__Bit0) ).
fof(f339,axiom,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0) = ti(int,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_zmult__1) ).
fof(f372,axiom,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_zadd__commute) ).
fof(f385,axiom,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_one__is__num__one) ).
fof(f395,axiom,
hAPP(int,int,bit0,pls) = pls,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_Bit0__Pls) ).
fof(f396,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_Pls__def) ).
fof(f575,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),min_1),pls)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_302_rel__simps_I23_J) ).
fof(f576,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),min_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_303_rel__simps_I20_J) ).
fof(f740,axiom,
hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(int,int,number_number_of(int),min_1)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_467__096s_A_094_A2_A_N_A_N1_A_061_As_A_094_A2_A_L_A1_096) ).
fof(f1172,axiom,
! [X0,X1] :
( ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1)))
=> hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1)))),one_one(int)) )
& ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1)))
=> hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1)))),one_one(int)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_899_zmod__number__of__Bit1) ).
fof(f1181,axiom,
! [X0] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),X0),zero_zero(int)) = zero_zero(int)
& hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),X0),zero_zero(int)) = ti(int,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_908_DIVISION__BY__ZERO) ).
fof(f1325,axiom,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1052_zmod__number__of__Bit0) ).
fof(f1338,axiom,
! [X0,X1] :
( ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1)))
=> hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1)) )
& ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1)))
=> hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1065_zdiv__number__of__Bit1) ).
fof(f1344,axiom,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),zero_zero(int)))
=> hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X0))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1071_neg__zdiv__mult__2) ).
fof(f1616,axiom,
! [X0] : hAPP(nat,nat,suc,X0) = hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),X0),one_one(nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1343_Suc__eq__plus1) ).
fof(f2416,axiom,
! [X0] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,uminus_uminus(int),X0)) = ti(int,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2143_zminus__zminus) ).
fof(f2430,axiom,
min_1 = hAPP(int,int,uminus_uminus(int),one_one(int)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2157_Int_OMin__def) ).
fof(f2433,axiom,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),min_1),X0) = hAPP(int,int,uminus_uminus(int),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2160_mult__Min) ).
fof(f2434,axiom,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),hAPP(int,int,uminus_uminus(int),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2161_diff__int__def) ).
fof(f2445,axiom,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),X0),hAPP(int,int,number_number_of(int),min_1)) = hAPP(int,int,uminus_uminus(int),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2172_zdiv__minus1__right) ).
fof(f5738,conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f5739,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(negated_conjecture,[status(cth)],[f5738]) ).
fof(f5740,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(flattening,[],[f5739]) ).
fof(f6045,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X0))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),zero_zero(int))) ),
inference(ennf_transformation,[],[f1344]) ).
fof(f6046,plain,
! [X0,X1] :
( ( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1))) )
& ( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1))) ) ),
inference(ennf_transformation,[],[f1338]) ).
fof(f6050,plain,
! [X0,X1] :
( ( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1)))),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1))) )
& ( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1)))),one_one(int))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1))) ) ),
inference(ennf_transformation,[],[f1172]) ).
fof(f9187,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),zero_zero(int))),
inference(cnf_transformation,[],[f5740]) ).
fof(f9254,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X1),X0),
inference(cnf_transformation,[],[f296]) ).
fof(f9306,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X1),X0),
inference(cnf_transformation,[],[f372]) ).
fof(f9321,plain,
! [X0] : ti(int,X0) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0),
inference(cnf_transformation,[],[f339]) ).
fof(f9336,plain,
! [X0] : hAPP(int,int,number_number_of(int),X0) = ti(int,X0),
inference(cnf_transformation,[],[f295]) ).
fof(f9342,plain,
! [X0] : ti(int,X0) = hAPP(int,int,uminus_uminus(int),hAPP(int,int,uminus_uminus(int),X0)),
inference(cnf_transformation,[],[f2416]) ).
fof(f9374,plain,
! [X2,X3,X0,X1] : hAPP(X1,X0,X2,X3) = ti(X0,hAPP(X1,X0,X2,X3)),
inference(cnf_transformation,[],[f266]) ).
fof(f9375,plain,
! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,ti(X0,X3)),
inference(cnf_transformation,[],[f265]) ).
fof(f9415,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X0))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),zero_zero(int))) ),
inference(cnf_transformation,[],[f6045]) ).
fof(f9416,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1))) ),
inference(cnf_transformation,[],[f6046]) ).
fof(f9420,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))),
inference(cnf_transformation,[],[f1325]) ).
fof(f9426,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1)))),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),zero_zero(int)),hAPP(int,int,number_number_of(int),X1))) ),
inference(cnf_transformation,[],[f6050]) ).
fof(f9471,plain,
pls = hAPP(int,int,bit0,pls),
inference(cnf_transformation,[],[f395]) ).
fof(f9483,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,X0)),X1) = hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),X0),X1)),
inference(cnf_transformation,[],[f336]) ).
fof(f9484,plain,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))) = hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),one_one(nat)),one_one(nat)),
inference(cnf_transformation,[],[f334]) ).
fof(f9524,plain,
one_one(int) = hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,pls)),
inference(cnf_transformation,[],[f385]) ).
fof(f9548,plain,
pls = zero_zero(int),
inference(cnf_transformation,[],[f396]) ).
fof(f9557,plain,
! [X0] : pls = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),X0),
inference(cnf_transformation,[],[f335]) ).
fof(f9566,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),pls)),
inference(cnf_transformation,[],[f307]) ).
fof(f9637,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),hAPP(int,int,number_number_of(int),min_1)),
inference(cnf_transformation,[],[f740]) ).
fof(f9647,plain,
hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)),
inference(cnf_transformation,[],[f276]) ).
fof(f9731,plain,
! [X0] : hAPP(nat,nat,hAPP(nat,fun(nat,nat),plus_plus(nat),X0),one_one(nat)) = hAPP(nat,nat,suc,X0),
inference(cnf_transformation,[],[f1616]) ).
fof(f9756,plain,
! [X0,X1] : hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),X1) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),hAPP(int,int,uminus_uminus(int),X1)),
inference(cnf_transformation,[],[f2434]) ).
fof(f9996,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),X0) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),X0),hAPP(int,int,number_number_of(int),min_1)),
inference(cnf_transformation,[],[f2445]) ).
fof(f10009,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),X0) = hAPP(int,int,hAPP(int,fun(int,int),times_times(int),min_1),X0),
inference(cnf_transformation,[],[f2433]) ).
fof(f10012,plain,
min_1 = hAPP(int,int,uminus_uminus(int),one_one(int)),
inference(cnf_transformation,[],[f2430]) ).
fof(f10806,plain,
! [X0] : ti(int,X0) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),X0),zero_zero(int)),
inference(cnf_transformation,[],[f1181]) ).
fof(f11265,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),zero_zero(int)))),
inference(cnf_transformation,[],[f275]) ).
fof(f11332,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),min_1)),
inference(cnf_transformation,[],[f576]) ).
fof(f11333,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),min_1),pls)),
inference(cnf_transformation,[],[f575]) ).
fof(f13476,plain,
hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))) = hAPP(nat,nat,suc,one_one(nat)),
inference(forward_demodulation,[],[f9484,f9731]) ).
fof(f13484,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),hAPP(int,int,number_number_of(int),X1)))
| hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1)))),one_one(int)) ),
inference(forward_demodulation,[],[f9426,f9548]) ).
fof(f13490,plain,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),hAPP(int,int,number_number_of(int),X1)))
| hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1)) ),
inference(forward_demodulation,[],[f9416,f9548]) ).
fof(f13492,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),pls))
| hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X0))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1) ),
inference(forward_demodulation,[],[f9415,f9548]) ).
fof(f13545,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),pls)),
inference(forward_demodulation,[],[f9187,f9548]) ).
fof(f13593,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),ti(int,X1)))
| hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1)))),one_one(int)) ),
inference(forward_demodulation,[],[f13484,f9336]) ).
fof(f13599,plain,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),ti(int,X1)))
| hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1)) ),
inference(forward_demodulation,[],[f13490,f9336]) ).
fof(f13601,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X0))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),ti(int,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),pls)) ),
inference(forward_demodulation,[],[f13492,f9336]) ).
fof(f13626,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))),pls)),
inference(forward_demodulation,[],[f13545,f9306]) ).
fof(f13646,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1))
| hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1)))),one_one(int)) ),
inference(forward_demodulation,[],[f13593,f9375]) ).
fof(f13652,plain,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1))
| hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),hAPP(int,int,number_number_of(int),X1)) ),
inference(forward_demodulation,[],[f13599,f9375]) ).
fof(f13654,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),X0))),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),pls)) ),
inference(forward_demodulation,[],[f13601,f9375]) ).
fof(f13673,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat))))),pls)),
inference(forward_demodulation,[],[f13626,f13476]) ).
fof(f13683,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),X0)),hAPP(int,int,number_number_of(int),X1))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13646,f9306]) ).
fof(f13689,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),ti(int,X1))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13652,f9336]) ).
fof(f13691,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))),X0))),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,pls)),X1)))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),pls)) ),
inference(forward_demodulation,[],[f13654,f9483]) ).
fof(f13707,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13683,f9420]) ).
fof(f13713,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,number_number_of(int),X0)),one_one(int))),X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13689,f9375]) ).
fof(f13715,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),X1),pls))
| hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),X1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,pls)),X0)))),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,pls)),X1))) ),
inference(forward_demodulation,[],[f13691,f9483]) ).
fof(f13724,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),ti(int,hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X0))),ti(int,hAPP(int,int,bit0,X1))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13707,f9336]) ).
fof(f13727,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,number_number_of(int),X0))),X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13713,f9306]) ).
fof(f13730,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),ti(int,hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X0))),hAPP(int,int,bit0,X1)))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13724,f9375]) ).
fof(f13731,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),ti(int,X0))),X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13727,f9336]) ).
fof(f13734,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),ti(int,hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),ti(int,hAPP(int,int,bit0,X0))),hAPP(int,int,bit0,X1)))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13730,f9336]) ).
fof(f13735,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13731,f9375]) ).
fof(f13738,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),ti(int,hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit0,X0)),hAPP(int,int,bit0,X1)))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13734,f9375]) ).
fof(f13739,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),ti(int,hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13735,f9336]) ).
fof(f13742,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit0,X0)),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,bit0,X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13738,f9375]) ).
fof(f13743,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit1,X0))),hAPP(int,int,bit0,X1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13739,f9375]) ).
fof(f13746,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit0,X0)),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),ti(int,hAPP(int,int,bit1,X0))),hAPP(int,int,bit0,X1))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13742,f9336]) ).
fof(f13747,plain,
! [X0,X1] :
( hAPP(int,int,hAPP(int,fun(int,int),div_div(int),ti(int,hAPP(int,int,bit1,X0))),hAPP(int,int,bit0,X1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),X1)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1)) ),
inference(forward_demodulation,[],[f13743,f9336]) ).
fof(f13750,plain,
! [X0,X1] :
( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1))
| hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit0,X0)),hAPP(int,int,bit0,X1))) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit1,X0)),hAPP(int,int,bit0,X1)) ),
inference(forward_demodulation,[],[f13746,f9375]) ).
fof(f13751,plain,
! [X0,X1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),pls),X1))
| hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,bit1,X0)),hAPP(int,int,bit0,X1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),X1) ),
inference(forward_demodulation,[],[f13747,f9375]) ).
fof(f13783,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),ti(int,min_1)),
inference(superposition,[],[f9637,f9336]) ).
fof(f13785,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),min_1),
inference(forward_demodulation,[],[f13783,f9375]) ).
fof(f13786,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),min_1),
inference(forward_demodulation,[],[f13785,f13476]) ).
fof(f13787,plain,
hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),min_1),
inference(forward_demodulation,[],[f13786,f9306]) ).
fof(f13811,plain,
one_one(int) = ti(int,hAPP(int,int,bit1,pls)),
inference(superposition,[],[f9336,f9524]) ).
fof(f13812,plain,
one_one(int) = ti(int,one_one(int)),
inference(superposition,[],[f9374,f9524]) ).
fof(f13813,plain,
one_one(int) = hAPP(int,int,bit1,pls),
inference(forward_demodulation,[],[f13811,f9374]) ).
fof(f13891,plain,
! [X0] : ti(int,X0) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),X0),pls),
inference(superposition,[],[f10806,f9548]) ).
fof(f14006,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit0,X0)),hAPP(int,int,bit0,pls))) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit1,X0)),hAPP(int,int,bit0,pls)),
inference(resolution,[],[f9566,f13750]) ).
fof(f14009,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit0,X0)),pls)) = hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit1,X0)),pls),
inference(forward_demodulation,[],[f14006,f9471]) ).
fof(f14011,plain,
! [X0] : ti(int,hAPP(int,int,bit1,X0)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),div_mod(int),hAPP(int,int,bit0,X0)),pls)),
inference(forward_demodulation,[],[f14009,f13891]) ).
fof(f14013,plain,
! [X0] : ti(int,hAPP(int,int,bit1,X0)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),ti(int,hAPP(int,int,bit0,X0))),
inference(forward_demodulation,[],[f14011,f13891]) ).
fof(f14015,plain,
! [X0] : ti(int,hAPP(int,int,bit1,X0)) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,X0)),
inference(forward_demodulation,[],[f14013,f9375]) ).
fof(f14016,plain,
! [X0] : hAPP(int,int,bit1,X0) = hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,X0)),
inference(forward_demodulation,[],[f14015,f9374]) ).
fof(f14368,plain,
hAPP(int,int,uminus_uminus(int),min_1) = ti(int,one_one(int)),
inference(superposition,[],[f9342,f10012]) ).
fof(f14370,plain,
one_one(int) = hAPP(int,int,uminus_uminus(int),min_1),
inference(forward_demodulation,[],[f14368,f13812]) ).
fof(f14626,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),X0) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),X0),ti(int,min_1)),
inference(superposition,[],[f9996,f9336]) ).
fof(f14634,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),X0) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),X0),min_1),
inference(forward_demodulation,[],[f14626,f9375]) ).
fof(f15373,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),min_1)),pls)),
inference(superposition,[],[f13673,f13787]) ).
fof(f16037,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,bit1,X0)),hAPP(int,int,bit0,min_1)) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),min_1),
inference(resolution,[],[f11332,f13751]) ).
fof(f16038,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,bit1,X0)),hAPP(int,int,bit0,min_1)) = hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),
inference(forward_demodulation,[],[f16037,f14634]) ).
fof(f19976,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int)) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),min_1),
inference(superposition,[],[f9756,f14370]) ).
fof(f21124,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,pls)),X0)))),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,pls)),min_1))),
inference(resolution,[],[f13715,f11333]) ).
fof(f21142,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,pls)),X0)))),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),min_1),hAPP(int,int,bit1,pls)))),
inference(forward_demodulation,[],[f21124,f9254]) ).
fof(f21151,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,bit1,pls)),X0)))),hAPP(int,int,bit0,hAPP(int,int,uminus_uminus(int),hAPP(int,int,bit1,pls)))),
inference(forward_demodulation,[],[f21142,f10009]) ).
fof(f21160,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0)))),hAPP(int,int,bit0,hAPP(int,int,uminus_uminus(int),one_one(int)))),
inference(forward_demodulation,[],[f21151,f13813]) ).
fof(f21169,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,bit0,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0)))),hAPP(int,int,bit0,min_1)),
inference(forward_demodulation,[],[f21160,f10012]) ).
fof(f21175,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,bit1,hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0))),hAPP(int,int,bit0,min_1)),
inference(forward_demodulation,[],[f21169,f14016]) ).
fof(f21181,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1) = hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),one_one(int)),X0))),
inference(forward_demodulation,[],[f21175,f16038]) ).
fof(f21185,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),ti(int,X0))) = hAPP(int,int,hAPP(int,fun(int,int),div_div(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),min_1),
inference(forward_demodulation,[],[f21181,f9321]) ).
fof(f21189,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),ti(int,X0))) = hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),X0),one_one(int))),
inference(forward_demodulation,[],[f21185,f14634]) ).
fof(f21193,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),ti(int,X0))) = hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),min_1)),
inference(forward_demodulation,[],[f21189,f19976]) ).
fof(f21194,plain,
! [X0] : hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)) = hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),min_1)),
inference(forward_demodulation,[],[f21193,f9375]) ).
fof(f21214,plain,
! [X0] : ti(int,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)) = hAPP(int,int,uminus_uminus(int),hAPP(int,int,uminus_uminus(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),min_1))),
inference(superposition,[],[f9342,f21194]) ).
fof(f21218,plain,
! [X0] : ti(int,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)) = ti(int,hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),min_1)),
inference(forward_demodulation,[],[f21214,f9342]) ).
fof(f21232,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),min_1) = ti(int,hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0)),
inference(forward_demodulation,[],[f21218,f9374]) ).
fof(f21235,plain,
! [X0] : hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),X0) = hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),X0),min_1),
inference(forward_demodulation,[],[f21232,f9374]) ).
fof(f24656,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),pls))),
inference(superposition,[],[f11265,f9548]) ).
fof(f24661,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),pls),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))))),
inference(forward_demodulation,[],[f24656,f9254]) ).
fof(f24674,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(int,int,hAPP(int,fun(int,int),times_times(int),hAPP(int,int,number_number_of(int),hAPP(int,int,bit0,hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),m)),one_one(int))),t)),pls)),
inference(forward_demodulation,[],[f24661,f9557]) ).
fof(f24687,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),one_one(int))),pls)),
inference(forward_demodulation,[],[f24674,f9647]) ).
fof(f24700,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),plus_plus(int),one_one(int)),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))))),pls)),
inference(forward_demodulation,[],[f24687,f9306]) ).
fof(f24713,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(int,nat,number_number_of(nat),hAPP(int,int,bit0,hAPP(int,int,bit1,pls))))),min_1)),pls)),
inference(forward_demodulation,[],[f24700,f21235]) ).
fof(f24726,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),hAPP(int,int,hAPP(int,fun(int,int),minus_minus(int),hAPP(nat,int,hAPP(int,fun(nat,int),power_power(int),s),hAPP(nat,nat,suc,one_one(nat)))),min_1)),pls)),
inference(forward_demodulation,[],[f24713,f13476]) ).
fof(f24739,plain,
$false,
inference(forward_subsumption_resolution,[],[f24726,f15373]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+8 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 % Computer : n004.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.41 % CPULimit : 300
% 0.11/0.41 % WCLimit : 300
% 0.11/0.41 % DateTime : Sun Sep 27 21:41:23 UTC 2026
% 0.11/0.41 % CPUTime :
% 0.11/0.41 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.45 Running first-order theorem proving
% 0.11/0.45 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.49/3.00 % (3900186)Detected formulas, will run a generic FOF schedule.
% 8.49/3.00 % (3900195)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1662672266:i=119:av=off:ss=axioms_2992 on theBenchmark for (2992ds/119Mi)
% 8.49/3.00 % (3900196)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4020541713:s2a=on:i=139:gtg=position_2992 on theBenchmark for (2992ds/139Mi)
% 8.49/3.00 % (3900192)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2450570625:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2992 on theBenchmark for (2992ds/134677Mi)
% 8.49/3.00 % (3900194)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2878024357:i=109:sd=1:ins=1:gsp=on:ss=axioms_2992 on theBenchmark for (2992ds/109Mi)
% 8.49/3.00 % (3900193)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1567233305:i=141695:sd=1:nm=32:gsp=on:ss=included_2992 on theBenchmark for (2992ds/141695Mi)
% 8.49/3.00 % (3900191)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=211764153:i=141193_2992 on theBenchmark for (2992ds/141193Mi)
% 8.49/3.00 % (3900197)dis-21_1_sil=8000:lcm=predicate:random_seed=2487049535:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2992 on theBenchmark for (2992ds/129Mi)
% 8.49/3.00 % (3900195)Instruction limit reached!
% 8.49/3.00 % (3900195)------------------------------
% 8.49/3.00 % (3900195)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.49/3.00 % (3900195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/3.00 % (3900195)CaDiCaL version: 2.1.3
% 8.49/3.00 % (3900195)Termination reason: Instruction limit
% 8.49/3.00 % (3900195)Termination phase: Property scanning
% 8.49/3.00 % (3900195)Time elapsed: 0.042 s
% 8.49/3.00 % (3900195)Peak memory usage: 93 MB
% 8.49/3.00 % (3900195)Instructions burned: 124 (million)
% 8.49/3.00 % (3900196)Instruction limit reached!
% 8.49/3.00 % (3900196)------------------------------
% 8.49/3.00 % (3900196)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.49/3.00 % (3900196)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/3.00 % (3900196)CaDiCaL version: 2.1.3
% 8.49/3.00 % (3900196)Termination reason: Instruction limit
% 8.49/3.00 % (3900196)Termination phase: Property scanning
% 8.49/3.00 % (3900196)Time elapsed: 0.050 s
% 8.49/3.00 % (3900196)Peak memory usage: 91 MB
% 8.49/3.00 % (3900196)Instructions burned: 140 (million)
% 8.49/3.00 % (3900194)Instruction limit reached!
% 8.49/3.00 % (3900194)------------------------------
% 8.49/3.00 % (3900194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.49/3.00 % (3900194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/3.00 % (3900194)CaDiCaL version: 2.1.3
% 8.49/3.00 % (3900194)Termination reason: Instruction limit
% 8.49/3.00 % (3900194)Termination phase: Saturation
% 8.49/3.00 % (3900194)Time elapsed: 0.061 s
% 8.49/3.00 % (3900194)Peak memory usage: 94 MB
% 8.49/3.00 % (3900194)Instructions burned: 109 (million)
% 8.49/3.00 % (3900197)Instruction limit reached!
% 8.49/3.00 % (3900197)------------------------------
% 8.49/3.00 % (3900197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.49/3.00 % (3900197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/3.00 % (3900197)CaDiCaL version: 2.1.3
% 8.49/3.00 % (3900197)Termination reason: Instruction limit
% 8.49/3.00 % (3900197)Termination phase: Naming
% 8.49/3.00 % (3900197)Time elapsed: 0.079 s
% 8.49/3.00 % (3900197)Peak memory usage: 93 MB
% 8.49/3.00 % (3900197)Instructions burned: 130 (million)
% 8.49/3.00 % (3900205)lrs+10_1_sil=8000:sp=occurrence:random_seed=1567198168:i=285:sd=3:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/285Mi)
% 8.49/3.00 % (3900205)Instruction limit reached!
% 8.49/3.00 % (3900205)------------------------------
% 8.49/3.00 % (3900205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.49/3.00 % (3900205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.49/3.00 % (3900205)CaDiCaL version: 2.1.3
% 8.49/3.00 % (3900205)Termination reason: Instruction limit
% 8.49/3.00 % (3900205)Termination phase: Saturation
% 8.49/3.00 % (3900205)Time elapsed: 0.075 s
% 8.49/3.00 % (3900205)Peak memory usage: 95 MB
% 8.49/3.00 % (3900205)Instructions burned: 288 (million)
% 18.60/4.15 % (3900206)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3217320932:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2990 on theBenchmark for (2990ds/157Mi)
% 18.60/4.15 % (3900207)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3275751375:i=325:sd=1:ss=axioms:sgt=32_2990 on theBenchmark for (2990ds/325Mi)
% 18.60/4.15 % (3900208)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3503308968:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 18.60/4.15 % (3900206)Instruction limit reached!
% 18.60/4.15 % (3900206)------------------------------
% 18.60/4.15 % (3900206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/4.15 % (3900206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/4.15 % (3900206)CaDiCaL version: 2.1.3
% 18.60/4.15 % (3900206)Termination reason: Instruction limit
% 18.60/4.15 % (3900206)Termination phase: Property scanning
% 18.60/4.15 % (3900206)Time elapsed: 0.061 s
% 18.60/4.15 % (3900206)Peak memory usage: 91 MB
% 18.60/4.15 % (3900206)Instructions burned: 160 (million)
% 18.60/4.15 % (3900211)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2027681538:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2988 on theBenchmark for (2988ds/294Mi)
% 18.60/4.15 % (3900208)Instruction limit reached!
% 18.60/4.15 % (3900208)------------------------------
% 18.60/4.15 % (3900208)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/4.15 % (3900208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/4.15 % (3900208)CaDiCaL version: 2.1.3
% 18.60/4.15 % (3900208)Termination reason: Instruction limit
% 18.60/4.15 % (3900208)Termination phase: Property scanning
% 18.60/4.15 % (3900208)Time elapsed: 0.088 s
% 18.60/4.15 % (3900208)Peak memory usage: 91 MB
% 18.60/4.15 % (3900208)Instructions burned: 250 (million)
% 18.60/4.15 % (3900211)Instruction limit reached!
% 18.60/4.15 % (3900211)------------------------------
% 18.60/4.15 % (3900211)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/4.15 % (3900211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/4.15 % (3900211)CaDiCaL version: 2.1.3
% 18.60/4.15 % (3900211)Termination reason: Instruction limit
% 18.60/4.15 % (3900211)Termination phase: Property scanning
% 18.60/4.15 % (3900211)Time elapsed: 0.076 s
% 18.60/4.15 % (3900211)Peak memory usage: 94 MB
% 18.60/4.15 % (3900211)Instructions burned: 295 (million)
% 18.60/4.15 % (3900214)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2064793111:i=2350_2988 on theBenchmark for (2988ds/2350Mi)
% 18.60/4.15 % (3900207)Instruction limit reached!
% 18.60/4.15 % (3900207)------------------------------
% 18.60/4.15 % (3900207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/4.15 % (3900207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/4.15 % (3900207)CaDiCaL version: 2.1.3
% 18.60/4.15 % (3900207)Termination reason: Instruction limit
% 18.60/4.15 % (3900207)Termination phase: Saturation
% 18.60/4.15 % (3900207)Time elapsed: 0.193 s
% 18.60/4.15 % (3900207)Peak memory usage: 96 MB
% 18.60/4.15 % (3900207)Instructions burned: 327 (million)
% 18.60/4.15 % (3900216)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1628044603:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 18.60/4.15 % (3900217)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=684689007:i=127:av=off:fsr=off:sup=off_2987 on theBenchmark for (2987ds/127Mi)
% 18.60/4.15 % (3900219)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4277868932:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 18.60/4.15 % (3900219)Instruction limit reached!
% 18.60/4.15 % (3900219)------------------------------
% 18.60/4.15 % (3900219)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.60/4.15 % (3900219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.60/4.15 % (3900219)CaDiCaL version: 2.1.3
% 18.60/4.15 % (3900219)Termination reason: Instruction limit
% 18.60/4.15 % (3900219)Termination phase: Property scanning
% 18.60/4.15 % (3900219)Time elapsed: 0.022 s
% 18.60/4.15 % (3900219)Peak memory usage: 91 MB
% 18.60/4.15 % (3900219)Instructions burned: 117 (million)
% 18.60/4.15 % (3900216)Instruction limit reached!
% 18.60/4.15 % (3900216)------------------------------
% 18.60/4.15 % (3900216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900216)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900216)Termination reason: Instruction limit
% 35.35/6.57 % (3900216)Termination phase: Preprocessing 1
% 35.35/6.57 % (3900216)Time elapsed: 0.067 s
% 35.35/6.57 % (3900216)Peak memory usage: 91 MB
% 35.35/6.57 % (3900216)Instructions burned: 113 (million)
% 35.35/6.57 % (3900217)Instruction limit reached!
% 35.35/6.57 % (3900217)------------------------------
% 35.35/6.57 % (3900217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900217)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900217)Termination reason: Instruction limit
% 35.35/6.57 % (3900217)Termination phase: Preprocessing 3
% 35.35/6.57 % (3900217)Time elapsed: 0.070 s
% 35.35/6.57 % (3900217)Peak memory usage: 94 MB
% 35.35/6.57 % (3900217)Instructions burned: 127 (million)
% 35.35/6.57 % (3900224)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=371744962:i=437:sd=1:aac=none:ss=included_2985 on theBenchmark for (2985ds/437Mi)
% 35.35/6.57 % (3900223)lrs+10_1_sil=8000:sp=occurrence:random_seed=962313902:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 35.35/6.57 % (3900225)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=347447179:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 35.35/6.57 % (3900224)Instruction limit reached!
% 35.35/6.57 % (3900224)------------------------------
% 35.35/6.57 % (3900224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900224)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900224)Termination reason: Instruction limit
% 35.35/6.57 % (3900224)Termination phase: Property scanning
% 35.35/6.57 % (3900224)Time elapsed: 0.116 s
% 35.35/6.57 % (3900224)Peak memory usage: 97 MB
% 35.35/6.57 % (3900224)Instructions burned: 443 (million)
% 35.35/6.57 % (3900229)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=700552785:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 35.35/6.57 % (3900229)Instruction limit reached!
% 35.35/6.57 % (3900229)------------------------------
% 35.35/6.57 % (3900229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900229)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900229)Termination reason: Instruction limit
% 35.35/6.57 % (3900229)Termination phase: NewCNF
% 35.35/6.57 % (3900229)Time elapsed: 0.044 s
% 35.35/6.57 % (3900229)Peak memory usage: 94 MB
% 35.35/6.57 % (3900229)Instructions burned: 136 (million)
% 35.35/6.57 % (3900231)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1626435309:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 35.35/6.57 % (3900223)Instruction limit reached!
% 35.35/6.57 % (3900223)------------------------------
% 35.35/6.57 % (3900223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900223)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900223)Termination reason: Instruction limit
% 35.35/6.57 % (3900223)Termination phase: Saturation
% 35.35/6.57 % (3900223)Time elapsed: 0.408 s
% 35.35/6.57 % (3900223)Peak memory usage: 100 MB
% 35.35/6.57 % (3900223)Instructions burned: 908 (million)
% 35.35/6.57 % (3900231)Instruction limit reached!
% 35.35/6.57 % (3900231)------------------------------
% 35.35/6.57 % (3900231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900231)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900231)Termination reason: Instruction limit
% 35.35/6.57 % (3900231)Termination phase: Property scanning
% 35.35/6.57 % (3900231)Time elapsed: 0.147 s
% 35.35/6.57 % (3900231)Peak memory usage: 97 MB
% 35.35/6.57 % (3900231)Instructions burned: 597 (million)
% 35.35/6.57 % (3900233)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2669056271:st=3:i=13193:sd=3:ss=axioms_2980 on theBenchmark for (2980ds/13193Mi)
% 35.35/6.57 % (3900234)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3079208743:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 35.35/6.57 % (3900234)Instruction limit reached!
% 35.35/6.57 % (3900234)------------------------------
% 35.35/6.57 % (3900234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900234)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900234)Termination reason: Instruction limit
% 35.35/6.57 % (3900234)Termination phase: Property scanning
% 35.35/6.57 % (3900234)Time elapsed: 0.049 s
% 35.35/6.57 % (3900234)Peak memory usage: 91 MB
% 35.35/6.57 % (3900234)Instructions burned: 126 (million)
% 35.35/6.57 % (3900237)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4268618755:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 35.35/6.57 % (3900237)Instruction limit reached!
% 35.35/6.57 % (3900237)------------------------------
% 35.35/6.57 % (3900237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900237)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900237)Termination reason: Instruction limit
% 35.35/6.57 % (3900237)Termination phase: Property scanning
% 35.35/6.57 % (3900237)Time elapsed: 0.049 s
% 35.35/6.57 % (3900237)Peak memory usage: 91 MB
% 35.35/6.57 % (3900237)Instructions burned: 136 (million)
% 35.35/6.57 % (3900239)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=780918803:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 35.35/6.57 % (3900239)Refutation not found, incomplete strategy
% 35.35/6.57 % (3900239)------------------------------
% 35.35/6.57 % (3900239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900239)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900239)Termination reason: Refutation not found, incomplete strategy
% 35.35/6.57 % (3900239)Time elapsed: 0.072 s
% 35.35/6.57 % (3900239)Peak memory usage: 95 MB
% 35.35/6.57 % (3900239)Instructions burned: 119 (million)
% 35.35/6.57 % (3900214)Instruction limit reached!
% 35.35/6.57 % (3900214)------------------------------
% 35.35/6.57 % (3900214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900214)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900214)Termination reason: Instruction limit
% 35.35/6.57 % (3900214)Termination phase: Saturation
% 35.35/6.57 % (3900214)Time elapsed: 1.367 s
% 35.35/6.57 % (3900214)Peak memory usage: 216 MB
% 35.35/6.57 % (3900214)Instructions burned: 2350 (million)
% 35.35/6.57 % (3900241)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2890900111:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2973 on theBenchmark for (2973ds/431Mi)
% 35.35/6.57 % (3900239)------------------------------
% 35.35/6.57 % (3900239)------------------------------
% 35.35/6.57 % (3900243)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3223852094:i=6060:aac=none:ins=25_2971 on theBenchmark for (2971ds/6060Mi)
% 35.35/6.57 % (3900241)Instruction limit reached!
% 35.35/6.57 % (3900241)------------------------------
% 35.35/6.57 % (3900241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900241)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900241)Termination reason: Instruction limit
% 35.35/6.57 % (3900241)Termination phase: Saturation
% 35.35/6.57 % (3900241)Time elapsed: 0.221 s
% 35.35/6.57 % (3900241)Peak memory usage: 96 MB
% 35.35/6.57 % (3900241)Instructions burned: 432 (million)
% 35.35/6.57 % (3900245)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2244564778:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 35.35/6.57 % (3900245)Instruction limit reached!
% 35.35/6.57 % (3900245)------------------------------
% 35.35/6.57 % (3900245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900245)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900245)Termination reason: Instruction limit
% 35.35/6.57 % (3900245)Termination phase: Preprocessing 3
% 35.35/6.57 % (3900245)Time elapsed: 0.090 s
% 35.35/6.57 % (3900245)Peak memory usage: 94 MB
% 35.35/6.57 % (3900245)Instructions burned: 151 (million)
% 35.35/6.57 % (3900247)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=735409187:i=14155:bd=all_2967 on theBenchmark for (2967ds/14155Mi)
% 35.35/6.57 % (3900225)Instruction limit reached!
% 35.35/6.57 % (3900225)------------------------------
% 35.35/6.57 % (3900225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900225)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900225)Termination reason: Instruction limit
% 35.35/6.57 % (3900225)Termination phase: Saturation
% 35.35/6.57 % (3900225)Time elapsed: 3.009 s
% 35.35/6.57 % (3900225)Peak memory usage: 197 MB
% 35.35/6.57 % (3900225)Instructions burned: 5204 (million)
% 35.35/6.57 % (3900249)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1063558690:i=667:av=off:fsr=off_2953 on theBenchmark for (2953ds/667Mi)
% 35.35/6.57 % (3900249)Instruction limit reached!
% 35.35/6.57 % (3900249)------------------------------
% 35.35/6.57 % (3900249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900249)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900249)Termination reason: Instruction limit
% 35.35/6.57 % (3900249)Termination phase: Property scanning
% 35.35/6.57 % (3900249)Time elapsed: 0.290 s
% 35.35/6.57 % (3900249)Peak memory usage: 98 MB
% 35.35/6.57 % (3900249)Instructions burned: 669 (million)
% 35.35/6.57 % (3900251)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=415767643:s2a=on:i=185:s2at=1.8:fdi=4_2949 on theBenchmark for (2949ds/185Mi)
% 35.35/6.57 % (3900251)Instruction limit reached!
% 35.35/6.57 % (3900251)------------------------------
% 35.35/6.57 % (3900251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900251)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900251)Termination reason: Instruction limit
% 35.35/6.57 % (3900251)Termination phase: NewCNF
% 35.35/6.57 % (3900251)Time elapsed: 0.109 s
% 35.35/6.57 % (3900251)Peak memory usage: 94 MB
% 35.35/6.57 % (3900251)Instructions burned: 185 (million)
% 35.35/6.57 % (3900233)First to succeed.
% 35.35/6.57 % (3900233)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3900186"
% 35.35/6.57 % (3900253)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2288736631:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2946 on theBenchmark for (2946ds/193Mi)
% 35.35/6.57 % (3900253)Instruction limit reached!
% 35.35/6.57 % (3900253)------------------------------
% 35.35/6.57 % (3900253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.35/6.57 % (3900253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.35/6.57 % (3900253)CaDiCaL version: 2.1.3
% 35.35/6.57 % (3900253)Termination reason: Instruction limit
% 35.35/6.57 % (3900253)Termination phase: Property scanning
% 35.35/6.57 % (3900253)Time elapsed: 0.114 s
% 35.35/6.57 % (3900253)Peak memory usage: 93 MB
% 35.35/6.57 % (3900253)Instructions burned: 194 (million)
% 35.35/6.57 % (3900192)Also succeeded, but the first one will report.
% 35.35/6.57 % (3900233)Refutation found. Thanks to Tanya!
% 35.35/6.57 % SZS status Theorem for theBenchmark
% 35.35/6.57 % SZS output start Proof for theBenchmark
% See solution above
% 36.00/6.76 % (3900233)------------------------------
% 36.00/6.76 % (3900233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 36.00/6.76 % (3900233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 36.00/6.76 % (3900233)CaDiCaL version: 2.1.3
% 36.00/6.76 % (3900233)Termination reason: Refutation
% 36.00/6.76 % (3900233)Time elapsed: 3.279 s
% 36.00/6.76 % (3900233)Peak memory usage: 194 MB
% 36.00/6.76 % (3900233)Instructions burned: 5612 (million)
% 36.00/6.76 % (3900233)------------------------------
% 36.00/6.76 % (3900233)------------------------------
% 36.00/6.76 % (3900186)Success in time 5.677 s
% 36.00/6.76 % Vampire exiting
%------------------------------------------------------------------------------