%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM924+1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/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:20 AM UTC 2026
% Result : Theorem 0.09s 0.40s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 10
% Syntax : Number of formulae : 47 ( 47 unt; 0 def)
% Number of atoms : 47 ( 26 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-2 aty)
% Number of variables : 18 ( 1 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_24_number__of__is__id,axiom,
! [K_1] : number_number_of_int(K_1) = K_1,
file('theBenchmark.p',fact_24_number__of__is__id) ).
fof(fact_25_zmult__commute,axiom,
! [Z,W] : times_times_int(Z,W) = times_times_int(W,Z),
file('theBenchmark.p',fact_25_zmult__commute) ).
fof(fact_33_zpower__zadd__distrib,axiom,
! [X,Y,Z] : power_power_int(X,plus_plus_nat(Y,Z)) = times_times_int(power_power_int(X,Y),power_power_int(X,Z)),
file('theBenchmark.p',fact_33_zpower__zadd__distrib) ).
fof(fact_66_mult__Pls,axiom,
! [W] : times_times_int(pls,W) = pls,
file('theBenchmark.p',fact_66_mult__Pls) ).
fof(fact_104_zadd__commute,axiom,
! [Z,W] : plus_plus_int(Z,W) = plus_plus_int(W,Z),
file('theBenchmark.p',fact_104_zadd__commute) ).
fof(conj_0,conjecture,
ord_less_int(plus_plus_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,
~ ord_less_int(plus_plus_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,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_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_90,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),times_times_int(plus_plus_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,
plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int) = times_times_int(plus_plus_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_91,plain,
plus_plus_int(power_power_int(s,number_number_of_nat(bit0(bit1(pls)))),one_one_int) = times_times_int(plus_plus_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_130,plain,
number_number_of_int(A) = A,
inference(clausify,[status(thm)],[fact_24_number__of__is__id]) ).
cnf(c_131,plain,
times_times_int(A,B) = times_times_int(B,A),
inference(clausify,[status(thm)],[fact_25_zmult__commute]) ).
cnf(c_141,plain,
power_power_int(A,plus_plus_nat(B,C)) = times_times_int(power_power_int(A,B),power_power_int(A,C)),
inference(clausify,[status(thm)],[fact_33_zpower__zadd__distrib]) ).
fof(fact_65_nat__1__add__1,axiom,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
file('theBenchmark.p',fact_65_nat__1__add__1) ).
cnf(c_200,plain,
plus_plus_nat(one_one_nat,one_one_nat) = number_number_of_nat(bit0(bit1(pls))),
inference(clausify,[status(thm)],[fact_65_nat__1__add__1]) ).
cnf(c_201,plain,
number_number_of_nat(bit0(bit1(pls))) = plus_plus_nat(one_one_nat,one_one_nat),
inference(copy,[status(thm)],[c_200]) ).
cnf(c_202,plain,
times_times_int(pls,A) = pls,
inference(clausify,[status(thm)],[fact_66_mult__Pls]) ).
cnf(c_258,plain,
plus_plus_int(A,B) = plus_plus_int(B,A),
inference(clausify,[status(thm)],[fact_104_zadd__commute]) ).
fof(fact_105_zero__is__num__zero,axiom,
zero_zero_int = number_number_of_int(pls),
file('theBenchmark.p',fact_105_zero__is__num__zero) ).
cnf(c_259,plain,
zero_zero_int = number_number_of_int(pls),
inference(clausify,[status(thm)],[fact_105_zero__is__num__zero]) ).
cnf(c_260,plain,
zero_zero_int = pls,
inference(paramod,[status(thm)],[c_130,c_259]) ).
cnf(c_261,negated_conjecture,
~ ord_less_int(plus_plus_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_273,negated_conjecture,
~ ord_less_int(plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int),zero_zero_int),
inference(paramod,[status(thm)],[c_201,c_261]) ).
cnf(c_274,negated_conjecture,
~ ord_less_int(plus_plus_int(times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat)),one_one_int),zero_zero_int),
inference(paramod,[status(thm)],[c_141,c_273]) ).
cnf(c_275,negated_conjecture,
~ ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),zero_zero_int),
inference(paramod,[status(thm)],[c_258,c_274]) ).
cnf(c_262,negated_conjecture,
~ ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),pls),
inference(paramod,[status(thm)],[c_260,c_275]) ).
cnf(c_276,plain,
plus_plus_int(power_power_int(s,plus_plus_nat(one_one_nat,one_one_nat)),one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),
inference(paramod,[status(thm)],[c_201,c_91]) ).
cnf(c_277,plain,
plus_plus_int(times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat)),one_one_int) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),
inference(paramod,[status(thm)],[c_141,c_276]) ).
cnf(c_278,plain,
plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))) = times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),t),
inference(paramod,[status(thm)],[c_258,c_277]) ).
cnf(c_279,plain,
plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))) = times_times_int(plus_plus_int(times_times_int(bit0(bit0(bit1(pls))),m),one_one_int),t),
inference(paramod,[status(thm)],[c_130,c_278]) ).
cnf(c_280,plain,
plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))) = times_times_int(plus_plus_int(times_times_int(m,bit0(bit0(bit1(pls)))),one_one_int),t),
inference(paramod,[status(thm)],[c_131,c_279]) ).
cnf(c_281,plain,
plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))) = times_times_int(plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls))))),t),
inference(paramod,[status(thm)],[c_258,c_280]) ).
cnf(c_282,plain,
plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))) = times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls)))))),
inference(paramod,[status(thm)],[c_131,c_281]) ).
cnf(c_271,plain,
times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls)))))) = plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),
inference(copy,[status(thm)],[c_282]) ).
cnf(c_283,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(bit0(bit0(bit1(pls))),m),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_130,c_90]) ).
cnf(c_284,plain,
ord_less_int(times_times_int(plus_plus_int(times_times_int(m,bit0(bit0(bit1(pls)))),one_one_int),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_131,c_283]) ).
cnf(c_285,plain,
ord_less_int(times_times_int(plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls))))),t),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_258,c_284]) ).
cnf(c_286,plain,
ord_less_int(times_times_int(t,plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls)))))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_131,c_285]) ).
cnf(c_287,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),times_times_int(plus_plus_int(times_times_int(number_number_of_int(bit0(bit0(bit1(pls)))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_271,c_286]) ).
cnf(c_288,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),times_times_int(plus_plus_int(times_times_int(bit0(bit0(bit1(pls))),m),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_130,c_287]) ).
cnf(c_289,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),times_times_int(plus_plus_int(times_times_int(m,bit0(bit0(bit1(pls)))),one_one_int),zero_zero_int)),
inference(paramod,[status(thm)],[c_131,c_288]) ).
cnf(c_290,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),times_times_int(plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls))))),zero_zero_int)),
inference(paramod,[status(thm)],[c_258,c_289]) ).
cnf(c_291,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),times_times_int(plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls))))),pls)),
inference(paramod,[status(thm)],[c_260,c_290]) ).
cnf(c_292,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),times_times_int(pls,plus_plus_int(one_one_int,times_times_int(m,bit0(bit0(bit1(pls))))))),
inference(paramod,[status(thm)],[c_131,c_291]) ).
cnf(c_293,plain,
ord_less_int(plus_plus_int(one_one_int,times_times_int(power_power_int(s,one_one_nat),power_power_int(s,one_one_nat))),pls),
inference(paramod,[status(thm)],[c_202,c_292]) ).
cnf(c_272,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_262,c_293]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM924+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 04:20:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 3113300 was started by sandbox on n015,
% 0.09/0.37 % Sat Sep 26 04:20:57 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.39
% 0.09/0.39 % From the command line: assign(max_seconds, 300).
% 0.09/0.40
% 0.09/0.40 % SZS status Theorem for theBenchmark
% 0.09/0.40
% 0.09/0.40 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.09/0.40 % Length of proof is 21.
% 0.09/0.40 % Level of proof is 4.
% 0.09/0.40 % Maximum clause weight is 73.000.
% 0.09/0.40 % Given clauses 0.
% 0.09/0.40
% 0.09/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------