%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM925+2 : 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 : n005.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:23 AM UTC 2026
% Result : Theorem 23.73s 3.94s
% Output : CNFRefutation 23.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of formulae : 21 ( 13 unt; 0 def)
% Number of atoms : 37 ( 24 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 36 ( 20 ~; 11 |; 1 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-2 aty)
% Number of variables : 17 ( 4 sgn 5 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_231_field__power__not__zero,axiom,
! [N_23,A_62] :
( A_62 != zero_zero_int
=> hAPP_nat_int(power_power_int(A_62),N_23) != zero_zero_int ),
file('theBenchmark.p',fact_231_field__power__not__zero) ).
fof(fact_476_add__nonneg__eq__0__iff,axiom,
! [Ya,Xa] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),Xa))
=> ( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),Ya))
=> ( hAPP_int_int(plus_plus_int(Xa),Ya) = zero_zero_int
<=> ( Ya = zero_zero_int
& Xa = zero_zero_int ) ) ) ),
file('theBenchmark.p',fact_476_add__nonneg__eq__0__iff) ).
fof(fact_512_zero__le__imp__of__nat,axiom,
! [M_2] : hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,M_2))),
file('theBenchmark.p',fact_512_zero__le__imp__of__nat) ).
fof(conj_0,conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_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,
~ ( hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) != zero_zero_int ),
inference(assume_negation,[status(cth)],[conj_0]) ).
fof(fact_99_int__0__neq__1,axiom,
zero_zero_int != one_one_int,
file('theBenchmark.p',fact_99_int__0__neq__1) ).
cnf(c_869,plain,
zero_zero_int != one_one_int,
inference(clausify,[status(thm)],[fact_99_int__0__neq__1]) ).
cnf(c_1044,plain,
( hAPP_nat_int(power_power_int(A),B) != zero_zero_int
| A = zero_zero_int ),
inference(clausify,[status(thm)],[fact_231_field__power__not__zero]) ).
cnf(c_1045,plain,
( hAPP_nat_int(power_power_int(A),B) != zero_zero_int
| zero_zero_int = A ),
inference(copy,[status(thm)],[c_1044]) ).
cnf(c_1243,plain,
( A = zero_zero_int
| hAPP_int_int(plus_plus_int(A),B) != zero_zero_int
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A)) ),
inference(clausify,[status(thm)],[fact_476_add__nonneg__eq__0__iff]) ).
cnf(c_1244,plain,
( zero_zero_int = A
| hAPP_int_int(plus_plus_int(A),B) != zero_zero_int
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),B))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A)) ),
inference(copy,[status(thm)],[c_1243]) ).
fof(fact_497_zero__le__one,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int)),
file('theBenchmark.p',fact_497_zero__le__one) ).
cnf(c_1269,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),one_one_int)),
inference(clausify,[status(thm)],[fact_497_zero__le__one]) ).
cnf(c_1285,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),hAPP_nat_int(semiri1621563631at_int,A))),
inference(clausify,[status(thm)],[fact_512_zero__le__imp__of__nat]) ).
cnf(c_1447,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_17262,plain,
( zero_zero_int = one_one_int
| hAPP_int_int(plus_plus_int(one_one_int),A) != zero_zero_int
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A)) ),
inference(resolve,[status(thm)],[c_1244,c_1269]) ).
cnf(c_13699,plain,
( hAPP_int_int(plus_plus_int(one_one_int),A) != zero_zero_int
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_eq_int,zero_zero_int),A)) ),
inference(resolve,[status(thm)],[c_869,c_17262]) ).
cnf(c_15261,plain,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,A)) != zero_zero_int,
inference(resolve,[status(thm)],[c_13699,c_1285]) ).
cnf(c_17263,negated_conjecture,
zero_zero_int = hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)),
inference(resolve,[status(thm)],[c_1447,c_1045]) ).
cnf(c_17264,negated_conjecture,
hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) = zero_zero_int,
inference(copy,[status(thm)],[c_17263]) ).
cnf(c_17261,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_15261,c_17264]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+2 : 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.36 % Computer : n005.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:18:01 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 1181825 was started by sandbox2 on n005,
% 0.09/0.36 % Sat Sep 26 04:18:01 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.22/0.49
% 0.22/0.49 % From the command line: assign(max_seconds, 300).
% 0.22/0.49
% 0.22/0.49 % SInE: 640 to sos, 67 to usable, of 707 axioms (tolerance 2.00, depth 0 fixpoint).
% 23.73/3.94
% 23.73/3.94 % given #500 (F,wt=21): 4881 hAPP_int_int(plus_plus_int(pls),one_one_int) != pls. [para(811(a,1),4877(a,1))].
% 23.73/3.94
% 23.73/3.94 % given #1000 (W,wt=19): 6350 number_number_of_int(pls) != one_one_nat | number_number_of_nat(one_one_int) = bit0(zero_zero_int). [para(981(a,1),6063(a,2))].
% 23.73/3.94
% 23.73/3.94 % given #1500 (F,wt=25): 6667 hAPP_nat_nat(power_power_nat(A),number_number_of_int(zero_zero_nat)) != hAPP_nat_nat(semiri984289939at_nat,number_number_of_nat(pls)). [para(6203(a,1),2220(a,1,2))].
% 23.73/3.94
% 23.73/3.94 % given #2000 (T,wt=20): 15308 number_number_of_int(pls) != bit0(zero_zero_nat) | number_number_of_nat(pls) = number_number_of_int(pls). [para(4216(a,1),3220(a,2)),flip(a)].
% 23.73/3.94
% 23.73/3.94 % SZS status Theorem for theBenchmark
% 23.73/3.94
% 23.73/3.94 % Proof 1 at 2.66 (+ 0.67) seconds.
% 23.73/3.94 % Length of proof is 15.
% 23.73/3.94 % Level of proof is 5.
% 23.73/3.94 % Maximum clause weight is 39.000.
% 23.73/3.94 % Given clauses 2290.
% 23.73/3.94
% 23.73/3.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------