%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM925+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 02:21:21 PM UTC 2026
% Result : Theorem 63.94s 9.75s
% Output : Proof 63.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 9
% Syntax : Number of formulae : 43 ( 37 unt; 0 def)
% Number of atoms : 57 ( 40 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 31 ( 17 ~; 10 |; 2 &)
% ( 1 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 18 ( 0 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f124,axiom,
! [K] : bit1(K) = plus_plus(int,plus_plus(int,one_one(int),K),K),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_Bit1__def) ).
fof(f124_nnf,plain,
! [K] : bit1(K) = plus_plus(int,plus_plus(int,one_one(int),K),K),
inference(nnf_transformation,[status(thm)],[f124]) ).
fof(f124_sk,plain,
! [K] : bit1(K) = plus_plus(int,plus_plus(int,one_one(int),K),K),
inference(skolemisation,[status(esa)],[f124_nnf]) ).
cnf(c166,plain,
bit1(X0) = plus_plus(int,plus_plus(int,one_one(int),X0),X0),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
fof(f107,axiom,
! [K] : plus_plus(int,K,pls) = K,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_75_add__Pls__right) ).
fof(f107_nnf,plain,
! [K] : plus_plus(int,K,pls) = K,
inference(nnf_transformation,[status(thm)],[f107]) ).
fof(f107_sk,plain,
! [K] : plus_plus(int,K,pls) = K,
inference(skolemisation,[status(esa)],[f107_nnf]) ).
cnf(c147,plain,
plus_plus(int,X0,pls) = X0,
inference(cnf_transformation,[status(esa)],[f107_sk]) ).
cnf(p412,plain,
bit1(pls) = one_one(int),
inference(superposition,[status(thm)],[c166,c147]) ).
fof(f37,axiom,
! [X_a] :
( ring_11004092258visors(X_a)
=> ! [A_2] :
( power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))) = zero_zero(X_a)
<=> ti(X_a,A_2) = zero_zero(X_a) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_zero__eq__power2) ).
fof(f37_nnf,plain,
! [X_a] :
( ! [A_2] :
( ( ti(X_a,A_2) != zero_zero(X_a)
| power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))) = zero_zero(X_a) )
& ( ti(X_a,A_2) = zero_zero(X_a)
| power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))) != zero_zero(X_a) ) )
| ~ ring_11004092258visors(X_a) ),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [X_a,A_2] :
( ( ( ti(X_a,A_2) != zero_zero(X_a)
| power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))) = zero_zero(X_a) )
& ( ti(X_a,A_2) = zero_zero(X_a)
| power_power(X_a,A_2,number_number_of(nat,bit0(bit1(pls)))) != zero_zero(X_a) ) )
| ~ ring_11004092258visors(X_a) ),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c43,plain,
( ti(X0,X1) = zero_zero(X0)
| power_power(X0,X1,number_number_of(nat,bit0(bit1(pls)))) != zero_zero(X0)
| ~ ring_11004092258visors(X0) ),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
fof(f131,axiom,
ring_11004092258visors(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',arity_Int_Oint___Rings_Oring__1__no__zero__divisors) ).
fof(f131_nnf,plain,
ring_11004092258visors(int),
inference(nnf_transformation,[status(thm)],[f131]) ).
cnf(c176,plain,
ring_11004092258visors(int),
inference(cnf_transformation,[status(esa)],[f131_nnf]) ).
cnf(p385,plain,
( X0 = pls
| power_power(int,X0,number_number_of(nat,bit0(bit1(pls)))) != pls ),
inference(resolution,[status(thm)],[c43,c176]) ).
cnf(p500,plain,
( X0 = pls
| power_power(int,X0,number_number_of(nat,bit0(one_one(int)))) != pls ),
inference(demodulation,[status(thm)],[p412,p385]) ).
fof(f105,axiom,
pls = zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_Pls__def) ).
fof(f105_nnf,plain,
pls = zero_zero(int),
inference(nnf_transformation,[status(thm)],[f105]) ).
cnf(c145,plain,
pls = zero_zero(int),
inference(cnf_transformation,[status(esa)],[f105_nnf]) ).
fof(f51,axiom,
zero_zero(int) = number_number_of(int,pls),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_zero__is__num__zero) ).
fof(f51_nnf,plain,
zero_zero(int) = number_number_of(int,pls),
inference(nnf_transformation,[status(thm)],[f51]) ).
cnf(c61,plain,
zero_zero(int) = number_number_of(int,pls),
inference(cnf_transformation,[status(esa)],[f51_nnf]) ).
cnf(p210,plain,
pls = number_number_of(int,pls),
inference(superposition,[status(thm)],[c145,c61]) ).
cnf(p211,plain,
zero_zero(int) = pls,
inference(superposition,[status(thm)],[p210,c61]) ).
fof(f152,conjecture,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f152_neg,negated_conjecture,
~ ( power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) != zero_zero(int) ),
inference(negated_conjecture,[status(cth)],[f152]) ).
fof(f152_nnf,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(nnf_transformation,[status(thm)],[f152_neg]) ).
cnf(c197,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(cnf_transformation,[status(esa)],[f152_nnf]) ).
cnf(p221,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = pls,
inference(demodulation,[status(thm)],[p211,c197]) ).
cnf(p440,plain,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(one_one(int)))) = pls,
inference(demodulation,[status(thm)],[p412,p221]) ).
cnf(p3320,plain,
plus_plus(int,one_one(int),semiring_1_of_nat(int,n)) = pls,
inference(resolution,[status(thm)],[p500,p440]) ).
fof(f32,axiom,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_n1pos) ).
fof(f32_nnf,plain,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c36,plain,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(p212,plain,
ord_less(int,pls,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(demodulation,[status(thm)],[p211,c36]) ).
cnf(p3321,plain,
ord_less(int,pls,pls),
inference(demodulation,[status(thm)],[p3320,p212]) ).
fof(f64,axiom,
~ ord_less(int,pls,pls),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_rel__simps_I2_J) ).
fof(f64_nnf,plain,
~ ord_less(int,pls,pls),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
~ ord_less(int,pls,pls),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c77,plain,
~ ord_less(int,pls,pls),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(p3345,plain,
$false,
inference(resolution,[status(thm)],[p3321,c77]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM925+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.41 % Computer : n005.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Thu Sep 24 05:43:02 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.41 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 63.94/9.75 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 63.94/9.75 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------