%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM924+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Sun Sep 27 08:18:21 AM UTC 2026
% Result : Theorem 0.30s 0.69s
% Output : CNFRefutation 0.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 14
% Syntax : Number of formulae : 80 ( 80 unt; 0 def)
% Number of atoms : 80 ( 48 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 8 ( 8 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 14 ( 4 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 7 con; 0-2 aty)
% Number of variables : 31 ( 1 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_35_zmult__commute,axiom,
! [Z,W] : hAPP_int_int(times_times_int(Z),W) = hAPP_int_int(times_times_int(W),Z),
file('theBenchmark.p',fact_35_zmult__commute) ).
fof(fact_88_mult__Pls,axiom,
! [W] : hAPP_int_int(times_times_int(pls),W) = pls,
file('theBenchmark.p',fact_88_mult__Pls) ).
fof(fact_132_zadd__assoc,axiom,
! [Z1,Z2,Z3] : hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(Z1),Z2)),Z3) = hAPP_int_int(plus_plus_int(Z1),hAPP_int_int(plus_plus_int(Z2),Z3)),
file('theBenchmark.p',fact_132_zadd__assoc) ).
fof(fact_134_zadd__commute,axiom,
! [Z,W] : hAPP_int_int(plus_plus_int(Z),W) = hAPP_int_int(plus_plus_int(W),Z),
file('theBenchmark.p',fact_134_zadd__commute) ).
fof(fact_182_Bit0__def,axiom,
! [K_1] : bit0(K_1) = hAPP_int_int(plus_plus_int(K_1),K_1),
file('theBenchmark.p',fact_182_Bit0__def) ).
fof(fact_236_Bit1__def,axiom,
! [K_1] : bit1(K_1) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),K_1)),K_1),
file('theBenchmark.p',fact_236_Bit1__def) ).
fof(fact_248_number__of__Bit1,axiom,
! [W_3] : number_number_of_int(bit1(W_3)) = hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(W_3))),number_number_of_int(W_3)),
file('theBenchmark.p',fact_248_number__of__Bit1) ).
fof(fact_285_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,axiom,
! [X_16] : hAPP_int_int(times_times_int(X_16),X_16) = hAPP_nat_int(power_power_int(X_16),number_number_of_nat(bit0(bit1(pls)))),
file('theBenchmark.p',fact_285_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J) ).
fof(conj_0,conjecture,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(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,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
file('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) ).
cnf(c_1292,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(clausify,[status(thm)],[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(fact_3_t,axiom,
hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
file('theBenchmark.p',fact_3_t) ).
cnf(c_1293,plain,
hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
inference(clausify,[status(thm)],[fact_3_t]) ).
cnf(c_1362,plain,
hAPP_int_int(times_times_int(A),B) = hAPP_int_int(times_times_int(B),A),
inference(clausify,[status(thm)],[fact_35_zmult__commute]) ).
cnf(c_1442,plain,
hAPP_int_int(times_times_int(pls),A) = pls,
inference(clausify,[status(thm)],[fact_88_mult__Pls]) ).
cnf(c_1505,plain,
hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(A),B)),C) = hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(B),C)),
inference(clausify,[status(thm)],[fact_132_zadd__assoc]) ).
cnf(c_1507,plain,
hAPP_int_int(plus_plus_int(A),B) = hAPP_int_int(plus_plus_int(B),A),
inference(clausify,[status(thm)],[fact_134_zadd__commute]) ).
fof(fact_135_zero__is__num__zero,axiom,
zero_zero_int = number_number_of_int(pls),
file('theBenchmark.p',fact_135_zero__is__num__zero) ).
cnf(c_1508,plain,
zero_zero_int = number_number_of_int(pls),
inference(clausify,[status(thm)],[fact_135_zero__is__num__zero]) ).
fof(fact_172_Pls__def,axiom,
pls = zero_zero_int,
file('theBenchmark.p',fact_172_Pls__def) ).
cnf(c_1590,plain,
pls = zero_zero_int,
inference(clausify,[status(thm)],[fact_172_Pls__def]) ).
cnf(c_3475,plain,
pls = number_number_of_int(pls),
inference(paramod,[status(thm)],[c_1508,c_1590]) ).
cnf(c_1591,plain,
number_number_of_int(pls) = pls,
inference(copy,[status(thm)],[c_3475]) ).
cnf(c_1602,plain,
hAPP_int_int(plus_plus_int(A),A) = bit0(A),
inference(clausify,[status(thm)],[fact_182_Bit0__def]) ).
cnf(c_1603,plain,
bit0(A) = hAPP_int_int(plus_plus_int(A),A),
inference(copy,[status(thm)],[c_1602]) ).
cnf(c_1687,plain,
hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),A)),A) = bit1(A),
inference(clausify,[status(thm)],[fact_236_Bit1__def]) ).
cnf(c_1688,plain,
hAPP_int_int(plus_plus_int(A),hAPP_int_int(plus_plus_int(one_one_int),A)) = bit1(A),
inference(paramod,[status(thm)],[c_1507,c_1687]) ).
cnf(c_1708,plain,
hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(A))),number_number_of_int(A)) = number_number_of_int(bit1(A)),
inference(clausify,[status(thm)],[fact_248_number__of__Bit1]) ).
cnf(c_3476,plain,
hAPP_int_int(plus_plus_int(number_number_of_int(A)),hAPP_int_int(plus_plus_int(one_one_int),number_number_of_int(A))) = number_number_of_int(bit1(A)),
inference(paramod,[status(thm)],[c_1507,c_1708]) ).
cnf(c_3477,plain,
bit1(number_number_of_int(A)) = number_number_of_int(bit1(A)),
inference(paramod,[status(thm)],[c_1688,c_3476]) ).
cnf(c_1709,plain,
number_number_of_int(bit1(A)) = bit1(number_number_of_int(A)),
inference(copy,[status(thm)],[c_3477]) ).
fof(fact_251_semiring__numeral__1__eq__1,axiom,
number_number_of_int(bit1(pls)) = one_one_int,
file('theBenchmark.p',fact_251_semiring__numeral__1__eq__1) ).
cnf(c_1712,plain,
number_number_of_int(bit1(pls)) = one_one_int,
inference(clausify,[status(thm)],[fact_251_semiring__numeral__1__eq__1]) ).
cnf(c_3478,plain,
bit1(number_number_of_int(pls)) = one_one_int,
inference(paramod,[status(thm)],[c_1709,c_1712]) ).
cnf(c_1713,plain,
bit1(pls) = one_one_int,
inference(paramod,[status(thm)],[c_1591,c_3478]) ).
cnf(c_1789,plain,
hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(bit1(pls)))) = hAPP_int_int(times_times_int(A),A),
inference(clausify,[status(thm)],[fact_285_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J]) ).
cnf(c_3479,plain,
hAPP_nat_int(power_power_int(A),number_number_of_nat(bit0(one_one_int))) = hAPP_int_int(times_times_int(A),A),
inference(paramod,[status(thm)],[c_1713,c_1789]) ).
cnf(c_1790,plain,
hAPP_nat_int(power_power_int(A),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int))) = hAPP_int_int(times_times_int(A),A),
inference(paramod,[status(thm)],[c_1603,c_3479]) ).
cnf(c_3464,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(bit1(pls))))),one_one_int)),zero_zero_int)),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_3480,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(one_one_int)))),one_one_int)),zero_zero_int)),
inference(paramod,[status(thm)],[c_1713,c_3464]) ).
cnf(c_3481,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),one_one_int)),zero_zero_int)),
inference(paramod,[status(thm)],[c_1603,c_3480]) ).
cnf(c_3482,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(s),s)),one_one_int)),zero_zero_int)),
inference(paramod,[status(thm)],[c_1790,c_3481]) ).
cnf(c_3483,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),zero_zero_int)),
inference(paramod,[status(thm)],[c_1507,c_3482]) ).
cnf(c_3484,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),number_number_of_int(pls))),
inference(paramod,[status(thm)],[c_1508,c_3483]) ).
cnf(c_3465,negated_conjecture,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),pls)),
inference(paramod,[status(thm)],[c_1591,c_3484]) ).
cnf(c_3485,plain,
hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(bit0(one_one_int)))),one_one_int) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1713,c_1293]) ).
cnf(c_3486,plain,
hAPP_int_int(plus_plus_int(hAPP_nat_int(power_power_int(s),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),one_one_int) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1603,c_3485]) ).
cnf(c_3487,plain,
hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(s),s)),one_one_int) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1790,c_3486]) ).
cnf(c_3488,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1507,c_3487]) ).
cnf(c_3489,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(one_one_int)))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1713,c_3488]) ).
cnf(c_3490,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1603,c_3489]) ).
cnf(c_3491,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1603,c_3490]) ).
cnf(c_3492,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1505,c_3491]) ).
cnf(c_3493,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))),m)),one_one_int)),t),
inference(paramod,[status(thm)],[c_1688,c_3492]) ).
cnf(c_3494,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int))))),one_one_int)),t),
inference(paramod,[status(thm)],[c_1362,c_3493]) ).
cnf(c_3495,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))),t),
inference(paramod,[status(thm)],[c_1507,c_3494]) ).
cnf(c_3496,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)) = hAPP_int_int(times_times_int(t),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))),
inference(paramod,[status(thm)],[c_1362,c_3495]) ).
cnf(c_3473,plain,
hAPP_int_int(times_times_int(t),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))) = hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s)),
inference(copy,[status(thm)],[c_3496]) ).
cnf(c_3497,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(one_one_int)))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1713,c_1292]) ).
cnf(c_3498,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1603,c_3497]) ).
cnf(c_3499,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1603,c_3498]) ).
cnf(c_3500,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1505,c_3499]) ).
cnf(c_3501,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))),m)),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1688,c_3500]) ).
cnf(c_3502,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int))))),one_one_int)),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1362,c_3501]) ).
cnf(c_3503,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))),t)),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1507,c_3502]) ).
cnf(c_3504,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(times_times_int(t),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int))))))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1362,c_3503]) ).
cnf(c_3505,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_3473,c_3504]) ).
cnf(c_3506,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(bit0(one_one_int)))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1713,c_3505]) ).
cnf(c_3507,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(bit0(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1603,c_3506]) ).
cnf(c_3508,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(one_one_int),one_one_int)),hAPP_int_int(plus_plus_int(one_one_int),one_one_int)))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1603,c_3507]) ).
cnf(c_3509,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(plus_plus_int(one_one_int),one_one_int))))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1505,c_3508]) ).
cnf(c_3510,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))),m)),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1688,c_3509]) ).
cnf(c_3511,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int))))),one_one_int)),zero_zero_int))),
inference(paramod,[status(thm)],[c_1362,c_3510]) ).
cnf(c_3512,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))),zero_zero_int))),
inference(paramod,[status(thm)],[c_1507,c_3511]) ).
cnf(c_3513,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))),number_number_of_int(pls)))),
inference(paramod,[status(thm)],[c_1508,c_3512]) ).
cnf(c_3514,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))),pls))),
inference(paramod,[status(thm)],[c_1591,c_3513]) ).
cnf(c_3515,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),hAPP_int_int(times_times_int(pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(m),number_number_of_int(hAPP_int_int(plus_plus_int(one_one_int),bit1(one_one_int)))))))),
inference(paramod,[status(thm)],[c_1362,c_3514]) ).
cnf(c_3516,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,hAPP_int_int(plus_plus_int(one_one_int),hAPP_int_int(times_times_int(s),s))),pls)),
inference(paramod,[status(thm)],[c_1442,c_3515]) ).
cnf(c_3474,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3465,c_3516]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM924+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n015.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Sat Sep 26 04:20:28 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.38 % Process 3112385 was started by sandbox2 on n015,
% 0.09/0.38 % Sat Sep 26 04:20:28 2026
% 0.09/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.21/0.54
% 0.21/0.54 % From the command line: assign(max_seconds, 300).
% 0.21/0.54
% 0.21/0.54 % SInE: 1119 to sos, 110 to usable, of 1229 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.30/0.69
% 0.30/0.69 % SZS status Theorem for theBenchmark
% 0.30/0.69
% 0.30/0.69 % Proof 1 at 0.07 (+ 0.03) seconds.
% 0.30/0.69 % Length of proof is 32.
% 0.30/0.69 % Level of proof is 7.
% 0.30/0.69 % Maximum clause weight is 207.000.
% 0.30/0.69 % Given clauses 0.
% 0.30/0.69
% 0.30/0.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------