%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM926+7 : 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 : n016.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:25 AM UTC 2026
% Result : Theorem 6.48s 16.30s
% Output : CNFRefutation 6.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 12
% Syntax : Number of formulae : 49 ( 33 unt; 0 def)
% Number of atoms : 69 ( 49 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 37 ( 17 ~; 13 |; 2 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 10 con; 0-4 aty)
% Number of variables : 29 ( 4 sgn 6 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_20_zle__refl,axiom,
! [W] : hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),W),W)),
file('theBenchmark.p',fact_20_zle__refl) ).
fof(fact_22_zless__le,axiom,
! [Z_2,W_1] :
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),Z_2),W_1))
<=> ( ti(int,Z_2) != ti(int,W_1)
& hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),Z_2),W_1)) ) ),
file('theBenchmark.p',fact_22_zless__le) ).
fof(tsy_c_IntFact_Ozfact_arg1,axiom,
! [B_1_1] : zfact(ti(int,B_1_1)) = zfact(B_1_1),
file('theBenchmark.p',tsy_c_IntFact_Ozfact_arg1) ).
fof(tsy_c_IntFact_Ozfact_res,axiom,
! [B_1_1] : ti(int,zfact(B_1_1)) = zfact(B_1_1),
file('theBenchmark.p',tsy_c_IntFact_Ozfact_res) ).
fof(fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( t = one_one(int)
=> ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) ),
file('theBenchmark.p',fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,axiom,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t))
=> ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) ),
file('theBenchmark.p',fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06) ).
fof(fact_754_zfact_Osimps,axiom,
! [N_1] :
( ( ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),N_1),zero_zero(int)))
=> zfact(N_1) = hAPP(int,int,times_times(int,N_1),zfact(hAPP(int,int,minus_minus(int,N_1),one_one(int)))) )
& ( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),N_1),zero_zero(int)))
=> zfact(N_1) = one_one(int) ) ),
file('theBenchmark.p',fact_754_zfact_Osimps) ).
fof(conj_0,conjecture,
? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_1106,plain,
zfact(ti(int,A)) = zfact(A),
inference(clausify,[status(thm)],[tsy_c_IntFact_Ozfact_arg1]) ).
cnf(c_1107,plain,
zfact(A) = ti(int,zfact(A)),
inference(clausify,[status(thm)],[tsy_c_IntFact_Ozfact_res]) ).
cnf(c_1108,plain,
ti(int,zfact(A)) = zfact(A),
inference(copy,[status(thm)],[c_1107]) ).
fof(tsy_v_t_____res,axiom,
ti(int,t) = t,
file('theBenchmark.p',tsy_v_t_____res) ).
cnf(c_1160,plain,
ti(int,t) = t,
inference(clausify,[status(thm)],[tsy_v_t_____res]) ).
fof(fact_0_tpos,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
file('theBenchmark.p',fact_0_tpos) ).
cnf(c_1161,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),one_one(int)),t)),
inference(clausify,[status(thm)],[fact_0_tpos]) ).
fof(nnf_708,plain,
( ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(fof_nnf,[status(thm)],[fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
fof(sk_fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,plain,
( hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK1),number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X,sK0),skolemize(Y,sK1)],[nnf_708]) ).
cnf(c_1162,plain,
( hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK1),number_number_of(nat,bit0(bit1(pls)))))
| one_one(int) != t ),
inference(split_conjunct,[status(thm)],[sk_fact_1__096t_A_061_A1_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
cnf(c_1163,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK0),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK1),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| one_one(int) != t ),
inference(copy,[status(thm)],[c_1162]) ).
fof(nnf_709,plain,
( ? [X,Y] : hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,X),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,Y),number_number_of(nat,bit0(bit1(pls)))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(fof_nnf,[status(thm)],[fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
fof(sk_fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06,plain,
( hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK3),number_number_of(nat,bit0(bit1(pls)))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X,sK2),skolemize(Y,sK3)],[nnf_709]) ).
cnf(c_1164,plain,
( hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) = hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK3),number_number_of(nat,bit0(bit1(pls)))))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(split_conjunct,[status(thm)],[sk_fact_2__0961_A_060_At_A_061_061_062_AEX_Ax_Ay_O_Ax_A_094_A2_A_L_Ay_A_094_A2_A_06]) ).
cnf(c_1165,plain,
( hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,sK2),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,sK3),number_number_of(nat,bit0(bit1(pls))))) = hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int))
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(copy,[status(thm)],[c_1164]) ).
cnf(c_1461,plain,
( zfact(A) = one_one(int)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),zero_zero(int))) ),
inference(clausify,[status(thm)],[fact_754_zfact_Osimps]) ).
fof(tsy_c_Int_OPls_res,axiom,
ti(int,pls) = pls,
file('theBenchmark.p',tsy_c_Int_OPls_res) ).
cnf(c_1825,plain,
ti(int,pls) = pls,
inference(clausify,[status(thm)],[tsy_c_Int_OPls_res]) ).
cnf(c_1845,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),A)),
inference(clausify,[status(thm)],[fact_20_zle__refl]) ).
cnf(c_1849,plain,
( ti(int,B) = ti(int,A)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less_eq(int),A),B))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),A),B)) ),
inference(clausify,[status(thm)],[fact_22_zless__le]) ).
fof(fact_204_Pls__def,axiom,
pls = zero_zero(int),
file('theBenchmark.p',fact_204_Pls__def) ).
cnf(c_2020,plain,
pls = zero_zero(int),
inference(clausify,[status(thm)],[fact_204_Pls__def]) ).
cnf(c_2757,negated_conjecture,
hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)) != hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,B),number_number_of(nat,bit0(bit1(pls))))),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_2758,negated_conjecture,
hAPP(int,int,plus_plus(int,hAPP(nat,int,power_power(int,A),number_number_of(nat,bit0(bit1(pls))))),hAPP(nat,int,power_power(int,B),number_number_of(nat,bit0(bit1(pls))))) != hAPP(int,int,plus_plus(int,hAPP(int,int,times_times(int,number_number_of(int,bit0(bit0(bit1(pls))))),m)),one_one(int)),
inference(copy,[status(thm)],[c_2757]) ).
cnf(c_2850,negated_conjecture,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)),
inference(resolve,[status(thm)],[c_2758,c_1165]) ).
cnf(c_2851,negated_conjecture,
one_one(int) != t,
inference(resolve,[status(thm)],[c_2758,c_1163]) ).
cnf(c_2883,plain,
ti(int,pls) = zero_zero(int),
inference(paramod,[status(thm)],[c_2020,c_1825]) ).
cnf(c_2928,plain,
zfact(zero_zero(int)) = zfact(pls),
inference(paramod,[status(thm)],[c_2883,c_1106]) ).
cnf(c_3500,plain,
zfact(zero_zero(int)) = one_one(int),
inference(resolve,[status(thm)],[c_1845,c_1461]) ).
cnf(c_6013,plain,
one_one(int) = zfact(pls),
inference(paramod,[status(thm)],[c_3500,c_2928]) ).
cnf(c_3544,plain,
zfact(pls) = one_one(int),
inference(copy,[status(thm)],[c_6013]) ).
cnf(c_3547,plain,
ti(int,one_one(int)) = zfact(pls),
inference(paramod,[status(thm)],[c_3544,c_1108]) ).
cnf(c_6014,plain,
( ti(int,t) = ti(int,one_one(int))
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(resolve,[status(thm)],[c_1849,c_1161]) ).
cnf(c_6015,plain,
( ti(int,one_one(int)) = ti(int,t)
| hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),one_one(int)),t)) ),
inference(copy,[status(thm)],[c_6014]) ).
cnf(c_3576,plain,
ti(int,one_one(int)) = ti(int,t),
inference(resolve,[status(thm)],[c_2850,c_6015]) ).
cnf(c_5970,plain,
ti(int,t) = zfact(pls),
inference(paramod,[status(thm)],[c_3576,c_3547]) ).
cnf(c_5993,plain,
zfact(pls) = t,
inference(paramod,[status(thm)],[c_5970,c_1160]) ).
cnf(c_6016,plain,
t = one_one(int),
inference(paramod,[status(thm)],[c_5993,c_3544]) ).
cnf(c_6017,plain,
one_one(int) = t,
inference(copy,[status(thm)],[c_6016]) ).
cnf(c_6012,plain,
$false,
inference(resolve,[status(thm)],[c_2851,c_6017]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : NUM926+7 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.03/15.24 % CPULimit : 300
% 0.03/15.24 % WCLimit : 300
% 0.03/15.24 % DateTime : Sat Sep 26 04:20:51 UTC 2026
% 0.03/15.24 % CPUTime :
% 0.03/15.25 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.03/15.25 % Process 3897882 was started by sandbox2 on n012,
% 0.03/15.25 % Sat Sep 26 04:20:51 2026
% 0.03/15.25 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/15.39
% 0.17/15.39 % From the command line: assign(max_seconds, 300).
% 0.17/15.39
% 0.17/15.39 % SInE: 678 to sos, 576 to usable, of 1254 axioms (tolerance 2.00, depth 0 fixpoint).
% 6.48/16.30
% 6.48/16.30 % SZS status Theorem for theBenchmark
% 6.48/16.30
% 6.48/16.30 % Proof 1 at 0.78 (+ 0.09) seconds.
% 6.48/16.30 % Length of proof is 35.
% 6.48/16.30 % Level of proof is 7.
% 6.48/16.30 % Maximum clause weight is 153.000.
% 6.48/16.30 % Given clauses 416.
% 6.48/16.30
% 6.48/16.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------