%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM925+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 : n012.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:22 AM UTC 2026
% Result : Theorem 0.08s 0.37s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 8
% Syntax : Number of formulae : 36 ( 26 unt; 0 def)
% Number of atoms : 46 ( 23 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 18 ( 8 ~; 8 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 12 ( 0 sgn 4 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_22_less__number__of,axiom,
! [Xa,Ya] :
( ord_less_int(number_number_of_int(Xa),number_number_of_int(Ya))
<=> ord_less_int(Xa,Ya) ),
file('theBenchmark.p',fact_22_less__number__of) ).
fof(fact_83_Bit0__def,axiom,
! [K] : bit0(K) = plus_plus_int(K,K),
file('theBenchmark.p',fact_83_Bit0__def) ).
fof(fact_103_zero__less__power2,axiom,
! [A_1] :
( ord_less_int(zero_zero_int,power_power_int(A_1,number_number_of_nat(bit0(bit1(pls)))))
<=> A_1 != zero_zero_int ),
file('theBenchmark.p',fact_103_zero__less__power2) ).
fof(conj_0,conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int,
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ( power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_77,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_85,plain,
( A = zero_zero_int
| ord_less_int(zero_zero_int,power_power_int(A,number_number_of_nat(bit0(bit1(pls))))) ),
inference(clausify,[status(thm)],[fact_103_zero__less__power2]) ).
cnf(c_86,plain,
( zero_zero_int = A
| ord_less_int(zero_zero_int,power_power_int(A,number_number_of_nat(bit0(bit1(pls))))) ),
inference(copy,[status(thm)],[c_85]) ).
fof(fact_89_semiring__norm_I112_J,axiom,
zero_zero_int = number_number_of_int(pls),
file('theBenchmark.p',fact_89_semiring__norm_I112_J) ).
cnf(c_114,plain,
zero_zero_int = number_number_of_int(pls),
inference(clausify,[status(thm)],[fact_89_semiring__norm_I112_J]) ).
cnf(c_115,plain,
number_number_of_int(pls) = zero_zero_int,
inference(copy,[status(thm)],[c_114]) ).
cnf(c_122,plain,
bit0(A) = plus_plus_int(A,A),
inference(clausify,[status(thm)],[fact_83_Bit0__def]) ).
fof(fact_78_Pls__def,axiom,
pls = zero_zero_int,
file('theBenchmark.p',fact_78_Pls__def) ).
cnf(c_128,plain,
pls = zero_zero_int,
inference(clausify,[status(thm)],[fact_78_Pls__def]) ).
cnf(c_129,plain,
zero_zero_int = pls,
inference(copy,[status(thm)],[c_128]) ).
fof(fact_62_bin__less__0__simps_I1_J,axiom,
~ ord_less_int(pls,zero_zero_int),
file('theBenchmark.p',fact_62_bin__less__0__simps_I1_J) ).
cnf(c_162,plain,
~ ord_less_int(pls,zero_zero_int),
inference(clausify,[status(thm)],[fact_62_bin__less__0__simps_I1_J]) ).
cnf(c_163,plain,
~ ord_less_int(pls,pls),
inference(paramod,[status(thm)],[c_129,c_162]) ).
cnf(c_236,plain,
( ~ ord_less_int(A,B)
| ord_less_int(number_number_of_int(A),number_number_of_int(B)) ),
inference(clausify,[status(thm)],[fact_22_less__number__of]) ).
fof(fact_0_n1pos,axiom,
ord_less_int(zero_zero_int,plus_plus_int(one_one_int,semiri1621563631at_int(n))),
file('theBenchmark.p',fact_0_n1pos) ).
cnf(c_278,plain,
ord_less_int(zero_zero_int,plus_plus_int(one_one_int,semiri1621563631at_int(n))),
inference(clausify,[status(thm)],[fact_0_n1pos]) ).
cnf(c_279,plain,
ord_less_int(pls,plus_plus_int(one_one_int,semiri1621563631at_int(n))),
inference(paramod,[status(thm)],[c_129,c_278]) ).
cnf(c_566,plain,
( zero_zero_int = A
| ord_less_int(pls,power_power_int(A,number_number_of_nat(bit0(bit1(pls))))) ),
inference(paramod,[status(thm)],[c_129,c_86]) ).
cnf(c_567,plain,
( zero_zero_int = A
| ord_less_int(pls,power_power_int(A,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls))))) ),
inference(paramod,[status(thm)],[c_122,c_566]) ).
cnf(c_290,plain,
( pls = A
| ord_less_int(pls,power_power_int(A,number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls))))) ),
inference(paramod,[status(thm)],[c_129,c_567]) ).
cnf(c_568,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))) = zero_zero_int,
inference(paramod,[status(thm)],[c_122,c_77]) ).
cnf(c_295,negated_conjecture,
power_power_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)),number_number_of_nat(plus_plus_int(bit1(pls),bit1(pls)))) = pls,
inference(paramod,[status(thm)],[c_129,c_568]) ).
cnf(c_297,plain,
number_number_of_int(pls) = pls,
inference(paramod,[status(thm)],[c_129,c_115]) ).
cnf(c_569,plain,
ord_less_int(number_number_of_int(pls),number_number_of_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)))),
inference(resolve,[status(thm)],[c_279,c_236]) ).
cnf(c_511,plain,
ord_less_int(pls,number_number_of_int(plus_plus_int(one_one_int,semiri1621563631at_int(n)))),
inference(paramod,[status(thm)],[c_297,c_569]) ).
cnf(c_570,plain,
( pls = plus_plus_int(one_one_int,semiri1621563631at_int(n))
| ord_less_int(pls,pls) ),
inference(paramod,[status(thm)],[c_295,c_290]) ).
cnf(c_571,plain,
( plus_plus_int(one_one_int,semiri1621563631at_int(n)) = pls
| ord_less_int(pls,pls) ),
inference(copy,[status(thm)],[c_570]) ).
cnf(c_563,plain,
plus_plus_int(one_one_int,semiri1621563631at_int(n)) = pls,
inference(resolve,[status(thm)],[c_163,c_571]) ).
cnf(c_572,plain,
ord_less_int(pls,number_number_of_int(pls)),
inference(paramod,[status(thm)],[c_563,c_511]) ).
cnf(c_573,plain,
ord_less_int(pls,pls),
inference(paramod,[status(thm)],[c_297,c_572]) ).
cnf(c_565,plain,
$false,
inference(resolve,[status(thm)],[c_163,c_573]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM925+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sat Sep 26 04:18:06 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.32 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/0.32 % Process 3894744 was started by sandbox on n012,
% 0.03/0.32 % Sat Sep 26 04:18:06 2026
% 0.03/0.32 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.32
% 0.08/0.32 % From the command line: assign(max_seconds, 300).
% 0.08/0.37
% 0.08/0.37 % SZS status Theorem for theBenchmark
% 0.08/0.37
% 0.08/0.37 % Proof 1 at 0.02 (+ 0.01) seconds.
% 0.08/0.37 % Length of proof is 23.
% 0.08/0.37 % Level of proof is 5.
% 0.08/0.37 % Maximum clause weight is 13.000.
% 0.08/0.37 % Given clauses 97.
% 0.08/0.37
% 0.08/0.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------