%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : NUM924+4 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:30 PM UTC 2026
% Result : ContradictoryAxioms 22.55s 4.95s
% Output : Refutation 27.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 36
% Syntax : Number of formulae : 192 ( 105 unt; 9 def)
% Number of atoms : 390 ( 104 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 369 ( 171 ~; 160 |; 15 &)
% ( 13 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 11 ( 9 usr; 8 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 26 con; 0-2 aty)
% Number of variables : 95 ( 0 sgn 95 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
is_int(min),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_Int_OMin) ).
fof(f12,axiom,
is_int(pls),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_Int_OPls) ).
fof(f34,axiom,
! [X0,X1] :
( is_int(X1)
=> is_int(hAPP_int_int(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__Int__Oint_000tc__Int__Oint) ).
fof(f36,axiom,
! [X0,X1] : is_int(hAPP_nat_int(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__Nat__Onat_000tc__Int__Oint) ).
fof(f50,axiom,
! [X0,X1] : is_int(hAPP_P1175774780nt_int(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__prod_Itc__Int__Oint_Mtc__Int__Oint_J_000tc__Int__Oint) ).
fof(f62,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_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/sandbox2/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(f63,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/sandbox2/benchmark/theBenchmark.p',fact_3_t) ).
fof(f113,axiom,
! [X0] :
( is_int(X0)
=> hAPP_int_int(number_number_of_int,X0) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_number__of__is__id) ).
fof(f123,axiom,
! [X0,X1] :
( ( is_int(X0)
& is_int(X1) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X1),X0))
=> X0 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_63_zle__antisym) ).
fof(f130,axiom,
! [X0,X1] :
( ( is_int(X0)
& is_int(X1) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_zless__le) ).
fof(f274,axiom,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_214_zero__le__power2) ).
fof(f286,axiom,
! [X0,X1] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_sum__power2__ge__zero) ).
fof(f316,axiom,
pls = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_256_Pls__def) ).
fof(f418,axiom,
! [X0,X1] :
( ( is_int(X0)
& is_int(X1) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int)))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| X0 = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_358_zless__add1__eq) ).
fof(f448,axiom,
one_one_int = hAPP_int_int(number_number_of_int,hAPP_int_int(bit1,pls)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_388_semiring__norm_I110_J) ).
fof(f874,axiom,
! [X0,X1] :
( ( is_int(X0)
& is_int(X1) )
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
=> ( X0 != X1
=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_814_order__le__neq__implies__less) ).
fof(f899,axiom,
! [X0] : hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),zero_zero_int) = zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_839_mult__zero__right) ).
fof(f920,axiom,
one_one_int != zero_zero_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_860_one__neq__zero) ).
fof(f1029,axiom,
! [X0] : hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,one_one_int),X0) = one_one_int,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_969_power__one) ).
fof(f1896,axiom,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),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/sandbox2/benchmark/theBenchmark.p',fact_1836__096sum2sq_A_Is_M_A1_J_A_061_A_I4_A_K_Am_A_L_A1_J_A_K_At_096) ).
fof(f3117,axiom,
one_one_nat = hAPP_nat_nat(suc,zero_zero_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3057_One__nat__def) ).
fof(f3256,axiom,
hAPP_nat_nat(suc,hAPP_nat_nat(suc,zero_zero_nat)) = hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3196_semiring__norm_I115_J) ).
fof(f3351,axiom,
hAPP_int_int(succ,pls) = hAPP_int_int(bit1,pls),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3291_succ__Pls) ).
fof(f3354,axiom,
! [X0] : hAPP_int_int(succ,X0) = hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X0),one_one_int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3294_succ__def) ).
fof(f3573,axiom,
! [X0] : hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,X0)) = hAPP_int_int(bit0,hAPP_int_int(uminus_uminus_int,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3513_minus__Bit0) ).
fof(f3598,axiom,
hAPP_int_int(uminus_uminus_int,min) = hAPP_int_int(bit1,pls),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3538_minus__Min) ).
fof(f4104,axiom,
hAPP_int_int(pred,min) = hAPP_int_int(bit0,min),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4044_pred__Min) ).
fof(f5542,plain,
! [X0,X1] :
( is_int(hAPP_int_int(X0,X1))
| ~ is_int(X1) ),
inference(ennf_transformation,[],[f34]) ).
fof(f5551,plain,
! [X0] :
( hAPP_int_int(number_number_of_int,X0) = X0
| ~ is_int(X0) ),
inference(ennf_transformation,[],[f113]) ).
fof(f5554,plain,
! [X0,X1] :
( X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X1),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(ennf_transformation,[],[f123]) ).
fof(f5555,plain,
! [X0,X1] :
( X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X1),X0))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(flattening,[],[f5554]) ).
fof(f5556,plain,
! [X0,X1] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(ennf_transformation,[],[f130]) ).
fof(f5557,plain,
! [X0,X1] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(flattening,[],[f5556]) ).
fof(f5662,plain,
! [X0,X1] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int)))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| X0 = X1 ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(ennf_transformation,[],[f418]) ).
fof(f5663,plain,
! [X0,X1] :
( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int)))
<=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| X0 = X1 ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(flattening,[],[f5662]) ).
fof(f5813,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(ennf_transformation,[],[f874]) ).
fof(f5814,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(flattening,[],[f5813]) ).
fof(f9527,plain,
! [X0,X1] :
( ( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| X0 = X1 )
& ( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(nnf_transformation,[],[f5557]) ).
fof(f9528,plain,
! [X0,X1] :
( ( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| X0 = X1 )
& ( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
& X0 != X1 )
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1)) ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(flattening,[],[f9527]) ).
fof(f9635,plain,
! [X0,X1] :
( ( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int)))
| ( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
& X0 != X1 ) )
& ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int))) ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(nnf_transformation,[],[f5663]) ).
fof(f9636,plain,
! [X0,X1] :
( ( ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int)))
| ( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
& X0 != X1 ) )
& ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int))) ) )
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(flattening,[],[f9635]) ).
fof(f11192,plain,
is_int(min),
inference(cnf_transformation,[],[f11]) ).
fof(f11193,plain,
is_int(pls),
inference(cnf_transformation,[],[f12]) ).
fof(f11215,plain,
! [X0,X1] :
( is_int(hAPP_int_int(X0,X1))
| ~ is_int(X1) ),
inference(cnf_transformation,[],[f5542]) ).
fof(f11217,plain,
! [X0,X1] : is_int(hAPP_nat_int(X0,X1)),
inference(cnf_transformation,[],[f36]) ).
fof(f11231,plain,
! [X0,X1] : is_int(hAPP_P1175774780nt_int(X0,X1)),
inference(cnf_transformation,[],[f50]) ).
fof(f11243,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_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,[],[f62]) ).
fof(f11244,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,[],[f63]) ).
fof(f11314,plain,
! [X0] :
( ~ is_int(X0)
| hAPP_int_int(number_number_of_int,X0) = X0 ),
inference(cnf_transformation,[],[f5551]) ).
fof(f11328,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X1),X0))
| X0 = X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(cnf_transformation,[],[f5555]) ).
fof(f11339,plain,
! [X0,X1] :
( X0 != X1
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(cnf_transformation,[],[f9528]) ).
fof(f11340,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(cnf_transformation,[],[f9528]) ).
fof(f11558,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))))),
inference(cnf_transformation,[],[f274]) ).
fof(f11576,plain,
! [X0,X1] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))))),
inference(cnf_transformation,[],[f286]) ).
fof(f11619,plain,
zero_zero_int = pls,
inference(cnf_transformation,[],[f316]) ).
fof(f11740,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X1),one_one_int)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(cnf_transformation,[],[f9636]) ).
fof(f11770,plain,
one_one_int = hAPP_int_int(number_number_of_int,hAPP_int_int(bit1,pls)),
inference(cnf_transformation,[],[f448]) ).
fof(f12297,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,X0),X1))
| X0 = X1
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(cnf_transformation,[],[f5814]) ).
fof(f12330,plain,
! [X0] : zero_zero_int = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),zero_zero_int),
inference(cnf_transformation,[],[f899]) ).
fof(f12351,plain,
one_one_int != zero_zero_int,
inference(cnf_transformation,[],[f920]) ).
fof(f12460,plain,
! [X0] : one_one_int = hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,one_one_int),X0),
inference(cnf_transformation,[],[f1029]) ).
fof(f13683,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_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)),
inference(cnf_transformation,[],[f1896]) ).
fof(f15356,plain,
one_one_nat = hAPP_nat_nat(suc,zero_zero_nat),
inference(cnf_transformation,[],[f3117]) ).
fof(f15548,plain,
hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))) = hAPP_nat_nat(suc,hAPP_nat_nat(suc,zero_zero_nat)),
inference(cnf_transformation,[],[f3256]) ).
fof(f15711,plain,
hAPP_int_int(bit1,pls) = hAPP_int_int(succ,pls),
inference(cnf_transformation,[],[f3351]) ).
fof(f15714,plain,
! [X0] : hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,X0),one_one_int) = hAPP_int_int(succ,X0),
inference(cnf_transformation,[],[f3354]) ).
fof(f16014,plain,
! [X0] : hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,X0)) = hAPP_int_int(bit0,hAPP_int_int(uminus_uminus_int,X0)),
inference(cnf_transformation,[],[f3573]) ).
fof(f16045,plain,
hAPP_int_int(bit1,pls) = hAPP_int_int(uminus_uminus_int,min),
inference(cnf_transformation,[],[f3598]) ).
fof(f16777,plain,
hAPP_int_int(pred,min) = hAPP_int_int(bit0,min),
inference(cnf_transformation,[],[f4104]) ).
fof(f18853,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_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(definition_unfolding,[],[f11243,f11619]) ).
fof(f18894,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))))),
inference(definition_unfolding,[],[f11558,f11619]) ).
fof(f18899,plain,
! [X0,X1] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls))))))),
inference(definition_unfolding,[],[f11576,f11619]) ).
fof(f18986,plain,
! [X0] : pls = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,X0),pls),
inference(definition_unfolding,[],[f12330,f11619,f11619]) ).
fof(f18989,plain,
one_one_int != pls,
inference(definition_unfolding,[],[f12351,f11619]) ).
fof(f20268,plain,
! [X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X1))
| ~ is_int(X1)
| ~ is_int(X1) ),
inference(equality_resolution,[],[f11339]) ).
fof(f20939,definition,
sF579 = hAPP_int_fun_nat_int(power_power_int,s),
introduced(definition,[new_symbols(definition,[sF579])],[function_definition]) ).
fof(f20940,plain,
hAPP_int_fun_nat_int(power_power_int,s) = sF579,
inference(reorient_equations,[],[f20939]) ).
fof(f20941,definition,
sF580 = hAPP_int_int(bit1,pls),
introduced(definition,[new_symbols(definition,[sF580])],[function_definition]) ).
fof(f20942,plain,
hAPP_int_int(bit1,pls) = sF580,
inference(reorient_equations,[],[f20941]) ).
fof(f21018,plain,
! [X1] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X1),X1))
| ~ is_int(X1) ),
inference(duplicate_literal_removal,[],[f20268]) ).
fof(f21104,definition,
( spl588_6
<=> is_int(pls) ),
introduced(definition,[new_symbols(definition,[spl588_6])],[avatar_definition]) ).
fof(f21105,plain,
( is_int(pls)
| ~ spl588_6 ),
inference(avatar_component_clause,[],[f21104]) ).
fof(f21695,plain,
hAPP_int_int(succ,pls) = hAPP_int_int(uminus_uminus_int,min),
inference(forward_demodulation,[],[f15711,f16045]) ).
fof(f21740,plain,
hAPP_nat_nat(suc,hAPP_nat_nat(suc,zero_zero_nat)) = hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(uminus_uminus_int,min))),
inference(forward_demodulation,[],[f15548,f16045]) ).
fof(f22028,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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))),t),
inference(forward_demodulation,[],[f13683,f15714]) ).
fof(f22456,plain,
one_one_int = hAPP_int_int(number_number_of_int,hAPP_int_int(uminus_uminus_int,min)),
inference(forward_demodulation,[],[f11770,f16045]) ).
fof(f22488,plain,
! [X0,X1] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),hAPP_int_int(succ,X1)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X0),X1))
| ~ is_int(X0)
| ~ is_int(X1) ),
inference(forward_demodulation,[],[f11740,f15714]) ).
fof(f22543,plain,
! [X0,X1] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(uminus_uminus_int,min))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(uminus_uminus_int,min))))))),
inference(forward_demodulation,[],[f18899,f16045]) ).
fof(f22556,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(uminus_uminus_int,min)))))),
inference(forward_demodulation,[],[f18894,f16045]) ).
fof(f22662,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(succ,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))))),
inference(forward_demodulation,[],[f11244,f15714]) ).
fof(f22663,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_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,[],[f18853,f18986]) ).
fof(f22664,plain,
spl588_6,
inference(avatar_split_clause,[],[f11193,f21104]) ).
fof(f22666,plain,
hAPP_int_int(uminus_uminus_int,min) = sF580,
inference(forward_demodulation,[],[f20942,f16045]) ).
fof(f22997,plain,
hAPP_nat_nat(suc,hAPP_nat_nat(suc,zero_zero_nat)) = hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,min))),
inference(forward_demodulation,[],[f21740,f16014]) ).
fof(f23122,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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(uminus_uminus_int,min))))),m))),t),
inference(forward_demodulation,[],[f22028,f16045]) ).
fof(f23432,plain,
! [X0,X1] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,min))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,min))))))),
inference(forward_demodulation,[],[f22543,f16014]) ).
fof(f23444,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,min)))))),
inference(forward_demodulation,[],[f22556,f16014]) ).
fof(f23522,plain,
hAPP_int_int(succ,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(uminus_uminus_int,min))))) = 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(uminus_uminus_int,min))))),m)),one_one_int)),t),
inference(forward_demodulation,[],[f22662,f16045]) ).
fof(f23523,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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))),t)),pls)),
inference(forward_demodulation,[],[f22663,f15714]) ).
fof(f23716,plain,
hAPP_nat_nat(suc,hAPP_nat_nat(suc,zero_zero_nat)) = hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))),
inference(forward_demodulation,[],[f22997,f16777]) ).
fof(f23814,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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(uminus_uminus_int,hAPP_int_int(bit0,min))))),m))),t),
inference(forward_demodulation,[],[f23122,f16014]) ).
fof(f23995,plain,
! [X0,X1] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X1),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))))))),
inference(forward_demodulation,[],[f23432,f16777]) ).
fof(f24007,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min)))))),
inference(forward_demodulation,[],[f23444,f16777]) ).
fof(f24078,plain,
hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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(uminus_uminus_int,min))))),m))),t) = hAPP_int_int(succ,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(uminus_uminus_int,min))))),
inference(forward_demodulation,[],[f23522,f15714]) ).
fof(f24079,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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(uminus_uminus_int,min))))),m))),t)),pls)),
inference(forward_demodulation,[],[f23523,f16045]) ).
fof(f24220,plain,
hAPP_nat_nat(suc,one_one_nat) = hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))),
inference(forward_demodulation,[],[f23716,f15356]) ).
fof(f24268,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,hAPP_int_int(bit0,min))))),m))),t),
inference(forward_demodulation,[],[f23814,f16014]) ).
fof(f24394,plain,
hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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(uminus_uminus_int,hAPP_int_int(bit0,min))))),m))),t) = hAPP_int_int(succ,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,min))))),
inference(forward_demodulation,[],[f24078,f16014]) ).
fof(f24395,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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(uminus_uminus_int,hAPP_int_int(bit0,min))))),m))),t)),pls)),
inference(forward_demodulation,[],[f24079,f16014]) ).
fof(f24526,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,hAPP_int_int(pred,min))))),m))),t),
inference(forward_demodulation,[],[f24268,f16777]) ).
fof(f24607,plain,
hAPP_int_int(succ,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))))) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,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(uminus_uminus_int,hAPP_int_int(pred,min))))),m))),t),
inference(forward_demodulation,[],[f24394,f16777]) ).
fof(f24608,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,hAPP_int_int(bit0,min))))),m))),t)),pls)),
inference(forward_demodulation,[],[f24395,f16014]) ).
fof(f24767,plain,
hAPP_int_int(succ,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))))) = hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,hAPP_int_int(pred,min))))),m))),t),
inference(forward_demodulation,[],[f24607,f16014]) ).
fof(f24768,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(succ,hAPP_int_int(hAPP_int_fun_int_int(times_times_int,hAPP_int_int(number_number_of_int,hAPP_int_int(uminus_uminus_int,hAPP_int_int(bit0,hAPP_int_int(pred,min))))),m))),t)),pls)),
inference(forward_demodulation,[],[f24608,f16777]) ).
fof(f24881,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(succ,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))))),
inference(forward_demodulation,[],[f24767,f24526]) ).
fof(f24882,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))),pls)),
inference(forward_demodulation,[],[f24768,f24526]) ).
fof(f24952,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(succ,hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,s),hAPP_nat_nat(suc,one_one_nat))),
inference(forward_demodulation,[],[f24881,f24220]) ).
fof(f25000,plain,
hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(succ,hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))),
inference(forward_demodulation,[],[f24952,f20940]) ).
fof(f25164,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))),pls))
| ~ is_int(hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)))
| ~ is_int(pls) ),
inference(resolution,[],[f11340,f24882]) ).
fof(f25171,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))),pls))
| ~ is_int(pls) ),
inference(forward_subsumption_resolution,[],[f25164,f11231]) ).
fof(f25172,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))),pls))
| ~ spl588_6 ),
inference(forward_subsumption_resolution,[],[f25171,f21105]) ).
fof(f25283,plain,
( pls = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))))
| ~ is_int(pls)
| ~ is_int(hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)))
| ~ spl588_6 ),
inference(resolution,[],[f25172,f11328]) ).
fof(f25286,plain,
( pls = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))))
| ~ is_int(hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)))
| ~ spl588_6 ),
inference(forward_subsumption_resolution,[],[f25283,f21105]) ).
fof(f25287,plain,
( pls = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))))
| ~ spl588_6 ),
inference(forward_subsumption_resolution,[],[f25286,f11231]) ).
fof(f25632,definition,
( spl588_81
<=> is_int(sF580) ),
introduced(definition,[new_symbols(definition,[spl588_81])],[avatar_definition]) ).
fof(f25633,plain,
( is_int(sF580)
| ~ spl588_81 ),
inference(avatar_component_clause,[],[f25632]) ).
fof(f25634,plain,
( ~ is_int(sF580)
| spl588_81 ),
inference(avatar_component_clause,[],[f25632]) ).
fof(f25640,definition,
( spl588_83
<=> one_one_int = sF580 ),
introduced(definition,[new_symbols(definition,[spl588_83])],[avatar_definition]) ).
fof(f25642,plain,
( one_one_int = sF580
| ~ spl588_83 ),
inference(avatar_component_clause,[],[f25640]) ).
fof(f25726,plain,
( is_int(sF580)
| ~ is_int(min) ),
inference(superposition,[],[f11215,f22666]) ).
fof(f25730,plain,
( ~ is_int(min)
| spl588_81 ),
inference(forward_subsumption_resolution,[],[f25726,f25634]) ).
fof(f25736,plain,
( $false
| spl588_81 ),
inference(forward_subsumption_resolution,[],[f25730,f11192]) ).
fof(f25737,plain,
spl588_81,
inference(avatar_contradiction_clause,[],[f25736]) ).
fof(f25903,plain,
( sF580 = hAPP_int_int(number_number_of_int,sF580)
| ~ spl588_81 ),
inference(resolution,[],[f25633,f11314]) ).
fof(f26055,plain,
one_one_int = hAPP_int_int(number_number_of_int,sF580),
inference(superposition,[],[f22456,f22666]) ).
fof(f26057,plain,
( one_one_int = sF580
| ~ spl588_81 ),
inference(forward_demodulation,[],[f26055,f25903]) ).
fof(f26229,plain,
( spl588_83
| ~ spl588_81 ),
inference(avatar_split_clause,[],[f26057,f25632,f25640]) ).
fof(f26447,plain,
( pls != sF580
| ~ spl588_83 ),
inference(superposition,[],[f18989,f25642]) ).
fof(f26896,plain,
( pls = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))))
| ~ spl588_6
| ~ spl588_83 ),
inference(forward_demodulation,[],[f25287,f25642]) ).
fof(f26916,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))))
| pls = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))
| ~ spl588_6
| ~ spl588_83 ),
inference(forward_demodulation,[],[f26896,f25642]) ).
fof(f26932,definition,
( spl588_145
<=> pls = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580)) ),
introduced(definition,[new_symbols(definition,[spl588_145])],[avatar_definition]) ).
fof(f26934,plain,
( pls = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))
| ~ spl588_145 ),
inference(avatar_component_clause,[],[f26932]) ).
fof(f26936,definition,
( spl588_146
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580)))) ),
introduced(definition,[new_symbols(definition,[spl588_146])],[avatar_definition]) ).
fof(f26938,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))))
| spl588_146 ),
inference(avatar_component_clause,[],[f26936]) ).
fof(f26939,plain,
( spl588_145
| ~ spl588_146
| ~ spl588_6
| ~ spl588_83 ),
inference(avatar_split_clause,[],[f26916,f25640,f21104,f26936,f26932]) ).
fof(f26961,plain,
! [X0] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(succ,X0)),X0))
| ~ is_int(hAPP_int_int(succ,X0))
| ~ is_int(X0)
| ~ is_int(hAPP_int_int(succ,X0)) ),
inference(resolution,[],[f22488,f21018]) ).
fof(f26974,plain,
! [X0] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(succ,X0)),X0))
| ~ is_int(hAPP_int_int(succ,X0))
| ~ is_int(X0) ),
inference(duplicate_literal_removal,[],[f26961]) ).
fof(f26985,plain,
! [X0] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(succ,X0)),X0))
| ~ is_int(X0) ),
inference(forward_subsumption_resolution,[],[f26974,f11215]) ).
fof(f27054,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(sF579,hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min))))))),
inference(superposition,[],[f23995,f20940]) ).
fof(f27069,plain,
! [X0] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))),hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,X0),hAPP_nat_nat(suc,one_one_nat))))),
inference(forward_demodulation,[],[f27054,f24220]) ).
fof(f27126,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))),one_one_int))),
inference(superposition,[],[f27069,f12460]) ).
fof(f27129,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_int_int(succ,hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))))),
inference(forward_demodulation,[],[f27126,f15714]) ).
fof(f27135,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)))),
inference(forward_demodulation,[],[f27129,f25000]) ).
fof(f27136,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))))
| ~ spl588_83 ),
inference(forward_demodulation,[],[f27135,f25642]) ).
fof(f27137,plain,
( $false
| ~ spl588_83
| spl588_146 ),
inference(forward_subsumption_resolution,[],[f27136,f26938]) ).
fof(f27138,plain,
( ~ spl588_83
| spl588_146 ),
inference(avatar_contradiction_clause,[],[f27137]) ).
fof(f27600,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(sF579,hAPP_int_nat(number_number_of_nat,hAPP_int_int(uminus_uminus_int,hAPP_int_int(pred,min)))))),
inference(superposition,[],[f24007,f20940]) ).
fof(f27603,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,pls),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat)))),
inference(forward_demodulation,[],[f27600,f24220]) ).
fof(f27634,plain,
( pls = hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))))
| ~ is_int(pls)
| ~ is_int(hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))) ),
inference(resolution,[],[f27603,f12297]) ).
fof(f28156,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))))
| ~ is_int(hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))) ),
inference(superposition,[],[f26985,f25000]) ).
fof(f28159,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int))),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat)))),
inference(forward_subsumption_resolution,[],[f28156,f11217]) ).
fof(f28162,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))))
| ~ spl588_83 ),
inference(forward_demodulation,[],[f28159,f25642]) ).
fof(f28164,plain,
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))))
| ~ spl588_83
| ~ spl588_145 ),
inference(forward_demodulation,[],[f28162,f26934]) ).
fof(f28170,plain,
( pls = hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))))
| ~ is_int(hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat)))
| ~ spl588_6 ),
inference(forward_subsumption_resolution,[],[f27634,f21105]) ).
fof(f28173,definition,
( spl588_198
<=> pls = hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat)) ),
introduced(definition,[new_symbols(definition,[spl588_198])],[avatar_definition]) ).
fof(f28175,plain,
( pls = hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))
| ~ spl588_198 ),
inference(avatar_component_clause,[],[f28173]) ).
fof(f28177,definition,
( spl588_199
<=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat)))) ),
introduced(definition,[new_symbols(definition,[spl588_199])],[avatar_definition]) ).
fof(f28181,plain,
( ~ spl588_199
| ~ spl588_83
| ~ spl588_145 ),
inference(avatar_split_clause,[],[f28164,f26932,f25640,f28177]) ).
fof(f28182,plain,
( pls = hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_nat_int(sF579,hAPP_nat_nat(suc,one_one_nat))))
| ~ spl588_6 ),
inference(forward_subsumption_resolution,[],[f28170,f11217]) ).
fof(f28184,plain,
( spl588_199
| spl588_198
| ~ spl588_6 ),
inference(avatar_split_clause,[],[f28182,f21104,f28173,f28177]) ).
fof(f29451,plain,
( hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(succ,pls)
| ~ spl588_198 ),
inference(superposition,[],[f25000,f28175]) ).
fof(f29472,plain,
( hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = hAPP_int_int(uminus_uminus_int,min)
| ~ spl588_198 ),
inference(forward_demodulation,[],[f29451,f21695]) ).
fof(f29475,plain,
( hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),one_one_int)) = sF580
| ~ spl588_198 ),
inference(forward_demodulation,[],[f29472,f22666]) ).
fof(f29478,plain,
( sF580 = hAPP_P1175774780nt_int(twoSqu1907779896sum2sq,hAPP_i1524277240nt_int(hAPP_i1584592887nt_int(product_Pair_int_int,s),sF580))
| ~ spl588_83
| ~ spl588_198 ),
inference(forward_demodulation,[],[f29475,f25642]) ).
fof(f29479,plain,
( pls = sF580
| ~ spl588_83
| ~ spl588_145
| ~ spl588_198 ),
inference(forward_demodulation,[],[f29478,f26934]) ).
fof(f29480,plain,
( $false
| ~ spl588_83
| ~ spl588_145
| ~ spl588_198 ),
inference(forward_subsumption_resolution,[],[f29479,f26447]) ).
fof(f29481,plain,
( ~ spl588_83
| ~ spl588_145
| ~ spl588_198 ),
inference(avatar_contradiction_clause,[],[f29480]) ).
cnf(s44,plain,
spl588_6,
inference(sat_conversion,[],[f22664]) ).
cnf(s84,plain,
spl588_81,
inference(sat_conversion,[],[f25737]) ).
cnf(s104,plain,
( ~ spl588_81
| spl588_83 ),
inference(sat_conversion,[],[f26229]) ).
cnf(s146,plain,
( ~ spl588_6
| ~ spl588_83
| spl588_145
| ~ spl588_146 ),
inference(sat_conversion,[],[f26939]) ).
cnf(s149,plain,
( ~ spl588_83
| spl588_146 ),
inference(sat_conversion,[],[f27138]) ).
cnf(s191,plain,
( ~ spl588_83
| ~ spl588_145
| ~ spl588_199 ),
inference(sat_conversion,[],[f28181]) ).
cnf(s192,plain,
( ~ spl588_6
| spl588_198
| spl588_199 ),
inference(sat_conversion,[],[f28184]) ).
cnf(s308,plain,
( ~ spl588_83
| ~ spl588_145
| ~ spl588_198 ),
inference(sat_conversion,[],[f29481]) ).
cnf(s309,plain,
spl588_83,
inference(rat,[],[s104,s84]) ).
cnf(s310,plain,
spl588_146,
inference(rat,[],[s149,s309]) ).
cnf(s316,plain,
spl588_145,
inference(rat,[],[s146,s310,s309,s44]) ).
cnf(s320,plain,
~ spl588_198,
inference(rat,[],[s308,s309,s316]) ).
cnf(s321,plain,
~ spl588_199,
inference(rat,[],[s191,s309,s316]) ).
cnf(s324,plain,
$false,
inference(rat,[],[s192,s44,s321,s320]) ).
fof(f29482,plain,
$false,
inference(avatar_sat_refutation,[],[s324]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n014.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.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 21:40:46 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.79/3.28 % (1196027)Detected formulas, will run a generic FOF schedule.
% 14.79/3.28 % (1196034)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=5870167:i=141695:sd=1:nm=32:gsp=on:ss=included_2996 on theBenchmark for (2996ds/141695Mi)
% 14.79/3.28 % (1196033)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=2985255897:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2996 on theBenchmark for (2996ds/134677Mi)
% 14.79/3.28 % (1196032)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=1128730266:i=141193_2996 on theBenchmark for (2996ds/141193Mi)
% 14.79/3.28 % (1196038)dis-21_1_sil=8000:lcm=predicate:random_seed=1687287594:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2996 on theBenchmark for (2996ds/129Mi)
% 14.79/3.28 % (1196037)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1257408658:s2a=on:i=139:gtg=position_2996 on theBenchmark for (2996ds/139Mi)
% 14.79/3.28 % (1196035)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1927674232:i=109:sd=1:ins=1:gsp=on:ss=axioms_2996 on theBenchmark for (2996ds/109Mi)
% 14.79/3.28 % (1196036)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2487100011:i=119:av=off:ss=axioms_2996 on theBenchmark for (2996ds/119Mi)
% 14.79/3.28 % (1196035)Instruction limit reached!
% 14.79/3.28 % (1196035)------------------------------
% 14.79/3.28 % (1196035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/3.28 % (1196035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/3.28 % (1196035)CaDiCaL version: 2.1.3
% 14.79/3.28 % (1196035)Termination reason: Instruction limit
% 14.79/3.28 % (1196035)Termination phase: Saturation
% 14.79/3.28 % (1196035)Time elapsed: 0.064 s
% 14.79/3.28 % (1196035)Peak memory usage: 94 MB
% 14.79/3.28 % (1196035)Instructions burned: 109 (million)
% 14.79/3.28 % (1196037)Instruction limit reached!
% 14.79/3.28 % (1196037)------------------------------
% 14.79/3.28 % (1196037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/3.28 % (1196037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/3.28 % (1196037)CaDiCaL version: 2.1.3
% 14.79/3.28 % (1196037)Termination reason: Instruction limit
% 14.79/3.28 % (1196037)Termination phase: SInE selection
% 14.79/3.28 % (1196037)Time elapsed: 0.066 s
% 14.79/3.28 % (1196037)Peak memory usage: 89 MB
% 14.79/3.28 % (1196037)Instructions burned: 140 (million)
% 14.79/3.28 % (1196036)Instruction limit reached!
% 14.79/3.28 % (1196036)------------------------------
% 14.79/3.28 % (1196036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/3.28 % (1196036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/3.28 % (1196036)CaDiCaL version: 2.1.3
% 14.79/3.28 % (1196036)Termination reason: Instruction limit
% 14.79/3.28 % (1196036)Termination phase: Function definition elimination
% 14.79/3.28 % (1196036)Time elapsed: 0.066 s
% 14.79/3.28 % (1196036)Peak memory usage: 92 MB
% 14.79/3.28 % (1196036)Instructions burned: 121 (million)
% 14.79/3.28 % (1196038)Instruction limit reached!
% 14.79/3.28 % (1196038)------------------------------
% 14.79/3.28 % (1196038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.79/3.28 % (1196038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.79/3.28 % (1196038)CaDiCaL version: 2.1.3
% 14.79/3.28 % (1196038)Termination reason: Instruction limit
% 14.79/3.28 % (1196038)Termination phase: Preprocessing 3
% 14.79/3.28 % (1196038)Time elapsed: 0.078 s
% 14.79/3.28 % (1196038)Peak memory usage: 93 MB
% 14.79/3.28 % (1196038)Instructions burned: 130 (million)
% 14.79/3.28 % (1196046)lrs+10_1_sil=8000:sp=occurrence:random_seed=1269003569:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 14.79/3.28 % (1196047)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3837247092:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 14.79/3.28 % (1196048)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2632108061:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 14.79/3.28 % (1196049)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=1655459591:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 14.79/3.28 % (1196047)Instruction limit reached!
% 21.95/4.23 % (1196047)------------------------------
% 21.95/4.23 % (1196047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.95/4.23 % (1196047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.95/4.23 % (1196047)CaDiCaL version: 2.1.3
% 21.95/4.23 % (1196047)Termination reason: Instruction limit
% 21.95/4.23 % (1196047)Termination phase: Saturation
% 21.95/4.23 % (1196047)Time elapsed: 0.072 s
% 21.95/4.23 % (1196047)Peak memory usage: 93 MB
% 21.95/4.23 % (1196047)Instructions burned: 157 (million)
% 21.95/4.23 % (1196049)Instruction limit reached!
% 21.95/4.23 % (1196049)------------------------------
% 21.95/4.23 % (1196049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.95/4.23 % (1196049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.95/4.23 % (1196049)CaDiCaL version: 2.1.3
% 21.95/4.23 % (1196049)Termination reason: Instruction limit
% 21.95/4.23 % (1196049)Termination phase: Preprocessing 3
% 21.95/4.23 % (1196049)Time elapsed: 0.124 s
% 21.95/4.23 % (1196049)Peak memory usage: 93 MB
% 21.95/4.23 % (1196049)Instructions burned: 249 (million)
% 21.95/4.23 % (1196046)Instruction limit reached!
% 21.95/4.23 % (1196046)------------------------------
% 21.95/4.23 % (1196046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.95/4.23 % (1196046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.95/4.23 % (1196046)CaDiCaL version: 2.1.3
% 21.95/4.23 % (1196046)Termination reason: Instruction limit
% 21.95/4.23 % (1196046)Termination phase: Saturation
% 21.95/4.23 % (1196046)Time elapsed: 0.154 s
% 21.95/4.23 % (1196046)Peak memory usage: 96 MB
% 21.95/4.23 % (1196046)Instructions burned: 286 (million)
% 21.95/4.23 % (1196048)Instruction limit reached!
% 21.95/4.23 % (1196048)------------------------------
% 21.95/4.23 % (1196048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.95/4.23 % (1196048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.95/4.23 % (1196048)CaDiCaL version: 2.1.3
% 21.95/4.23 % (1196048)Termination reason: Instruction limit
% 21.95/4.23 % (1196048)Termination phase: Saturation
% 21.95/4.23 % (1196048)Time elapsed: 0.201 s
% 21.95/4.23 % (1196048)Peak memory usage: 96 MB
% 21.95/4.23 % (1196048)Instructions burned: 325 (million)
% 21.95/4.23 % (1196054)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2404821415:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 21.95/4.23 % (1196055)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=570760842:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 21.95/4.23 % (1196056)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=503494982:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 21.95/4.23 % (1196057)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3515270009:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 21.95/4.23 % (1196054)Instruction limit reached!
% 21.95/4.23 % (1196054)------------------------------
% 21.95/4.23 % (1196054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.95/4.23 % (1196054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.95/4.23 % (1196054)CaDiCaL version: 2.1.3
% 21.95/4.23 % (1196054)Termination reason: Instruction limit
% 21.95/4.23 % (1196054)Termination phase: Property scanning
% 21.95/4.23 % (1196054)Time elapsed: 0.152 s
% 21.95/4.23 % (1196054)Peak memory usage: 94 MB
% 21.95/4.23 % (1196054)Instructions burned: 294 (million)
% 21.95/4.23 % (1196056)Instruction limit reached!
% 21.95/4.23 % (1196056)------------------------------
% 21.95/4.23 % (1196056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.95/4.23 % (1196056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.95/4.23 % (1196056)CaDiCaL version: 2.1.3
% 21.95/4.23 % (1196056)Termination reason: Instruction limit
% 21.95/4.23 % (1196056)Termination phase: Preprocessing 3
% 21.95/4.23 % (1196056)Time elapsed: 0.075 s
% 21.95/4.23 % (1196056)Peak memory usage: 93 MB
% 21.95/4.23 % (1196056)Instructions burned: 118 (million)
% 21.95/4.23 % (1196057)Instruction limit reached!
% 21.95/4.23 % (1196057)------------------------------
% 21.95/4.23 % (1196057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.95/4.23 % (1196057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.95/4.23 % (1196057)CaDiCaL version: 2.1.3
% 21.95/4.23 % (1196057)Termination reason: Instruction limit
% 22.55/4.95 % (1196057)Termination phase: Property scanning
% 22.55/4.95 % (1196057)Time elapsed: 0.079 s
% 22.55/4.95 % (1196057)Peak memory usage: 95 MB
% 22.55/4.95 % (1196057)Instructions burned: 128 (million)
% 22.55/4.95 % (1196062)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1414437077:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2988 on theBenchmark for (2988ds/114Mi)
% 22.55/4.95 % (1196063)lrs+10_1_sil=8000:sp=occurrence:random_seed=3823562876:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 22.55/4.95 % (1196062)Instruction limit reached!
% 22.55/4.95 % (1196062)------------------------------
% 22.55/4.95 % (1196062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196062)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196062)Termination reason: Instruction limit
% 22.55/4.95 % (1196062)Termination phase: Initialization
% 22.55/4.95 % (1196062)Time elapsed: 0.044 s
% 22.55/4.95 % (1196062)Peak memory usage: 89 MB
% 22.55/4.95 % (1196062)Instructions burned: 115 (million)
% 22.55/4.95 % (1196064)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1866846331:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 22.55/4.95 % (1196067)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1414697935:i=5202:ss=axioms:sgt=16_2986 on theBenchmark for (2986ds/5202Mi)
% 22.55/4.95 % (1196064)Instruction limit reached!
% 22.55/4.95 % (1196064)------------------------------
% 22.55/4.95 % (1196064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196064)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196064)Termination reason: Instruction limit
% 22.55/4.95 % (1196064)Termination phase: Property scanning
% 22.55/4.95 % (1196064)Time elapsed: 0.203 s
% 22.55/4.95 % (1196064)Peak memory usage: 95 MB
% 22.55/4.95 % (1196064)Instructions burned: 437 (million)
% 22.55/4.95 % (1196070)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1158684424:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2984 on theBenchmark for (2984ds/134Mi)
% 22.55/4.95 % (1196063)Instruction limit reached!
% 22.55/4.95 % (1196063)------------------------------
% 22.55/4.95 % (1196063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196063)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196063)Termination reason: Instruction limit
% 22.55/4.95 % (1196063)Termination phase: Saturation
% 22.55/4.95 % (1196063)Time elapsed: 0.491 s
% 22.55/4.95 % (1196063)Peak memory usage: 103 MB
% 22.55/4.95 % (1196063)Instructions burned: 908 (million)
% 22.55/4.95 % (1196070)Instruction limit reached!
% 22.55/4.95 % (1196070)------------------------------
% 22.55/4.95 % (1196070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196070)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196070)Termination reason: Instruction limit
% 22.55/4.95 % (1196070)Termination phase: NewCNF
% 22.55/4.95 % (1196070)Time elapsed: 0.091 s
% 22.55/4.95 % (1196070)Peak memory usage: 95 MB
% 22.55/4.95 % (1196070)Instructions burned: 134 (million)
% 22.55/4.95 % (1196072)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2146614505:st=8:i=592:sd=3:ep=RST:ss=axioms_2981 on theBenchmark for (2981ds/592Mi)
% 22.55/4.95 % (1196073)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4100925350:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 22.55/4.95 % (1196072)Instruction limit reached!
% 22.55/4.95 % (1196072)------------------------------
% 22.55/4.95 % (1196072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196072)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196072)Termination reason: Instruction limit
% 22.55/4.95 % (1196072)Termination phase: Property scanning
% 22.55/4.95 % (1196072)Time elapsed: 0.282 s
% 22.55/4.95 % (1196072)Peak memory usage: 97 MB
% 22.55/4.95 % (1196072)Instructions burned: 594 (million)
% 22.55/4.95 % (1196076)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=3898459327:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 22.55/4.95 % (1196076)Instruction limit reached!
% 22.55/4.95 % (1196076)------------------------------
% 22.55/4.95 % (1196076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196076)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196076)Termination reason: Instruction limit
% 22.55/4.95 % (1196076)Termination phase: SInE selection
% 22.55/4.95 % (1196076)Time elapsed: 0.055 s
% 22.55/4.95 % (1196076)Peak memory usage: 89 MB
% 22.55/4.95 % (1196076)Instructions burned: 126 (million)
% 22.55/4.95 % (1196055)Instruction limit reached!
% 22.55/4.95 % (1196055)------------------------------
% 22.55/4.95 % (1196055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196055)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196055)Termination reason: Instruction limit
% 22.55/4.95 % (1196055)Termination phase: Saturation
% 22.55/4.95 % (1196055)Time elapsed: 1.481 s
% 22.55/4.95 % (1196055)Peak memory usage: 219 MB
% 22.55/4.95 % (1196055)Instructions burned: 2350 (million)
% 22.55/4.95 % (1196078)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=324968127:i=134:gtgl=5:slsql=off:gtg=exists_sym_2975 on theBenchmark for (2975ds/134Mi)
% 22.55/4.95 % (1196079)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1425432374:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2974 on theBenchmark for (2974ds/141Mi)
% 22.55/4.95 % (1196078)Instruction limit reached!
% 22.55/4.95 % (1196078)------------------------------
% 22.55/4.95 % (1196078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196078)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196078)Termination reason: Instruction limit
% 22.55/4.95 % (1196078)Termination phase: Property scanning
% 22.55/4.95 % (1196078)Time elapsed: 0.055 s
% 22.55/4.95 % (1196078)Peak memory usage: 89 MB
% 22.55/4.95 % (1196078)Instructions burned: 135 (million)
% 22.55/4.95 % (1196079)Instruction limit reached!
% 22.55/4.95 % (1196079)------------------------------
% 22.55/4.95 % (1196079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196079)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196079)Termination reason: Instruction limit
% 22.55/4.95 % (1196079)Termination phase: Saturation
% 22.55/4.95 % (1196079)Time elapsed: 0.090 s
% 22.55/4.95 % (1196079)Peak memory usage: 95 MB
% 22.55/4.95 % (1196079)Instructions burned: 142 (million)
% 22.55/4.95 % (1196082)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3863712355:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 22.55/4.95 % (1196083)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=2253162124:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 22.55/4.95 % (1196082)Instruction limit reached!
% 22.55/4.95 % (1196082)------------------------------
% 22.55/4.95 % (1196082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196082)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196082)Termination reason: Instruction limit
% 22.55/4.95 % (1196082)Termination phase: Saturation
% 22.55/4.95 % (1196082)Time elapsed: 0.234 s
% 22.55/4.95 % (1196082)Peak memory usage: 96 MB
% 22.55/4.95 % (1196082)Instructions burned: 432 (million)
% 22.55/4.95 % (1196086)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=2095023762:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2968 on theBenchmark for (2968ds/150Mi)
% 22.55/4.95 % (1196086)Instruction limit reached!
% 22.55/4.95 % (1196086)------------------------------
% 22.55/4.95 % (1196086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/4.95 % (1196086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/4.95 % (1196086)CaDiCaL version: 2.1.3
% 22.55/4.95 % (1196086)Termination reason: Instruction limit
% 22.55/4.95 % (1196086)Termination phase: Preprocessing 3
% 22.55/4.95 % (1196086)Time elapsed: 0.090 s
% 22.55/4.95 % (1196086)Peak memory usage: 94 MB
% 22.55/4.95 % (1196086)Instructions burned: 152 (million)
% 22.55/4.95 % (1196088)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3683179407:i=14155:bd=all_2966 on theBenchmark for (2966ds/14155Mi)
% 22.55/4.95 % (1196032)First to succeed.
% 22.55/4.95 % (1196032)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1196027"
% 22.55/4.95 % (1196033)Also succeeded, but the first one will report.
% 22.55/4.95 % (1196032)Refutation found. Thanks to Tanya!
% 22.55/4.95 % SZS status ContradictoryAxioms for theBenchmark
% 22.55/4.95 % SZS output start Proof for theBenchmark
% See solution above
% 27.46/5.17 % (1196032)------------------------------
% 27.46/5.17 % (1196032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.46/5.17 % (1196032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.46/5.17 % (1196032)CaDiCaL version: 2.1.3
% 27.46/5.17 % (1196032)Termination reason: Refutation
% 27.46/5.17 % (1196032)Time elapsed: 3.283 s
% 27.46/5.17 % (1196032)Peak memory usage: 208 MB
% 27.46/5.17 % (1196032)Instructions burned: 5615 (million)
% 27.46/5.17 % (1196032)------------------------------
% 27.46/5.17 % (1196032)------------------------------
% 27.46/5.17 % (1196027)Success in time 4.089 s
% 27.46/5.17 % Vampire exiting
%------------------------------------------------------------------------------