%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM925+4 : 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 : n019.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 100.51s 15.13s
% Output : CNFRefutation 115.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 6
% Syntax : Number of formulae : 20 ( 11 unt; 0 def)
% Number of atoms : 34 ( 17 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 32 ( 18 ~; 9 |; 1 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 12 con; 0-2 aty)
% Number of variables : 25 ( 11 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(gsy_c_hAPP_000tc__Int__Oint_000tc__Int__Oint,axiom,
! [B_1_1,B_2_1] :
( is_int(B_2_1)
=> is_int(hAPP_int_int(B_1_1,B_2_1)) ),
file('theBenchmark.p',gsy_c_hAPP_000tc__Int__Oint_000tc__Int__Oint) ).
fof(gsy_c_hAPP_000tc__Nat__Onat_000tc__Int__Oint,axiom,
! [B_1_1,B_2_1] : is_int(hAPP_nat_int(B_1_1,B_2_1)),
file('theBenchmark.p',gsy_c_hAPP_000tc__Nat__Onat_000tc__Int__Oint) ).
fof(fact_451_power__eq__0__iff,axiom,
! [A_1,Na] :
( is_int(A_1)
=> ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A_1),Na) = zero_zero_int
<=> ( Na != zero_zero_nat
& A_1 = zero_zero_int ) ) ),
file('theBenchmark.p',fact_451_power__eq__0__iff) ).
fof(fact_1824_less__imp__neq,axiom,
! [X_32,Y_26] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,X_32),Y_26))
=> X_32 != Y_26 ),
file('theBenchmark.p',fact_1824_less__imp__neq) ).
fof(conj_0,conjecture,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) != zero_zero_int,
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) != zero_zero_int ),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_2531,plain,
( A = zero_zero_int
| hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A),B) != zero_zero_int
| ~ is_int(A) ),
inference(clausify,[status(thm)],[fact_451_power__eq__0__iff]) ).
cnf(c_2532,plain,
( zero_zero_int = A
| hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A),B) != zero_zero_int
| ~ is_int(A) ),
inference(copy,[status(thm)],[c_2531]) ).
cnf(c_2900,plain,
( B != A
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,A),B)) ),
inference(clausify,[status(thm)],[fact_1824_less__imp__neq]) ).
cnf(c_4409,plain,
( is_int(hAPP_int_int(B,A))
| ~ is_int(A) ),
inference(clausify,[status(thm)],[gsy_c_hAPP_000tc__Int__Oint_000tc__Int__Oint]) ).
cnf(c_4410,plain,
is_int(hAPP_nat_int(A,B)),
inference(clausify,[status(thm)],[gsy_c_hAPP_000tc__Nat__Onat_000tc__Int__Oint]) ).
fof(fact_0_n1pos,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
file('theBenchmark.p',fact_0_n1pos) ).
cnf(c_4414,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(clausify,[status(thm)],[fact_0_n1pos]) ).
cnf(c_6220,negated_conjecture,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),hAPP_int_nat(number_number_of_nat,hAPP_int_int(bit0,hAPP_int_int(bit1,pls)))) = zero_zero_int,
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_8250,plain,
is_int(hAPP_int_int(A,hAPP_nat_int(B,C))),
inference(resolve,[status(thm)],[c_4409,c_4410]) ).
cnf(c_11145,plain,
hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n)) != zero_zero_int,
inference(resolve,[status(thm)],[c_4414,c_2900]) ).
cnf(c_59335,plain,
( A = zero_zero_int
| hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,A),B) != zero_zero_int
| ~ is_int(A) ),
inference(copy,[status(thm)],[c_2532]) ).
cnf(c_59336,plain,
( hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),A) != zero_zero_int
| ~ is_int(hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))) ),
inference(resolve,[status(thm)],[c_11145,c_59335]) ).
cnf(c_59333,plain,
hAPP_nat_int(hAPP_int_fun_nat_int(power_power_int,hAPP_int_int(hAPP_int_fun_int_int(plus_plus_int,one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),A) != zero_zero_int,
inference(resolve,[status(thm)],[c_8250,c_59336]) ).
cnf(c_59334,plain,
$false,
inference(resolve,[status(thm)],[c_59333,c_6220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM925+4 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.38 % Computer : n019.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:19:06 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 390773 was started by sandbox on n019,
% 0.09/0.38 % Sat Sep 26 04:19:06 2026
% 0.09/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 100.51/15.13
% 100.51/15.13 % SInE (scan): 1722 to sos (tol 1.5x), 784 to usable (tol 2.0x), 2980 zapped, of 5486 axioms (depth 3).
% 100.51/15.13
% 100.51/15.13 % From the command line: assign(max_seconds, 300).
% 100.51/15.13
% 100.51/15.13 % given #500 (T,wt=18): 25831 hAPP_int_int(bit0,c5) = pls | pls != c5. [resolve(4494,a,3181,a)].
% 100.51/15.13
% 100.51/15.13 % given #1000 (F,wt=23): 31694 hAPP_int_int(legacy_zgcd(one_one_int),f169(one_one_int,v)) != pls. [para(4499(a,1),24548(a,2))].
% 100.51/15.13
% 100.51/15.13 % SZS status Theorem for theBenchmark
% 100.51/15.13
% 100.51/15.13 % Proof 1 at 12.20 (+ 1.91) seconds.
% 100.51/15.13 % Length of proof is 16.
% 100.51/15.13 % Level of proof is 4.
% 100.51/15.13 % Maximum clause weight is 44.000.
% 100.51/15.13 % Given clauses 1302.
% 100.51/15.13
% 100.51/15.13 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------